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/2] 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 d394dc703a7ba837ec11e569b21e780119d56652 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 10:19:55 -0400 Subject: [PATCH 2/2] port GenHeap and InvHeap --- Iris/Iris/Algebra/Heap.lean | 66 ++++++ Iris/Iris/BI/Lib.lean | 1 + Iris/Iris/BI/Lib/Fractional.lean | 29 +++ Iris/Iris/BI/Lib/GenHeap.lean | 32 +++ Iris/Iris/BI/Lib/InvHeap.lean | 386 +++++++++++++++++++++++++++++++ 5 files changed, 514 insertions(+) create mode 100644 Iris/Iris/BI/Lib/InvHeap.lean diff --git a/Iris/Iris/Algebra/Heap.lean b/Iris/Iris/Algebra/Heap.lean index 6dd4ca9d5..f7cb71be3 100644 --- a/Iris/Iris/Algebra/Heap.lean +++ b/Iris/Iris/Algebra/Heap.lean @@ -6,6 +6,7 @@ Authors: Markus de Medeiros, Puming Liu module public import Iris.Algebra.CMRA +public import Iris.Algebra.LocalUpdates public import Iris.Algebra.OFE public import Iris.Std.Set public import Iris.Std.PartialMap @@ -563,6 +564,71 @@ nonrec instance [HD : CMRA.Discrete V] [LawfulPartialMap M K] : Discrete (M V) w discrete_0 {_ _} H := OFE.eq_dist.mpr fun _ k => (OFE.Discrete.discrete_0 (H k)).dist discrete_valid {_} := (CMRA.Discrete.discrete_valid <| · ·) +section LocalUpdates + +variable {m m1 m2 m1' m2' : M V} {i : K} {x y x' y' : V} + +@[rocq_alias gmap_local_update] +theorem local_update (h : ∀ j, (get? m1 j, get? m2 j) ~l~> (get? m1' j, get? m2' j)) : + ((m1, m2) : M V × M V) ~l~> (m1', m2') := by + refine local_update_unital.mpr fun n z hv he => ?_ + have key j : ✓{n} get? m1' j ∧ get? m1' j ≡{n}≡ get? m2' j • get? z j := by + refine h j n (some (get? z j)) (hv j) ?_ + show get? m1 j ≡{n}≡ get? m2 j • get? z j + rw [← get?_op] + exact he j + refine ⟨fun j => (key j).1, fun j => ?_⟩ + show get? m1' j ≡{n}≡ get? (m2' • z) j + rw [get?_op] + exact (key j).2 + +variable [DecidableEq K] + +@[rocq_alias alloc_local_update] +theorem alloc_local_update (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 hij : i = j + · subst hij + rw [get?_insert_eq rfl, get?_insert_eq rfl, hi] + exact LocalUpdate.alloc_option _ hx + · rw [get?_insert_ne hij, get?_insert_ne hij] + +@[rocq_alias alloc_singleton_local_update] +theorem alloc_singleton_local_update (hi : get? m i = none) (hx : ✓ x) : + ((m, ∅) : M V × M V) ~l~> (insert m i x, {[i := x]}) := + alloc_local_update hi hx + +@[rocq_alias insert_local_update] +theorem insert_local_update (h1 : get? m1 i = some x) (h2 : 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 hij : i = j + · subst hij + rw [get?_insert_eq rfl, get?_insert_eq rfl, h1, h2] + exact h.option + · rw [get?_insert_ne hij, get?_insert_ne hij] + +@[rocq_alias singleton_local_update_any] +theorem singleton_local_update_any (h : ∀ x, get? m i = some x → (x, y) ~l~> (x', y')) : + ((m, {[i := y]}) : M V × M V) ~l~> (insert m i x', {[i := y']}) := by + refine local_update fun j => ?_ + by_cases hij : i = j + · subst hij + rw [get?_singleton_eq rfl, get?_singleton_eq rfl, get?_insert_eq rfl] + rcases hm : get? m i with _ | x + · exact fun _ mz _ he => nomatch mz, he + · exact (h x hm).option + · rw [get?_insert_ne hij, get?_singleton_ne hij, get?_singleton_ne hij] + +@[rocq_alias singleton_local_update] +theorem singleton_local_update (hm : get? m i = some x) (h : (x, y) ~l~> (x', y')) : + ((m, {[i := y]}) : M V × M V) ~l~> (insert m i x', {[i := y']}) := + singleton_local_update_any fun _ hx => (Option.some.inj (hm ▸ hx)) ▸ h + +end LocalUpdates + end Heap section HeapFunctor diff --git a/Iris/Iris/BI/Lib.lean b/Iris/Iris/BI/Lib.lean index d04264b29..d8c15b8e2 100644 --- a/Iris/Iris/BI/Lib.lean +++ b/Iris/Iris/BI/Lib.lean @@ -7,6 +7,7 @@ public import Iris.BI.Lib.Fixpoint public import Iris.BI.Lib.FixpointBanach public import Iris.BI.Lib.Fractional public import Iris.BI.Lib.GenHeap +public import Iris.BI.Lib.InvHeap public import Iris.BI.Lib.Laterable public import Iris.BI.Lib.MonoNat public import Iris.BI.Lib.ProphMap diff --git a/Iris/Iris/BI/Lib/Fractional.lean b/Iris/Iris/BI/Lib/Fractional.lean index 2522c4be2..c709d97a2 100644 --- a/Iris/Iris/BI/Lib/Fractional.lean +++ b/Iris/Iris/BI/Lib/Fractional.lean @@ -25,6 +25,12 @@ class AsFractional {PROP : Type u} [BI PROP] (P : PROP) (ioΦ : InOut) as_fractional : P ⊣⊢ Φ q as_fractional_fractional : Fractional Φ +/-- `FrameFractionalQp qR qP r` is used for fractional framing: it subtracts the +fraction `qR` from `qP`, leaving `r`. See `frame_fractional` for how it is used. -/ +@[rocq_alias FrameFractionalQp] +class FrameFractionalQp (qR qP : Qp) (r : outParam Qp) where + frame_fractional_qp : qP = qR + r + section Lemmas variable {PROP : Type _} [BI PROP] {P P1 P2 : PROP} {Φ : Qp → PROP} {q q1 q2 : Qp} @@ -100,6 +106,29 @@ instance (priority := default - 10) combineSepAsFractionalHalf _ ⊢ Φ (q.half + q.half) := (hP.as_fractional_fractional.fractional q.half q.half).mpr _ ⊢ Φ q := Qp.half_add_half _ ▸ .rfl +@[rocq_alias frame_fractional_qp_add_l] +instance frameFractionalQpAddLeft (q q' : Qp) : FrameFractionalQp q (q + q') q' := ⟨rfl⟩ + +@[rocq_alias frame_fractional_qp_add_r] +instance frameFractionalQpAddRight (q q' : Qp) : FrameFractionalQp q' (q + q') q := + ⟨Subtype.ext (Rat.add_comm ..)⟩ + +@[rocq_alias frame_fractional_qp_half] +instance frameFractionalQpHalf (q : Qp) : FrameFractionalQp q.half q q.half := + ⟨(Qp.half_add_half q).symm⟩ + +/-- Not an instance, for performance reasons; concrete instances are provided for +particular fractional assertions such as `↦`. -/ +@[rocq_alias frame_fractional] +theorem frame_fractional [hR : AsFractional R .in Φ .in qR] [hP : AsFractional P .in Φ .in qP] + [hr : FrameFractionalQp qR qP r] : Frame p R P (Φ r) where + frame := calc + _ ⊢ R ∗ Φ r := sep_mono_left intuitionisticallyIf_elim + _ ⊢ Φ qR ∗ Φ r := sep_mono_left hR.as_fractional.mp + _ ⊢ Φ (qR + r) := (hP.as_fractional_fractional.fractional qR r).mpr + _ ⊢ Φ qP := hr.frame_fractional_qp ▸ .rfl + _ ⊢ P := hP.as_fractional.mpr + end Lemmas section Divide diff --git a/Iris/Iris/BI/Lib/GenHeap.lean b/Iris/Iris/BI/Lib/GenHeap.lean index 33b0b8404..4db79ba50 100644 --- a/Iris/Iris/BI/Lib/GenHeap.lean +++ b/Iris/Iris/BI/Lib/GenHeap.lean @@ -85,6 +85,10 @@ def pointsTo (l : L) (dq : DFrac) (v : V) : IProp GF := heapName ↪◯MAP[l]{dq notation:50 l:50 " ↦{" dq "} " v:50 => pointsTo l dq v notation:50 l:50 " ↦ " v:50 => pointsTo l (DFrac.own 1) v +#rocq_ignore pointsto_def "Rocq unsealed definition body; use pointsTo." +#rocq_ignore pointsto_aux "Rocq sealing auxiliary definition." +#rocq_ignore pointsto_unseal "Rocq unsealing lemma." + /-- The token witnessing that no meta data has been associated with the namespace mask `E` at location `l`. -/ @[rocq_alias meta_token] @@ -92,6 +96,10 @@ def metaToken (l : L) (E : CoPset) : IProp GF := iprop% ∃ γm, (metaName ↪◯MAP[l]{.discard} γm) ∗ iOwn (E := genHeapPreS.metaData (L := L) (V := V)) γm (ReservationMap.mkToken E) +#rocq_ignore meta_token_def "Rocq unsealed definition body; use metaToken." +#rocq_ignore meta_token_aux "Rocq sealing auxiliary definition." +#rocq_ignore meta_token_unseal "Rocq unsealing lemma." + /-- Persistent assertion that the meta-data `x : A` has been associated with namespace `N` to the location `l`. The type `A` must be `Pos.Countable`. -/ @[rocq_alias «meta»] @@ -100,6 +108,10 @@ def metaInfo [Pos.Countable A] (l : L) (N : Namespace) (x : A) : IProp GF := ipr iOwn (E := genHeapPreS.metaData (L := L) (V := V)) γm (.singleton (CoPset.pick (↑N)) (toAgree ⟨Pos.Countable.encode x⟩)) +#rocq_ignore meta_def "Rocq unsealed definition body; use metaInfo." +#rocq_ignore meta_aux "Rocq sealing auxiliary definition." +#rocq_ignore meta_unseal "Rocq unsealing lemma." + end definitions section lemmas @@ -145,6 +157,11 @@ theorem pointsTo_agree : l ↦{dq₁} v₁ ∗ l ↦{dq₂} v₂ ⊢@{IProp GF} unfold pointsTo iapply ghost_map_elem_agree +@[rocq_alias pointsto_combine_sep_gives] +instance instCombineSepGivesPointsTo (l : L) (dq₁ dq₂ : DFrac) (v₁ v₂ : V) : + CombineSepGives (l ↦{dq₁} v₁) (l ↦{dq₂} v₂) iprop(⌜✓ (dq₁ • dq₂) ∧ v₁ = v₂⌝) := + inferInstanceAs (CombineSepGives (heapName ↪◯MAP[l]{dq₁} v₁) (heapName ↪◯MAP[l]{dq₂} v₂) _) + @[rocq_alias pointsto_combine] theorem pointsTo_combine : l ↦{dq₁} v₁ ∗ l ↦{dq₂} v₂ ⊢@{IProp GF} l ↦{dq₁ • dq₂} v₁ ∗ ⌜v₁ = v₂⌝ := by @@ -152,6 +169,13 @@ theorem pointsTo_combine : iintro ⟨H₁, H₂⟩ iapply ghost_map_elem_combine $$ H₁ H₂ +/-- Lower priority than `combineSepAsFractional`, which kicks in for `DFrac.own`. -/ +@[rocq_alias pointsto_combine_as] +instance (priority := default - 20) instCombineSepAsPointsTo + (l : L) (dq₁ dq₂ : DFrac) (v₁ v₂ : V) : + CombineSepAs (l ↦{dq₁} v₁) (l ↦{dq₂} v₂) (l ↦{dq₁ • dq₂} v₁) := + inferInstanceAs (CombineSepAs (heapName ↪◯MAP[l]{dq₁} v₁) (heapName ↪◯MAP[l]{dq₂} v₂) _) + @[rocq_alias pointsto_frac_ne] theorem pointsTo_frac_ne {l₁ l₂ : L} {dq₁ dq₂ : DFrac} {v₁ v₂ : V} (Hk : ¬ ✓ (dq₁ • dq₂)) : @@ -185,6 +209,14 @@ instance instPersistentPointsTo (l : L) (v : V) : unfold pointsTo infer_instance +/-! ### Framing support -/ + +@[rocq_alias frame_pointsto] +instance (priority := high) instFramePointsTo (p : Bool) (l : L) (v : V) (q₁ q₂ r : Qp) + [FrameFractionalQp q₁ q₂ r] : + Frame p (l ↦{.own q₁} v) (l ↦{.own q₂} v) (l ↦{.own r} v) := + frame_fractional (Φ := (l ↦{.own ·} v)) (qR := q₁) (qP := q₂) + /-! ### General properties of `metaInfo` and `metaToken` -/ @[rocq_alias meta_token_timeless] diff --git a/Iris/Iris/BI/Lib/InvHeap.lean b/Iris/Iris/BI/Lib/InvHeap.lean new file mode 100644 index 000000000..17f71eef4 --- /dev/null +++ b/Iris/Iris/BI/Lib/InvHeap.lean @@ -0,0 +1,386 @@ +/- +Copyright (c) 2026 . All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: +-/ +module + +public import Iris.Algebra +public import Iris.Algebra.Auth +public import Iris.Algebra.Excl +public import Iris.BI.Lib.GenHeap +public import Iris.Instances.Lib.Invariants + +@[expose] public section + +namespace Iris + +open Std Std.PartialMap Std.LawfulPartialMap Iris.Algebra CMRA BI ProofMode + +/-! An "invariant" location is a location that has some invariant about its value +attached to it, and that can never be deallocated explicitly by the program. It +provides a persistent witness that will always allow reading the location, +guaranteeing that the value read will satisfy the invariant. + +This is useful for data structures like RDCSS that need to read locations long +after their ownership has been passed back to the client, but do not care *what* +it is that they are reading in that case. In that extreme case, the invariant may +just be `True`. + +Since invariant locations cannot be deallocated, they only make sense when modeling +languages with garbage collection. HeapLang can be used to model either language by +choosing whether or not to use the `Free` operation. By using a separate assertion +`invPointsToOwn` for "invariant" locations, we can keep all the other proofs that do +not need it conservative. + +Where Rocq uses the discrete-function OFE `V -d> PropO`, whose equivalence is +pointwise `Iff`, we use `DiscreteO (V → Prop)`, whose equivalence is Lean equality. +By `propext` and `funext` these agree, so the Rocq statements that conclude +`∀ w, I w ↔ I' w` conclude `I = I'` here. -/ + +@[rocq_alias inv_heapN] +def invHeapN : Namespace := nroot.@"inv_heap" + +/-- The per-location entry: the exclusively-owned current value paired with the +agreed-upon invariant. -/ +@[rocq_alias inv_heap_mapUR] +abbrev InvHeapMapUR (V : Type _) (H : Type _ → Type _) : Type _ := + H (Option (Excl (DiscreteO V)) × Agree (DiscreteO (V → Prop))) + +section toInvHeap + +variable {L V : Type _} {H : Type _ → Type _} [LawfulFiniteMap H L] + +@[rocq_alias to_inv_heap] +def toInvHeap (h : H (V × (V → Prop))) : InvHeapMapUR V H := + Std.PartialMap.map + (fun (p : V × (V → Prop)) => ((some (.excl ⟨p.1⟩), toAgree ⟨p.2⟩) : + Option (Excl (DiscreteO V)) × Agree (DiscreteO (V → Prop)))) h + +@[rocq_alias lookup_to_inv_heap_None] +theorem get?_toInvHeap_none {h : H (V × (V → Prop))} {l : L} (hl : get? h l = none) : + get? (toInvHeap h) l = none := by + rw [toInvHeap, get?_map, hl, Option.map_none] + +@[rocq_alias lookup_to_inv_heap_Some] +theorem get?_toInvHeap_some {h : H (V × (V → Prop))} {l : L} {v : V} {I : V → Prop} + (hl : get? h l = some (v, I)) : + get? (toInvHeap h) l = some (some (.excl ⟨v⟩), toAgree ⟨I⟩) := by + rw [toInvHeap, get?_map, hl, Option.map_some] + +@[rocq_alias lookup_to_inv_heap_Some_2] +theorem get?_toInvHeap_some_2 {h : H (V × (V → Prop))} {l : L} + {v' : Option (Excl (DiscreteO V))} {I' : Agree (DiscreteO (V → Prop))} + (hl : get? (toInvHeap h) l = some (v', I')) : + ∃ v I, v' = some (.excl ⟨v⟩) ∧ I' = toAgree ⟨I⟩ ∧ get? h l = some (v, I) := by + rw [toInvHeap, get?_map] at hl + rcases hh : get? h l with _ | ⟨v, I⟩ <;> rw [hh] at hl <;> simp_all + +@[rocq_alias to_inv_heap_valid] +theorem toInvHeap_valid (h : H (V × (V → Prop))) : ✓ toInvHeap (H := H) h := by + intro l + rcases hh : get? h l with _ | ⟨v, I⟩ + · rw [get?_toInvHeap_none hh]; trivial + · rw [get?_toInvHeap_some hh]; exact ⟨trivial, Agree.toAgree_valid⟩ + +@[rocq_alias to_inv_heap_singleton] +theorem toInvHeap_singleton [DecidableEq L] (l : L) (v : V) (I : V → Prop) : + toInvHeap (H := H) {[l := (v, I)]} = {[l := (some (.excl ⟨v⟩), toAgree ⟨I⟩)]} := by + rw [PartialMap.singleton, toInvHeap, map_insert, map_empty] + rfl + +@[rocq_alias to_inv_heap_insert] +theorem toInvHeap_insert [DecidableEq L] (l : L) (v : V) (I : V → Prop) + (h : H (V × (V → Prop))) : + toInvHeap (insert h l (v, I)) = + insert (toInvHeap h) l (some (.excl ⟨v⟩), toAgree ⟨I⟩) := + map_insert + +end toInvHeap + +@[rocq_alias inv_heapGpreS] +class invHeapPreS (L V : Type _) (GF : BundledGFunctors) (H : outParam <| Type _ → Type _) + [LawfulFiniteMap H L] where + invHeap : ElemG GF (constOF (Auth (InvHeapMapUR V H))) + +attribute [reducible, instance] invHeapPreS.invHeap + +@[rocq_alias inv_heapGS] +class invHeapGS (L V : outParam <| Type _) (GF : outParam <| BundledGFunctors) + (H : outParam <| Type _ → Type _) [LawfulFiniteMap H L] + extends invHeapPreS L V GF H where + invHeapName : GName + +#rocq_ignore «inv_heapΣ» "Subsumed by BundledGFunctors typeclass synthesis" +#rocq_ignore «subG_inv_heapGpreS» "Subsumed by BundledGFunctors typeclass synthesis" + +section definitions + +variable {GF : BundledGFunctors} {L V : Type _} +variable {H : outParam <| Type _ → Type _} [LawfulFiniteMap H L] +variable [InvGS_gen hlc GF] [genHeapGS L V GF H] [G : invHeapGS L V GF H] + +open invHeapGS + +@[rocq_alias inv_heap_inv_P] +def invHeapInvP : IProp GF := iprop( + ∃ h : H (V × (V → Prop)), + iOwn (E := invHeapPreS.invHeap (L := L)) invHeapName (● toInvHeap h) ∗ + [∗map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1) + +@[rocq_alias inv_heap_inv] +def invHeapInv : IProp GF := inv invHeapN invHeapInvP + +@[rocq_alias inv_pointsto_own] +def invPointsToOwn (l : L) (v : V) (I : V → Prop) : IProp GF := + iOwn (E := invHeapPreS.invHeap (L := L)) invHeapName + (◯ {[l := (some (.excl ⟨v⟩), toAgree ⟨I⟩)]}) + +@[rocq_alias inv_pointsto] +def invPointsTo (l : L) (I : V → Prop) : IProp GF := + iOwn (E := invHeapPreS.invHeap (L := L)) invHeapName + (◯ {[l := ((none : Option (Excl (DiscreteO V))), toAgree ⟨I⟩)]}) + +end definitions + +notation:50 l:50 " ↦_" I:max v:50 => invPointsToOwn l v I +notation:50 l:50 " ↦_" I:max "□" => invPointsTo l I + +section lemmas + +variable {GF : BundledGFunctors} {L V : Type _} +variable {H : Type _ → Type _} [LawfulFiniteMap H L] [DecidableEq L] +variable [InvGS_gen hlc GF] [genHeapGS L V GF H] [G : invHeapGS L V GF H] + +open invHeapGS + +/-! ### Helpers -/ + +omit [DecidableEq L] [genHeapGS L V GF H] in +@[rocq_alias inv_pointsto_lookup_Some] +theorem invPointsTo_get?_some (l : L) (h : H (V × (V → Prop))) (I : V → Prop) : + invPointsTo l I -∗ + iOwn (E := invHeapPreS.invHeap (L := L)) invHeapName (● toInvHeap h) -∗ + ⌜∃ v I', get? h l = some (v, I') ∧ I = I'⌝ := by + unfold invPointsTo + iintro Hl Hauth + icombine Hauth Hl gives %Hvalid + ipureintro + obtain ⟨hinc, -⟩ := Auth.auth_both_valid_discrete.mp Hvalid + obtain ⟨⟨y₁, y₂⟩, hy, hyinc⟩ := Heap.singleton_inc_iff.mp hinc + obtain ⟨v', I', rfl, rfl, hh⟩ := get?_toInvHeap_some_2 hy + obtain ⟨⟨_, z₂⟩, hz⟩ := (Option.some_inc_some_iff.mp hyinc).elim + (fun heq => ⟨(none, toAgree ⟨I⟩), heq.symm.trans (Prod.ext rfl Agree.idemp.symm)⟩) id + exact ⟨v', I', hh, DiscreteO.eqv_inj (Agree.toAgree_included.mp ⟨z₂, congrArg Prod.snd hz⟩)⟩ + +omit [DecidableEq L] [genHeapGS L V GF H] in +@[rocq_alias inv_pointsto_own_lookup_Some] +theorem invPointsToOwn_get?_some (l : L) (v : V) (h : H (V × (V → Prop))) (I : V → Prop) : + invPointsToOwn l v I -∗ + iOwn (E := invHeapPreS.invHeap (L := L)) invHeapName (● toInvHeap h) -∗ + ⌜∃ I', get? h l = some (v, I') ∧ I = I'⌝ := by + unfold invPointsToOwn + iintro Hl Hauth + icombine Hauth Hl gives %Hvalid + ipureintro + obtain ⟨hinc, -⟩ := Auth.auth_both_valid_discrete.mp Hvalid + obtain ⟨⟨y₁, y₂⟩, hy, hyinc⟩ := Heap.singleton_inc_iff.mp hinc + obtain ⟨v', I', rfl, rfl, hh⟩ := get?_toInvHeap_some_2 hy + obtain ⟨⟨z₁, z₂⟩, hz⟩ := (Option.some_inc_some_iff.mp hyinc).elim + (fun heq => ⟨(none, toAgree ⟨I⟩), heq.symm.trans (Prod.ext rfl Agree.idemp.symm)⟩) id + obtain rfl : v = v' := DiscreteO.eqv_inj (Excl.excl_included.mp ⟨z₁, congrArg Prod.fst hz⟩) + exact ⟨I', hh, DiscreteO.eqv_inj (Agree.toAgree_included.mp ⟨z₂, congrArg Prod.snd hz⟩)⟩ + +/-! ### Typeclass instances -/ + +#rocq_ignore inv_pointsto_own_proper + "Pointwise `Iff` on `V → Prop` is Lean equality by `propext`; congruence is definitional." +#rocq_ignore inv_pointsto_proper + "Pointwise `Iff` on `V → Prop` is Lean equality by `propext`; congruence is definitional." + +/-- Rocq gets this from typeclass search on the unfolded body of `inv_heap_inv_P`; in Lean +instance search neither unfolds `invHeapInvP` nor applies `BI.exists_timeless`, so the +instance that `inv_acc_timeless` needs is spelled out here. -/ +instance instTimelessInvHeapInvP : Timeless (invHeapInvP (L := L) (V := V) (H := H)) := by + unfold invHeapInvP + refine @BI.exists_timeless _ _ _ _ ?_ + intro h + infer_instance + +@[rocq_alias inv_heap_inv_persistent] +instance instPersistentInvHeapInv : Persistent (invHeapInv (L := L) (V := V) (H := H)) := by + unfold invHeapInv + infer_instance + +/-- The `none` in the exclusive component is the unit of `Option`, but instance search +does not see through `UCMRA.unit`, so the `CoreId` witness is supplied by hand. -/ +@[rocq_alias inv_pointsto_persistent] +instance instPersistentInvPointsTo (l : L) (I : V → Prop) : + Persistent (PROP := IProp GF) (invPointsTo l I) := by + have : CoreId (none : Option (Excl (DiscreteO V))) := unit_CoreId + unfold invPointsTo + infer_instance + +@[rocq_alias inv_pointsto_timeless] +instance instTimelessInvPointsTo (l : L) (I : V → Prop) : + Timeless (PROP := IProp GF) (invPointsTo l I) := by + unfold invPointsTo + infer_instance + +@[rocq_alias inv_pointsto_own_timeless] +instance instTimelessInvPointsToOwn (l : L) (v : V) (I : V → Prop) : + Timeless (PROP := IProp GF) (invPointsToOwn l v I) := by + unfold invPointsToOwn + infer_instance + +/-! ### Public lemmas -/ + +@[rocq_alias make_inv_pointsto] +theorem make_invPointsTo {l : L} {v : V} {I : V → Prop} {E : CoPset} + (hN : (↑invHeapN : CoPset) ⊆ E) (hI : I v) : + invHeapInv (L := L) (V := V) (H := H) -∗ l ↦ v ={E}=∗ invPointsToOwn l v I := by + unfold invHeapInv + iintro #Hinv Hl + imod inv_acc_timeless hN $$ Hinv with ⟨HP, Hclose⟩ + iunfold invHeapInvP at HP + icases HP with ⟨%h, Hauth, HsepM⟩ + rcases hlk : get? h l with _ | ⟨v', I'⟩ + · imod iOwn_update (Auth.auth_update_alloc (Heap.alloc_singleton_local_update + (x := ((some (.excl ⟨v⟩), toAgree ⟨I⟩) : + Option (Excl (DiscreteO V)) × Agree (DiscreteO (V → Prop)))) + (get?_toInvHeap_none hlk) ⟨trivial, Agree.toAgree_valid⟩)) $$ Hauth with ⟨Hauth, Hfrag⟩ + ihave HP : invHeapInvP $$ [Hauth HsepM Hl] + · unfold invHeapInvP + iexists (insert h l (v, I)) + rw [toInvHeap_insert] + iframe Hauth + iapply (BigSepM.bigSepM_insert hlk) + ieval (dsimp only) + iframe Hl HsepM %hI + imod Hclose $$ HP with - + imodintro + unfold invPointsToOwn + iexact Hfrag + · icases (BigSepM.bigSepM_lookup hlk) $$ HsepM with ⟨-, Hl'⟩ + icases pointsTo_ne $$ Hl Hl' with %hne + exact absurd rfl hne + +omit [DecidableEq L] [genHeapGS L V GF H] in +@[rocq_alias inv_pointsto_own_inv] +theorem invPointsToOwn_inv (l : L) (v : V) (I : V → Prop) : + invPointsToOwn (GF := GF) l v I -∗ invPointsTo l I := by + have hinc : ((none : Option (Excl (DiscreteO V))), toAgree (⟨I⟩ : DiscreteO (V → Prop))) ≼ + (some (.excl ⟨v⟩), toAgree ⟨I⟩) := + ⟨(some (.excl ⟨v⟩), toAgree ⟨I⟩), Prod.ext rfl Agree.idemp.symm⟩ + unfold invPointsToOwn invPointsTo + iintro Hl + iapply iOwn_mono (Auth.frag_inc_of_inc (Heap.singleton_inc_singleton_mono hinc)) $$ Hl + +/-- An accessor to make use of `invPointsToOwn`. This opens the invariant *before* +consuming `invPointsToOwn`, so that it can be used before opening an atomic update +that provides `invPointsToOwn`. -/ +@[rocq_alias inv_pointsto_own_acc_strong] +theorem invPointsToOwn_acc_strong {E : CoPset} (hN : (↑invHeapN : CoPset) ⊆ E) : + invHeapInv (L := L) (V := V) (H := H) ={E, E \ ↑invHeapN}=∗ + ∀ (l : L) (v : V) (I : V → Prop), invPointsToOwn l v I -∗ + (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w⌝ -∗ l ↦ w ==∗ + invPointsToOwn l w I ∗ |={E \ ↑invHeapN, E}=> True)) := by + unfold invHeapInv + iintro #Hinv + imod inv_acc_timeless hN $$ Hinv with ⟨HP, Hclose⟩ + imodintro + iintro %l %v %I Hl_inv + iunfold invHeapInvP at HP + icases HP with ⟨%h, Hauth, HsepM⟩ + icases invPointsToOwn_get?_some l v h I $$ Hl_inv Hauth with %⟨I', hh, rfl⟩ + unfold invPointsToOwn + icases (BigSepM.bigSepM_delete hh) $$ HsepM with ⟨⟨%hIv, Hl⟩, HsepM⟩ + iframe Hl %hIv + iintro %w %hIw Hl + imod iOwn_update_op (Auth.auth_update (Heap.singleton_local_update + (get?_toInvHeap_some hh) + (LocalUpdate.prod_1 _ _ + (LocalUpdate.option (LocalUpdate.exclusive (x' := Excl.excl ⟨w⟩) trivial))))) + $$ [$Hauth $Hl_inv] with ⟨Hauth, Hfrag⟩ + ihave HP : invHeapInvP $$ [Hauth HsepM Hl] + · unfold invHeapInvP + iexists (insert h l (w, I)) + rw [toInvHeap_insert] + iframe Hauth + iapply BigSepM.bigSepM_insert_delete + ieval (dsimp only) + iframe Hl HsepM %hIw + imodintro + iframe Hfrag + iapply Hclose $$ HP + +/-- A more standard accessor, derived from `invPointsToOwn_acc_strong`. -/ +@[rocq_alias inv_pointsto_own_acc] +theorem invPointsToOwn_acc {E : CoPset} {l : L} {v : V} {I : V → Prop} + (hN : (↑invHeapN : CoPset) ⊆ E) : + invHeapInv (L := L) (V := V) (H := H) -∗ invPointsToOwn l v I ={E, E \ ↑invHeapN}=∗ + (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w⌝ -∗ l ↦ w ={E \ ↑invHeapN, E}=∗ invPointsToOwn l w I)) := by + iintro #Hinv Hl + imod invPointsToOwn_acc_strong hN $$ Hinv with Hacc + icases Hacc $$ %l %v %I Hl with ⟨%hIv, Hl, Hclose⟩ + imodintro + iframe Hl %hIv + iintro %w %hIw Hl + imod Hclose $$ %w [//] Hl with ⟨Hfrag, Hcl⟩ + imod Hcl with - + imodintro + iexact Hfrag + +omit [DecidableEq L] in +@[rocq_alias inv_pointsto_acc] +theorem invPointsTo_acc {E : CoPset} {l : L} {I : V → Prop} + (hN : (↑invHeapN : CoPset) ⊆ E) : + invHeapInv (L := L) (V := V) (H := H) -∗ invPointsTo l I ={E, E \ ↑invHeapN}=∗ + ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E \ ↑invHeapN, E}=∗ ⌜True⌝) := by + unfold invHeapInv + iintro #Hinv Hl_inv + imod inv_acc_timeless hN $$ Hinv with ⟨HP, Hclose⟩ + imodintro + iunfold invHeapInvP at HP + icases HP with ⟨%h, Hauth, HsepM⟩ + icases invPointsTo_get?_some l h I $$ Hl_inv Hauth with %⟨v, I', hh, rfl⟩ + icases (BigSepM.bigSepM_lookup_acc hh) $$ HsepM with ⟨⟨%hIv, Hl⟩, HsepM⟩ + iexists v + iframe Hl %hIv + iintro Hl + ihave HP : invHeapInvP $$ [Hauth HsepM Hl] + · unfold invHeapInvP + iexists h + iframe Hauth + iapply HsepM + ieval (dsimp only) + iframe Hl %hIv + imod Hclose $$ HP with - + imodintro + itrivial + +end lemmas + +@[rocq_alias inv_heap_init] +theorem invHeap_init (L V : Type _) {GF : BundledGFunctors} {H : Type _ → Type _} + [LawfulFiniteMap H L] [DecidableEq L] [InvGS_gen hlc GF] [genHeapGS L V GF H] + [invHeapPreS L V GF H] (E : CoPset) : + ⊢ |==> ∃ _ : invHeapGS L V GF H, |={E}=> invHeapInv (L := L) (V := V) (H := H) := by + imod (iOwn_alloc (E := invHeapPreS.invHeap (L := L)) + (● toInvHeap (∅ : H (V × (V → Prop)))) (Auth.auth_valid.mpr (toInvHeap_valid ∅))) + with ⟨%γ, Hauth⟩ + letI G : invHeapGS L V GF H := ⟨γ⟩ + imodintro + iexists G + unfold invHeapInv + ihave HP : invHeapInvP $$ [Hauth] + · unfold invHeapInvP + iexists (∅ : H (V × (V → Prop))) + iframe Hauth + iapply BigSepM.bigSepM_empty + itrivial + iapply inv_alloc invHeapN E invHeapInvP $$ [HP] + inext + iexact HP + +end Iris