[Iris-Club] Iris proof mode artifact ideas for proof automation class

[Robbert Krebbers]

Hi Talia,

Great to hear that you will be using the Iris proof mode for your course!

For "user experience" (1), it probably makes most sense to go through 
our tutorial at POPL'21, see 
https://gitlab.mpi-sws.org/iris/tutorial-popl21/. There's also a 
recording of the talk, that includes some live coding. If the course 
mostly focuses at Coq hacking, the concurrency reasoning part of the 
tutorial might be less relevant (and more difficult to understand), but 
it still is an important motivation for the style of proofs that we want 
to have in Iris.

For "how the tool is actually" (2) it could make sense to implement a 
small tactic. One tactic (that has actually come up as a user request, 
but has not been implemented) is `iApply ... in ...`. I have attached a 
simple attempt.

It is not easy for me to determine how hard this will be for students. I 
basically obtained this solution by copying `tac_specialize` and 
adjusting it according. It of course requires a reasonable understanding 
of the general way how tactics are defined in Iris proof mode. The 
POPL'17 paper hopefully gives a good overview of the key ideas, but the 
current version with all the subtleties of the current implementation 
might make things harder, especially if you want to understand all 
details really work (instead of just hacking things until things work).

There are various ways to make the tactic easier:

- Drop support for the intuitionistic context (i.e., use `false` instead 
of these Booleans `pi` and `pj` everywhere.)
- Don't attempt error reporting at all.
- Instead of using the Type class `IntoWand`, have a premise 
`envs_lookup i Δ = Some (pi, P -∗ Q)%I`. This means that the tactic only 
works at hypotheses that are syntactically equal to a wand, instead of 
those that can be semantically converted into a wand.

There are also various ways to make the tactic harder:

- Include support for `iApply term in H` where `term` can also be a 
lemma, or even a lemma with arguments (called a proof mode term).
- Include support for `iApply term in H as ipat`

Robbert

On 13/01/2022 22.51, Talia Ringer wrote:
> Hi all,
> 
> I'm teaching a class on proof automation 
> <https://dependenttyp.es/classes/598sp2022.html> this spring. The way 
> the course works is by alternating between reading discussions and 
> artifact hacking sessions, where the artifacts are typically derived 
> directly from the readings. Those sessions are in person, in groups, 
> with a discussion following the hacking.
> 
> One of the readings is the Iris proof mode paper 
> <https://dependenttyp.es/classes/readings/7-logics.html>. For the 
> artifact that Thursday, I'd like to make an exercise derived from the 
> Iris proof mode artifact. I've had no trouble installing the development 
> version from source (yay), so now it's time to make the actual 
> assignment for the hacking session.
> 
> I'm curious if any of you have ideas for that. Typically these session 
> include diving into the source of an artifact, looking at some mix of 1) 
> user experience for the tool, and 2) how the tool is actually 
> implemented. Ideally this also includes modifying some code to implement 
> some small and simple extension to the tool, though this isn't always 
> possible.
> 
> Goals for the Iris proof mode artifact assignment are /any nonempty 
> subset /of these goals:
> 1) get a sense of how the Iris proof mode is implemented, and how one 
> could implement something similar for another domain or logic,
> 2) get a sense of how reflection works, and its costs and benefits,
> 3) get a sense of how language design and automation feed into one 
> another, and what design decisions make the Iris proof mode possible,
> 4) get a sense of how type classes work, and whether they impact 
> scalability.
> 
> I'm also open to other goals you all find interesting, though. This is a 
> brand new class I'm designing from scratch, and I'm very open.
> 
> The assignment itself isn't graded, just the discussion question after, 
> so it's also fine if it's something that can't be finished in one class, 
> though it's ideal if there's some intermediate progress.
> 
> I figured I'd ask the Iris experts if you all have any ideas. Please let 
> me know if you do!
> 
> Thanks,
> 
> Talia
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: apply_in.v
Type: text/x-verilog
Size: 1919 bytes
Desc: not available
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20220114/b76e93eb/attachment.bin>