feat: add Heap instances for TreeMap and ExtTreeMap

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9371548b6ac4467fea4dfc675881f6212cc5565d",
+   "rev": "9a599e9f9d787540a9d3a6f6aa5b1c6c4a387127",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.25.1

src/Iris/Algebra/CMRA.lean

@@ -1136,7 +1136,7 @@ theorem inc_iff {ma mb : Option α} :
     · exact .inl Hmc.symm
     · exact .inr ⟨_, Hmc⟩
   · rintro (H|⟨_, _, _, _, (H|⟨z, _⟩)⟩) <;> subst_eqs
-    · exists mb
+    · exists mb; simp [op]
     · exists none; simp [op]; exact H.symm
     · exists some z
 
@@ -1147,7 +1147,7 @@ theorem incN_iff {ma mb : Option α} :
     · exact .inl Hmc.symm
     · exact .inr ⟨_, Hmc⟩
   · rintro (H|⟨_, _, _, _, (H|⟨z, _⟩)⟩) <;> subst_eqs
-    · exists mb
+    · exists mb; simp [op]
     · exists none; simp [op]; exact H.symm
     · exists some z
 

src/Iris/Algebra/COFESolver.lean

@@ -131,7 +131,7 @@ protected def Tower.embed (k) : A F k -n> Tower F := by
       rintro a _ eq rfl
       rw [Nat.add_assoc, Nat.add_left_cancel_iff] at eq; subst a
       apply down_up
-    · cases (Nat.lt_or_eq_of_le h₁).resolve_left (h₂ ∘ Nat.lt_succ_iff.1)
+    · cases (Nat.lt_or_eq_of_le h₁).resolve_left (h₂ ∘ Nat.lt_succ.1)
       have {a b} (e₁ : i+1+a = i+1) (e₂ : i+1 = i+b) :
           down F i (eqToHom e₁ (upN F a n)) ≡ downN F b (eqToHom e₂ n) := by
         cases Nat.add_left_cancel (k := 0) e₁; cases Nat.add_left_cancel e₂

src/Iris/BI/Plainly.lean

@@ -302,9 +302,6 @@ theorem impl_wand_plainly : (■ P → Q) ⊣⊢ (■ P -∗ Q) :=
 
 end AffineBI
 
-instance plainly_absorbing (P : PROP) : Absorbing iprop(■ P) where
-  absorbing := absorbingly_elim_plainly.1
-
 end PlainlyLaws
 
 end Iris.BI

src/Iris/Examples/Resources.lean

@@ -3,6 +3,7 @@ Copyright (c) 2025 Markus de Medeiros. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus de Medeiros
 -/
+import Iris.BI
 import Iris.ProofMode
 import Iris.Algebra.IProp
 import Iris.Instances.UPred.Instance

src/Iris/Instances/UPred/Instance.lean

@@ -9,7 +9,6 @@ import Iris.Algebra.OFE
 import Iris.Algebra.CMRA
 import Iris.Algebra.UPred
 import Iris.Algebra.Updates
-import Iris.BI.Lib.BUpdPlain
 
 section UPredInstance
 
@@ -494,45 +493,3 @@ instance : BIAffine (UPred M) := ⟨by infer_instance⟩
 -- TODO: Port derived lemmas
 
 end UPred
-
-section UPredAlt
-
-open BUpdPlain CMRA UPred
-
-/-
-## Compatibility between the UPred model of BUpd and the BUpd construction for generic BIPlainly instances
--/
-
-def BUpdPlain_pred [UCMRA M] (P : UPred M) (y : M) : UPred M where
-  holds k _ := ∃ x'', ✓{k} (x'' • y) ∧ P k x''
-  mono {_} := fun ⟨z, Hz1, Hz2⟩ _ Hn =>
-    ⟨z, validN_of_le Hn Hz1, P.mono Hz2 (incN_refl z) Hn⟩
-
-/-- The alternative definition entails the ordinary basic update -/
-theorem BUpdPlain_bupd [UCMRA M] (P : UPred M) : BUpdPlain P ⊢ |==> P := by
-  intro n x Hx H k y Hkn Hxy
-  refine (H _ ⟨BUpdPlain_pred P y, rfl⟩) k y Hkn Hxy ?_
-  intro _ z _ Hvyz HP
-  refine ⟨z, validN_ne op_commN Hvyz, HP⟩
-
-theorem BUpdPlain_bupd_iff [UCMRA M] (P : UPred M) : BUpdPlain P ⊣⊢ |==> P :=
-  ⟨BUpdPlain_bupd P, BUpd_BUpdPlain⟩
-
-theorem ownM_updateP [UCMRA M] {x : M} {R : UPred M} (Φ : M → Prop) (Hup : x ~~>: Φ) :
-    ownM x ∗ (∀ y, iprop(⌜Φ y⌝) -∗ ownM y -∗ ■ R) ⊢ ■ R := by
-  intro n z Hv ⟨x1, z2, Hx, ⟨z1, Hz1⟩, HR⟩
-  have Hvalid : ✓{n} (x •? some (z1 • z2)) := by
-    show ✓{n} (x • (z1 • z2))
-    refine CMRA.validN_ne ?_ Hv
-    calc z ≡{n}≡ x1 • z2 := Hx
-         _ ≡{n}≡ (x • z1) • z2 := Hz1.op_l
-         _ ≡{n}≡ x • (z1 • z2) := CMRA.assoc.symm.dist
-  have ⟨y, HΦy, Hvalid_y⟩ := Hup n (some (z1 • z2)) Hvalid
-  have Hp := HR (iprop(⌜Φ y⌝ -∗ (UPred.ownM y -∗ ■ R))) ⟨y, rfl⟩
-  refine Hp n z1 (Nat.le_refl _) ?_ HΦy n y (Nat.le_refl _) ?_ (incN_refl y)
-  · exact CMRA.validN_ne CMRA.comm.dist (CMRA.validN_op_right Hvalid)
-  · apply CMRA.validN_ne ?_ Hvalid_y
-    calc y • (z1 • z2) ≡{n}≡ y • (z2 • z1) := CMRA.comm.dist.op_r
-         _ ≡{n}≡ (z2 • z1) • y := CMRA.comm.symm.dist
-
-section UPredAlt

src/Iris/Std.lean

@@ -1,5 +1,7 @@
 import Iris.Std.Classes
 import Iris.Std.Expr
+import Iris.Std.Heap
+import Iris.Std.HeapInstances
 import Iris.Std.Nat
 import Iris.Std.Prod
 import Iris.Std.Qq