refactor: retire setoids by Kaptch · Pull Request #533 · leanprover-community/iris-lean

Kaptch · 2026-07-24T00:56:38Z

Description

Pass over deprecating equiv in favor of eq. The remaining task is a small cleanup. I've tried to keep this one minimal by preserving the proofs as much as possible, while eliminating equiv in signatures. I'll make a pass over proofs in a separate PR.

Kaptch · 2026-07-24T09:30:55Z

Short summary: deprecated OFE.Equiv, maps to/from equality, congruence rules wrt OFE.Equiv, then went fixing the downstream proofs, until none of the code is using those. At this point, OFE.Equiv should be safely deleted (can also do it now, but I would wait a week or two in case any downstream project continues to use it).
I tried to preserve all signatures by just changing OFE.Equiv to equality. The only naming changes come from congruence rules for BigOps, because they combine extensionality and congruence. There, I made a pass to merge some lemmas.

The proofs are mostly the same, and I'll make a separate pass to use simp/rw in them instead of manual chains of equalities.
I can also split the PR a bit, but it seems that is the cleanest way to change all signatures in one go to avoid to_eq/from_eq casting.

markusdemedeiros · 2026-07-24T10:05:56Z

Don't worry about breaking downstream projects (a week or two changes nothing since they should be using the versioned releases anyways). I'll do my best to review this promptly!

markusdemedeiros

The usual nits. Read them, but I'll leave the final say to you on if you want the edits.

I'd suggest removing the deprecated stuff now, or in a follow-up PR. No need to keep that around.

markusdemedeiros · 2026-07-24T10:26:18Z

 @[rocq_alias to_dfrac_agree_discrete]
 instance mk_discrete {d : DFrac} {a : A} [DiscreteE a] : DiscreteE (mk d a) :=
-  ⟨fun h n => ⟨(is_discrete.discrete h.1) n, (Agree.toAgree.is_discrete.discrete h.2) n⟩⟩
+  ⟨fun h => OFE.eq_dist.mpr <| by


Suggested change

⟨fun h => OFE.eq_dist.mpr <| by

⟨fun h => OFE.eq_dist.mpr <| fun n => ⟨(is_discrete.discrete h.1).dist, (Agree.toAgree.is_discrete.discrete h.2).dist⟩⟩

markusdemedeiros · 2026-07-25T11:58:19Z

-  simp
+theorem bigOpL_snoc_eq (Φ : Nat → A → M) (l : List A) (a : A) :
+    ([^ op list] k ↦ x ∈ l ++ [a], Φ k x) = op ([^ op list] k ↦ x ∈ l, Φ k x) (Φ l.length a) := by
+  rw [bigOpL_append_eq]; simp [op_right_id]


Suggested change

rw [bigOpL_append_eq]; simp [op_right_id]

simp [bigOpL_append_eq, op_right_id]

markusdemedeiros · 2026-07-25T12:03:15Z

