NML

Stream: iris-lean

[Markus de Medeiros]

Here is the program logic I am working on for my job. This morning I proved adequacy for it (I subsequently broke it because I need to finish iris-lean#63 and iris-lean#64 first). This thread is to A) make the code available, especially for people working on the tactics, and B) talk about how to use Iris-Lean to develop a program logic before we have all of the Iris machinery.

[Markus de Medeiros]

Some notes:

• Not having iApply is really painful. I find that I had to be very careful about the different forms a lemma can take (like, P ⊢ Q -∗ R vs P ∗ Q ⊢ R vs ⊢ P ∗ Q -∗ R). Converting lemmas between these forms meant going out and back into proofmode.
• Iris 0.5 doesn't have dynamic allocation of ghost code like Iris does. This matters for the adequacy theorems. "Normal" Iris adequacy theorems dynamically allocate all of the ghost state, and then use Iris's soundness theorems to with are of the form (True ⊢ ... P → P). To avoid dynamically allocating ghost state I generalized the Iris soundness theorems to be of the form ✓ a → (ownM a ⊢ ... P → P), allocating all ghost state upfront. This works but the normal Iris way is a lot cleaner. I'm going to PR the generalized versions into both Iris's (though I doubt that Rocq-Iris cares about this).
• Minor, but I'll just point out that this issue was also a nuisance.

[Markus de Medeiros]

I have some very simple proof rules and two extremely simple examples. Most of the junk in this proof is just stuff that I need to fix, but it's cool that it's an end-to-end proof using the system :)
Screenshot 2025-07-16 at 12.02.16 PM.png

[suhr]

It seems like everyone needs iapply badly.

[suhr]

By the way, why Iris needs turnstyles? Why can't you use use ⊢ ... everywhere?

[Markus de Medeiros]

What do you mean by "needs turnstyles"?

[suhr]

I mean, if P ⊢ Q and ⊢ P -∗ Q essentially the same, why would you need the first one?

[Markus de Medeiros]

Just muscle memory from Iris :sweat_smile: You are right that there is no logical difference

[Michael Sammler]

In theory they are equivalent, but in practice there are some differences. In fact, Iris switched from P ⊢ Q to ⊢ P -∗ Q by default recently:
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/791

[Oliver Soeser]

suhr said:

It seems like everyone needs iapply badly.

Indeed. I'm hoping to get my iapply to a useable state within the next few days. Most of the functionality is done, but crucially it is missing the ability to use specialisation patterns like [H1, ..., Hn]. (And after that a lot of refactoring needs to be done :sweat_smile: )