Next steps

Stream: iris-lean

[Markus de Medeiros]

Thanks Mario for making this channel! It'll be good to have somewhere central to discuss this project.

For people who want to contribute I think that there's a number of results that are within reach:

• The lemmas about (C)OFE's from ofe.v and CMRA's from cmra.v, many of which are self-contained
• The definition of the UPred CMRA, and the connectives defining a BIBase instance
• oFunctor/rFunctor instances, we have a definition for oFunctors and the fixpoint theorem but no instances!

Once more COFE and CMRA lemmas are ported, much more of algebra/ will be accessible: local_updates.v, algebra/lib/ etc.

If anyone else has any ideas of easy tasks to point people to maybe you can put them here too. Sadly I'll be too busy to contribute for the next few weeks but I'm hoping to pick it back up afterwards!

[suhr]

As a long-term goal: port λRust?

[Shreyas Srinivas]

I guess I can try my hand at lambda rust because I worked with very similar code and if I have trouble understanding it, Derek’s group is in a very nearby building

[Shreyas Srinivas]

I’ll probably not get to it before end of March though (possibly even middle of April)

[suhr]

By the way, HeapLang also needs porting?

[Markus de Medeiros]

Indeed, both of these things should eventually be done! At the moment we don't even have a definition for iProp so there's more foundational work to do :sweat_smile:

One could probably port the operational semantics of HeapLang (HeapLang/lang.v) or the language hierarchy (iris/program_logic/langauge.v, iris/program_logic/ectx*) but I don't think there is not enough Iris ported yet to even state lemmas about the HeapLang program logic.

[suhr]

I was curious what exercises could I do to get familiar with Iris in Lean, but it seems like not too many yet.

Porting the whole thing is not exactly a quick exercise to do in a spare time.

[Markus de Medeiros]

Definitely haha. How familiar are you with Iris?

The most accessible lemmas to port are probably the lemmas from algebra/ofe.v and algebra/cmra.v since Mario already has the relevant definitions stated and the lemmas are mostly self-contained (I know this from experience). If you're more familiar with Iris, you could pick and port a CMRA from Algebra/ like Leo did a few weeks ago.

[suhr]

By the way, seems like https://github.com/logsem/iris-tutorial/blob/master/exercises/basics.v needs only iProp, so when iProp is ported I could try to do it.

How familiar are you with Iris?

“Heard about it” level of familiarity.

[suhr]

Judging from imports, there's the following dependency chain iprop → gmap → gset → crma. So iProp port is far away.

[suhr]

There's already some definition CMRA in the repo, so I guess it only needs a ton of lemmas to be ported. But https://github.com/leanprover-community/iris-lean/pull/11 suggests a different definition.

[Markus de Medeiros]

Yep. For context:iProp is uPred instantiated with a particular CMRA; the gmap and gset OFE's are used to construct this CMRA (alongside the fixpoint solver which Mario has already ported!). I think that uPred is accessible to us in the short term, but most stuff is blocked by CMRA and COFE lemmas so porting that is helpful!

Once I have time again, and if nobody else has picked it up, porting CMRA lemmas is where I'll start.

[Markus de Medeiros]

As for that PR, don't worry about it. There's a new definition of CMRA that is (as far as I can tell) in the process of being upstreamed to Iris, and we're waiting until they upstream it to do the same.

[suhr]

All right, basic lemmas are very straightforward. I proved a few: https://github.com/leanprover-community/iris-lean/pull/14.

The Coq proof of cmra_pcore_l' looks like this:

Lemma cmra_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_l. Qed.

But I don't quite understand Some_equiv_eq here. How equivalence is turned into equality?

[suhr]

By the way, it seems like in Coq there's a some kind of rewriting tactic for equivalences which simplifies proofs quite a bit.

[Mario Carneiro]

iris-lean has a rw' tactic which you can use, although I prefer to avoid it most of the time

[Mario Carneiro]