+theorem bigOpM_eq_strong [OFE A] {Φ Ψ : K → A → M} {m1 m2 : M' A} (hm : ∀ k, get? m1 k = get? m2 k)
+    (hf : ∀ {k y1 y2}, get? m1 k = some y1 → get? m2 k = some y2 → y1 = y2 → Φ k y1 = Ψ k y2) :
+    ([^ op map] k ↦ x ∈ m1, Φ k x) = ([^ op map] k ↦ x ∈ m2, Ψ k x) :=
+  bigOpM_gen_proper_2 id ⟨fun _ => rfl, Eq.symm, Eq.trans⟩ (· ▸ · ▸ rfl) (fun k => by rw [hm k])


⟨fun _ => rfl, Eq.symm, Eq.trans⟩

Extract to definition (probably already exists)

markusdemedeiros · 2026-07-25T12:14:06Z

  refine (intuitionistically_ownM_core a).trans ?_
  refine intuitionistically_mono ?_
-  exact (ownM_eqv (core_eqv_self a).symm).mpr
+  simp only [core_eqv_self, BIBase.Entails.rfl]


Suggested change

simp only [core_eqv_self, BIBase.Entails.rfl]

simp [core_eqv_self, BIBase.Entails.rfl]

markusdemedeiros · 2026-07-25T12:14:21Z

    refine (persistently_ownM_core a).trans ?_
-    exact persistently_mono (ownM_eqv (core_eqv_self a)).mp
+    refine persistently_mono ?_
+    simp only [core_eqv_self, BIBase.Entails.rfl]


Suggested change

simp only [core_eqv_self, BIBase.Entails.rfl]

simp [core_eqv_self, BIBase.Entails.rfl]

markusdemedeiros · 2026-07-25T13:39:50Z

-  refine NonExpansive₂.eqv (f := fA) Hp.symm ?_
+    (fA : α -c> β -n> α) (fB : α -c> β -c> β) (Hp : fA p q = p) (Hq : fB p q = q) :
+    p = (fixpointA fA fB) := by
+  have hq : q = fixpointAB fB p := fixpoint_unique Hq.symm


Inline this?

markusdemedeiros · 2026-07-25T13:42:26Z

  ⟨(mono · Ha Hb.symm.to_incN n.le_refl), (mono · Ha.symm Hb.to_incN n.le_refl)⟩

-@[rocq_alias view_rel_proper]
+@[rocq_alias view_rel_proper, deprecated "OFE is Leibniz; use `congrArg`/`rw`" (since := "2026-07")]


markusdemedeiros · 2026-07-25T13:43:03Z

+    simp only [Pcore, Option.some.injEq]
    rcases cx
    simp only [mk.injEq, and_imp]
    intro H1 H2


rintro rfl rfl instead

markusdemedeiros · 2026-07-25T13:43:17Z

+    have Hle : g y1 ≼ g y2 := ⟨g z, congrArg g Hy2⟩
+    obtain ⟨_, Hcgy2, x, Hcx⟩ :=
+      CMRA.pcore_mono' Hle (Hg_core.mp Hy1)
+    exact ⟨_, rfl, f x,


markusdemedeiros · 2026-07-25T15:48:32Z

-  have hf : f1 = f2 := funext fun a => (h1 a).to_eq
-  have hg : g1 = g2 := funext fun b => (h2 b).to_eq
+    View.map R' f1 g1 v = View.map R' f2 g2 v := by
+  have hf : f1 = f2 := funext fun a => OFE.eq_dist.mpr (h1 a)


Suggested change

have hf : f1 = f2 := funext fun a => OFE.eq_dist.mpr (h1 a)

obtain rfl : f1 = f2 := funext fun a => OFE.eq_dist.mpr (h1 a)

obtain rfl : g1 = g2 := funext fun a => OFE.eq_dist.mpr (h2 b)

rfl

Kaptch · 2026-07-26T18:47:42Z

Thanks, @markusdemedeiros! I'll remove the deprecated things and do a final minor pass over proofs.
I'll later do a more involved pass in a separate PR to see where it's possible to significantly shorten stuff by rewriting within 1-2 weeks.

Kaptch added 14 commits July 22, 2026 18:47

pass over OFE signatures

253b111

pass over CMRA signatures

2a6a869

pass over algebra signatures

cb3eb76

pass over BI signatures

bcb677a

pass over residual signatures

8e44e58

pass over residual signatures

a520c3e

pass over congruences

5d40114

pass over congruences

2d97671

pass over congruences

ffabaa4

pass over to_eq of_eq

fc924bd

pass over congruences

a290e44

finish deprecating equiv

07b447b

cleanup pass

047e3e6

Merge remote-tracking branch 'origin/master' into eq-leaves

8f57ed5

Kaptch marked this pull request as ready for review July 24, 2026 09:19

Kaptch requested review from lzy0505 and markusdemedeiros July 24, 2026 09:31

markusdemedeiros approved these changes Jul 25, 2026

View reviewed changes

Kaptch mentioned this pull request Jul 27, 2026

feat: port algebra/stepindex.v #515

Merged

53 tasks

Kaptch added 3 commits July 27, 2026 02:51

Merge remote-tracking branch 'origin/master' into eq-leaves

c5b4c79

cleanup pass

10d0918

Merge remote-tracking branch 'origin/master' into eq-leaves

0bf89fb

Kaptch merged commit 1f6eaa0 into leanprover-community:master Jul 27, 2026
5 checks passed

alvinylt mentioned this pull request Jul 28, 2026

feat: OFE step-indexing parametrisation, port algebra/stepindex_finite.v #550

Draft

2 tasks

	⟨fun h => OFE.eq_dist.mpr <\| by
	⟨fun h => OFE.eq_dist.mpr <\| fun n => ⟨(is_discrete.discrete h.1).dist, (Agree.toAgree.is_discrete.discrete h.2).dist⟩⟩

	rw [bigOpL_append_eq]; simp [op_right_id]
	simp [bigOpL_append_eq, op_right_id]

	simp only [core_eqv_self, BIBase.Entails.rfl]
	simp [core_eqv_self, BIBase.Entails.rfl]

-  have hf : f1 = f2 := funext fun a => OFE.eq_dist.mpr (h1 a)
+  obtain rfl : f1 = f2 := funext fun a => OFE.eq_dist.mpr (h1 a)
+  obtain rfl : g1 = g2 := funext fun a => OFE.eq_dist.mpr (h2 b)
+  rfl

Uh oh!

Conversation

Kaptch commented Jul 24, 2026

Description

Uh oh!

Kaptch commented Jul 24, 2026

Uh oh!

markusdemedeiros commented Jul 24, 2026

Uh oh!

markusdemedeiros left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Kaptch commented Jul 26, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants