From d9595c8c2dba8ef5ec3404b1b08b1d5ee9a89c99 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 09:57:22 -0400 Subject: [PATCH 1/6] gmap aliases --- Iris/Iris/Algebra/BigOp.lean | 39 +- Iris/Iris/Algebra/CMRA.lean | 9 + Iris/Iris/Algebra/Heap.lean | 568 +++++++++++++++++++++++++++++- Iris/Iris/Algebra/List.lean | 16 + Iris/Iris/BI/BigOp/BigAndMap.lean | 2 +- Iris/Iris/Std/PartialMap.lean | 33 ++ 6 files changed, 659 insertions(+), 8 deletions(-) diff --git a/Iris/Iris/Algebra/BigOp.lean b/Iris/Iris/Algebra/BigOp.lean index 20642200c..e4bc4e23a 100644 --- a/Iris/Iris/Algebra/BigOp.lean +++ b/Iris/Iris/Algebra/BigOp.lean @@ -7,6 +7,7 @@ module public import Iris.Algebra.Monoid public import Iris.Algebra.CMRA +public import Iris.Algebra.Heap import Batteries.Data.List.Perm public import Iris.Std.List public import Iris.Std.PartialMap @@ -439,7 +440,7 @@ theorem bigOpM_const_unit_eq [DecidableEq K] (m : M' V) : @[rocq_alias big_opM_fmap] theorem bigOpM_map_eq (h : V → B) (Φ : K → B → M) (m : M' V) : - ([^ op map] k ↦ x ∈ PartialMap.map h m, Φ k x) = ([^ op map] k ↦ v ∈ m, Φ k (h v)) := + ([^ op map] k ↦ x ∈ Std.PartialMap.map h m, Φ k x) = ([^ op map] k ↦ v ∈ m, Φ k (h v)) := (bigOpL_eq_of_perm _ LawfulFiniteMap.toList_map).trans (bigOpL_map_eq _ _ _) @[rocq_alias big_opM_omap] @@ -597,6 +598,27 @@ theorem bigOpM_weak_hom [DecidableEq K] [ι : WeakMonoidHomomorphism op₁ op₂ show (LawfulFiniteMap.toList m) = [] from List.nil_eq.mpr Hk |>.symm] rfl +@[rocq_alias big_opM_ne_2] +theorem bigOpM_dist_2 [OFE V] {Φ Ψ : K → V → M} {m₁ m₂ : M' V} {n : Nat} (hm : m₁ ≡{n}≡ m₂) + (hf : ∀ {k y₁ y₂}, get? m₁ k = some y₁ → get? m₂ k = some y₂ → y₁ ≡{n}≡ y₂ → + Φ k y₁ ≡{n}≡ Ψ k y₂) : + ([^ op map] k ↦ y ∈ m₁, Φ k y) ≡{n}≡ ([^ op map] k ↦ y ∈ m₂, Ψ k y) := + bigOpM_gen_proper_2 OFE.Dist.of_eq OFE.dist_equivalence op_dist + (PartialMap.isSome_get?_eq_of_dist hm) fun {k _ _} h₁ h₂ => hf h₁ h₂ <| by + have hmk := hm k + rw [h₁, h₂] at hmk + exact OFE.some_dist_some.mp hmk + +open Classical in +@[rocq_alias big_opM_singletons] +theorem bigOpM_singletons [CMRA V] (m : M' V) : + ([^ CMRA.op map] k ↦ x ∈ m, PartialMap.singleton k x) = m := by + induction m using LawfulFiniteMap.induction_on with + | hemp => exact bigOpM_empty _ + | hins i x m hi ih => + rw [bigOpM_insert_eq _ x hi, ih] + exact (equiv_iff_eq.mp (Heap.insert_equiv_singleton_op_singleton hi)).symm + #rocq_ignore big_opM_ne' "Use bigOpM_dist" #rocq_ignore big_opM_proper' "Use bigOpM_eq" @@ -637,6 +659,21 @@ theorem bigOpS_const_unit (s : S) : ([^ op set] _x ∈ s, unit) = unit := by theorem bigOpS_singleton {Φ : A → M} {a : A} : ([^ op set] x ∈ ({a} : S), Φ x) = Φ a := by simp only [bigOpS, toList_singleton]; exact bigOpL_singleton_eq _ _ +open Classical in +@[rocq_alias big_opS_gset_to_gmap] +theorem bigOpS_ofSet {M' : Type _ → Type _} {V : Type _} [LawfulFiniteMap M' A] [CMRA V] + (a : V) (s : S) : + ([^ CMRA.op set] k ∈ s, (PartialMap.singleton k a : M' V)) = FiniteMap.ofSet a s := by + induction s using set_ind with + | hemp => + rw [bigOpS_empty, LawfulFiniteMap.ofSet_empty] + rfl + | hadd x X hx ih => + refine (bigOpS_insert hx).trans ?_ + rw [ih, LawfulFiniteMap.ofSet_insert] + exact (LawfulPartialMap.equiv_iff_eq.mp + (Heap.insert_equiv_singleton_op_singleton (LawfulFiniteMap.get?_ofSet_of_not_mem hx))).symm + @[rocq_alias big_opS_union] theorem bigOpS_union {Φ : A → M} {s₁ s₂ : S} (Hdisj : s₁ ## s₂) : ([^ op set] x ∈ (s₁ ∪ s₂), Φ x) = op ([^ op set] x ∈ s₁, Φ x) ([^ op set] x ∈ s₂, Φ x) := by diff --git a/Iris/Iris/Algebra/CMRA.lean b/Iris/Iris/Algebra/CMRA.lean index cf238df17..144a3cb68 100644 --- a/Iris/Iris/Algebra/CMRA.lean +++ b/Iris/Iris/Algebra/CMRA.lean @@ -1481,6 +1481,15 @@ theorem some_inc_some_iff_is_total [IsTotal α] {a b : α} : some a ≼ some b · exact ⟨_, H.symm.trans (op_core a).symm⟩ · exact H +@[rocq_alias option_fmap_mono] +theorem map_mono {β : Type _} [CMRA β] (f : α → β) {ma mb : Option α} + (hf : ∀ x y : α, x ≼ y → f x ≼ f y) (h : ma ≼ mb) : ma.map f ≼ mb.map f := by + rcases inc_iff.mp h with rfl | ⟨a, b, rfl, rfl, hab⟩ + · exact ⟨mb.map f, by cases mb.map f <;> rfl⟩ + · rcases hab with rfl | hab + · exact .rfl + · exact some_inc_some_iff.mpr (.inr (hf a b hab)) + @[rocq_alias Some_includedN_total] theorem some_incN_some_iff_is_total [IsTotal α] {a b : α} : some a ≼{n} some b ↔ a ≼{n} b := by apply some_incN_some_iff.trans diff --git a/Iris/Iris/Algebra/Heap.lean b/Iris/Iris/Algebra/Heap.lean index 6dd4ca9d5..442b170fb 100644 --- a/Iris/Iris/Algebra/Heap.lean +++ b/Iris/Iris/Algebra/Heap.lean @@ -7,8 +7,13 @@ module public import Iris.Algebra.CMRA public import Iris.Algebra.OFE +public import Iris.Algebra.IsOp +public import Iris.Algebra.LocalUpdates +public import Iris.Algebra.Updates +public import Iris.Std.Infinite public import Iris.Std.Set public import Iris.Std.PartialMap +meta import Iris.Std.RocqPorting @[expose] public section @@ -20,6 +25,7 @@ open OFE namespace PartialMap +@[rocq_alias gmap_dist, rocq_alias gmap_ofe_mixin, rocq_alias gmapO] instance instOFE [LawfulPartialMap M K] [OFE V] : OFE (M V) where Dist n s0 s1 := get? s0 ≡{n}≡ get? s1 dist_eqv := ⟨fun _ => .of_eq rfl, (·.symm), (·.trans ·)⟩ @@ -36,9 +42,11 @@ instance instOFE [LawfulPartialMap M K] [OFE V] : OFE (M V) where f x := of_fun x ne.1 {_ _ _} H k := by simp only [get_of_fun, H k] +@[rocq_alias lookup_ne] instance get?_ne [LawfulPartialMap M K] [OFE V] (k : K) : NonExpansive (get? · k : M V → Option V) where ne {_ _ _} Ht := Ht k +@[rocq_alias insert_ne] instance [LawfulPartialMap M K] [OFE V] (k : K) : NonExpansive₂ (insert · k · : M V → V → M V) where ne {_ _ _} Hv {_ _} Ht k' := by by_cases h : k = k' @@ -52,7 +60,103 @@ instance [LawfulPartialMap M K] [OFE V] (op : K → V → V → V) [∀ k, NonEx NonExpansive₂ (merge (M := M) op) where ne _ {_ _} Ht {_ _} Hs k := by simp only [get?_merge]; exact NonExpansive₂.ne (Ht k) (Hs k) +open Classical in +@[rocq_alias delete_ne] +instance [LawfulPartialMap M K] [OFE V] (k : K) : NonExpansive (delete · k : M V → M V) where + ne {_ _ _} Ht k' := by + by_cases h : k = k' + · simp [get?_delete_eq h] + · simp [get?_delete_ne h, Ht k'] + +/-- `bindAlter` is non-expansive in both the alteration and the map. -/ +@[rocq_alias partial_alter_ne, rocq_alias alter_ne] +theorem bindAlter_dist [LawfulPartialMap M K] [OFE V] [OFE V'] {n : Nat} + {f g : K → V → Option V'} {m₁ m₂ : M V} + (Hf : ∀ {k v w}, v ≡{n}≡ w → f k v ≡{n}≡ g k w) (Hm : m₁ ≡{n}≡ m₂) : + bindAlter f m₁ ≡{n}≡ bindAlter g m₂ := by + intro k + specialize Hm k + revert Hm + simp only [OFE.Dist, Option.Forall₂, get?_bindAlter] + cases get? m₁ k <;> cases get? m₂ k <;> simp_all + exact Hf + +/-- `merge` is non-expansive in both the merge function and the maps. -/ +@[rocq_alias merge_ne, rocq_alias union_with_ne] +theorem merge_dist [LawfulPartialMap M K] [OFE V] {n : Nat} {f g : K → V → V → V} + {m₁ m₁' m₂ m₂' : M V} + (Hf : ∀ {k v v' w w'}, v ≡{n}≡ v' → w ≡{n}≡ w' → f k v w ≡{n}≡ g k v' w') + (H₁ : m₁ ≡{n}≡ m₁') (H₂ : m₂ ≡{n}≡ m₂') : merge f m₁ m₂ ≡{n}≡ merge g m₁' m₂' := by + intro k + specialize H₁ k + specialize H₂ k + revert H₁ H₂ + simp only [OFE.Dist, Option.Forall₂, get?_merge, Option.merge] + cases get? m₁ k <;> cases get? m₁' k <;> cases get? m₂ k <;> cases get? m₂' k <;> simp_all + +/-- `zipWith` is non-expansive in both the combining function and the maps. -/ +@[rocq_alias map_zip_with_ne] +theorem zipWith_dist [LawfulPartialMap M K] [OFE V] [OFE V'] [OFE V''] {n : Nat} + {f g : V → V' → V''} {m₁ m₁' : M V} {m₂ m₂' : M V'} + (Hf : ∀ {v v' w w'}, v ≡{n}≡ v' → w ≡{n}≡ w' → f v w ≡{n}≡ g v' w') + (H₁ : m₁ ≡{n}≡ m₁') (H₂ : m₂ ≡{n}≡ m₂') : + PartialMap.zipWith f m₁ m₂ ≡{n}≡ PartialMap.zipWith g m₁' m₂' := by + intro k + specialize H₁ k + specialize H₂ k + revert H₁ H₂ + simp only [OFE.Dist, Option.Forall₂, LawfulPartialMap.get?_zipWith] + cases get? m₁ k <;> cases get? m₁' k <;> cases get? m₂ k <;> cases get? m₂' k <;> simp_all + +theorem isSome_get?_eq_of_dist [LawfulPartialMap M K] [OFE V] {n : Nat} {m₁ m₂ : M V} + (H : m₁ ≡{n}≡ m₂) (k : K) : (get? m₁ k).isSome = (get? m₂ k).isSome := by + specialize H k + revert H + simp only [OFE.Dist, Option.Forall₂] + cases get? m₁ k <;> cases get? m₂ k <;> simp_all + +@[rocq_alias gmap_union_ne] +instance [LawfulPartialMap M K] [OFE V] : NonExpansive₂ ((· ∪ ·) : M V → M V → M V) where + ne _ {_ _} H₁ {_ _} H₂ := merge_dist (fun H _ => H) H₁ H₂ + +@[rocq_alias gmap_difference_ne] +instance [LawfulPartialMap M K] [OFE V] : NonExpansive₂ ((· \ ·) : M V → M V → M V) where + ne _ {m₁ m₁'} H₁ {_ m₂'} H₂ k := by + specialize H₁ k + revert H₁ + simp only [OFE.Dist, Option.Forall₂, LawfulPartialMap.get?_difference, + isSome_get?_eq_of_dist H₂ k] + cases get? m₁ k <;> cases get? m₁' k <;> cases get? m₂' k <;> simp_all + +@[rocq_alias gmap_disjoint_ne] +theorem disjoint_dist_iff [LawfulPartialMap M K] [OFE V] {n : Nat} {m₁ m₁' m₂ m₂' : M V} + (H₁ : m₁ ≡{n}≡ m₁') (H₂ : m₂ ≡{n}≡ m₂') : + PartialMap.disjoint m₁ m₂ ↔ PartialMap.disjoint m₁' m₂' := + forall_congr' fun k => not_congr <| and_congr + (by rw [isSome_get?_eq_of_dist H₁ k]) (by rw [isSome_get?_eq_of_dist H₂ k]) + +open Classical in +@[rocq_alias gmap_union_dist_eq] +theorem union_dist_iff [LawfulPartialMap M K] [OFE V] {n : Nat} {m m₁ m₂ : M V} : + m ≡{n}≡ m₁ ∪ m₂ ↔ ∃ m₁' m₂', m = m₁' ∪ m₂' ∧ m₁' ≡{n}≡ m₁ ∧ m₂' ≡{n}≡ m₂ := by + refine ⟨fun hm => ⟨PartialMap.filter (fun k _ => (get? m₁ k).isSome) m, + PartialMap.zipWith (fun v _ => v) m₂ m₁ ∪ PartialMap.filter (fun k _ => (get? m₂ k).isSome) m, + LawfulPartialMap.equiv_iff_eq.mp fun k => ?_, fun k => ?_, fun k => ?_⟩, + fun ⟨_, _, hm, h₁, h₂⟩ => hm ▸ NonExpansive₂.ne h₁ h₂⟩ + all_goals + specialize hm k + revert hm + simp only [OFE.Dist, Option.Forall₂, LawfulPartialMap.get?_union, + LawfulPartialMap.get?_filter, LawfulPartialMap.get?_zipWith] + cases get? m k <;> cases get? m₁ k <;> cases get? m₂ k <;> simp_all + +@[rocq_alias gmap_dom_ne] +theorem dom_eq_of_dist [LawfulPartialMap M K] [OFE V] {n : Nat} {m₁ m₂ : M V} + (H : m₁ ≡{n}≡ m₂) : PartialMap.dom m₁ = PartialMap.dom m₂ := + funext fun k => congrArg (· = true) (isSome_get?_eq_of_dist H k) + /-- Project a chain of stores through its kth coordinate to a chain of values. -/ +@[rocq_alias gmap_chain] def chain [LawfulPartialMap M K] [OFE V] (k : K) (c : Chain (M V)) : Chain (Option V) where chain i := get? (c i) k cauchy Hni := c.cauchy Hni k @@ -62,6 +166,7 @@ theorem chain_get [LawfulPartialMap M K] [OFE V] (k : K) (c : Chain (M V)) : end PartialMap +@[rocq_alias gmap_compl, rocq_alias gmap_cofe] instance Heap.instCOFE [LawfulPartialMap M K] [COFE V] : COFE (M V) where compl c := bindAlter (fun _ => COFE.compl <| c.map ⟨_, PartialMap.get?_ne ·⟩) (c 0) conv_compl {_ c} k := by @@ -70,11 +175,13 @@ instance Heap.instCOFE [LawfulPartialMap M K] [COFE V] : COFE (M V) where · simp [← PartialMap.chain_get, chain_none_const (c := PartialMap.chain k c) (n := 0) (H▸rfl)] · exact IsCOFE.conv_compl +@[rocq_alias gmap_ofe_discrete] instance instDiscreteHeap [LawfulPartialMap M K] [OFE V] [Discrete V] : Discrete (M V) where discrete_0 h := OFE.eq_dist.mpr <| by intro _ k exact (Discrete.discrete_0 (h k)).dist +@[rocq_alias gmap_singleton_discrete] instance instDiscreteESingleton [LawfulPartialMap M K] [DecidableEq K] [OFE V] {v : V} [ha : DiscreteE v] {k : K} : DiscreteE (PartialMap.singleton (M := M) k v) where discrete {y} h := OFE.eq_dist.mpr <| by @@ -87,6 +194,7 @@ instance instDiscreteESingleton [LawfulPartialMap M K] [DecidableEq K] [OFE V] { refine (Option.none_is_discrete.discrete (.trans ?_ (h k'))).dist simp [LawfulPartialMap.get?_singleton, hh, ↓reduceIte] +@[rocq_alias gmap_empty_discrete] instance instDiscreteEEmpty [LawfulPartialMap M K] [OFE V] : DiscreteE (∅ : M V) where discrete {y} h := OFE.eq_dist.mpr <| by intro n k @@ -94,12 +202,51 @@ instance instDiscreteEEmpty [LawfulPartialMap M K] [OFE V] : DiscreteE (∅ : M refine (DiscreteE.discrete (.trans ?_ (h k))).dist simp [LawfulPartialMap.get?_empty] +@[rocq_alias singleton_ne] theorem singleton_dist [LawfulPartialMap M K] [DecidableEq K] [OFE V] {n : Nat} {x y : V} (h : x ≡{n}≡ y) (k : K) : PartialMap.singleton (M := M) k x ≡{n}≡ PartialMap.singleton k y := by intro k' simp only [LawfulPartialMap.get?_singleton] split <;> simp [h] +open Classical in +@[rocq_alias insert_idN] +theorem insert_idN [LawfulPartialMap M K] [OFE V] {n : Nat} {m : M V} {i : K} {x : V} + (h : get? m i ≡{n}≡ some x) : insert m i x ≡{n}≡ m := fun k => by + by_cases hk : i = k + · subst hk + rw [get?_insert_eq rfl] + exact h.symm + · rw [get?_insert_ne hk] + +open Classical in +@[rocq_alias gmap_lookup_discrete] +instance instDiscreteEGet? [LawfulPartialMap M K] [OFE V] {m : M V} [DiscreteE m] {i : K} : + DiscreteE (get? m i) where + discrete {y} h := by + rcases y with _ | v + · revert h + cases get? m i <;> simp_all [OFE.Dist, Option.Forall₂] + · refine (congrArg (get? · i) + (DiscreteE.discrete (y := insert m i v) fun k => ?_)).trans (get?_insert_eq rfl) + by_cases hk : i = k + · subst hk + rw [get?_insert_eq rfl] + exact h + · rw [get?_insert_ne hk] + +open Classical in +@[rocq_alias gmap_insert_discrete] +instance [LawfulPartialMap M K] [OFE V] {m : M V} {i : K} {x : V} [DiscreteE x] [DiscreteE m] : + DiscreteE (insert m i x) where + discrete {y} h := LawfulPartialMap.equiv_iff_eq.mp fun k => by + have hk' := h k + by_cases hk : i = k + · rw [get?_insert_eq hk] at hk' ⊢ + exact Option.some_is_discrete.discrete hk' + · rw [get?_insert_ne hk] at hk' ⊢ + exact DiscreteE.discrete hk' + end OFE section CMRA @@ -113,12 +260,18 @@ open PartialMap variable [LawfulPartialMap M K] [CMRA V] -@[simp] def op (s1 s2 : M V) : M V := merge (fun _ => CMRA.op) s1 s2 -@[simp] def unit : M V := ∅ -@[simp] def pcore (s : M V) : Option (M V) := some <| bindAlter (fun _ => CMRA.pcore) s -@[simp] def valid (s : M V) : Prop := ∀ k, ✓ get? s k -@[simp] def validN (n : Nat) (s : M V) : Prop := ∀ k, ✓{n} get? s k - +@[simp, rocq_alias gmap_op_instance, rocq_alias gmap_op] +def op (s1 s2 : M V) : M V := merge (fun _ => CMRA.op) s1 s2 +@[simp, rocq_alias gmap_unit_instance] +def unit : M V := ∅ +@[simp, rocq_alias gmap_pcore_instance] +def pcore (s : M V) : Option (M V) := some <| bindAlter (fun _ => CMRA.pcore) s +@[simp, rocq_alias gmap_valid_instance] +def valid (s : M V) : Prop := ∀ k, ✓ get? s k +@[simp, rocq_alias gmap_validN_instance] +def validN (n : Nat) (s : M V) : Prop := ∀ k, ✓{n} get? s k + +@[rocq_alias lookup_includedN] theorem lookup_incN {n} {m1 m2 : M V} : (∃ (z : M V), m2 ≡{n}≡ op m1 z) ↔ ∀ i, (∃ z, (get? m2 i) ≡{n}≡ (get? m1 i) • z) := by @@ -134,6 +287,7 @@ theorem lookup_incN {n} {m1 m2 : M V} : simp [CMRA.op, get?_merge, get?_bindAlter] cases get? m2 i <;> cases get? m1 i <;> cases f i <;> simp +@[rocq_alias lookup_included] theorem lookup_inc {m1 m2 : M V} : (∃ (z : M V), m2 = op m1 z) ↔ ∀ i, (∃ z, (get? m2 i) = (get? m1 i) • z) := by @@ -151,6 +305,7 @@ theorem lookup_inc {m1 m2 : M V} : exact fun h => (OFE.not_none_eqv_some h).elim open OFE in +@[rocq_alias gmap_cmra_mixin, rocq_alias gmapR] instance instStoreCMRA : CMRA (M V) where pcore := pcore op := op @@ -255,6 +410,7 @@ instance instStoreCMRA : CMRA (M V) where simp only [h, Option.bind_some] refine Hz2.trans (.of_eq h) +@[rocq_alias gmap_ucmra_mixin, rocq_alias gmapUR] instance instStoreUCMRA : UCMRA (M V) where unit := unit unit_valid := by simp [CMRA.Valid, get?_empty] @@ -277,13 +433,38 @@ variable {K V : Type _} [LawfulPartialMap M K] [CMRA V] open CMRA +@[rocq_alias lookup_op] theorem get?_op (x y : M V) : get? (x • y) i = get? x i • get? y i := by simp only [CMRA.op, op, get?_merge, Option.merge, optionOp] grind +@[rocq_alias lookup_opM] +theorem get?_opM (m : M V) (mm : Option (M V)) (i : K) : + get? (m •? mm) i = get? m i • mm.bind (get? · i) := by + cases mm with + | none => + show get? m i = get? m i • none + cases get? m i <;> rfl + | some m' => exact get?_op m m' + +@[rocq_alias lookup_core] +theorem get?_core (m : M V) (i : K) : get? (core m) i = core (get? m i) := by + simp only [core, CMRA.pcore, pcore, Option.getD_some, get?_bindAlter, optionCore] + +@[rocq_alias lookup_op_homomorphism] +instance (i : K) : Algebra.MonoidHomomorphism (CMRA.op (α := M V)) (CMRA.op (α := Option V)) + UCMRA.unit UCMRA.unit (· = ·) (get? · i) where + rel_refl := rfl + rel_trans := Eq.trans + op_proper h₁ h₂ := h₁ ▸ h₂ ▸ rfl + map_ne := get?_ne i + map_op := get?_op .. + map_unit := get?_empty i + theorem valid_empty : ✓ (∅ : M V) := fun k => by simp [Valid, show get? ∅ k = none from get?_empty (M := M) k] +@[rocq_alias lookup_validN_Some] theorem validN_get?_validN {m : M V} (Hv : ✓{n} m) (He : get? m i ≡{n}≡ some x) : ✓{n} x := by specialize Hv i; revert Hv rcases h : get? m i <;> simp [h] at He @@ -294,6 +475,7 @@ theorem validN_get? {m : M V} (v : ✓{n} m) : ✓{n} get? m i := | none => ⟨⟩ | some z => show ✓{n} z from validN_get?_validN v (OFE.Dist.of_eq hh) +@[rocq_alias lookup_valid_Some] theorem valid_get?_valid {m : M V} (Hv : ✓ m) (He : get? m i = some x) : ✓ x := valid_iff_validN.mpr (fun _ => validN_get?_validN Hv.validN He.dist) @@ -301,38 +483,45 @@ theorem valid_get? {m : M V} (v : ✓ m) : ✓ get? m i := valid_iff_validN.mpr (fun _ => Valid.validN (v i)) open Classical in +@[rocq_alias insert_validN] theorem insert_validN {m : M V} (Hx : ✓{n} x) (Hm : ✓{n} m) : ✓{n} (insert m i x) := by intro k rw [get?_insert]; split · exact Hx · apply Hm +@[rocq_alias insert_valid] theorem insert_valid {m : M V} (Hx : ✓ x) (Hm : ✓ m) : ✓ (insert m i x) := valid_iff_validN.mpr (fun _ => insert_validN Hx.validN Hm.validN) open Classical in +@[rocq_alias singleton_valid] theorem singleton_valid_iff : ✓ (singleton i x : M V) ↔ ✓ x := by refine ⟨fun H => ?_, fun H k => ?_⟩ · specialize H i; rw [get?_singleton_eq rfl] at H; trivial · rw [get?_singleton]; split <;> trivial open Classical in +@[rocq_alias singleton_validN] theorem singleton_validN_iff : ✓{n} (singleton i x : M V) ↔ ✓{n} x := by refine ⟨fun H => ?_, fun H k => ?_⟩ · specialize H i; rw [get?_singleton_eq rfl] at H; trivial · rw [get?_singleton]; split <;> trivial open Classical in +@[rocq_alias delete_validN] theorem delete_validN {m : M V} (Hv : ✓{n} m) : ✓{n} (delete m i) := by intro k rw [get?_delete]; split · trivial · exact Hv k +@[rocq_alias delete_valid] theorem delete_valid {m : M V} (Hv : ✓ m) : ✓ (delete m i) := valid_iff_validN.mpr (fun _ => delete_validN Hv.validN) open Classical in +@[rocq_alias insert_singleton_op] theorem insert_equiv_singleton_op_singleton {m : M V} (Hemp : get? m i = none) : equiv (insert m i x) (singleton i x • m) := by refine (fun k => ?_) @@ -350,6 +539,7 @@ theorem core_empty : core (∅ : M V) = ∅ := OFE.eq_dist.mpr <| by simp [core, CMRA.pcore, get?_empty, get?_bindAlter] open Classical in +@[rocq_alias singleton_core'] theorem core_singleton_equiv {i : K} {x : V} {cx : V} (Hpcore : CMRA.pcore x = some cx) : equiv (core <| singleton i x : M V) (singleton i cx) := by refine fun k => ?_ @@ -361,12 +551,14 @@ theorem singleton_core_eq [IsoFunMap M K] {i : K} {x : V} {cx} (Hpcore : CMRA.pc IsoFunMap.ext (core_singleton_equiv Hpcore) open Classical in +@[rocq_alias singleton_core] theorem singleton_core_eqv {i : K} {x : V} {cx} (Hpcore : CMRA.pcore x = some cx) : core (singleton i x : M V) = singleton i cx := OFE.eq_dist.mpr <| by intro n k simp [core, CMRA.pcore, get?_singleton, get?_bindAlter] split <;> first | exact Hpcore.dist | trivial +@[rocq_alias singleton_core_total] theorem singleton_core_total [IsTotal V] {i : K} {x : V} : equiv (core <| singleton i x : M V) ((singleton i (core x))) := core_singleton_equiv (pcore_eq_core x) @@ -376,6 +568,7 @@ theorem singleton_core_total_eq [IsTotal V] [IsoFunMap M K] {i : K} {x : V} : IsoFunMap.ext singleton_core_total open Classical in +@[rocq_alias singleton_op] theorem singleton_op_singleton {i : K} {x y : V} : equiv ((singleton i x : M V) • (singleton i y)) (singleton i (x • y)) := by refine fun k => ?_ @@ -386,6 +579,24 @@ theorem singleton_op_singleton_eq [IsoFunMap M K] {i : K} {x y : V} : (singleton i x : M V) • (singleton i y) = (singleton i (x • y)) := IsoFunMap.ext singleton_op_singleton +open Classical in +set_option synthInstance.checkSynthOrder false in +@[rocq_alias singleton_is_op] +instance {d : IsOp.Direction} {i : K} {x x₁ x₂ : V} [h : IsOp d x x₁ x₂] : + IsOp d (singleton i x : M V) (singleton i x₁ : M V) (singleton i x₂ : M V) where + is_op := by rw [h.is_op, ← equiv_iff_eq.mp singleton_op_singleton] + +open Classical in +@[rocq_alias gmap_core_id] +theorem coreId_of_get? {m : M V} (h : ∀ {i x}, get? m i = some x → CoreId x) : CoreId m where + core_id := OFE.eq_dist.mpr fun _ => by + refine OFE.some_dist_some.mpr fun k => ?_ + rw [get?_bindAlter] + rcases hk : get? m k with _ | v + · simp + · simp [(h hk).core_id] + +@[rocq_alias gmap_core_id'] instance {m : M V} [I : ∀ x : V, CoreId x] : CoreId m where core_id := OFE.eq_dist.mpr fun _ => by refine OFE.some_dist_some.mpr fun k => ?_ @@ -394,6 +605,7 @@ instance {m : M V} [I : ∀ x : V, CoreId x] : CoreId m where exact core_id.dist open Classical in +@[rocq_alias gmap_singleton_core_id] instance [CoreId (x : V)] : CoreId (singleton i x : M V) where core_id := OFE.eq_dist.mpr fun _ => by refine OFE.some_dist_some.mpr fun k => ?_ @@ -402,6 +614,7 @@ instance [CoreId (x : V)] : CoreId (singleton i x : M V) where exact core_id.dist open Classical in +@[rocq_alias singleton_includedN_l] theorem singleton_incN_iff {m : M V} : (singleton i x) ≼{n} m ↔ ∃ y, (get? m i ≡{n}≡ some y) ∧ some x ≼{n} some y := by refine ⟨fun ⟨z, Hz⟩ => ?_, fun ⟨y, Hy, z, Hz⟩ => ?_⟩ @@ -434,6 +647,7 @@ theorem singleton_incN_iff {m : M V} : · simp open Classical in +@[rocq_alias singleton_included_l] theorem singleton_inc_iff {m : M V} : (singleton i x) ≼ m ↔ ∃ y, (get? m i = some y) ∧ some x ≼ some y := by refine ⟨fun ⟨z, Hz⟩ => ?_, fun ⟨y, Hy, z, Hz⟩ => ?_⟩ @@ -465,6 +679,7 @@ theorem singleton_inc_iff {m : M V} : simp [CMRA.op] · simp +@[rocq_alias singleton_included_exclusive_l] theorem exclusive_singleton_inc_iff {m : M V} (He : Exclusive x) (Hv : ✓ m) : (singleton i x) ≼ m ↔ (get? m i = some x) := by refine singleton_inc_iff.trans ⟨fun ⟨y, Hy, Hxy⟩ => ?_, fun _ => ?_⟩ @@ -472,21 +687,25 @@ theorem exclusive_singleton_inc_iff {m : M V} (He : Exclusive x) (Hv : ✓ m) : exact Option.eqv_of_inc_exclusive Hxy <| valid_get?_valid Hv Hy · exists x +@[rocq_alias singleton_included] theorem singleton_inc_singleton_iff : (singleton i x : M V) ≼ (singleton i y : M V) ↔ some x ≼ some y := by refine singleton_inc_iff.trans ⟨fun ⟨z, Hz, Hxz⟩ => ?_, fun H => ?_⟩ · exact (Hz.symm.trans <| get?_singleton_eq rfl) ▸ Hxz · refine ⟨y, ?_, H⟩ exact get?_singleton_eq rfl +@[rocq_alias singleton_included_total] theorem total_singleton_inc_singleton_iff [IsTotal V] : (singleton i x : M V) ≼ (singleton i y) ↔ x ≼ y := singleton_inc_singleton_iff.trans <| Option.some_inc_some_iff_is_total +@[rocq_alias singleton_included_mono] theorem singleton_inc_singleton_mono (Hinc : x ≼ y) : (singleton i x : M V) ≼ (singleton i y) := singleton_inc_singleton_iff.mpr <| Option.some_inc_some_iff.mpr <| .inr Hinc open Classical in +@[rocq_alias singleton_cancelable] instance [H : Cancelable (some x)] : Cancelable (singleton i x : M V) where cancelableN {n m1 m2} Hv He j := by specialize Hv j; revert Hv @@ -500,6 +719,7 @@ instance [H : Cancelable (some x)] : Cancelable (singleton i x : M V) where all_goals simp_all [CMRA.op, optionOp] · cases get? m1 j <;> cases get? m2 j <;> simp_all +@[rocq_alias gmap_cancelable] instance {m : M V} [Hid : ∀ x : V, IdFree x] [Hc : ∀ x : V, Cancelable x] : Cancelable m where cancelableN {n m1 m2} Hv He i := by apply cancelableN (x := get? m i) @@ -510,6 +730,7 @@ instance {m : M V} [Hid : ∀ x : V, IdFree x] [Hc : ∀ x : V, Cancelable x] : simp [get?_merge, CMRA.op, Heap.op, optionOp] cases get? m i <;> cases get? m1 i <;> cases get? m2 i <;> simp_all +@[rocq_alias insert_op] theorem insert_op_equiv {m1 m2 : M V} : equiv ((insert (m1 • m2) i (x • y))) (insert m1 i x • insert m2 i y) := by refine fun j => ?_ @@ -521,6 +742,7 @@ theorem insert_op_eq [IsoFunMap M K] {m1 m2 : M (Option V)} : (insert (m1 • m2) i (x • y)) = (insert m1 i x • insert m2 i y) := IsoFunMap.ext insert_op_equiv +@[rocq_alias gmap_op_union] theorem disjoint_op_equiv_union {m1 m2 : M V} (Hd : Set.Disjoint (dom m1) (dom m2)) : equiv (m1 • m2) (union m1 m2) := by refine fun j => ?_ @@ -533,6 +755,7 @@ theorem disjoint_op_eq_union [IsoFunMap M K] {m1 m2 : M V} (H : Set.Disjoint (do m1 • m2 = union m1 m2 := IsoFunMap.ext (disjoint_op_equiv_union H) +@[rocq_alias gmap_op_valid0_disjoint] theorem valid0_disjoint_dom {m1 m2 : M V} (Hv : ✓{0} (m1 • m2)) (H : ∀ {k x}, get? m1 k = some x → Exclusive x) : Set.Disjoint (dom m1) (dom m2) := by rintro k @@ -543,14 +766,17 @@ theorem valid0_disjoint_dom {m1 m2 : M V} (Hv : ✓{0} (m1 • m2)) (H : ∀ {k simp [CMRA.op, CMRA.ValidN] at Hv; specialize Hv k; revert Hv simp [get?_merge, HX, HY] +@[rocq_alias gmap_op_valid_disjoint] theorem valid_disjoint_dom {m1 m2 : M V} (Hv : ✓ (m1 • m2)) (H : ∀ {k x}, get? m1 k = some x → Exclusive x) : Set.Disjoint (dom m1) (dom m2) := valid0_disjoint_dom (Valid.validN Hv) H +@[rocq_alias dom_op] theorem dom_op_union (m1 m2 : M V) : dom (m1 • m2) = Set.Union (dom m1) (dom m2) := by refine funext fun k => ?_ cases get? m1 k <;> cases get? m2 k <;> simp_all [CMRA.op, dom, Set.Union, get?_merge] +@[rocq_alias dom_included] theorem inc_dom_inc {m1 m2 : M V} (Hinc : m1 ≼ m2) : Set.Included (dom m1) (dom m2) := by intro i unfold dom @@ -559,12 +785,329 @@ theorem inc_dom_inc {m1 m2 : M V} (Hinc : m1 ≼ m2) : Set.Included (dom m1) (do cases get? m1 i <;> cases get? m2 i <;> cases z <;> simp [CMRA.op, optionOp] <;> exact fun h => (OFE.not_none_eqv_some h).elim +@[rocq_alias gmap_fmap_mono] +theorem map_mono [CMRA V'] (f : V → V') (hf : ∀ x y : V, x ≼ y → f x ≼ f y) {m1 m2 : M V} + (Hinc : m1 ≼ m2) : PartialMap.map f m1 ≼ PartialMap.map f m2 := by + refine lookup_inc.mpr fun i => ?_ + obtain ⟨z, hz⟩ := Option.map_mono f hf (lookup_inc.mp Hinc i) + exact ⟨z, by rw [get?_map, get?_map, hz]⟩ + +@[rocq_alias gmap_cmra_discrete] nonrec instance [HD : CMRA.Discrete V] [LawfulPartialMap M K] : Discrete (M V) where discrete_0 {_ _} H := OFE.eq_dist.mpr fun _ k => (OFE.Discrete.discrete_0 (H k)).dist discrete_valid {_} := (CMRA.Discrete.discrete_valid <| · ·) +/-! ## Frame-preserving updates -/ + +open Classical in +@[rocq_alias insert_updateP] +theorem insert_updateP {P : V → Prop} {Q : M V → Prop} {m : M V} {i : K} {x : V} + (hx : x ~~>: P) (hQ : ∀ y, P y → Q (insert m i y)) : insert m i x ~~>: Q := by + refine UpdateP.total.mpr fun n mf hv => ?_ + have hi : ✓{n} (some x • get? mf i) := by + have hvi := hv i + rwa [get?_op, get?_insert_eq rfl] at hvi + obtain ⟨_ | y, hy, hvy⟩ := UpdateP.option' P x hx n (some (get? mf i)) hi + · exact hy.elim + refine ⟨insert m i y, hQ y hy, fun k => ?_⟩ + by_cases hk : i = k + · subst hk + rw [get?_op, get?_insert_eq rfl] + exact hvy + · have hvk := hv k + rw [get?_op, get?_insert_ne hk] at hvk ⊢ + exact hvk + +@[rocq_alias insert_updateP'] +theorem insert_updateP' {P : V → Prop} {m : M V} {i : K} {x : V} (hx : x ~~>: P) : + insert m i x ~~>: fun m' => ∃ y, m' = insert m i y ∧ P y := + insert_updateP hx fun y hy => ⟨y, rfl, hy⟩ + +@[rocq_alias insert_update] +theorem insert_update {m : M V} {i : K} {x y : V} (h : x ~~> y) : + insert m i x ~~> insert m i y := + .of_updateP <| insert_updateP (.of_update h) fun _ => congrArg _ + +@[rocq_alias singleton_updateP] +theorem singleton_updateP {P : V → Prop} {Q : M V → Prop} {i : K} {x : V} + (hx : x ~~>: P) (hQ : ∀ y, P y → Q (singleton i y)) : (singleton i x : M V) ~~>: Q := + insert_updateP hx hQ + +@[rocq_alias singleton_updateP'] +theorem singleton_updateP' {P : V → Prop} {i : K} {x : V} (hx : x ~~>: P) : + (singleton i x : M V) ~~>: fun m => ∃ y, m = singleton i y ∧ P y := + insert_updateP' hx + +@[rocq_alias singleton_update] +theorem singleton_update {i : K} {x y : V} (h : x ~~> y) : + (singleton i x : M V) ~~> singleton i y := + insert_update h + +open Classical in +@[rocq_alias delete_update] +theorem delete_update {m : M V} {i : K} : m ~~> delete m i := by + refine Update.total.mpr fun n mf hv k => ?_ + have hvk := hv k + rw [get?_op] at hvk ⊢ + by_cases hk : i = k + · rw [get?_delete_eq hk] + exact validN_op_right hvk + · rwa [get?_delete_ne hk] + end Heap +/-! ## Allocation -/ + +section Freshness + +open CMRA PartialMap LawfulPartialMap + +variable [LawfulFiniteMap M K] + +namespace Heap + +theorem get?_eq_none_of_not_mem_keys {m : M V} {i : K} + (hi : i ∉ (toList m).map (·.1)) : get? m i = none := by + rcases hm : get? m i with _ | v + · rfl + · exact absurd (List.mem_map_of_mem (toList_get.mpr hm)) hi + +variable [CMRA V] + +open Classical in +@[rocq_alias alloc_updateP_strong_dep] +theorem alloc_updateP_strong_dep {Q : M V → Prop} {I : K → Prop} {m : M V} {f : K → V} + (hI : PredInfinite I) (hf : ∀ i, get? m i = none → I i → ✓ f i) + (hQ : ∀ i, get? m i = none → I i → Q (insert m i (f i))) : m ~~>: Q := by + refine UpdateP.total.mpr fun n mf hv => ?_ + obtain ⟨i, hIi, hi⟩ := hI ((toList (m • mf)).map (·.1)) + obtain ⟨hmi, hmfi⟩ := (Option.op_none_iff _ _).mp <| + get?_op m mf ▸ get?_eq_none_of_not_mem_keys hi + refine ⟨insert m i (f i), hQ i hmi hIi, fun k => ?_⟩ + by_cases hk : i = k + · subst hk + rw [get?_op, get?_insert_eq rfl, hmfi] + exact (hf i hmi hIi).validN + · have hvk := hv k + rw [get?_op, get?_insert_ne hk] + rwa [get?_op] at hvk + +@[rocq_alias alloc_updateP_strong] +theorem alloc_updateP_strong {Q : M V → Prop} {I : K → Prop} {m : M V} {x : V} + (hI : PredInfinite I) (hx : ✓ x) + (hQ : ∀ i, get? m i = none → I i → Q (insert m i x)) : m ~~>: Q := + alloc_updateP_strong_dep (f := fun _ => x) hI (fun _ _ _ => hx) hQ + +@[rocq_alias alloc_updateP] +theorem alloc_updateP [InfiniteType K] {Q : M V → Prop} {m : M V} {x : V} (hx : ✓ x) + (hQ : ∀ i, get? m i = none → Q (insert m i x)) : m ~~>: Q := + alloc_updateP_strong PredInfinite.true hx fun i hi _ => hQ i hi + +@[rocq_alias alloc_updateP_cofinite] +theorem alloc_updateP_cofinite [InfiniteType K] {Q : M V → Prop} {m : M V} {x : V} + (J : List K) (hx : ✓ x) + (hQ : ∀ i, get? m i = none → i ∉ J → Q (insert m i x)) : m ~~>: Q := + alloc_updateP_strong (PredInfinite.not_mem J) hx hQ + +@[rocq_alias alloc_updateP_strong_dep'] +theorem alloc_updateP_strong_dep' {I : K → Prop} {m : M V} {f : K → V} + (hI : PredInfinite I) (hf : ∀ i, get? m i = none → I i → ✓ f i) : + m ~~>: fun m' => ∃ i, I i ∧ m' = insert m i (f i) ∧ get? m i = none := + alloc_updateP_strong_dep hI hf fun i hi hIi => ⟨i, hIi, rfl, hi⟩ + +@[rocq_alias alloc_updateP_strong'] +theorem alloc_updateP_strong' {I : K → Prop} {m : M V} {x : V} + (hI : PredInfinite I) (hx : ✓ x) : + m ~~>: fun m' => ∃ i, I i ∧ m' = insert m i x ∧ get? m i = none := + alloc_updateP_strong hI hx fun i hi hIi => ⟨i, hIi, rfl, hi⟩ + +@[rocq_alias alloc_updateP'] +theorem alloc_updateP' [InfiniteType K] {m : M V} {x : V} (hx : ✓ x) : + m ~~>: fun m' => ∃ i, m' = insert m i x ∧ get? m i = none := + alloc_updateP hx fun i hi => ⟨i, rfl, hi⟩ + +@[rocq_alias alloc_updateP_cofinite'] +theorem alloc_updateP_cofinite' [InfiniteType K] {m : M V} {x : V} (J : List K) (hx : ✓ x) : + m ~~>: fun m' => ∃ i, i ∉ J ∧ m' = insert m i x ∧ get? m i = none := + alloc_updateP_cofinite J hx fun i hi hJ => ⟨i, hJ, rfl, hi⟩ + +end Heap + +end Freshness + +section Properties + +open CMRA PartialMap LawfulPartialMap + +variable [LawfulPartialMap M K] [CMRA V] + +namespace Heap + +open Classical in +@[rocq_alias alloc_unit_singleton_updateP] +theorem alloc_unit_singleton_updateP {P : V → Prop} {Q : M V → Prop} {u : V} {i : K} + (hu : ✓ u) (hid : ∀ x : V, u • x = x) (hx : u ~~>: P) + (hQ : ∀ y, P y → Q (singleton i y)) : (∅ : M V) ~~>: Q := by + refine UpdateP.total.mpr fun n gf hv => ?_ + have hi : ✓{n} (u •? get? gf i) := by + have hvi := hv i + rw [get?_op, get?_empty] at hvi + rcases hgf : get? gf i with _ | z + · exact hu.validN + · rw [hgf] at hvi + show ✓{n} (u • z) + rw [hid z] + exact hvi + obtain ⟨y, hy, hvy⟩ := hx n (get? gf i) hi + refine ⟨singleton i y, hQ y hy, fun k => ?_⟩ + by_cases hk : i = k + · subst hk + rw [get?_op, get?_singleton_eq rfl, Option.some_op_opM] + exact hvy + · have hvk := hv k + rw [get?_op, get?_singleton_ne hk] + rwa [get?_op, get?_empty] at hvk + +@[rocq_alias alloc_unit_singleton_updateP'] +theorem alloc_unit_singleton_updateP' {P : V → Prop} {u : V} {i : K} + (hu : ✓ u) (hid : ∀ x : V, u • x = x) (hx : u ~~>: P) : + (∅ : M V) ~~>: fun m => ∃ y, m = singleton i y ∧ P y := + alloc_unit_singleton_updateP hu hid hx fun y hy => ⟨y, rfl, hy⟩ + +@[rocq_alias alloc_unit_singleton_update] +theorem alloc_unit_singleton_update {u : V} {i : K} {y : V} + (hu : ✓ u) (hid : ∀ x : V, u • x = x) (h : u ~~> y) : + (∅ : M V) ~~> (singleton i y : M V) := + .of_updateP <| alloc_unit_singleton_updateP hu hid (.of_update h) fun _ => congrArg _ + +/-! ## Local updates -/ + +@[rocq_alias gmap_local_update] +theorem local_update {m1 m2 m1' m2' : M V} + (h : ∀ i, (get? m1 i, get? m2 i) ~l~> (get? m1' i, get? m2' i)) : + ((m1, m2) : M V × M V) ~l~> (m1', m2') := by + refine local_update_unital.mpr fun n z hv he => ?_ + have he' i : get? m1 i ≡{n}≡ get? m2 i •? some (get? z i) := + (he i).trans (.of_eq (get?_op m2 z)) + exact ⟨fun i => (h i n _ (hv i) (he' i)).1, + fun i => (h i n _ (hv i) (he' i)).2.trans (.of_eq (get?_op m2' z).symm)⟩ + +open Classical in +@[rocq_alias alloc_local_update] +theorem alloc_local_update {m1 m2 : M V} {i : K} {x : V} + (hi : get? m1 i = none) (hx : ✓ x) : + ((m1, m2) : M V × M V) ~l~> (insert m1 i x, insert m2 i x) := by + refine local_update fun j => ?_ + by_cases hj : i = j + · subst hj + rw [get?_insert_eq rfl, get?_insert_eq rfl, hi] + exact LocalUpdate.alloc_option _ hx + · rw [get?_insert_ne hj, get?_insert_ne hj] + +@[rocq_alias alloc_singleton_local_update] +theorem alloc_singleton_local_update {m : M V} {i : K} {x : V} + (hi : get? m i = none) (hx : ✓ x) : + ((m, ∅) : M V × M V) ~l~> (insert m i x, singleton i x) := + alloc_local_update hi hx + +open Classical in +@[rocq_alias insert_local_update] +theorem insert_local_update {m1 m2 : M V} {i : K} {x y x' y' : V} + (hi1 : get? m1 i = some x) (hi2 : get? m2 i = some y) (h : (x, y) ~l~> (x', y')) : + ((m1, m2) : M V × M V) ~l~> (insert m1 i x', insert m2 i y') := by + refine local_update fun j => ?_ + by_cases hj : i = j + · subst hj + rw [get?_insert_eq rfl, get?_insert_eq rfl, hi1, hi2] + exact .option h + · rw [get?_insert_ne hj, get?_insert_ne hj] + +open Classical in +@[rocq_alias singleton_local_update_any] +theorem singleton_local_update_any {m : M V} {i : K} {y x' y' : V} + (h : ∀ x, get? m i = some x → (x, y) ~l~> (x', y')) : + ((m, singleton i y) : M V × M V) ~l~> (insert m i x', singleton i y') := by + refine local_update fun j => ?_ + by_cases hj : i = j + · subst hj + rw [get?_insert_eq rfl, get?_singleton_eq rfl, get?_singleton_eq rfl] + rcases hm : get? m i with _ | x + · refine LocalUpdate.total_valid0 fun _ _ hinc => ?_ + obtain ⟨_ | z, hz⟩ := hinc <;> simp_all [CMRA.op, optionOp] + · exact .option (h x hm) + · rw [get?_insert_ne hj, get?_singleton_ne hj, get?_singleton_ne hj] + +@[rocq_alias singleton_local_update] +theorem singleton_local_update {m : M V} {i : K} {x y x' y' : V} + (hi : get? m i = some x) (h : (x, y) ~l~> (x', y')) : + ((m, singleton i y) : M V × M V) ~l~> (insert m i x', singleton i y') := + singleton_local_update_any fun _ hx => Option.some.inj (hi.symm.trans hx) ▸ h + +open Classical in +@[rocq_alias delete_local_update] +theorem delete_local_update {m1 m2 : M V} {i : K} (x : V) [Exclusive x] + (hi : get? m2 i = some x) : + ((m1, m2) : M V × M V) ~l~> (delete m1 i, delete m2 i) := by + refine local_update fun j => ?_ + by_cases hj : i = j + · subst hj + rw [get?_delete_eq rfl, get?_delete_eq rfl, hi] + exact LocalUpdate.delete_option _ x + · rw [get?_delete_ne hj, get?_delete_ne hj] + +@[rocq_alias delete_singleton_local_update] +theorem delete_singleton_local_update {m : M V} {i : K} (x : V) [Exclusive x] : + ((m, singleton i x) : M V × M V) ~l~> (delete m i, ∅) := + delete_singleton_eq (M := M) ▸ + delete_local_update x (get?_singleton_eq rfl) + +open Classical in +@[rocq_alias delete_local_update_cancelable] +theorem delete_local_update_cancelable {m1 m2 : M V} {i : K} (mx : Option V) + [Cancelable mx] (hi1 : get? m1 i = mx) (hi2 : get? m2 i = mx) : + ((m1, m2) : M V × M V) ~l~> (delete m1 i, delete m2 i) := by + refine local_update fun j => ?_ + by_cases hj : i = j + · subst hj + rw [get?_delete_eq rfl, get?_delete_eq rfl, hi1, hi2] + exact LocalUpdate.delete_option_cancelable mx + · rw [get?_delete_ne hj, get?_delete_ne hj] + +@[rocq_alias delete_singleton_local_update_cancelable] +theorem delete_singleton_local_update_cancelable {m : M V} {i : K} {x : V} + [Cancelable (some x)] (hi : get? m i = some x) : + ((m, singleton i x) : M V × M V) ~l~> (delete m i, ∅) := + delete_singleton_eq (M := M) ▸ + delete_local_update_cancelable (some x) hi (get?_singleton_eq rfl) + +end Heap + +end Properties + +section UnitalProperties + +open CMRA PartialMap LawfulPartialMap + +variable [LawfulPartialMap M K] [UCMRA V] + +namespace Heap + +open Classical in +@[rocq_alias insert_alloc_local_update] +theorem insert_alloc_local_update {m1 m2 : M V} {i : K} {x x' y' : V} + (hi1 : get? m1 i = some x) (hi2 : get? m2 i = none) (h : (x, UCMRA.unit) ~l~> (x', y')) : + ((m1, m2) : M V × M V) ~l~> (insert m1 i x', insert m2 i y') := by + refine local_update fun j => ?_ + by_cases hj : i = j + · subst hj + rw [get?_insert_eq rfl, get?_insert_eq rfl, hi1, hi2] + exact .option_none h + · rw [get?_insert_ne hj, get?_insert_ne hj] + +end Heap + +end UnitalProperties + section HeapFunctor variable {K} (H : Type _ → Type _) [LawfulPartialMap H K] @@ -573,6 +1116,7 @@ namespace PartialMap def map (f : α → β) : H α → H β := PartialMap.bindAlter (fun _ a => some <| f a) +@[rocq_alias map_fmap_ne, rocq_alias gmap_fmap_ne] instance [OFE α] [OFE β] {f : α → β} [hne : OFE.NonExpansive f] : OFE.NonExpansive (map H f) where ne := by simp only [OFE.Dist, Option.Forall₂, map, get?_bindAlter, Option.bind] @@ -586,10 +1130,12 @@ theorem map_id [OFE α] (a : H α) : simp [PartialMap.map, get?_bindAlter, Option.bind] rcases get? a x <;> simp +@[rocq_alias gmapO_map] def mapO [OFE α] [OFE β] (f : α -n> β) : OFE.Hom (H α) (H β) where f := map H f ne := inferInstance +@[rocq_alias gmap_fmap_ne_ext, rocq_alias gmapO_map_ne] theorem map_ne [OFE α] [OFE β] (f g : α -> β) {heq : f ≡{n}≡ g} : map H f m ≡{n}≡ map H g m := by simp [OFE.Dist, Option.Forall₂, map, get?_bindAlter] intro k @@ -602,6 +1148,7 @@ theorem map_compose [OFE α] [OFE β] [OFE γ] (f : α -> β) (g : β -> γ) m : simp [map, get?_bindAlter] cases get? m k <;> simp +@[rocq_alias gmap_fmap_cmra_morphism] def mapC [CMRA α] [CMRA β] (f : α -C> β) : CMRA.Hom (H α) (H β) where f := PartialMap.map H f ne := inferInstance @@ -630,6 +1177,7 @@ def mapC [CMRA α] [CMRA β] (f : α -C> β) : CMRA.Hom (H α) (H β) where abbrev PartialMapOF (F : COFE.OFunctorPre) : COFE.OFunctorPre := fun A B _ _ => H (F A B) +@[rocq_alias gmapOF] instance {F} [COFE.OFunctor F] : COFE.OFunctor (PartialMapOF H F) where ofe := inferInstance map f g := mapO H (COFE.OFunctor.map f g) @@ -648,6 +1196,13 @@ instance {F} [COFE.OFunctor F] : COFE.OFunctor (PartialMapOF H F) where cases get? m x <;> simp exact (COFE.OFunctor.map_comp f g f' g' _).dist +@[rocq_alias gmapOF_contractive] +instance {F} [COFE.OFunctorContractive F] : COFE.OFunctorContractive (PartialMapOF H F) where + map_contractive.1 h m := by + apply map_ne _ _ + exact COFE.OFunctorContractive.map_contractive.1 h + +@[rocq_alias gmapURF] instance {F} [RFunctor F] : URFunctor (PartialMapOF H F) where map f g := mapC H (RFunctor.map f g) map_ne {_} _ _ _ _ _ _ _ := by @@ -665,6 +1220,7 @@ instance {F} [RFunctor F] : URFunctor (PartialMapOF H F) where cases get? m x <;> simp exact (RFunctor.map_comp f g f' g' _).dist +@[rocq_alias gmapURF_contractive] instance {F} [RFunctorContractive F] : URFunctorContractive (PartialMapOF H F) where map_contractive.1 H m := by apply map_ne _ _ diff --git a/Iris/Iris/Algebra/List.lean b/Iris/Iris/Algebra/List.lean index c162a93e9..52f8b652c 100644 --- a/Iris/Iris/Algebra/List.lean +++ b/Iris/Iris/Algebra/List.lean @@ -379,4 +379,20 @@ instance [OFunctorContractive F] : OFunctorContractive (ListOF F) where end functor +section MapSeq + +open Std OFE + +/-- Building a map out of a list of consecutive keys is non-expansive. -/ +@[rocq_alias map_seq_ne] +instance [LawfulFiniteMap M Nat] [OFE V] (start : Nat) : + NonExpansive (FiniteMap.map_seq (M := M) start : List V → M V) where + ne {_ _ _} h k := by + rw [LawfulFiniteMap.get?_map_seq, LawfulFiniteMap.get?_map_seq] + split + · exact NonExpansive.ne (f := fun l : List V => l[k - start]?) h + · exact .rfl + +end MapSeq + end Iris diff --git a/Iris/Iris/BI/BigOp/BigAndMap.lean b/Iris/Iris/BI/BigOp/BigAndMap.lean index 897393887..2d464cd79 100644 --- a/Iris/Iris/BI/BigOp/BigAndMap.lean +++ b/Iris/Iris/BI/BigOp/BigAndMap.lean @@ -239,7 +239,7 @@ theorem bigAndM_toList {Φ : K → V → PROP} {m : M V} : @[rocq_alias big_andM_fmap] theorem bigAndM_map {Φ : K → V → PROP} {m : M V} {f : V → V} : - ([∧map] k ↦ y ∈ PartialMap.map f m, Φ k y) = [∧map] k ↦ y ∈ m, Φ k (f y) := + ([∧map] k ↦ y ∈ Std.PartialMap.map f m, Φ k y) = [∧map] k ↦ y ∈ m, Φ k (f y) := bigOpM_map_eq f Φ m @[rocq_alias big_andM_omap] diff --git a/Iris/Iris/Std/PartialMap.lean b/Iris/Iris/Std/PartialMap.lean index a5d2fdb80..5d9c4a7fd 100644 --- a/Iris/Iris/Std/PartialMap.lean +++ b/Iris/Iris/Std/PartialMap.lean @@ -261,6 +261,10 @@ def mapFold {A : Type _} (f : K → V → A → A) (a : A) (m : M V) : A := def map_seq [FiniteMap M Nat] (start : Nat) (l : List V) : M V := PartialMap.ofList (l.mapIdx (fun i v => (start + i, v))) +/-- The map sending every element of the finite set `s` to `a`. -/ +def ofSet [FiniteSet S K] (a : V) (s : S) : M V := + PartialMap.ofList ((FiniteSet.toList s).map (·, a)) + def dom_set [LawfulSet S K] (m : M V) : S := LawfulSet.ofList (mapFold (fun k _ acc => k :: acc) [] m) @@ -956,6 +960,35 @@ theorem NoDupKeys_noDup {L : List (K × V)} : NoDupKeys L → L.Nodup := by theorem nodup_toList {m : M V} : (toList m).Nodup := NoDupKeys_noDup toList_noDupKeys +theorem noDupKeys_map_const [LawfulFiniteSet S K] {a : V} {s : S} : + NoDupKeys ((FiniteSet.toList s).map (·, a) : List (K × V)) := by + simpa [NoDupKeys, List.map_map, Function.comp_def] using FiniteSet.toList_nodup (m := s) + +theorem get?_ofSet_of_mem [DecidableEq K] [LawfulFiniteSet S K] {a : V} {s : S} {k : K} + (h : k ∈ s) : get? (FiniteMap.ofSet (M := M) a s) k = some a := + get?_ofList_some (List.mem_map_of_mem (FiniteSet.mem_toList.mpr h)) noDupKeys_map_const + +theorem get?_ofSet_of_not_mem [LawfulFiniteSet S K] {a : V} {s : S} {k : K} + (h : k ∉ s) : get? (FiniteMap.ofSet (M := M) a s) k = none := + get?_ofList_none (fun ⟨_, hv⟩ => by + obtain ⟨_, hmem, rfl, _⟩ := by simpa using hv + exact h (FiniteSet.mem_toList.mp hmem)) noDupKeys_map_const + +theorem ofSet_empty [LawfulFiniteSet S K] {a : V} : (FiniteMap.ofSet a (∅ : S) : M V) = ∅ := + equiv_iff_eq.mp fun k => by rw [get?_ofSet_of_not_mem mem_empty, get?_empty] + +theorem ofSet_insert [DecidableEq K] [LawfulFiniteSet S K] {a : V} {x : K} {s : S} : + (FiniteMap.ofSet a (Insert.insert x s) : M V) = insert (FiniteMap.ofSet a s) x a := by + refine equiv_iff_eq.mp fun k => ?_ + by_cases hk : x = k + · subst hk + rw [get?_insert_eq rfl, get?_ofSet_of_mem (LawfulSet.mem_insert.mpr (.inl rfl))] + · rw [get?_insert_ne hk] + by_cases hks : k ∈ s + · rw [get?_ofSet_of_mem (LawfulSet.mem_insert.mpr (.inr hks)), get?_ofSet_of_mem hks] + · rw [get?_ofSet_of_not_mem fun hc => (LawfulSet.mem_insert.mp hc).elim + (fun h => hk h.symm) hks, get?_ofSet_of_not_mem hks] + theorem ofList_toList [DecidableEq K] {m : M V} : ofList (toList m) = m := by apply equiv_iff_eq.mp From 227623cb1644c7b725d63ace2b125aaa766cc9b1 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Wed, 12 Aug 2026 11:34:29 -0400 Subject: [PATCH 2/6] remove what seems to be a bogus annotation --- Iris/Iris/Algebra/Heap.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Iris/Iris/Algebra/Heap.lean b/Iris/Iris/Algebra/Heap.lean index 442b170fb..7fafc149e 100644 --- a/Iris/Iris/Algebra/Heap.lean +++ b/Iris/Iris/Algebra/Heap.lean @@ -119,7 +119,6 @@ theorem isSome_get?_eq_of_dist [LawfulPartialMap M K] [OFE V] {n : Nat} {m₁ m instance [LawfulPartialMap M K] [OFE V] : NonExpansive₂ ((· ∪ ·) : M V → M V → M V) where ne _ {_ _} H₁ {_ _} H₂ := merge_dist (fun H _ => H) H₁ H₂ -@[rocq_alias gmap_difference_ne] instance [LawfulPartialMap M K] [OFE V] : NonExpansive₂ ((· \ ·) : M V → M V → M V) where ne _ {m₁ m₁'} H₁ {_ m₂'} H₂ k := by specialize H₁ k From 2b52f4c400699398957befdb891ffde9f7dcb6f5 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Wed, 12 Aug 2026 12:48:39 -0400 Subject: [PATCH 3/6] loose ends --- Iris/Iris/Algebra/BigOp.lean | 2 +- Iris/Iris/Algebra/Heap.lean | 73 ++++++++++++++++++++++++++++------- Iris/Iris/Std/PartialMap.lean | 37 ++++++++++++++++-- 3 files changed, 93 insertions(+), 19 deletions(-) diff --git a/Iris/Iris/Algebra/BigOp.lean b/Iris/Iris/Algebra/BigOp.lean index e4bc4e23a..959fd7967 100644 --- a/Iris/Iris/Algebra/BigOp.lean +++ b/Iris/Iris/Algebra/BigOp.lean @@ -660,7 +660,7 @@ theorem bigOpS_singleton {Φ : A → M} {a : A} : ([^ op set] x ∈ ({a} : S), simp only [bigOpS, toList_singleton]; exact bigOpL_singleton_eq _ _ open Classical in -@[rocq_alias big_opS_gset_to_gmap] +@[rocq_alias big_opS_gset_to_gmap, rocq_alias big_opS_gset_to_gmap_L] theorem bigOpS_ofSet {M' : Type _ → Type _} {V : Type _} [LawfulFiniteMap M' A] [CMRA V] (a : V) (s : S) : ([^ CMRA.op set] k ∈ s, (PartialMap.singleton k a : M' V)) = FiniteMap.ofSet a s := by diff --git a/Iris/Iris/Algebra/Heap.lean b/Iris/Iris/Algebra/Heap.lean index 7fafc149e..f9174371f 100644 --- a/Iris/Iris/Algebra/Heap.lean +++ b/Iris/Iris/Algebra/Heap.lean @@ -42,10 +42,21 @@ instance instOFE [LawfulPartialMap M K] [OFE V] : OFE (M V) where f x := of_fun x ne.1 {_ _ _} H k := by simp only [get_of_fun, H k] +#rocq_ignore gmapO_leibniz "OFE is Leibniz; use equality" + @[rocq_alias lookup_ne] instance get?_ne [LawfulPartialMap M K] [OFE V] (k : K) : NonExpansive (get? · k : M V → Option V) where ne {_ _ _} Ht := Ht k +/-- Total lookup is non-expansive in the map. -/ +@[rocq_alias lookup_total_ne] +instance getD_ne [LawfulPartialMap M K] [OFE V] (k : K) (d : V) : + NonExpansive (PartialMap.getD · k d : M V → V) where + ne {_ m₁ m₂} Ht := by + have h := Ht k + rcases h₁ : get? m₁ k with _ | v <;> rcases h₂ : get? m₂ k with _ | w <;> + simp_all [PartialMap.getD, OFE.Dist, Option.Forall₂] + @[rocq_alias insert_ne] instance [LawfulPartialMap M K] [OFE V] (k : K) : NonExpansive₂ (insert · k · : M V → V → M V) where ne {_ _ _} Hv {_ _} Ht k' := by @@ -100,32 +111,53 @@ theorem zipWith_dist [LawfulPartialMap M K] [OFE V] [OFE V'] [OFE V''] {n : Nat} {f g : V → V' → V''} {m₁ m₁' : M V} {m₂ m₂' : M V'} (Hf : ∀ {v v' w w'}, v ≡{n}≡ v' → w ≡{n}≡ w' → f v w ≡{n}≡ g v' w') (H₁ : m₁ ≡{n}≡ m₁') (H₂ : m₂ ≡{n}≡ m₂') : - PartialMap.zipWith f m₁ m₂ ≡{n}≡ PartialMap.zipWith g m₁' m₂' := by - intro k - specialize H₁ k - specialize H₂ k - revert H₁ H₂ - simp only [OFE.Dist, Option.Forall₂, LawfulPartialMap.get?_zipWith] - cases get? m₁ k <;> cases get? m₁' k <;> cases get? m₂ k <;> cases get? m₂' k <;> simp_all + PartialMap.zipWith f m₁ m₂ ≡{n}≡ PartialMap.zipWith g m₁' m₂' := + bindAlter_dist (fun {k _ _} Hv => by + have h := H₂ k + revert h + cases get? m₂ k <;> cases get? m₂' k <;> simp_all [OFE.Dist, Option.Forall₂]) H₁ theorem isSome_get?_eq_of_dist [LawfulPartialMap M K] [OFE V] {n : Nat} {m₁ m₂ : M V} (H : m₁ ≡{n}≡ m₂) (k : K) : (get? m₁ k).isSome = (get? m₂ k).isSome := by specialize H k revert H - simp only [OFE.Dist, Option.Forall₂] - cases get? m₁ k <;> cases get? m₂ k <;> simp_all + cases get? m₁ k <;> cases get? m₂ k <;> simp_all [OFE.Dist, Option.Forall₂] @[rocq_alias gmap_union_ne] instance [LawfulPartialMap M K] [OFE V] : NonExpansive₂ ((· ∪ ·) : M V → M V → M V) where ne _ {_ _} H₁ {_ _} H₂ := merge_dist (fun H _ => H) H₁ H₂ +/-- `intersectionWith` is non-expansive in the combining function and in both maps. -/ +@[rocq_alias intersection_with_ne] +theorem intersectionWith_dist [LawfulPartialMap M K] [OFE V] {n : Nat} + {f g : K → V → V → Option V} {m₁ m₁' m₂ m₂' : M V} + (Hf : ∀ {k v v' w w'}, v ≡{n}≡ v' → w ≡{n}≡ w' → f k v w ≡{n}≡ g k v' w') + (H₁ : m₁ ≡{n}≡ m₁') (H₂ : m₂ ≡{n}≡ m₂') : + PartialMap.intersectionWith f m₁ m₂ ≡{n}≡ PartialMap.intersectionWith g m₁' m₂' := + bindAlter_dist (fun {k _ _} Hv => by + have h := H₂ k + revert h + cases get? m₂ k <;> cases get? m₂' k <;> simp_all [OFE.Dist, Option.Forall₂]) H₁ + +/-- `differenceWith` is non-expansive in the combining function and in both maps. -/ +@[rocq_alias difference_with_ne] +theorem differenceWith_dist [LawfulPartialMap M K] [OFE V] {n : Nat} + {f g : K → V → V → Option V} {m₁ m₁' m₂ m₂' : M V} + (Hf : ∀ {k v v' w w'}, v ≡{n}≡ v' → w ≡{n}≡ w' → f k v w ≡{n}≡ g k v' w') + (H₁ : m₁ ≡{n}≡ m₁') (H₂ : m₂ ≡{n}≡ m₂') : + PartialMap.differenceWith f m₁ m₂ ≡{n}≡ PartialMap.differenceWith g m₁' m₂' := + bindAlter_dist (fun {k _ _} Hv => by + have h := H₂ k + revert h + cases get? m₂ k <;> cases get? m₂' k <;> simp_all [OFE.Dist, Option.Forall₂]) H₁ + +@[rocq_alias gmap_intersection_ne] +instance [LawfulPartialMap M K] [OFE V] : NonExpansive₂ ((· ∩ ·) : M V → M V → M V) where + ne _ {_ _} H₁ {_ _} H₂ := intersectionWith_dist (fun H _ => H) H₁ H₂ + +@[rocq_alias gmap_difference_ne] instance [LawfulPartialMap M K] [OFE V] : NonExpansive₂ ((· \ ·) : M V → M V → M V) where - ne _ {m₁ m₁'} H₁ {_ m₂'} H₂ k := by - specialize H₁ k - revert H₁ - simp only [OFE.Dist, Option.Forall₂, LawfulPartialMap.get?_difference, - isSome_get?_eq_of_dist H₂ k] - cases get? m₁ k <;> cases get? m₁' k <;> cases get? m₂' k <;> simp_all + ne _ {_ _} H₁ {_ _} H₂ := differenceWith_dist (fun _ _ => .of_eq rfl) H₁ H₂ @[rocq_alias gmap_disjoint_ne] theorem disjoint_dist_iff [LawfulPartialMap M K] [OFE V] {n : Nat} {m₁ m₁' m₂ m₂' : M V} @@ -418,6 +450,12 @@ instance instStoreUCMRA : UCMRA (M V) where refine OFE.some_dist_some.mpr fun k => ?_ simp [get?_bindAlter, get?_empty] +@[rocq_alias gmap_op_empty_l_L] +theorem op_empty_left {m : M V} : (∅ : M V) • m = m := CMRA.unit_left_id_L + +@[rocq_alias gmap_op_empty_r] +theorem op_empty_right {m : M V} : m • (∅ : M V) = m := CMRA.unit_right_id_L + instance instIsTotalHeap : IsTotal (M V) where total _ := Option.isSome_iff_exists.mp rfl @@ -1225,4 +1263,9 @@ instance {F} [RFunctorContractive F] : URFunctorContractive (PartialMapOF H F) w apply map_ne _ _ exact (RFunctorContractive.map_contractive.1 H) +-- The unital functor instances above already give the non-unital ones, through +-- `URFunctor.toRFunctor` and `URFunctorContractive.toRFunctorContractive`. +#rocq_ignore gmapRF "Found by typeclass inference" +#rocq_ignore gmapRF_contractive "Found by typeclass inference" + end PartialMap diff --git a/Iris/Iris/Std/PartialMap.lean b/Iris/Iris/Std/PartialMap.lean index 5d9c4a7fd..c7ff0003a 100644 --- a/Iris/Iris/Std/PartialMap.lean +++ b/Iris/Iris/Std/PartialMap.lean @@ -116,6 +116,9 @@ def mem (m : M V) (k : K) : Prop := (get? m k).isSome /-- Keys can be tested for membership in partial maps using `∈`. -/ instance : Membership K (M V) := ⟨fun m k => (get? m k).isSome⟩ +/-- Total lookup: the value stored at `k`, or `d` when `k` is absent. -/ +def getD (m : M V) (k : K) (d : V) : V := (get? m k).getD d + /-- Universal quantification over map entries. -/ def all (P : K → V → Prop) (m : M V) : Prop := ∀ k v, get? m k = some v → P k v @@ -141,9 +144,21 @@ def filterMap (f : V → Option V) : M V → M V := def filter (φ : K → V → Bool) : M V → M V := bindAlter (fun k v => if φ k v then some v else none) +/-- Intersection with a combining function: a key present in both maps is combined with `f`, +every other key is dropped. -/ +def intersectionWith (f : K → V → V → Option V) (m₁ m₂ : M V) : M V := + bindAlter (fun k v => (get? m₂ k).bind (f k v)) m₁ + +/-- Intersection: keep the entries of `m₁` whose keys also occur in `m₂`. -/ +def intersection (m₁ m₂ : M V) : M V := intersectionWith (fun _ v _ => some v) m₁ m₂ + +/-- Difference with a combining function: a key present in both maps is combined with `f`, +a key present only in `m₁` is kept. -/ +def differenceWith (f : K → V → V → Option V) (m₁ m₂ : M V) : M V := + bindAlter (fun k v => (get? m₂ k).elim (some v) (f k v)) m₁ + /-- Difference: remove all keys in `m₂` from `m₁`. -/ -def difference (m₁ m₂ : M V) : M V := - bindAlter (fun k v => if (get? m₂ k).isSome then none else some v) m₁ +def difference (m₁ m₂ : M V) : M V := differenceWith (fun _ _ _ => none) m₁ m₂ def zipWith (f : V → V' → V'') (m₁ : M V) (m₂ : M V') : M V'' := bindAlter (fun k v => (get? m₂ k).bind fun v' => some <| f v v') m₁ @@ -152,6 +167,9 @@ set_option linter.checkUnivs false in def zip (m₁ : M V) (m₂ : M V') : M (V × V') := zipWith (fun x y => (x, y)) m₁ m₂ +/-- Partial maps support the intersection operation `∩` via intersection. -/ +instance : Inter (M V) := ⟨intersection⟩ + /-- Partial maps support the set difference operation `\` via difference. -/ instance : SDiff (M V) := ⟨difference⟩ @@ -636,9 +654,22 @@ theorem get?_delete_isSome [DecidableEq K] {m : M V} {i j : K} : rw [get?_delete] split <;> simp_all +theorem get?_intersectionWith {f : K → V → V → Option V} {m₁ m₂ : M V} {k : K} : + get? (intersectionWith f m₁ m₂) k = (get? m₁ k).bind fun v => (get? m₂ k).bind (f k v) := by + simp only [PartialMap.intersectionWith, get?_bindAlter] + +theorem get?_differenceWith {f : K → V → V → Option V} {m₁ m₂ : M V} {k : K} : + get? (differenceWith f m₁ m₂) k = (get? m₁ k).bind fun v => (get? m₂ k).elim (some v) (f k v) := by + simp only [PartialMap.differenceWith, get?_bindAlter] + +theorem get?_intersection {m₁ m₂ : M V} {k : K} : + get? (m₁ ∩ m₂) k = if (get? m₂ k).isSome then get? m₁ k else none := by + simp only [Inter.inter, PartialMap.intersection, get?_intersectionWith] + cases hm2 : get? m₂ k <;> cases hm1 : get? m₁ k <;> simp + theorem get?_difference {m₁ m₂ : M V} {k : K} : get? (m₁ \ m₂) k = if (get? m₂ k).isSome then none else get? m₁ k := by - simp only [SDiff.sdiff, PartialMap.difference, get?_bindAlter] + simp only [SDiff.sdiff, PartialMap.difference, get?_differenceWith] cases hm2 : get? m₂ k <;> cases hm1 : get? m₁ k <;> simp theorem disjoint_difference_right {m₁ m₂ : M V} : From b900148497de68143c1e2f321929a366cdcd044e Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Thu, 13 Aug 2026 18:37:14 +0200 Subject: [PATCH 4/6] Pass --- Iris/Iris/Algebra.lean | 1 + Iris/Iris/Algebra/BigOp.lean | 118 ++++++------------------------ Iris/Iris/Algebra/CMRABigOp.lean | 49 +++++++++++++ Iris/Iris/Algebra/Heap.lean | 114 ++++++++++++++++++++--------- Iris/Iris/Algebra/HeapView.lean | 2 +- Iris/Iris/Algebra/List.lean | 16 ---- Iris/Iris/BI/BigOp/BigAndMap.lean | 2 +- Iris/Iris/Std/HeapInstances.lean | 2 +- Iris/Iris/Std/PartialMap.lean | 16 ---- 9 files changed, 157 insertions(+), 163 deletions(-) create mode 100644 Iris/Iris/Algebra/CMRABigOp.lean diff --git a/Iris/Iris/Algebra.lean b/Iris/Iris/Algebra.lean index 9bbe19fd7..4940226d1 100644 --- a/Iris/Iris/Algebra.lean +++ b/Iris/Iris/Algebra.lean @@ -5,6 +5,7 @@ public import Iris.Algebra.Auth public import Iris.Algebra.BigOp public import Iris.Algebra.Chain public import Iris.Algebra.CMRA +public import Iris.Algebra.CMRABigOp public import Iris.Algebra.COFESolver public import Iris.Algebra.Csum public import Iris.Algebra.DFrac diff --git a/Iris/Iris/Algebra/BigOp.lean b/Iris/Iris/Algebra/BigOp.lean index e10b9726b..d4f8bc619 100644 --- a/Iris/Iris/Algebra/BigOp.lean +++ b/Iris/Iris/Algebra/BigOp.lean @@ -7,7 +7,6 @@ module public import Iris.Algebra.Monoid public import Iris.Algebra.CMRA -public import Iris.Algebra.Heap import Batteries.Data.List.Perm public import Iris.Std.List public import Iris.Std.PartialMap @@ -262,25 +261,6 @@ theorem bigOpL_zip_op_eq {B : Type v} {l₁ : List A} {l₂ : List B} {Φ : Nat op ([^ op list] k ↦ x ∈ l₁, Φ k x) ([^ op list] k ↦ x ∈ l₂, Ψ k x) := bigOpL_zipWith_op_eq rfl rfl hlen -section CMRA -variable {M : Type _} [CMRA M] - -@[rocq_alias big_opL_None] -theorem bigOpL_none {f : Nat → A → Option M} {l : List A} : - ([^ CMRA.op list] k ↦ x ∈ l, f k x) = none ↔ ∀ k x, l[k]? = some x → f k x = none := by - induction l generalizing f with - | nil => exact iff_of_true rfl (by simp) - | cons a l ih => - rw [bigOpL_cons, Iris.Option.op_none_iff, ih] - refine ⟨fun ⟨h0, hl⟩ k x hx => ?_, fun h => ⟨h 0 a rfl, fun k x hx => h (k + 1) x hx⟩⟩ - match k with - | 0 => - simp only [List.getElem?_cons_zero, Option.some.injEq] at hx - exact hx ▸ h0 - | k + 1 => exact hl k x hx - -end CMRA - #rocq_ignore big_opL_ne' "Use bigOpL_dist" #rocq_ignore big_opL_proper' "Use bigOpL_eq" #rocq_ignore big_opL_permutation' "Use bigOpL_eq_of_perm" @@ -563,20 +543,6 @@ theorem bigOpM_sep_zip_eq {A : Type _} {B : Type _} op ([^ op map] k ↦ x ∈ m1, h1 k x) ([^ op map] k ↦ x ∈ m2, h2 k x) := bigOpM_sep_zipWith_eq _ _ rfl rfl hdom -section CMRA -variable {M : Type _} [CMRA M] - -@[rocq_alias big_opM_None] -theorem bigOpM_none {f : K → V → Option M} {m : M' V} : - ([^ CMRA.op map] k ↦ x ∈ m, f k x) = none ↔ ∀ k x, get? m k = some x → f k x = none := by - simp only [bigOpM, bigOpL_none] - refine ⟨fun h k x hk => ?_, - fun h i kx hi => h kx.1 kx.2 (toList_get.mp (List.mem_of_getElem? hi))⟩ - obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp (toList_get.mpr hk) - exact h i (k, x) hi - -end CMRA - variable {M₁} [OFE M₁] variable {M₂} [OFE M₂] variable {op₁ : M₁ → M₁ → M₁} {op₂ : M₂ → M₂ → M₂} {unit₁ : M₁} {unit₂ : M₂} @@ -597,26 +563,15 @@ theorem bigOpM_weak_hom [DecidableEq K] [ι : WeakMonoidHomomorphism op₁ op₂ show (LawfulFiniteMap.toList m) = [] from List.nil_eq.mpr Hk |>.symm] rfl -@[rocq_alias big_opM_ne_2] -theorem bigOpM_dist_2 [OFE V] {Φ Ψ : K → V → M} {m₁ m₂ : M' V} {n : Nat} (hm : m₁ ≡{n}≡ m₂) - (hf : ∀ {k y₁ y₂}, get? m₁ k = some y₁ → get? m₂ k = some y₂ → y₁ ≡{n}≡ y₂ → - Φ k y₁ ≡{n}≡ Ψ k y₂) : - ([^ op map] k ↦ y ∈ m₁, Φ k y) ≡{n}≡ ([^ op map] k ↦ y ∈ m₂, Ψ k y) := - bigOpM_gen_proper_2 OFE.Dist.of_eq OFE.dist_equivalence op_dist - (PartialMap.isSome_get?_eq_of_dist hm) fun {k _ _} h₁ h₂ => hf h₁ h₂ <| by - have hmk := hm k - rw [h₁, h₂] at hmk - exact OFE.some_dist_some.mp hmk - -open Classical in -@[rocq_alias big_opM_singletons] -theorem bigOpM_singletons [CMRA V] (m : M' V) : - ([^ CMRA.op map] k ↦ x ∈ m, PartialMap.singleton k x) = m := by - induction m using LawfulFiniteMap.induction_on with - | hemp => exact bigOpM_empty _ - | hins i x m hi ih => - rw [bigOpM_insert_eq _ x hi, ih] - exact (equiv_iff_eq.mp (Heap.insert_equiv_singleton_op_singleton hi)).symm +-- open Classical in +-- @[rocq_alias big_opM_singletons] +-- theorem bigOpM_singletons [CMRA V] (m : M' V) : +-- ([^ CMRA.op map] k ↦ x ∈ m, PartialMap.singleton k x) = m := by +-- induction m using LawfulFiniteMap.induction_on with +-- | hemp => exact bigOpM_empty _ +-- | hins i x m hi ih => +-- rw [bigOpM_insert_eq _ x hi, ih] +-- exact (equiv_iff_eq.mp (Heap.insert_equiv_singleton_op_singleton hi)).symm #rocq_ignore big_opM_ne' "Use bigOpM_dist" #rocq_ignore big_opM_proper' "Use bigOpM_eq" @@ -658,20 +613,20 @@ theorem bigOpS_const_unit (s : S) : ([^ op set] _x ∈ s, unit) = unit := by theorem bigOpS_singleton {Φ : A → M} {a : A} : ([^ op set] x ∈ ({a} : S), Φ x) = Φ a := by simp only [bigOpS, toList_singleton]; exact bigOpL_singleton_eq _ _ -open Classical in -@[rocq_alias big_opS_gset_to_gmap, rocq_alias big_opS_gset_to_gmap_L] -theorem bigOpS_ofSet {M' : Type _ → Type _} {V : Type _} [LawfulFiniteMap M' A] [CMRA V] - (a : V) (s : S) : - ([^ CMRA.op set] k ∈ s, (PartialMap.singleton k a : M' V)) = FiniteMap.ofSet a s := by - induction s using set_ind with - | hemp => - rw [bigOpS_empty, LawfulFiniteMap.ofSet_empty] - rfl - | hadd x X hx ih => - refine (bigOpS_insert hx).trans ?_ - rw [ih, LawfulFiniteMap.ofSet_insert] - exact (LawfulPartialMap.equiv_iff_eq.mp - (Heap.insert_equiv_singleton_op_singleton (LawfulFiniteMap.get?_ofSet_of_not_mem hx))).symm +-- open Classical in +-- @[rocq_alias big_opS_gset_to_gmap, rocq_alias big_opS_gset_to_gmap_L] +-- theorem bigOpS_ofSet {M' : Type _ → Type _} {V : Type _} [LawfulFiniteMap M' A] [CMRA V] +-- (a : V) (s : S) : +-- ([^ CMRA.op set] k ∈ s, (PartialMap.singleton k a : M' V)) = FiniteMap.ofSet a s := by +-- induction s using set_ind with +-- | hemp => +-- rw [bigOpS_empty, LawfulFiniteMap.ofSet_empty] +-- rfl +-- | hadd x X hx ih => +-- refine (bigOpS_insert hx).trans ?_ +-- rw [ih, LawfulFiniteMap.ofSet_insert] +-- exact (LawfulPartialMap.equiv_iff_eq.mp +-- (Heap.insert_equiv_singleton_op_singleton (LawfulFiniteMap.get?_ofSet_of_not_mem hx))).symm @[rocq_alias big_opS_union] theorem bigOpS_union {Φ : A → M} {s₁ s₂ : S} (Hdisj : s₁ ## s₂) : @@ -738,19 +693,6 @@ theorem bigOpS_gen_proper (R : M → M → Prop) {Φ Ψ : A → M} {s : S} #rocq_ignore big_opS_ne' "Use bigOpS_dist" #rocq_ignore big_opS_proper' "Use bigOpS_eq" -section CMRA -variable {M : Type _} [CMRA M] - -@[rocq_alias big_opS_None] -theorem bigOpS_none {f : A → Option M} {s : S} : - ([^ CMRA.op set] x ∈ s, f x) = none ↔ ∀ x, x ∈ s → f x = none := by - simp only [bigOpS, bigOpL_none] - refine ⟨fun h x hx => ?_, fun h k x hi => h x (FiniteSet.mem_toList.mp (List.mem_of_getElem? hi))⟩ - obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp (FiniteSet.mem_toList.mpr hx) - exact h i x hi - -end CMRA - section Homomorphism variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] @@ -876,20 +818,6 @@ theorem bigOpMS_gen_proper (R : M → M → Prop) {Φ Ψ : A → M} {X : MS} #rocq_ignore big_opMS_ext "Merged into bigOpMS_eq" -section CMRA -variable {M : Type _} [CMRA M] - -@[rocq_alias big_opMS_None] -theorem bigOpMS_none {f : A → Option M} {X : MS} : - ([^ CMRA.op mset] x ∈ X, f x) = none ↔ ∀ x, x ∈ X → f x = none := by - simp only [bigOpMS, bigOpL_none] - refine ⟨fun h x hx => ?_, - fun h k x hi => h x (LawfulFiniteMultiSet.mem_toList.mp (List.mem_of_getElem? hi))⟩ - obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp (LawfulFiniteMultiSet.mem_toList.mpr hx) - exact h i x hi - -end CMRA - section Homomorphism variable {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] diff --git a/Iris/Iris/Algebra/CMRABigOp.lean b/Iris/Iris/Algebra/CMRABigOp.lean new file mode 100644 index 000000000..ee9797384 --- /dev/null +++ b/Iris/Iris/Algebra/CMRABigOp.lean @@ -0,0 +1,49 @@ +/- +Copyright (c) 2026 Zongyuan Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zongyuan Liu +-/ +module + +public import Iris.Algebra.BigOp +public import Iris.Algebra.CMRA + +@[expose] public section + +namespace Iris.Algebra + +open OFE Iris.Std + +variable [CMRA M] + +@[rocq_alias big_opL_None] +theorem bigOpL_none {f : Nat → A → Option M} {l : List A} : + ([^ CMRA.op list] k ↦ x ∈ l, f k x) = none ↔ ∀ k x, l[k]? = some x → f k x = none := by + induction l generalizing f with + | nil => exact iff_of_true rfl (by simp) + | cons a l ih => + rw [BigOpL.bigOpL_cons, Iris.Option.op_none_iff, ih] + refine ⟨fun ⟨h0, hl⟩ k x hx => ?_, fun h => ⟨h 0 a rfl, fun k x hx => h (k + 1) x hx⟩⟩ + match k with + | 0 => + simp only [List.getElem?_cons_zero, Option.some.injEq] at hx + exact hx ▸ h0 + | k + 1 => exact hl k x hx + + +@[rocq_alias big_opS_None] +theorem bigOpS_none [LawfulFiniteSet S A] {f : A → Option M} {s : S} : + ([^ CMRA.op set] x ∈ s, f x) = none ↔ ∀ x, x ∈ s → f x = none := by + simp only [bigOpS, bigOpL_none] + refine ⟨fun h x hx => ?_, fun h k x hi => h x (FiniteSet.mem_toList.mp (List.mem_of_getElem? hi))⟩ + obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp (FiniteSet.mem_toList.mpr hx) + exact h i x hi + +@[rocq_alias big_opMS_None] +theorem bigOpMS_none [LawfulFiniteMultiSet MS A] {f : A → Option M} {X : MS} : + ([^ CMRA.op mset] x ∈ X, f x) = none ↔ ∀ x, x ∈ X → f x = none := by + simp only [bigOpMS, bigOpL_none] + refine ⟨fun h x hx => ?_, + fun h k x hi => h x (LawfulFiniteMultiSet.mem_toList.mp (List.mem_of_getElem? hi))⟩ + obtain ⟨i, hi⟩ := List.mem_iff_getElem?.mp (LawfulFiniteMultiSet.mem_toList.mpr hx) + exact h i x hi diff --git a/Iris/Iris/Algebra/Heap.lean b/Iris/Iris/Algebra/Heap.lean index f9174371f..5d0d8985e 100644 --- a/Iris/Iris/Algebra/Heap.lean +++ b/Iris/Iris/Algebra/Heap.lean @@ -10,6 +10,8 @@ public import Iris.Algebra.OFE public import Iris.Algebra.IsOp public import Iris.Algebra.LocalUpdates public import Iris.Algebra.Updates +public import Iris.Algebra.List +public import Iris.Algebra.BigOp public import Iris.Std.Infinite public import Iris.Std.Set public import Iris.Std.PartialMap @@ -25,7 +27,7 @@ open OFE namespace PartialMap -@[rocq_alias gmap_dist, rocq_alias gmap_ofe_mixin, rocq_alias gmapO] +@[rocq_alias gmap_ofe_mixin, rocq_alias gmapO] instance instOFE [LawfulPartialMap M K] [OFE V] : OFE (M V) where Dist n s0 s1 := get? s0 ≡{n}≡ get? s1 dist_eqv := ⟨fun _ => .of_eq rfl, (·.symm), (·.trans ·)⟩ @@ -34,6 +36,8 @@ instance instOFE [LawfulPartialMap M K] [OFE V] : OFE (M V) where exact ⟨fun h n k => Dist.of_eq (h k), fun h k => eq_dist.mpr fun n => h n k⟩ dist_lt := dist_lt +#rocq_ignore gmap_dist "Included in the OFE instance" + @[simp] def toMap [LawfulPartialMap M K] [OFE V] : (M V) -n> (K → Option V) where f x := get? x ne.1 {_ _ _} H k := H k @@ -181,11 +185,34 @@ theorem union_dist_iff [LawfulPartialMap M K] [OFE V] {n : Nat} {m m₁ m₂ : M LawfulPartialMap.get?_filter, LawfulPartialMap.get?_zipWith] cases get? m k <;> cases get? m₁ k <;> cases get? m₂ k <;> simp_all +open Iris.Algebra in +@[rocq_alias big_opM_ne_2] +theorem bigOpM_dist_2 [LawfulFiniteMap M' K] [OFE M] [MonoidOps op unit] [OFE V] + {Φ Ψ : K → V → M} {m₁ m₂ : M' V} {n : Nat} (hm : m₁ ≡{n}≡ m₂) + (hf : ∀ {k y₁ y₂}, get? m₁ k = some y₁ → get? m₂ k = some y₂ → y₁ ≡{n}≡ y₂ → + Φ k y₁ ≡{n}≡ Ψ k y₂) : + ([^ op map] k ↦ y ∈ m₁, Φ k y) ≡{n}≡ ([^ op map] k ↦ y ∈ m₂, Ψ k y) := + BigOpM.bigOpM_gen_proper_2 OFE.Dist.of_eq OFE.dist_equivalence MonoidOps.op_dist + (PartialMap.isSome_get?_eq_of_dist hm) fun {k _ _} h₁ h₂ => hf h₁ h₂ <| by + have hmk := hm k + rw [h₁, h₂] at hmk + exact OFE.some_dist_some.mp hmk + @[rocq_alias gmap_dom_ne] theorem dom_eq_of_dist [LawfulPartialMap M K] [OFE V] {n : Nat} {m₁ m₂ : M V} (H : m₁ ≡{n}≡ m₂) : PartialMap.dom m₁ = PartialMap.dom m₂ := funext fun k => congrArg (· = true) (isSome_get?_eq_of_dist H k) +/-- Building a map out of a list of consecutive keys is non-expansive. -/ +@[rocq_alias map_seq_ne] +instance [LawfulFiniteMap M Nat] [OFE V] (start : Nat) : + NonExpansive (FiniteMap.map_seq (M := M) start : List V → M V) where + ne {_ _ _} h k := by + rw [LawfulFiniteMap.get?_map_seq, LawfulFiniteMap.get?_map_seq] + split + · exact NonExpansive.ne (f := fun l : List V => l[k - start]?) h + · exact .rfl + /-- Project a chain of stores through its kth coordinate to a chain of values. -/ @[rocq_alias gmap_chain] def chain [LawfulPartialMap M K] [OFE V] (k : K) (c : Chain (M V)) : Chain (Option V) where @@ -206,6 +233,8 @@ instance Heap.instCOFE [LawfulPartialMap M K] [COFE V] : COFE (M V) where · simp [← PartialMap.chain_get, chain_none_const (c := PartialMap.chain k c) (n := 0) (H▸rfl)] · exact IsCOFE.conv_compl +#rocq_ignore gmap_compl "Included in COFE instance" + @[rocq_alias gmap_ofe_discrete] instance instDiscreteHeap [LawfulPartialMap M K] [OFE V] [Discrete V] : Discrete (M V) where discrete_0 h := OFE.eq_dist.mpr <| by @@ -567,9 +596,9 @@ theorem insert_equiv_singleton_op_singleton {m : M V} (Hemp : get? m i = none) : · rw [← He, Hemp] · cases (get? m k) <;> rfl -theorem insert_eq_singleton_op_singleton [IsoFunMap M K] {m : M V} (Hemp : get? m i = none) : +theorem insert_eq_singleton_op_singleton {m : M V} (Hemp : get? m i = none) : insert m i x = singleton i x • m := - IsoFunMap.ext (insert_equiv_singleton_op_singleton Hemp) + equiv_iff_eq.mp (insert_equiv_singleton_op_singleton Hemp) theorem core_empty : core (∅ : M V) = ∅ := OFE.eq_dist.mpr <| by intro n k @@ -583,38 +612,31 @@ theorem core_singleton_equiv {i : K} {x : V} {cx : V} (Hpcore : CMRA.pcore x = s simp [← Hpcore, core, CMRA.pcore, get?_singleton, get?_bindAlter] split <;> rfl -theorem singleton_core_eq [IsoFunMap M K] {i : K} {x : V} {cx} (Hpcore : CMRA.pcore x = some cx) : - core (singleton i x : M V) = singleton i cx := - IsoFunMap.ext (core_singleton_equiv Hpcore) - -open Classical in @[rocq_alias singleton_core] -theorem singleton_core_eqv {i : K} {x : V} {cx} (Hpcore : CMRA.pcore x = some cx) : - core (singleton i x : M V) = singleton i cx := OFE.eq_dist.mpr <| by - intro n k - simp [core, CMRA.pcore, get?_singleton, get?_bindAlter] - split <;> first | exact Hpcore.dist | trivial +theorem singleton_core_eq {i : K} {x : V} {cx} (Hpcore : CMRA.pcore x = some cx) : + core (singleton i x : M V) = singleton i cx := + equiv_iff_eq.mp (core_singleton_equiv Hpcore) -@[rocq_alias singleton_core_total] theorem singleton_core_total [IsTotal V] {i : K} {x : V} : equiv (core <| singleton i x : M V) ((singleton i (core x))) := core_singleton_equiv (pcore_eq_core x) -theorem singleton_core_total_eq [IsTotal V] [IsoFunMap M K] {i : K} {x : V} : +@[rocq_alias singleton_core_total] +theorem singleton_core_total_eq [IsTotal V] {i : K} {x : V} : core (singleton i x : M V) = singleton i (core x) := - IsoFunMap.ext singleton_core_total + equiv_iff_eq.mp singleton_core_total open Classical in -@[rocq_alias singleton_op] theorem singleton_op_singleton {i : K} {x y : V} : equiv ((singleton i x : M V) • (singleton i y)) (singleton i (x • y)) := by refine fun k => ?_ simp only [CMRA.op, Heap.op, get?_merge, get?_singleton] split <;> simp [Option.merge] -theorem singleton_op_singleton_eq [IsoFunMap M K] {i : K} {x y : V} : +@[rocq_alias singleton_op] +theorem singleton_op_singleton_eq {i : K} {x y : V} : (singleton i x : M V) • (singleton i y) = (singleton i (x • y)) := - IsoFunMap.ext singleton_op_singleton + equiv_iff_eq.mp singleton_op_singleton open Classical in set_option synthInstance.checkSynthOrder false in @@ -725,7 +747,8 @@ theorem exclusive_singleton_inc_iff {m : M V} (He : Exclusive x) (Hv : ✓ m) : · exists x @[rocq_alias singleton_included] -theorem singleton_inc_singleton_iff : (singleton i x : M V) ≼ (singleton i y : M V) ↔ some x ≼ some y := by +theorem singleton_inc_singleton_iff : + (singleton i x : M V) ≼ (singleton i y : M V) ↔ some x ≼ some y := by refine singleton_inc_iff.trans ⟨fun ⟨z, Hz, Hxz⟩ => ?_, fun H => ?_⟩ · exact (Hz.symm.trans <| get?_singleton_eq rfl) ▸ Hxz · refine ⟨y, ?_, H⟩ @@ -767,7 +790,6 @@ instance {m : M V} [Hid : ∀ x : V, IdFree x] [Hc : ∀ x : V, Cancelable x] : simp [get?_merge, CMRA.op, Heap.op, optionOp] cases get? m i <;> cases get? m1 i <;> cases get? m2 i <;> simp_all -@[rocq_alias insert_op] theorem insert_op_equiv {m1 m2 : M V} : equiv ((insert (m1 • m2) i (x • y))) (insert m1 i x • insert m2 i y) := by refine fun j => ?_ @@ -775,9 +797,10 @@ theorem insert_op_equiv {m1 m2 : M V} : · simp [CMRA.op, get?_insert_eq He, get?_merge] · simp [CMRA.op, get?_insert_ne He, get?_merge] -theorem insert_op_eq [IsoFunMap M K] {m1 m2 : M (Option V)} : +@[rocq_alias insert_op] +theorem insert_op_eq {m1 m2 : M (Option V)} : (insert (m1 • m2) i (x • y)) = (insert m1 i x • insert m2 i y) := - IsoFunMap.ext insert_op_equiv + equiv_iff_eq.mp insert_op_equiv @[rocq_alias gmap_op_union] theorem disjoint_op_equiv_union {m1 m2 : M V} (Hd : Set.Disjoint (dom m1) (dom m2)) : @@ -788,9 +811,9 @@ theorem disjoint_op_equiv_union {m1 m2 : M V} (Hd : Set.Disjoint (dom m1) (dom m refine (Hd j ?_).elim simp_all [dom] -theorem disjoint_op_eq_union [IsoFunMap M K] {m1 m2 : M V} (H : Set.Disjoint (dom m1) (dom m2)) : +theorem disjoint_op_eq_union {m1 m2 : M V} (H : Set.Disjoint (dom m1) (dom m2)) : m1 • m2 = union m1 m2 := - IsoFunMap.ext (disjoint_op_equiv_union H) + equiv_iff_eq.mp (disjoint_op_equiv_union H) @[rocq_alias gmap_op_valid0_disjoint] theorem valid0_disjoint_dom {m1 m2 : M V} (Hv : ✓{0} (m1 • m2)) (H : ∀ {k x}, get? m1 k = some x → Exclusive x) : @@ -829,6 +852,34 @@ theorem map_mono [CMRA V'] (f : V → V') (hf : ∀ x y : V, x ≼ y → f x ≼ obtain ⟨z, hz⟩ := Option.map_mono f hf (lookup_inc.mp Hinc i) exact ⟨z, by rw [get?_map, get?_map, hz]⟩ +open Iris.Algebra in +open Classical in +@[rocq_alias big_opM_singletons] +theorem bigOpM_singletons {M' : Type _ → Type _} {K V : Type _} + [LawfulFiniteMap M' K] [CMRA V] (m : M' V) : + ([^ CMRA.op map] k ↦ x ∈ m, PartialMap.singleton k x) = m := by + induction m using LawfulFiniteMap.induction_on with + | hemp => exact BigOpM.bigOpM_empty _ + | hins i x m hi ih => + rw [BigOpM.bigOpM_insert_eq _ x hi, ih] + exact (equiv_iff_eq.mp (Heap.insert_equiv_singleton_op_singleton hi)).symm + +open Iris.Algebra in +open Classical in +@[rocq_alias big_opS_gset_to_gmap, rocq_alias big_opS_gset_to_gmap_L] +theorem bigOpS_ofSet {A S : Type _} [LawfulFiniteSet S A] {M' : Type _ → Type _} + {V : Type _} [LawfulFiniteMap M' A] [CMRA V] (a : V) (s : S) : + ([^ CMRA.op set] k ∈ s, (PartialMap.singleton k a : M' V)) = FiniteMap.ofSet a s := by + induction s using FiniteSet.set_ind with + | hemp => + rw [BigOpS.bigOpS_empty, LawfulFiniteMap.ofSet_empty] + rfl + | hadd x X hx ih => + refine (BigOpS.bigOpS_insert hx).trans ?_ + rw [ih, LawfulFiniteMap.ofSet_insert] + exact (LawfulPartialMap.equiv_iff_eq.mp + (Heap.insert_equiv_singleton_op_singleton (LawfulFiniteMap.get?_ofSet_of_not_mem hx))).symm + @[rocq_alias gmap_cmra_discrete] nonrec instance [HD : CMRA.Discrete V] [LawfulPartialMap M K] : Discrete (M V) where discrete_0 {_ _} H := OFE.eq_dist.mpr fun _ k => (OFE.Discrete.discrete_0 (H k)).dist @@ -903,12 +954,6 @@ variable [LawfulFiniteMap M K] namespace Heap -theorem get?_eq_none_of_not_mem_keys {m : M V} {i : K} - (hi : i ∉ (toList m).map (·.1)) : get? m i = none := by - rcases hm : get? m i with _ | v - · rfl - · exact absurd (List.mem_map_of_mem (toList_get.mpr hm)) hi - variable [CMRA V] open Classical in @@ -918,8 +963,11 @@ theorem alloc_updateP_strong_dep {Q : M V → Prop} {I : K → Prop} {m : M V} { (hQ : ∀ i, get? m i = none → I i → Q (insert m i (f i))) : m ~~>: Q := by refine UpdateP.total.mpr fun n mf hv => ?_ obtain ⟨i, hIi, hi⟩ := hI ((toList (m • mf)).map (·.1)) - obtain ⟨hmi, hmfi⟩ := (Option.op_none_iff _ _).mp <| - get?_op m mf ▸ get?_eq_none_of_not_mem_keys hi + obtain ⟨hmi, hmfi⟩ := (Option.op_none_iff _ _).mp (by + rw [← get?_op m mf (i := i)] + rcases hm : get? (m • mf) i with _ | v + · rfl + · exact absurd (List.mem_map_of_mem (toList_get.mpr hm)) hi) refine ⟨insert m i (f i), hQ i hmi hIi, fun k => ?_⟩ by_cases hk : i = k · subst hk diff --git a/Iris/Iris/Algebra/HeapView.lean b/Iris/Iris/Algebra/HeapView.lean index 2ae70662b..0ac74b498 100644 --- a/Iris/Iris/Algebra/HeapView.lean +++ b/Iris/Iris/Algebra/HeapView.lean @@ -276,7 +276,7 @@ instance [Hdq : CoreId dq] [Hv1 : CoreId v1] : CoreId (Frag (H := H) k dq v1) wh obtain ⟨H⟩ := Hdq simp [CMRA.pcore] at H simp only [CMRA.pcore, View.Pcore] - refine congrArg some (congrArg (View.mk _) (singleton_core_eqv ?_)) + refine congrArg some (congrArg (View.mk _) (singleton_core_eq ?_)) simp [CMRA.pcore, Prod.pcore] cases h : CMRA.pcore v1 · exact OFE.not_none_eqv_some (h ▸ Hv1.core_id) |>.elim diff --git a/Iris/Iris/Algebra/List.lean b/Iris/Iris/Algebra/List.lean index 055f05062..273b3aa1d 100644 --- a/Iris/Iris/Algebra/List.lean +++ b/Iris/Iris/Algebra/List.lean @@ -378,20 +378,4 @@ instance [OFunctorContractive F] : OFunctorContractive (ListOF F) where end functor -section MapSeq - -open Std OFE - -/-- Building a map out of a list of consecutive keys is non-expansive. -/ -@[rocq_alias map_seq_ne] -instance [LawfulFiniteMap M Nat] [OFE V] (start : Nat) : - NonExpansive (FiniteMap.map_seq (M := M) start : List V → M V) where - ne {_ _ _} h k := by - rw [LawfulFiniteMap.get?_map_seq, LawfulFiniteMap.get?_map_seq] - split - · exact NonExpansive.ne (f := fun l : List V => l[k - start]?) h - · exact .rfl - -end MapSeq - end Iris diff --git a/Iris/Iris/BI/BigOp/BigAndMap.lean b/Iris/Iris/BI/BigOp/BigAndMap.lean index 9ef6cc867..162608bb6 100644 --- a/Iris/Iris/BI/BigOp/BigAndMap.lean +++ b/Iris/Iris/BI/BigOp/BigAndMap.lean @@ -238,7 +238,7 @@ theorem bigAndM_toList {Φ : K → V → PROP} {m : M V} : @[rocq_alias big_andM_fmap] theorem bigAndM_map {Φ : K → V → PROP} {m : M V} {f : V → V} : - ([∧map] k ↦ y ∈ Std.PartialMap.map f m, Φ k y) = [∧map] k ↦ y ∈ m, Φ k (f y) := + ([∧map] k ↦ y ∈ PartialMap.map f m, Φ k y) = [∧map] k ↦ y ∈ m, Φ k (f y) := bigOpM_map_eq f Φ m @[rocq_alias big_andM_omap] diff --git a/Iris/Iris/Std/HeapInstances.lean b/Iris/Iris/Std/HeapInstances.lean index b186b721a..149bd1f77 100644 --- a/Iris/Iris/Std/HeapInstances.lean +++ b/Iris/Iris/Std/HeapInstances.lean @@ -16,7 +16,7 @@ This file provides a library of `PartialMap`, `Heap`, and `UnboundedHeap` instances for types from the Lean standard library. ## Instances -- Plain functions: `PartialMap`, `IsoFunMap` +- Plain functions: `PartialMap` - Functions into `Option`: `Heap` - Classical functions into `Option`: `UnboundedHeap` - Association lists: `UnboundedHeap` diff --git a/Iris/Iris/Std/PartialMap.lean b/Iris/Iris/Std/PartialMap.lean index c7ff0003a..569fd525a 100644 --- a/Iris/Iris/Std/PartialMap.lean +++ b/Iris/Iris/Std/PartialMap.lean @@ -58,22 +58,6 @@ class RepFunMap (T : Type _ → Type _) (K : outParam (Type _)) [PartialMap T K] get_of_fun (f : K → Option V) (k : K) : get? (of_fun f) k = f k export RepFunMap (of_fun get_of_fun) -/-- IsoFunStore: The map T is isomorphic to the type of functions out of `K`. In -other words, equality of T is the same as equality of functions, so the CMRA on -these partial functions is leibniz. -/ -class IsoFunMap (T : Type _ → Type _) (K : outParam (Type _)) [PartialMap T K] - extends RepFunMap T K where - of_fun_get {t : T V} : of_fun (get? t) = t -export IsoFunMap (of_fun_get) - -@[ext] -theorem IsoFunMap.ext [PartialMap T K] [IsoFunMap T K] {t1 t2 : T V} - (h : ∀ k, get? t1 k = get? t2 k) : t1 = t2 := by - rw [← of_fun_get (t := t1), ← of_fun_get (t := t2)] - congr 1 - funext k - exact h k - /-- An AllocHeap is a heap which can allocate elements under some condition. -/ class Heap (M : Type _ → Type _) (K : outParam (Type _)) extends PartialMap M K where notFull : M V → Prop From 390762c3bc59e716c869192cf6e8a4df158df486 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Thu, 13 Aug 2026 18:44:58 +0200 Subject: [PATCH 5/6] Fix build --- Iris/Iris/Algebra/CMRA.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/Iris/Iris/Algebra/CMRA.lean b/Iris/Iris/Algebra/CMRA.lean index aaa5bc785..b24f9d941 100644 --- a/Iris/Iris/Algebra/CMRA.lean +++ b/Iris/Iris/Algebra/CMRA.lean @@ -2134,15 +2134,6 @@ open CMRA variable {α β : Type _} [CMRA α] [CMRA β] -@[rocq_alias option_fmap_mono] -theorem Option.map_mono (f : α → β) (hf : ∀ a b : α, a ≼ b → f a ≼ f b) - {ma mb : Option α} (h : ma ≼ mb) : ma.map f ≼ mb.map f := by - rcases Option.inc_iff.mp h with rfl | ⟨a, b, rfl, rfl, hab⟩ - · exact Option.inc_iff.mpr (.inl rfl) - · rcases hab with rfl | hab - · exact Option.some_inc_some_of_eq rfl - · exact Option.some_inc_some_of_inc (hf a b hab) - @[rocq_alias option_fmap_cmra_morphism] def Option.mapC (f : α -C> β) : Option α -C> Option β where toHom := optionMap f.toHom From 6baabfa95611f1bea33fb47416f13d99d0745d8d Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Thu, 13 Aug 2026 18:47:21 +0200 Subject: [PATCH 6/6] Clean up --- Iris/Iris/Algebra/BigOp.lean | 27 +-------------------------- 1 file changed, 1 insertion(+), 26 deletions(-) diff --git a/Iris/Iris/Algebra/BigOp.lean b/Iris/Iris/Algebra/BigOp.lean index d4f8bc619..0c1a2095d 100644 --- a/Iris/Iris/Algebra/BigOp.lean +++ b/Iris/Iris/Algebra/BigOp.lean @@ -419,7 +419,7 @@ theorem bigOpM_const_unit_eq [DecidableEq K] (m : M' V) : @[rocq_alias big_opM_fmap] theorem bigOpM_map_eq (h : V → B) (Φ : K → B → M) (m : M' V) : - ([^ op map] k ↦ x ∈ Std.PartialMap.map h m, Φ k x) = ([^ op map] k ↦ v ∈ m, Φ k (h v)) := + ([^ op map] k ↦ x ∈ PartialMap.map h m, Φ k x) = ([^ op map] k ↦ v ∈ m, Φ k (h v)) := (bigOpL_eq_of_perm _ LawfulFiniteMap.toList_map).trans (bigOpL_map_eq _ _ _) @[rocq_alias big_opM_omap] @@ -563,16 +563,6 @@ theorem bigOpM_weak_hom [DecidableEq K] [ι : WeakMonoidHomomorphism op₁ op₂ show (LawfulFiniteMap.toList m) = [] from List.nil_eq.mpr Hk |>.symm] rfl --- open Classical in --- @[rocq_alias big_opM_singletons] --- theorem bigOpM_singletons [CMRA V] (m : M' V) : --- ([^ CMRA.op map] k ↦ x ∈ m, PartialMap.singleton k x) = m := by --- induction m using LawfulFiniteMap.induction_on with --- | hemp => exact bigOpM_empty _ --- | hins i x m hi ih => --- rw [bigOpM_insert_eq _ x hi, ih] --- exact (equiv_iff_eq.mp (Heap.insert_equiv_singleton_op_singleton hi)).symm - #rocq_ignore big_opM_ne' "Use bigOpM_dist" #rocq_ignore big_opM_proper' "Use bigOpM_eq" @@ -613,21 +603,6 @@ theorem bigOpS_const_unit (s : S) : ([^ op set] _x ∈ s, unit) = unit := by theorem bigOpS_singleton {Φ : A → M} {a : A} : ([^ op set] x ∈ ({a} : S), Φ x) = Φ a := by simp only [bigOpS, toList_singleton]; exact bigOpL_singleton_eq _ _ --- open Classical in --- @[rocq_alias big_opS_gset_to_gmap, rocq_alias big_opS_gset_to_gmap_L] --- theorem bigOpS_ofSet {M' : Type _ → Type _} {V : Type _} [LawfulFiniteMap M' A] [CMRA V] --- (a : V) (s : S) : --- ([^ CMRA.op set] k ∈ s, (PartialMap.singleton k a : M' V)) = FiniteMap.ofSet a s := by --- induction s using set_ind with --- | hemp => --- rw [bigOpS_empty, LawfulFiniteMap.ofSet_empty] --- rfl --- | hadd x X hx ih => --- refine (bigOpS_insert hx).trans ?_ --- rw [ih, LawfulFiniteMap.ofSet_insert] --- exact (LawfulPartialMap.equiv_iff_eq.mp --- (Heap.insert_equiv_singleton_op_singleton (LawfulFiniteMap.get?_ofSet_of_not_mem hx))).symm - @[rocq_alias big_opS_union] theorem bigOpS_union {Φ : A → M} {s₁ s₂ : S} (Hdisj : s₁ ## s₂) : ([^ op set] x ∈ (s₁ ∪ s₂), Φ x) = op ([^ op set] x ∈ s₁, Φ x) ([^ op set] x ∈ s₂, Φ x) := by