I think that theorem Some_equiv_eq is saying that the ≡ relation on option is the same as = when one side is a Some

[Mario Carneiro]

because keep in mind that this ≡ relation is not the one on the cmra, it's a lifted version of it operating on options

[Mario Carneiro]

I think in lean this proof would look something like

theorem cmra_pcore_l' (x cx) (h : pcore x ≡ Some cx) : cx ⋅ x ≡ x :=
  cmra_pcore_l (Some_equiv_eq.1 h)

which is why I wouldn't bother with rw' for this

[Mario Carneiro]

it's not even clear whether this theorem is really needed, the two are probably defeq

[suhr]

Mario Carneiro said:

because keep in mind that this ≡ relation is not the one on the cmra, it's a lifted version of it operating on options

I see, thanks.

[suhr]

Lemma cmra_pcore_idemp' is more tricky than I expected, I don't quite see how to prove it.

[Mario Carneiro]

If pcore ≡ some cx, then that means pcore = some cx' for some cx' ≡ cx. Then pcore cx ≡ pcore cx' because pcore is nonexpansive, and pcore cx' ≡ some cx' from pcore_idem, so pcore cx ≡ some cx by transitivity

[suhr]

This requires proving a different tricky lemma:

theorem pcore_ne_equiv {x y: α}: x ≡ y → cmr.pcore x = some cx →
      ∃ cy, cmr.pcore y = some cy ∧ cx ≡ cy :=
    sorry

Because CRMA.pcore_ne has the following type:

pcore_ne : x ≡{n}≡ y → pcore x = some cx →
    ∃ cy, pcore y = some cy ∧ cx ≡{n}≡ cy

So one needs to somehow convert ≡{n}≡ into ≡.

[suhr]

Anyway, in https://github.com/leanprover-community/iris-lean/pull/14 I proved almost all lemmas I was going to prove except for three tricky ones. There's so much more to port from Coq, but I already did a dangerous amount of procrastination.

Coq naming is a mess, I hope you figure out better names for all these lemmas.

[suhr]

Unlike Coq proofs, Coq proof terms are somewhat readable. So maybe I will figure out proofs for other lemmas.

[suhr]

Thinking a bit ahead: which Lean types should be used for gset, gmap and gmultiset from Coq's stdpp?

[Quang Dao]

Why not use mathlib's existing Finset and Multiset APIs? And for efficiency there's also Std.HashMap

[Markus de Medeiros]

suhr said:

Unlike Coq proofs, Coq proof terms are somewhat readable. So maybe I will figure out proofs for other lemmas.

FYI one big source of difficulty when porting is that Rocq has generalized rewriting and Lean doesn't (yet). So if you see a rewrite or apply that doesn't seem to make sense, it's possible that Rocq is applying some lemmas under the hood.

[Markus de Medeiros]

I think in this part of the development these are typically Proper instances. For now, we need to do all of this by hand.

[Markus de Medeiros]

I'm not sure why Iris uses gset/gmap for the ghost resources, I agree with Quang that we should use the regular finite set/map API's for this before overcomplicating our lives. If they're just resources, efficiency doesn't matter.

[Shreyas Srinivas]

This means adding mathlib since finsets are in mathlib afaik

[Shreyas Srinivas]

docs#Finset

[Shreyas Srinivas]

In the other thread the discussion seems to be tending against adding mathlib

[Markus de Medeiros]

Ah okay--it's probably not that hard to write our own interface for finsets and finmaps anyways (it would be nice to have the ghost constructions support mathlib types by instantiating a typeclass; all of the projects I have in mind personally involve mathlib heavily). As long as we avoid reimplementing gmap and gset I'm happy.

[Shreyas Srinivas]

Tbh I would like to see a computationally easier to use fin map like coq

[Shreyas Srinivas]

It was easier to toy around with than mathlib’s finmap last year

[suhr]

By the way, my pull request is complete (no sorryies) and ready for a review.

[Andrés Goens]

Markus de Medeiros said:

suhr said:

Unlike Coq proofs, Coq proof terms are somewhat readable. So maybe I will figure out proofs for other lemmas.

FYI one big source of difficulty when porting is that Rocq has generalized rewriting and Lean doesn't (yet). So if you see a rewrite or apply that doesn't seem to make sense, it's possible that Rocq is applying some lemmas under the hood.

you might already be aware, but just in case, there are some efforts to port Rocq's generalized rewriting, see this thread: #lean4 > Rewriting congruent relations

[Markus de Medeiros]

Ah yes--Leo Stefanesco did try it out a couple weeks ago

[suhr]

While generalized rewriting would be very nice to have, I'm not sure if it's such a big deal. One can always dance with calc like so:

theorem mono (x1 x2 y1 y2: α) : x1 ≼ y1 → x2 ≼ y2 → x1 • x2 ≼ y1 • y2 :=
    λl1 l2 ↦
      let ⟨w, hw⟩ := l1;  let ⟨t, ht⟩ := l2
      suffices h: y1 • y2 ≡ (x1 • x2) • (w • t) from ⟨w • t, h⟩
      calc
        y1 • y2 ≡ (x1 • w) • y2 := op_left_equiv _ hw
        _       ≡ (x1 • w) • (x2 • t) := op_right_equiv _ ht
        _       ≡ x1 • (w • (x2 • t)) := cmr.assoc.symm
        _       ≡ x1 • ((x2 • t) • w) := op_right_equiv _ (cmr.comm)
        _       ≡ (x1 • (x2 • t)) • w := cmr.assoc
        _       ≡ ((x1 • x2) • t) • w := op_left_equiv _ cmr.assoc
        _       ≡ (x1 • x2) • (t • w) := cmr.assoc.symm
        _       ≡ (x1 • x2) • (w • t) := op_right_equiv _ (cmr.comm)

The difficult part for me was the case where you seem to need =, but you only have ≡, so you need to play with lemmas that give you some kind of existence from which you can finally get what you need. Compared with that, chaining a few ≡ is not a big deal.

Hopefully, with enough lemmas having too many kinds of equality stops being painful.

[Markus de Medeiros]

In draft PR iris-lean#21 I wrote stubs for everything in the first half of CMRA.v (building on top of the great work @suhr did of course!)

There are 70 sorry's and many of them are very easy, if you're thinking of contributing this would be a good way to get your feet wet!

[Markus de Medeiros]

Check it out y'all: an Iris proof that everybody agrees that iris-lean is great :)

Screenshot 2025-04-13 at 5.20.41 PM.png

The iProp PR is pretty sizable, but after it's done being reviewed and merged, there's going to be a lot of new opportunities for things to work on. In particular, finishing iProp meant getting the rest of the core definitions in Algebra right, so I think a lot of that folder could be ported independently now. I will post another list of independent jobs soon.

We're not quite at the point where we can comfortably work inside the base logic yet, I think that's the next big milestone. This involves mechanizing updates, refining the tactic suite (imod, iapply...), and refining the way we construct gFunctors (which above is done by hand and is very nasty). If anyone has a burning desire to take ownership of any of these, do let me know!

[suhr]

I wonder if it's possible to make some kind of term syntax for iris-lean. I like my λh ↦ ..., it would be nice to have something similar in iris proofs.

[Markus de Medeiros]

Ah that's quite an interesting thought!

[Mario Carneiro]

I just pushed a bunch of cleanup and golf stuff. The PR is too big to merge in one go, I suggest you break it up into pieces roughly along file boundaries

[Markus de Medeiros]

Sounds good, I'll look it over with some fresh eyes tomorrow

[suhr]

I didn't look at iris-lean for a while. Any low-hanging fruits in the need of being proved?

[Markus de Medeiros]

We have a bunch of issues with the good first issue tag now!

[Markus de Medeiros]

If those seem too big, I have a half-finished PR for porting a bunch of stuff from BI. If you'd prefer, I could also sorry out a bunch of lemmas this weekend and hand it over to you.

[suhr]

sorrying a bunch of lemmas is always a good idea.

[suhr]

I have a question about https://github.com/leanprover-community/iris-lean/pull/49. Somehow this proof

  Lemma alloc_option_local_update {A : cmra} (x : A) y :
    ✓ x →
    (None, y) ~l~> (Some x, Some x).
  Proof.
    move=>Hx. apply local_update_unital=> n z _ /= Heq. split.
    { rewrite Some_validN. apply cmra_valid_validN. done. }
    destruct z as [z|]; last done. destruct y; inversion Heq.
  Qed.

simplified into this proof

  theorem alloc_option_local_update {α : Type} [CMRA α]
      {x : α} (y : α) (_: ✓ x): (none, y) ~l~> (some x, some x) :=
    fun _ mz _ e =>
      match mz with
      | .none           => False.elim e
      | .some .none     => False.elim e
      | .some (.some _) => False.elim e

I have a suspicion that it really shouldn't.

[Markus de Medeiros]

In your statement of the theorem, y should have type Option α. This breaks your proof.

[Markus de Medeiros]

I really hate automatic a : A -> some a : Option A coercions. I've been bitten by it multiple times in both Rocq and Lean.

[suhr]

All right, with y : Option α it looks better

  theorem alloc_option_local_update {α : Type} [CMRA α]
      {x : α} (y : Option α) (vx: ✓ x): (none, y) ~l~> (some x, some x) :=
    fun n mz _ e =>
      match mz with
      | .none           => ⟨CMRA.Valid.validN vx, OFE.Dist.of_eq rfl⟩
      | .some .none     => ⟨CMRA.Valid.validN vx, OFE.Dist.of_eq rfl⟩
      | .some (.some z) =>
        have ⟨_, hw⟩ := CMRA.exists_op_some_dist_some (n := n) y z
        False.elim (e.trans hw)

Still looks too easy compared to original proof, but more reasonable.

[suhr]

Now we have all kinds of things, including IProp. What should be the next goal?

I need HeapLang for iris-tutorial, is it the right time to work on it?

[Shreyas Srinivas]

A full heaplang port will require up streaming all the remaining bitwise files from mathlib to batteries

[Shreyas Srinivas]

That’s where I left my PR in limbo

[Markus de Medeiros]

A 1-1 port of the HeapLang logic still needs invariants which we have not ported but would be a reasonable next step. On the other hand, it also requires a formalization of the HeapLang operational semantics which is not blocked at all.

[suhr]

Can we just remove bitwise operations from HeapLang for now?

[Markus de Medeiros]

Yes. That is not a real blocker.

[Markus de Medeiros]

You could start by porting heap_lang/language.v, ectx_language.v, and ectxi_language.v if you wanted to

[Markus de Medeiros]

I will merge some of the remaining PR's before Friday this week. Likely not iProp yet because there are still some gaps to fill and cleanup to do

[Shreyas Srinivas]

In that case I will remove bitwise operations and submit my PR for review

[Shreyas Srinivas]

@suhr could you build your PR on top of mine?

[Shreyas Srinivas]

I should be able to bring it up to speed in a few hours

[suhr]

Shreyas Srinivas said:

suhr could you build your PR on top of mine?

Sure, why not.

[Shreyas Srinivas]

@suhr I have one annoying sorry left inside a mutual block

[Shreyas Srinivas]

1. I might need help with that sorry
2. You might be able to use this material to define the op sem anyway, since it is in an instance definition for DecidableEq for Expr and Val

[Shreyas Srinivas]

ideally lean should already know that all the Expr's with identical constructors have been handled, but somehow lean can't figure this out in that particular match arm

[Shreyas Srinivas]

Another point : Although this DecidableEq instance cost me a disproportionate amount of time to write, I am in favour of junking it and just using Classical whenever necessary. At some point I was just determined to push it as far as I could.