From e3ad5879d7d8641003e949d6631222d735bbad42 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Tue, 7 Jul 2026 13:11:19 +0200 Subject: [PATCH 1/3] Port --- Iris/Iris/Algebra/DynReservationMap.lean | 686 +++++++++++++++++++++++ Iris/Iris/Std/CoPset.lean | 98 ++++ Iris/Iris/Std/GenSets.lean | 8 + 3 files changed, 792 insertions(+) create mode 100644 Iris/Iris/Algebra/DynReservationMap.lean diff --git a/Iris/Iris/Algebra/DynReservationMap.lean b/Iris/Iris/Algebra/DynReservationMap.lean new file mode 100644 index 000000000..835e89a7c --- /dev/null +++ b/Iris/Iris/Algebra/DynReservationMap.lean @@ -0,0 +1,686 @@ +/- +Copyright (c) 2026 Zongyuan Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zongyuan Liu +-/ +module + +import Iris.Std.Positives +public import Iris.Std.CoPset +public import Iris.Std.GenSets +public import Iris.Std.PartialMap +public import Iris.Algebra.CMRA +public import Iris.Algebra.Heap +public import Iris.Algebra.IsOp +public import Iris.Algebra.Updates +public import Iris.Algebra.LeibnizSet + +namespace Iris + +@[expose] public section + +open Iris Std PartialMap + +/-! +The camera [DynReservationMap A H] over a camera [A] extends [LawfulPartialMap H Pos] +with a notion of "reservation tokens" for a (potentially infinite) set +[E : CoPset] which represent the right to allocate a map entry at any position +[k ∈ E]. Unlike [ReservationMap], [DynReservationMap] supports dynamically +allocating these tokens, including infinite sets of them. +-/ + +@[rocq_alias dyn_reservation_map] +structure DynReservationMap (A : Type) (H : Type → Type) where + data : H A + token : DisjointLeibnizSet CoPset + +def DynReservationMap.mkData [LawfulPartialMap H Pos] (data : H A) : + DynReservationMap A H := .mk data ∅ + +@[rocq_alias dyn_reservation_map_data] +def DynReservationMap.singleton [LawfulPartialMap H Pos] (k : Pos) (a : A) : + DynReservationMap A H := DynReservationMap.mkData {[k := a]} + +@[rocq_alias dyn_reservation_map_token] +def DynReservationMap.mkToken [LawfulPartialMap H Pos] (e : CoPset) : + DynReservationMap A H := .mk ∅ (.valid e) + +#rocq_ignore to_reservation_map "Not needed; the OFE/CMRA are built directly, not via an isomorphism" +#rocq_ignore from_reservation_map "Not needed; the OFE/CMRA are built directly, not via an isomorphism" + +section OFE + +open OFE + +variable [LawfulPartialMap H Pos] [OFE A] + +#rocq_ignore dyn_reservation_map_ofe_mixin "Not needed" + +@[rocq_alias dyn_reservation_mapO] +instance : OFE (DynReservationMap A H) where + Equiv x y := x.data ≡ y.data ∧ x.token ≡ y.token + Dist n x y := x.data ≡{n}≡ y.data ∧ x.token ≡{n}≡ y.token + dist_eqv := { + refl _ := ⟨.rfl, rfl⟩, + symm h := ⟨h.left.symm, h.right.symm⟩, + trans h₁ h₂ := ⟨h₁.left.trans h₂.left, h₁.right.trans h₂.right⟩ + } + equiv_dist := + ⟨fun h n => ⟨equiv_dist.mp h.left n, h.right⟩, + fun h => ⟨equiv_dist.mpr (h · |>.left), (h 0).right⟩⟩ + dist_lt h lt := ⟨dist_lt h.left lt, dist_lt h.right lt⟩ + +@[rocq_alias dyn_reservation_map_ofe_discrete] +instance instDiscreteDynReservationMap [Discrete A] : Discrete (DynReservationMap A H) where + discrete_0 h := ⟨discrete_0 h.left, discrete_0 h.right⟩ + +instance instNonExpansiveDynReservationMapData : + NonExpansive (DynReservationMap.mkData (H := H) (A := A)) where + ne _ _ _ h := ⟨h, rfl⟩ + +#rocq_ignore dyn_reservation_map_data_proper "Derivable using NonExpansive.eqv" + +@[rocq_alias dyn_reservation_map_data_ne] +instance instNonExpansiveDynReservationMapSingleton : + NonExpansive (DynReservationMap.singleton (H := H) (A := A) k) where + ne _ _ _ h := ⟨singleton_dist h k, rfl⟩ + +@[rocq_alias DynReservationMap_discrete] +instance instDiscreteEDynReservationMapMk {a : H A} [DiscreteE a] : + DiscreteE (DynReservationMap.mk a b) where + discrete := fun ⟨ha, hb⟩ => ⟨DiscreteE.discrete ha, DiscreteE.discrete hb⟩ + +@[rocq_alias dyn_reservation_map_data_discrete] +instance instDiscreteEDynReservationMapSingleton {a : A} [DiscreteE a] : + DiscreteE (DynReservationMap.singleton (H := H) k a) := + by unfold DynReservationMap.singleton DynReservationMap.mkData; infer_instance + +@[rocq_alias dyn_reservation_map_token_discrete] +instance instDiscreteEDynReservationMapToken : + DiscreteE (DynReservationMap.mkToken (H := H) (A := A) e) := + by unfold DynReservationMap.mkToken; infer_instance + +end OFE + +section CMRA + +open OFE CMRA DisjointLeibnizSet LawfulSet + +namespace DynReservationMap + +section + +variable [LawfulPartialMap H Pos] [CMRA A] + +def ValidN (n : Nat) (x : DynReservationMap A H) : Prop := + match x.token with + | .valid e => ✓{n} x.data ∧ setInfinite (⊤ \ e) ∧ ∀ i, get? x.data i = none ∨ i ∉ e + | .error => False + +def Valid (x : DynReservationMap A H) : Prop := + match x.token with + | .valid e => ✓ x.data ∧ setInfinite (⊤ \ e) ∧ ∀ i, get? x.data i = none ∨ i ∉ e + | .error => False + +/-- The complement of the token's mask `e` is infinite, i.e. there are always infinitely many keys +still available to reserve. This is a validity requirement of `DynReservationMap`. -/ +def Infinite (x : DynReservationMap A H) : Prop := + match x.token with + | .valid e => setInfinite ((⊤ : CoPset) \ e) + | .error => True + +theorem validN_iff {n : Nat} {x : DynReservationMap A H} : + x.ValidN n ↔ ✓{n} x.data ∧ ✓{n} x.token ∧ x.Infinite ∧ + ∀ i, get? x.data i = none ∨ i ∉ x.token := by + refine ⟨fun h => ?_, fun ⟨vd, vt, inf, disj⟩ => ?_⟩ + · simp only [ValidN, Infinite] at h ⊢ + cases eq : x.token with + | valid s => + simp only [eq] at h ⊢ + exact ⟨h.left, trivial, h.right.left, h.right.right⟩ + | error => simp only [eq] at h + · simp only [ValidN] + cases h : x.token + · simp only [h, Infinite] at disj inf + exact ⟨vd, inf, disj⟩ + · exact ((h ▸ not_valid_invalid (S := CoPset)) vt) + +theorem valid_iff {x : DynReservationMap A H} : + x.Valid ↔ ✓ x.data ∧ ✓ x.token ∧ x.Infinite ∧ + ∀ i, get? x.data i = none ∨ i ∉ x.token := by + refine ⟨fun h => ?_, fun ⟨vd, vt, inf, disj⟩ => ?_⟩ + · simp only [Valid, Infinite] at h ⊢ + cases eq : x.token with + | valid s => + simp only [eq] at h ⊢ + exact ⟨h.left, valid_set, h.right.left, h.right.right⟩ + | error => simp only [eq] at h + · simp only [Valid] + cases h : x.token + · simp only [h, Infinite] at disj inf + exact ⟨vd, inf, disj⟩ + · exact ((h ▸ not_valid_invalid (S := CoPset)) vt) + +theorem validN_data_of_validN {n : Nat} {x : DynReservationMap A H} (h : x.ValidN n) : + ✓{n} x.data := (validN_iff.mp h).left + +theorem validN_token_of_validN {n : Nat} {x : DynReservationMap A H} (h : x.ValidN n) : + ✓{n} x.token := (validN_iff.mp h).right.left + +theorem validN_infinite {n : Nat} {x : DynReservationMap A H} (h : x.ValidN n) : + x.Infinite := (validN_iff.mp h).right.right.left + +theorem validN_disj {n : Nat} {x : DynReservationMap A H} (h : x.ValidN n) (i : Pos) : + get? x.data i = none ∨ i ∉ x.token := (validN_iff.mp h).right.right.right i + +theorem valid_data_of_valid {x : DynReservationMap A H} (h : x.Valid) : + ✓ x.data := (valid_iff.mp h).left + +theorem valid_token_of_valid {x : DynReservationMap A H} (h : x.Valid) : + ✓ x.token := (valid_iff.mp h).right.left + +theorem valid_infinite {x : DynReservationMap A H} (h : x.Valid) : + x.Infinite := (valid_iff.mp h).right.right.left + +theorem valid_disj {x : DynReservationMap A H} (h : x.Valid) (i : Pos) : + get? x.data i = none ∨ i ∉ x.token := (valid_iff.mp h).right.right.right i + +def core (x : DynReservationMap A H) : DynReservationMap A H := mk (CMRA.core x.data) ∅ + +@[simp] +theorem core_data (x : DynReservationMap A H) : x.core.data = CMRA.core x.data := rfl + +@[simp] +theorem core_token (x : DynReservationMap A H) : x.core.token = CMRA.core x.token := rfl + +def op (x y : DynReservationMap A H) : DynReservationMap A H := + mk (x.data • y.data) (x.token • y.token) + +@[simp] +theorem op_data' (x y : DynReservationMap A H) : (x.op y).data = x.data • y.data := rfl + +@[simp] +theorem op_token' (x y : DynReservationMap A H) : (x.op y).token = x.token • y.token := rfl + +theorem infinite_op_left {x y : DynReservationMap A H} (vt : ✓{n} (x.token • y.token)) + (inf : (x.op y).Infinite) : x.Infinite := by + match ht : x.token, hy : y.token with + | .error, _ => exact (not_validN_invalid (ht ▸ validN_op_left vt)).elim + | .valid e₁, .error => exact (not_validN_invalid (hy ▸ validN_op_right vt)).elim + | .valid e₁, .valid e₂ => + have hv : ✓{n} (DisjointLeibnizSet.valid e₁ • DisjointLeibnizSet.valid e₂) := + ht ▸ hy ▸ vt + have hdisj : e₁ ## e₂ := by + by_cases h : e₁ ## e₂ + · exact h + · simp only [CMRA.op, h, ↓reduceIte] at hv; exact hv.elim + simp only [Infinite, ht] at ⊢ + simp only [Infinite, op_token', ht, hy, CMRA.op, hdisj, ↓reduceIte] at inf + exact setInfinite_mono + (fun i hi => mem_diff.mpr ⟨(mem_diff.mp hi).left, + fun hc => (mem_diff.mp hi).right (mem_union.mpr (.inl hc))⟩) inf + +#rocq_ignore dyn_reservation_map_cmra_mixin "Not needed" +#rocq_ignore dyn_reservation_map_ucmra_mixin "Not needed" +#rocq_ignore dyn_reservation_mapR "Derivable using UCMRA" + +@[rocq_alias dyn_reservation_mapUR] +instance : UCMRA (DynReservationMap A H) where + pcore := some ∘ core + Valid := Valid + ValidN := ValidN + op := op + op_ne := ⟨fun n x₁ x₂ h => ⟨Dist.op_r h.left, Dist.op_r h.right⟩⟩ + pcore_ne {n x y cx} e pe := by + cases Option.some_inj.mp pe.symm + refine ⟨core y, rfl, ?_, ?_⟩ + · simp [Dist.core e.left] + · simp [Dist.core e.right] + validN_ne {n x y} h v := by + refine validN_iff.mpr ⟨?_, ?_, ?_, fun i => ?_⟩ + · exact (Dist.validN h.left).mp (validN_data_of_validN v) + · exact (Dist.validN h.right).mp (validN_token_of_validN v) + · have hinf := validN_infinite v + simp only [Infinite] at hinf ⊢ + rw [← h.right] + exact hinf + · cases (validN_disj v) i with + | inl gn => + refine .inl <| ?_ + rw [←dist_none (n := n)] + refine .trans (h.left i).symm ?_ + simp [gn] + | inr ni => + refine .inr fun hc => ni ?_ + rw [congrFun ((congrArg Membership.mem h.right)) i] + exact hc + valid_iff_validN {x} := by + refine ⟨fun h n => ?_, fun v => ?_⟩ + · refine validN_iff.mpr ⟨?_, ?_, ?_, ?_⟩ + · exact Valid.validN (valid_data_of_valid h) + · exact (valid_0_iff_validN n).mp (valid_token_of_valid h) + · exact valid_infinite h + · exact valid_disj h + · refine valid_iff.mpr ⟨?_, ?_, ?_, ?_⟩ + · exact valid_iff_validN.mpr (fun n => validN_data_of_validN (v n)) + · exact valid_iff_validN.mpr (fun n => validN_token_of_validN (v n)) + · exact validN_infinite (v 0) + · exact validN_disj (v 0) + validN_succ {x n} v := by + refine validN_iff.mpr ⟨?_, ?_, ?_, ?_⟩ + · exact validN_succ (validN_data_of_validN v) + · exact (valid_0_iff_validN n).mp (validN_token_of_validN (n := n.succ) v) + · exact validN_infinite v + · exact validN_disj v + validN_op_left {n x y} v := by + refine validN_iff.mpr ⟨?_, ?_, ?_, fun i => ?_⟩ + · exact validN_op_left (validN_data_of_validN v) + · exact validN_op_left (validN_token_of_validN v) + · exact infinite_op_left (validN_token_of_validN v) (validN_infinite v) + · cases (validN_disj v) i with + | inl aa => + simp only [op_data', Heap.get?_op] at aa + exact .inl <| Option.eq_none_of_op_eq_none_left aa + | inr bb => + refine .inr fun HK => bb ?_ + refine (mem_iff_of_validN_union (validN_token_of_validN v) i).mpr ?_ + exact .inl HK + assoc := ⟨CMRA.assoc, CMRA.assoc⟩ + comm := ⟨CMRA.comm, CMRA.comm⟩ + pcore_op_left {x cx} h := by + refine ⟨?_, ?_⟩ + · simp [←Option.some_inj.mp h, op_data', core_data, core_op x.data] + · simp [←Option.some_inj.mp h, op_token', core_token, core_op_L] + pcore_idem {x cx} h := by + refine ⟨?_, ?_⟩ + · simp [←Option.some_inj.mp h, core_data, core_idem x.data] + · simp [←Option.some_inj.mp h, core_token, core_idem_L] + pcore_op_mono {x cx} h y := by + obtain ⟨z, hz⟩ := core_op_mono x.data y.data + obtain ⟨w, hw⟩ := core_op_mono x.token y.token + refine ⟨mk z w, ?_, ?_⟩ + · simp [op_data', core_data, (Option.some_inj.mp h.symm), hz] + · simp only [core_token, op_token', (Option.some_inj.mp h.symm), leibniz] + exact hw + extend {n x y₁ y₂} v exy := by + obtain ⟨z₁, z₂, xzz, zy₁, zy₂⟩ := CMRA.extend (validN_data_of_validN v) exy.left + refine ⟨mk z₁ y₁.token, mk z₂ y₂.token, ?_, ?_, ?_⟩ + · refine ⟨?_, ?_⟩ + · simp [op_data', xzz] + · simp only [op_token', leibniz] + exact exy.right + · exact ⟨zy₁, rfl⟩ + · exact ⟨zy₂, rfl⟩ + unit := mk ∅ ∅ + unit_valid := valid_iff.mpr ⟨Heap.valid_empty, valid_set, + show setInfinite ((⊤ : CoPset) \ ∅) by rw [diff_empty]; exact top_infinite, + fun _ => .inr (mem_empty _)⟩ + unit_left_id {x} := ⟨by simp only [op, Algebra.MonoidOps.op_left_id], pcore_op_left' rfl⟩ + pcore_unit := ⟨Heap.core_empty, .rfl⟩ + +@[simp] +theorem op_data (x y : DynReservationMap A H) : (x • y).data = x.data • y.data := rfl + +@[simp] +theorem op_token (x y : DynReservationMap A H) : (x • y).token = x.token • y.token := rfl + +@[rocq_alias dyn_reservation_map_included] +theorem included {x y : DynReservationMap A H} : + x ≼ y ↔ x.data ≼ y.data ∧ x.token ≼ y.token := by + refine ⟨fun ⟨z, hz⟩ => ⟨⟨z.data, hz.left⟩, ⟨z.token, hz.right⟩⟩, ?_⟩ + exact fun ⟨⟨z₁, hz₁⟩, ⟨z₂, hz₂⟩⟩ => ⟨mk z₁ z₂, hz₁, hz₂⟩ + +@[rocq_alias dyn_reservation_map_data_proj_validN] +theorem data_proj_validN {n} {x : DynReservationMap A H} (h : ✓{n} x) : ✓{n} x.data := + validN_data_of_validN h + +@[rocq_alias dyn_reservation_map_token_proj_validN] +theorem token_proj_validN {n} {x : DynReservationMap A H} (h : ✓{n} x) : ✓{n} x.token := + validN_token_of_validN h + +@[rocq_alias dyn_reservation_map_cmra_discrete] +instance [CMRA.Discrete A] : CMRA.Discrete (DynReservationMap A H) where + discrete_valid {_} v := by + refine valid_iff.mpr ⟨?_, ?_, ?_, ?_⟩ + · exact discrete_valid (validN_data_of_validN v) + · exact validN_token_of_validN v + · exact validN_infinite v + · exact validN_disj v + +@[rocq_alias dyn_reservation_map_data_core_id] +instance instCoreIdSingleton {a : A} [CoreId a] : CoreId (singleton (H := H) k a) where + core_id := by + refine ⟨?_, rfl⟩ + simp [singleton, mkData, core_eqv_self (PartialMap.singleton k a)] + +theorem empty_infinite : setInfinite ((⊤ : CoPset) \ ∅) := by + rw [diff_empty]; exact top_infinite + +theorem split_valid {x : DynReservationMap A H} (vx : ✓ x) : + ∃ (d : H A) (t : CoPset), x ≡ mkData d • mkToken t := by + rcases x with ⟨xd, xt⟩ + match hh : xt with + | .error => + exact ((not_valid_invalid (S := CoPset)) (hh ▸ (valid_token_of_valid vx))).elim + | .valid t => + refine ⟨xd, t, ?_, ?_⟩ + · simp [mkData, mkToken, op_data, Algebra.MonoidOps.op_right_id.symm] + · simp only [mkData, mkToken, op_token, leibniz] + exact (pcore_op_left_L rfl).symm + +theorem split_validN {x : DynReservationMap A H} (vx : ✓{n} x) : + ∃ (d : H A) (t : CoPset), x ≡ mkData d • mkToken t := by + rcases x with ⟨xd, xt⟩ + have h := validN_token_of_validN vx + match hh : xt with + | .error => exact ((not_valid_invalid (S := CoPset)) (hh ▸ h)).elim + | .valid t => + refine ⟨xd, t, ?_, ?_⟩ + · simpa [mkData, mkToken, op_data] using Algebra.MonoidOps.op_right_id.symm + · exact (pcore_op_left' rfl).symm + +theorem valid_data {d : H A} : ✓ (mkData (H := H) d) ↔ ✓ d := + ⟨valid_data_of_valid, fun h => valid_iff.mpr ⟨h, valid_set, empty_infinite, + fun p => .inr (mem_empty p)⟩⟩ + +theorem validN_data {d : H A} : ✓{n} (mkData (H := H) d) ↔ ✓{n} d := + ⟨validN_data_of_validN, fun h => validN_iff.mpr ⟨h, validN_set, empty_infinite, + fun p => .inr (mem_empty p)⟩⟩ + +@[rocq_alias dyn_reservation_map_data_valid] +theorem valid_singleton (k : Pos) (a : A) : ✓ (singleton (H := H) k a) ↔ ✓ a := + valid_data.trans Heap.singleton_valid_iff + +theorem validN_singleton (k : Pos) (a : A) : ✓{n} (singleton (H := H) k a) ↔ ✓{n} a := + validN_data.trans Heap.singleton_validN_iff + +@[rocq_alias dyn_reservation_map_token_valid] +theorem valid_token {e : CoPset} : + ✓ (mkToken (H := H) (A := A) e) ↔ setInfinite ((⊤ : CoPset) \ e) := by + refine ⟨fun h => valid_infinite h, fun hinf => + valid_iff.mpr ⟨Heap.valid_empty, valid_set, ?_, ?_⟩⟩ + · exact hinf + · exact fun i => .inl (get?_empty i) + +theorem data_op (a b : H A) : mkData (a • b) ≡ mkData a • mkData b := + ⟨.rfl, (pcore_op_right_L rfl).symm⟩ + +@[rocq_alias dyn_reservation_map_data_op] +theorem singleton_op k (a b : A) : + singleton (H := H) k (a • b) ≡ singleton (H := H) k a • singleton k b := by + refine ((data_op _ _).symm.trans ?_).symm + exact NonExpansive.eqv (fun i => .of_eq (Heap.singleton_op_singleton i)) + +@[rocq_alias dyn_reservation_map_data_mono] +theorem singleton_mono {k} {a b : A} (Hab : a ≼ b) : + singleton (H := H) k a ≼ singleton k b := + let ⟨z, hz⟩ := Hab + ⟨singleton k z, (NonExpansive.eqv hz).trans (singleton_op k a z)⟩ + +set_option synthInstance.checkSynthOrder false in +@[rocq_alias dyn_reservation_map_data_is_op] +instance {ia ib₁ ib₂ : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp ia a ib₁ b₁ ib₂ b₂] : + IsOp ia (singleton (H := H) k a) ib₁ (singleton k b₁) ib₂ (singleton k b₂) where + is_op := .trans (NonExpansive.eqv hv.is_op) (singleton_op k b₁ b₂) + +@[rocq_alias dyn_reservation_map_token_union] +theorem token_union {e₁ e₂} (he : e₁ ## e₂) : + mkToken (H := H) (A := A) (e₁ ∪ e₂) ≡ mkToken e₁ • mkToken e₂ := by + refine ⟨fun i => ?_, ?_⟩ + · simpa only [mkToken, get?_empty, op_data, Heap.get?_op] using .rfl + · simp [mkToken, CMRA.op, he] + +@[rocq_alias dyn_reservation_map_token_difference] +theorem token_difference {e₁ e₂} (he : e₁ ⊆ e₂) : + mkToken (H := H) (A := A) e₂ ≡ mkToken e₁ • mkToken (e₂ \ e₁) := by + refine .trans ?_ (token_union LawfulSet.disjoint_diff_right) + rw [LawfulSet.subset_union_diff he] + +@[rocq_alias dyn_reservation_map_token_valid_op] +theorem valid_token_op {e₁ e₂} : + ✓ (mkToken (H := H) (A := A) e₁ • mkToken e₂) ↔ + e₁ ## e₂ ∧ setInfinite ((⊤ : CoPset) \ (e₁ ∪ e₂)) := by + refine ⟨fun h => ⟨?_, ?_⟩, fun ⟨hdisj, hinf⟩ => ?_⟩ + · exact valid_op_iff_disj.mp (valid_token_of_valid h) + · have hdisj := valid_op_iff_disj.mp (valid_token_of_valid h) + have hinf := valid_infinite h + have htok : + (mkToken (H := H) (A := A) e₁ • mkToken e₂).token = .valid (e₁ ∪ e₂) := by + show DisjointLeibnizSet.valid e₁ • DisjointLeibnizSet.valid e₂ = _ + simp only [CMRA.op, hdisj, ↓reduceIte] + simp only [Infinite, htok] at hinf + exact hinf + · exact (Equiv.valid (token_union hdisj)).mp (valid_token.mpr hinf) + +theorem disj_of_validN_data_op_token {a : H A} {b : CoPset} (h : ✓{n} mkData a • mkToken b) + (i : Pos) : get? a i = none ∨ i ∉ b := by + cases validN_disj h i with + | inl h => + simp only [mkData, mkToken, op_data, Heap.get?_op, get?_empty] at h + exact .inl <| Option.eq_none_of_op_eq_none_left h + | inr h' => + simp only [mkData, mkToken, op_token] at h' + rw [mem_iff_of_valid_union, not_or] at h' + · exact .inr <| h'.right + · exact valid_of_eqv (pcore_op_left' rfl).symm valid_set + +theorem infinite_data_op_token {a : H A} {b : CoPset} (h : ✓{n} mkData a • mkToken b) : + setInfinite ((⊤ : CoPset) \ b) := by + have hinf := validN_infinite h + have eo : (mkData a • mkToken b).token = .valid b := pcore_op_left_L rfl + rw [Infinite, eo] at hinf + exact hinf + +theorem validN_data_op_token {n : Nat} (a : H A) (b : CoPset) (vd : ✓{n} mkData a) + (inf : setInfinite ((⊤ : CoPset) \ b)) (disj : ∀ i, get? a i = none ∨ i ∉ b) : + ✓{n} mkData a • mkToken b := by + have abdp : (mkData a • mkToken b).data ≡ a := + show a • ∅ ≡ a from Algebra.MonoidOps.op_right_id + have eo : ∅ • DisjointLeibnizSet.valid b = .valid b := pcore_op_left_L rfl + refine validN_iff.mpr ⟨?_, ?_, ?_, fun i => ?_⟩ + · exact validN_of_eqv abdp.symm ((validN_data).mp vd) + · simp [mkData, mkToken, eo, validN_set] + · rw [Infinite, show (mkData a • mkToken b).token = .valid b from pcore_op_left_L rfl] + exact inf + · simp [mkData, mkToken, op_data, Heap.get?_op, get?_empty, op_token] + cases disj i with + | inl h => simpa [h] using .inl <| rfl + | inr h => simpa [eo] using .inr h + +theorem valid_op?_of_valid_singleton_op {a : A} {x : H A} (h : ✓{n} (singleton k a • mkData x)) : + ✓{n} a •? get? x k := by + match h' : get? x k with + | none => simpa [op?] using (validN_singleton (H := H) k a).mp (validN_op_left h) + | some g => + simp only [op?] + have vdp := (validN_data_of_validN h) k + simp only [CMRA.op, singleton, mkData, op_data', Heap.op, get?_merge, Option.merge, + LawfulPartialMap.get?_singleton, ↓reduceIte, h'] at vdp + exact vdp + +theorem valid_singleton_op_of_valid_op? {a : A} {x : H A} (vx : ✓{n} x) (h : ✓{n} a •? get? x k) : + ✓{n} singleton k a • mkData x := by + refine validN_of_eqv (data_op (PartialMap.singleton k a) x) ?_ + refine (validN_data).mpr fun i => ?_ + rw [Heap.get?_op] + by_cases ki : k = i + · simp only [← ki, LawfulPartialMap.get?_singleton, ↓reduceIte, Option.some_op_opM]; exact h + · simp only [LawfulPartialMap.get?_singleton, ki, ↓reduceIte]; exact Heap.validN_get? vx + +theorem validN_token_op_iff_disj {e₁ e₂} : + ✓{n} (mkToken (H := H) (A := A) e₁ • mkToken e₂) ↔ + e₁ ## e₂ ∧ setInfinite ((⊤ : CoPset) \ (e₁ ∪ e₂)) where + mp h := ⟨valid_op_iff_disj.mp (validN_token_of_validN h), by + have hdisj := valid_op_iff_disj.mp (validN_token_of_validN h) + have hinf := validN_infinite h + have htok : + (mkToken (H := H) (A := A) e₁ • mkToken e₂).token = .valid (e₁ ∪ e₂) := by + show DisjointLeibnizSet.valid e₁ • DisjointLeibnizSet.valid e₂ = _ + simp only [CMRA.op, hdisj, ↓reduceIte] + simp only [Infinite, htok] at hinf + exact hinf⟩ + mpr := fun ⟨hdisj, hinf⟩ => validN_of_eqv (token_union hdisj) (valid_token.mpr hinf).validN + +@[rocq_alias dyn_reservation_map_alloc] +theorem alloc {e k} {a : A} (hke : k ∈ e) (va : ✓ a) : + mkToken (H := H) e ~~> singleton k a := by + intro n mz vo + match mz with + | none => exact Valid.validN <| (valid_singleton k a).mpr va + | some z => + have ⟨d, t, ze⟩ := split_validN (validN_op_right vo) + have vedt : ✓{n} mkToken e • (mkData d • mkToken t) := validN_of_eqv (op_right_eqv _ ze) vo + have disj : ∀ (i : Pos), get? d i = none ∨ ¬i ∈ e := + disj_of_validN_data_op_token (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt))) + have inf : setInfinite ((⊤ : CoPset) \ t) := + infinite_data_op_token (validN_of_eqv ze (validN_op_right vo)) + refine validN_of_eqv (op_right_eqv _ ze.symm) ?_ + refine validN_of_eqv CMRA.assoc.symm ?_ + refine validN_of_eqv (op_left_eqv (mkToken t) (data_op _ _)) ?_ + refine validN_data_op_token (PartialMap.singleton k a • d) t ?_ inf ?_ + · refine validN_of_eqv (data_op _ _).symm ?_ + apply valid_singleton_op_of_valid_op? + · exact validN_data.mp + (validN_op_left (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt)))) + · exact (disj k).elim (fun h => h ▸ Valid.validN va) (absurd hke) + · simp only [CMRA.op, Heap.op, get?_merge, LawfulPartialMap.get?_singleton, + Option.merge_eq_none_iff, ite_eq_right_iff, reduceCtorEq, imp_false] + intro i + grind [disj_of_validN_data_op_token (validN_of_eqv ze (validN_op_right vo)), + (validN_token_op_iff_disj.mp + (validN_op_right (validN_of_eqv assoc.symm (validN_of_eqv comm vedt)))).left i] + +@[rocq_alias dyn_reservation_map_updateP] +theorem updateP {P} {Q : DynReservationMap A H → Prop} k a (ap : a ~~>: P) + (apq : ∀ a', P a' → Q (singleton k a')) : singleton k a ~~>: Q := by + intro n mz vaz + match mz with + | none => + obtain ⟨y, py, vy⟩ := ap n none ((validN_singleton k a).mp vaz) + exact ⟨_, (apq y py), (validN_singleton k y).mpr vy⟩ + | some z => + obtain ⟨d, t, ze⟩ := split_validN (validN_op_right vaz) + obtain ⟨y, py, vy⟩ := ap n (get? d k) + (valid_op?_of_valid_singleton_op + (validN_op_left (validN_of_eqv CMRA.assoc + (validN_of_eqv (op_right_eqv (singleton k a) ze) vaz)))) + refine ⟨singleton k y, apq y py, ?_⟩ + simp only [CMRA.op?] at vaz ⊢ + have inf : setInfinite ((⊤ : CoPset) \ t) := + infinite_data_op_token (validN_of_eqv ze (validN_op_right vaz)) + refine validN_of_eqv (op_right_eqv (singleton k y) ze).symm ?_ + refine validN_of_eqv CMRA.assoc.symm ?_ + refine validN_of_eqv (op_left_eqv (mkToken t) (data_op _ _)) ?_ + refine validN_data_op_token _ _ ?_ inf ?_ + · refine validN_of_eqv (data_op _ _).symm ?_ + refine valid_singleton_op_of_valid_op? ?_ vy + refine validN_data.mp ?_ + exact validN_op_left <| validN_of_eqv ze (validN_op_right vaz) + · have ddt := disj_of_validN_data_op_token (validN_of_eqv ze (validN_op_right vaz)) + have dde := disj_of_validN_data_op_token <| validN_of_eqv CMRA.comm + (validN_op_right (validN_of_eqv CMRA.assoc.symm + (validN_of_eqv CMRA.comm (validN_of_eqv (CMRA.cmra_op_ne2.eqv .rfl ze) vaz)))) + simp only [CMRA.op, Heap.op, get?_merge, LawfulPartialMap.get?_singleton, + Option.merge_eq_none_iff, ite_eq_right_iff, reduceCtorEq, imp_false] at ddt dde ⊢ + grind + +@[rocq_alias dyn_reservation_map_update] +theorem update {k} {a b : A} (uab : a ~~> b) : + singleton (H := H) k a ~~> singleton k b := + Update.of_updateP <| updateP k a (.of_update uab) fun _ => congrArg (singleton k) + +end + +-- The dynamic reservation of a fresh infinite token set requires a finite map, so that its +-- domain can be avoided when picking the fresh set. +section + +variable [LawfulFiniteMap H Pos] + +/-- The domain of a finite map `m : H A`, viewed as a finite `CoPset`. -/ +def domCoPset (m : H A) : CoPset := FiniteMap.dom_set m + +theorem mem_domCoPset {m : H A} {i : Pos} : i ∈ domCoPset m ↔ get? m i ≠ none := + (LawfulFiniteMap.mem_dom_set (S := CoPset)).trans (Option.isSome_iff_ne_none (o := get? m i)) + +theorem domCoPset_finite {m : H A} : setFinite (domCoPset m) := ofList_finite + +variable [CMRA A] + +@[rocq_alias dyn_reservation_map_reserve] +theorem reserve (Q : DynReservationMap A H → Prop) + (HQ : ∀ e : CoPset, setInfinite e → Q (mkToken e)) : + (UCMRA.unit : DynReservationMap A H) ~~>: Q := by + intro n mz vo + have ⟨mf, Ef, hz, vmf, hinf, hdisj⟩ : + ∃ (mf : H A) (Ef : CoPset), (UCMRA.unit •? mz) ≡ mkData mf • mkToken Ef ∧ + ✓{n} mf ∧ setInfinite ((⊤ : CoPset) \ Ef) ∧ + ∀ i, get? mf i = none ∨ i ∉ Ef := by + match mz with + | none => + exact ⟨∅, ∅, ⟨show (∅ : H A) ≡ ∅ • ∅ from Algebra.MonoidOps.op_left_id.symm, + (pcore_op_left_L rfl).symm⟩, Heap.valid_empty.validN, empty_infinite, + fun i => .inl (get?_empty i)⟩ + | some z => + have vz : ✓{n} z := validN_of_eqv (unit_left_id (x := z)) vo + obtain ⟨mf, Ef, hze⟩ := split_validN vz + refine ⟨mf, Ef, (unit_left_id (x := z)).trans hze, ?_, ?_, ?_⟩ + · exact validN_data.mp (validN_op_left (validN_of_eqv hze vz)) + · exact infinite_data_op_token (validN_of_eqv hze vz) + · exact disj_of_validN_data_op_token (validN_of_eqv hze vz) + obtain ⟨E₁, E₂, hEunion, hEdisj, hE₁inf, hE₂inf⟩ := + CoPset.split_infinite ((⊤ : CoPset) \ (Ef ∪ domCoPset mf)) + (setInfinite_mono + (fun i hi => + have ⟨hiTEf, hiD⟩ := LawfulSet.mem_diff.mp hi + LawfulSet.mem_diff.mpr ⟨CoPset.mem_full, fun hmem => + (LawfulSet.mem_union.mp hmem).elim (LawfulSet.mem_diff.mp hiTEf).right hiD⟩) + (difference_infinite hinf domCoPset_finite)) + have hE₁Ef : E₁ ## Ef := fun i ⟨h₁, hEf⟩ => + (LawfulSet.mem_diff.mp (hEunion ▸ LawfulSet.mem_union.mpr (.inl h₁))).right + (LawfulSet.mem_union.mpr (.inl hEf)) + have hframe : mkToken E₁ •? mz ≡ mkToken E₁ • (mkData mf • mkToken Ef) := + (show mkToken E₁ •? mz ≡ mkToken E₁ • (UCMRA.unit •? mz) from + match mz with + | none => (unit_right_id (x := mkToken E₁)).symm + | some z => op_right_eqv (mkToken E₁) (unit_left_id (x := z)).symm).trans + (op_right_eqv (mkToken E₁) hz) + refine ⟨mkToken E₁, HQ E₁ hE₁inf, ?_⟩ + refine validN_of_eqv hframe.symm ?_ + have hrearrange : + mkToken E₁ • (mkData mf • mkToken Ef) ≡ mkData mf • (mkToken E₁ • mkToken Ef) := + CMRA.assoc.trans + ((op_left_eqv (mkToken Ef) (CMRA.comm (x := mkToken E₁) (y := mkData mf))).trans + CMRA.assoc.symm) + refine validN_of_eqv hrearrange.symm ?_ + refine validN_of_eqv (op_right_eqv (mkData mf) (token_union hE₁Ef)) ?_ + refine validN_data_op_token mf (E₁ ∪ Ef) (validN_data.mpr vmf) ?_ ?_ + · refine setInfinite_mono (fun i hi => ?_) hE₂inf + have hiX := hEunion ▸ LawfulSet.mem_union.mpr (.inr hi) + refine LawfulSet.mem_diff.mpr ⟨(LawfulSet.mem_diff.mp hiX).left, fun hmem => ?_⟩ + cases LawfulSet.mem_union.mp hmem with + | inl h₁ => exact hEdisj i ⟨h₁, hi⟩ + | inr hEf => exact (LawfulSet.mem_diff.mp hiX).right (LawfulSet.mem_union.mpr (.inl hEf)) + · intro i + by_cases hmem : i ∈ E₁ ∪ Ef + · refine .inl ?_ + cases LawfulSet.mem_union.mp hmem with + | inl h₁ => + have hiX := hEunion ▸ LawfulSet.mem_union.mpr (.inl h₁) + have hnd : i ∉ domCoPset mf := + fun hd => (LawfulSet.mem_diff.mp hiX).right (LawfulSet.mem_union.mpr (.inr hd)) + exact Decidable.not_not.mp (mt mem_domCoPset.mpr hnd) + | inr hEf => exact (hdisj i).elim id fun h => absurd hEf h + · exact .inr hmem + +@[rocq_alias dyn_reservation_map_reserve'] +theorem reserve' : + (UCMRA.unit : DynReservationMap A H) ~~>: + fun x => ∃ e : CoPset, setInfinite e ∧ x = mkToken e := + reserve _ fun e hinf => ⟨e, hinf, rfl⟩ + +end + +end DynReservationMap + +end CMRA diff --git a/Iris/Iris/Std/CoPset.lean b/Iris/Iris/Std/CoPset.lean index c860d2776..b2174cce6 100644 --- a/Iris/Iris/Std/CoPset.lean +++ b/Iris/Iris/Std/CoPset.lean @@ -555,6 +555,75 @@ def splitRight (X : CoPset) : CoPset := ⟨rightRaw X.tree, right_wf _⟩ def split (X : CoPset) : CoPset × CoPset := (splitLeft X, splitRight X) +theorem isFinite_node' (b : Bool) (l r : CoPsetRaw) : + CoPsetRaw.isFinite (CoPsetRaw.node' b l r) + = (CoPsetRaw.isFinite l && CoPsetRaw.isFinite r) := by + cases b <;> rcases l with ⟨⟨⟩⟩ | _ <;> rcases r with ⟨⟨⟩⟩ | _ <;> + simp [CoPsetRaw.node', CoPsetRaw.isFinite] + +theorem isFinite_leftRaw (t : CoPsetRaw) : + CoPsetRaw.isFinite (leftRaw t) = CoPsetRaw.isFinite t := by + induction t with + | leaf b => cases b <;> simp [leftRaw, CoPsetRaw.isFinite] + | node b l r IHl IHr => simp [leftRaw, isFinite_node', CoPsetRaw.isFinite, IHl, IHr] + +theorem isFinite_rightRaw (t : CoPsetRaw) : + CoPsetRaw.isFinite (rightRaw t) = CoPsetRaw.isFinite t := by + induction t with + | leaf b => cases b <;> simp [rightRaw, CoPsetRaw.isFinite] + | node b l r IHl IHr => simp [rightRaw, isFinite_node', CoPsetRaw.isFinite, IHl, IHr] + +theorem elemOf_leftRaw_imp (t : CoPsetRaw) (p : Pos) : + ElemOf p (leftRaw t) = true → ElemOf p t = true := by + induction t generalizing p with + | leaf b => cases b <;> cases p <;> simp [leftRaw, ElemOf] + | node b l r IHl IHr => + cases p with + | xH => simp only [leftRaw, elem_of_node, ElemOf]; exact id + | xO p' => simp only [leftRaw, elem_of_node, ElemOf]; exact IHl _ + | xI p' => simp only [leftRaw, elem_of_node, ElemOf]; exact IHr _ + +theorem elemOf_rightRaw_imp (t : CoPsetRaw) (p : Pos) : + ElemOf p (rightRaw t) = true → ElemOf p t = true := by + induction t generalizing p with + | leaf b => cases b <;> cases p <;> simp [rightRaw, ElemOf] + | node b l r IHl IHr => + cases p with + | xH => simp [rightRaw, elem_of_node, ElemOf] + | xO p' => simp only [rightRaw, elem_of_node, ElemOf]; exact IHl _ + | xI p' => simp only [rightRaw, elem_of_node, ElemOf]; exact IHr _ + +theorem elemOf_leftRaw_or_rightRaw (t : CoPsetRaw) (p : Pos) : + ElemOf p t = true → ElemOf p (leftRaw t) = true ∨ ElemOf p (rightRaw t) = true := by + induction t generalizing p with + | leaf b => cases b <;> cases p <;> simp [leftRaw, rightRaw, ElemOf] + | node b l r IHl IHr => + cases p with + | xH => simp only [leftRaw, rightRaw, elem_of_node, ElemOf]; exact .inl + | xO p' => simp only [leftRaw, rightRaw, elem_of_node, ElemOf]; exact IHl _ + | xI p' => simp only [leftRaw, rightRaw, elem_of_node, ElemOf]; exact IHr _ + +theorem not_elemOf_leftRaw_and_rightRaw (t : CoPsetRaw) (p : Pos) : + ¬(ElemOf p (leftRaw t) = true ∧ ElemOf p (rightRaw t) = true) := by + induction t generalizing p with + | leaf b => cases b <;> cases p <;> simp [leftRaw, rightRaw, ElemOf] + | node b l r IHl IHr => + cases p with + | xH => simp [leftRaw, rightRaw, elem_of_node, ElemOf] + | xO p' => + simp only [leftRaw, rightRaw, elem_of_node, ElemOf] + exact fun ⟨h, hr⟩ => IHl _ ⟨h, hr⟩ + | xI p' => + simp only [leftRaw, rightRaw, elem_of_node, ElemOf] + exact fun ⟨h, hr⟩ => IHr _ ⟨h, hr⟩ + +theorem splitLeft_union_splitRight (X : CoPset) : splitLeft X ∪ splitRight X = X := by + apply CoPset.ext + intro p + rw [in_union] + refine ⟨fun h => ?_, fun h => elemOf_leftRaw_or_rightRaw X.tree p h⟩ + exact h.elim (elemOf_leftRaw_imp X.tree p) (elemOf_rightRaw_imp X.tree p) + end CoPset section Instances @@ -653,6 +722,11 @@ theorem isFinite_setFinite {X : CoPset} : isFinite X ↔ LawfulSet.setFinite X : theorem not_isFinite_setInfinite {X : CoPset} : ¬isFinite X ↔ LawfulSet.setInfinite X := by rw [isFinite_setFinite, LawfulSet.not_finite_infinite] +theorem top_infinite : LawfulSet.setInfinite (⊤ : CoPset) := + not_isFinite_setInfinite.mp (by + simp only [isFinite, Iris.Std.Top.top, full, CoPsetRaw.isFinite, Bool.not_true, + Bool.false_eq_true, not_false_eq_true]) + theorem set_to_coPset_finite {S : Type _} [LawfulFiniteSet S Pos] (X : S) : isFinite (set_to_coPset X) := by simp only [set_to_coPset] @@ -662,4 +736,28 @@ theorem set_to_coPset_finite {S : Type _} [LawfulFiniteSet S Pos] (X : S) simp only [LawfulSet.ofList_cons, LawfulSet.insert_union, isFinite_setFinite] exact LawfulSet.union_finite LawfulSet.singleton_finite (isFinite_setFinite.mp IH) +theorem CoPset.splitLeft_disjoint_splitRight (X : CoPset) : + CoPset.splitLeft X ## CoPset.splitRight X := + fun p ⟨hl, hr⟩ => CoPset.not_elemOf_leftRaw_and_rightRaw X.tree p ⟨hl, hr⟩ + +theorem CoPset.splitLeft_infinite {X : CoPset} (h : LawfulSet.setInfinite X) : + LawfulSet.setInfinite (CoPset.splitLeft X) := + not_isFinite_setInfinite.mp fun hf => + (not_isFinite_setInfinite.mpr h) (by + simp only [isFinite, CoPset.splitLeft, CoPset.isFinite_leftRaw] at hf; exact hf) + +theorem CoPset.splitRight_infinite {X : CoPset} (h : LawfulSet.setInfinite X) : + LawfulSet.setInfinite (CoPset.splitRight X) := + not_isFinite_setInfinite.mp fun hf => + (not_isFinite_setInfinite.mpr h) (by + simp only [isFinite, CoPset.splitRight, CoPset.isFinite_rightRaw] at hf; exact hf) + +/-- Every infinite `X : CoPset` splits into two disjoint parts whose union is `X`, both of which +are again infinite. -/ +theorem CoPset.split_infinite (X : CoPset) (h : LawfulSet.setInfinite X) : + ∃ E₁ E₂ : CoPset, E₁ ∪ E₂ = X ∧ E₁ ## E₂ ∧ + LawfulSet.setInfinite E₁ ∧ LawfulSet.setInfinite E₂ := + ⟨CoPset.splitLeft X, CoPset.splitRight X, CoPset.splitLeft_union_splitRight X, + CoPset.splitLeft_disjoint_splitRight X, CoPset.splitLeft_infinite h, CoPset.splitRight_infinite h⟩ + end Set diff --git a/Iris/Iris/Std/GenSets.lean b/Iris/Iris/Std/GenSets.lean index 3c40aa10b..13fbc2d5f 100644 --- a/Iris/Iris/Std/GenSets.lean +++ b/Iris/Iris/Std/GenSets.lean @@ -767,6 +767,9 @@ def setFinite (X : S) : Prop := ∃ xs : List A, ∀ x ∈ X, x ∈ xs def setInfinite (X : S) : Prop := ∀ xs : List A, ∃ x ∈ X, x ∉ xs +theorem ofList_finite {xs : List A} : setFinite (ofList xs : S) := + ⟨xs, fun _ h => mem_ofList.mpr h⟩ + theorem not_finite_infinite {X : S} : ¬ setFinite X ↔ setInfinite X := by simp [setFinite, setInfinite] theorem not_infinite_finite {X : S} : ¬ setInfinite X ↔ setFinite X := by simp [setFinite, setInfinite] @@ -825,6 +828,11 @@ theorem difference_infinite {X Y : S} : simp only [mem_diff] grind +theorem setInfinite_mono {X Y : S} (H : X ⊆ Y) : setInfinite X → setInfinite Y := by + intro Hinf xs + obtain ⟨x, Hx, Hxs⟩ := Hinf xs + exact ⟨x, H x Hx, Hxs⟩ + theorem diff_not_finite_finite_ne_empty {X Y : S} (hX : setInfinite X) (hY : setFinite Y) : X \ Y ≠ ∅ := by intro Heq From a798153e4b146523c2dfce34f8676b4aedfe3b45 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Tue, 14 Jul 2026 11:21:27 +0200 Subject: [PATCH 2/3] Update --- Iris/Iris/Algebra/DynReservationMap.lean | 347 +++++++++++------------ Iris/Iris/Std/GenSets.lean | 4 +- 2 files changed, 163 insertions(+), 188 deletions(-) diff --git a/Iris/Iris/Algebra/DynReservationMap.lean b/Iris/Iris/Algebra/DynReservationMap.lean index 835e89a7c..fd947d019 100644 --- a/Iris/Iris/Algebra/DynReservationMap.lean +++ b/Iris/Iris/Algebra/DynReservationMap.lean @@ -34,12 +34,9 @@ structure DynReservationMap (A : Type) (H : Type → Type) where data : H A token : DisjointLeibnizSet CoPset -def DynReservationMap.mkData [LawfulPartialMap H Pos] (data : H A) : - DynReservationMap A H := .mk data ∅ - @[rocq_alias dyn_reservation_map_data] -def DynReservationMap.singleton [LawfulPartialMap H Pos] (k : Pos) (a : A) : - DynReservationMap A H := DynReservationMap.mkData {[k := a]} +def DynReservationMap.mkData [LawfulPartialMap H Pos] (k : Pos) (a : A) : + DynReservationMap A H := .mk {[k := a]} ∅ @[rocq_alias dyn_reservation_map_token] def DynReservationMap.mkToken [LawfulPartialMap H Pos] (e : CoPset) : @@ -58,42 +55,39 @@ variable [LawfulPartialMap H Pos] [OFE A] @[rocq_alias dyn_reservation_mapO] instance : OFE (DynReservationMap A H) where - Equiv x y := x.data ≡ y.data ∧ x.token ≡ y.token Dist n x y := x.data ≡{n}≡ y.data ∧ x.token ≡{n}≡ y.token dist_eqv := { refl _ := ⟨.rfl, rfl⟩, symm h := ⟨h.left.symm, h.right.symm⟩, trans h₁ h₂ := ⟨h₁.left.trans h₂.left, h₁.right.trans h₂.right⟩ } - equiv_dist := - ⟨fun h n => ⟨equiv_dist.mp h.left n, h.right⟩, - fun h => ⟨equiv_dist.mpr (h · |>.left), (h 0).right⟩⟩ + eq_dist {x y} := by + refine ⟨fun h _ => h ▸ ⟨.rfl, .rfl⟩, fun H => ?_⟩ + obtain ⟨xd, xt⟩ := x; obtain ⟨yd, yt⟩ := y + simp only [DynReservationMap.mk.injEq] + exact ⟨eq_dist.mpr fun n => (H n).1, eq_dist.mpr fun n => (H n).2⟩ dist_lt h lt := ⟨dist_lt h.left lt, dist_lt h.right lt⟩ @[rocq_alias dyn_reservation_map_ofe_discrete] instance instDiscreteDynReservationMap [Discrete A] : Discrete (DynReservationMap A H) where - discrete_0 h := ⟨discrete_0 h.left, discrete_0 h.right⟩ - -instance instNonExpansiveDynReservationMapData : - NonExpansive (DynReservationMap.mkData (H := H) (A := A)) where - ne _ _ _ h := ⟨h, rfl⟩ + discrete_0 h := fun n => ⟨(discrete_0 h.left) n, (discrete_0 h.right) n⟩ #rocq_ignore dyn_reservation_map_data_proper "Derivable using NonExpansive.eqv" @[rocq_alias dyn_reservation_map_data_ne] instance instNonExpansiveDynReservationMapSingleton : - NonExpansive (DynReservationMap.singleton (H := H) (A := A) k) where + NonExpansive (DynReservationMap.mkData (H := H) (A := A) k) where ne _ _ _ h := ⟨singleton_dist h k, rfl⟩ @[rocq_alias DynReservationMap_discrete] instance instDiscreteEDynReservationMapMk {a : H A} [DiscreteE a] : DiscreteE (DynReservationMap.mk a b) where - discrete := fun ⟨ha, hb⟩ => ⟨DiscreteE.discrete ha, DiscreteE.discrete hb⟩ + discrete := fun h n => ⟨(DiscreteE.discrete h.1) n, (DiscreteE.discrete h.2) n⟩ @[rocq_alias dyn_reservation_map_data_discrete] instance instDiscreteEDynReservationMapSingleton {a : A} [DiscreteE a] : - DiscreteE (DynReservationMap.singleton (H := H) k a) := - by unfold DynReservationMap.singleton DynReservationMap.mkData; infer_instance + DiscreteE (DynReservationMap.mkData (H := H) k a) := + by unfold DynReservationMap.mkData; infer_instance @[rocq_alias dyn_reservation_map_token_discrete] instance instDiscreteEDynReservationMapToken : @@ -210,10 +204,7 @@ theorem infinite_op_left {x y : DynReservationMap A H} (vt : ✓{n} (x.token • | .valid e₁, .valid e₂ => have hv : ✓{n} (DisjointLeibnizSet.valid e₁ • DisjointLeibnizSet.valid e₂) := ht ▸ hy ▸ vt - have hdisj : e₁ ## e₂ := by - by_cases h : e₁ ## e₂ - · exact h - · simp only [CMRA.op, h, ↓reduceIte] at hv; exact hv.elim + have hdisj : e₁ ## e₂ := valid_op_iff_disj.mp hv simp only [Infinite, ht] at ⊢ simp only [Infinite, op_token', ht, hy, CMRA.op, hdisj, ↓reduceIte] at inf exact setInfinite_mono @@ -225,7 +216,7 @@ theorem infinite_op_left {x y : DynReservationMap A H} (vt : ✓{n} (x.token • #rocq_ignore dyn_reservation_mapR "Derivable using UCMRA" @[rocq_alias dyn_reservation_mapUR] -instance : UCMRA (DynReservationMap A H) where +instance instUCMRADynReservationMap: UCMRA (DynReservationMap A H) where pcore := some ∘ core Valid := Valid ValidN := ValidN @@ -285,38 +276,37 @@ instance : UCMRA (DynReservationMap A H) where refine .inr fun HK => bb ?_ refine (mem_iff_of_validN_union (validN_token_of_validN v) i).mpr ?_ exact .inl HK - assoc := ⟨CMRA.assoc, CMRA.assoc⟩ - comm := ⟨CMRA.comm, CMRA.comm⟩ + assoc := fun n => ⟨CMRA.assoc n, CMRA.assoc n⟩ + comm := fun n => ⟨CMRA.comm n, CMRA.comm n⟩ pcore_op_left {x cx} h := by - refine ⟨?_, ?_⟩ - · simp [←Option.some_inj.mp h, op_data', core_data, core_op x.data] + refine fun n => ⟨?_, ?_⟩ + · simp only [←Option.some_inj.mp h, op_data', core_data] + exact (core_op x.data) n · simp [←Option.some_inj.mp h, op_token', core_token, core_op_L] pcore_idem {x cx} h := by - refine ⟨?_, ?_⟩ - · simp [←Option.some_inj.mp h, core_data, core_idem x.data] + refine fun n => ⟨?_, ?_⟩ + · simp only [←Option.some_inj.mp h, core_data] + exact (core_idem x.data) n · simp [←Option.some_inj.mp h, core_token, core_idem_L] pcore_op_mono {x cx} h y := by obtain ⟨z, hz⟩ := core_op_mono x.data y.data obtain ⟨w, hw⟩ := core_op_mono x.token y.token - refine ⟨mk z w, ?_, ?_⟩ - · simp [op_data', core_data, (Option.some_inj.mp h.symm), hz] - · simp only [core_token, op_token', (Option.some_inj.mp h.symm), leibniz] - exact hw + refine ⟨mk z w, fun n => ⟨?_, ?_⟩⟩ + · simp only [op_data', core_data, (Option.some_inj.mp h.symm)] + exact hz n + · simp only [core_token, op_token', (Option.some_inj.mp h.symm)] + exact hw n extend {n x y₁ y₂} v exy := by obtain ⟨z₁, z₂, xzz, zy₁, zy₂⟩ := CMRA.extend (validN_data_of_validN v) exy.left - refine ⟨mk z₁ y₁.token, mk z₂ y₂.token, ?_, ?_, ?_⟩ - · refine ⟨?_, ?_⟩ - · simp [op_data', xzz] - · simp only [op_token', leibniz] - exact exy.right - · exact ⟨zy₁, rfl⟩ - · exact ⟨zy₂, rfl⟩ + exact ⟨mk z₁ y₁.token, mk z₂ y₂.token, (fun m => ⟨xzz m, exy.right⟩), + ⟨zy₁, rfl⟩, ⟨zy₂, rfl⟩⟩ unit := mk ∅ ∅ unit_valid := valid_iff.mpr ⟨Heap.valid_empty, valid_set, show setInfinite ((⊤ : CoPset) \ ∅) by rw [diff_empty]; exact top_infinite, fun _ => .inr (mem_empty _)⟩ - unit_left_id {x} := ⟨by simp only [op, Algebra.MonoidOps.op_left_id], pcore_op_left' rfl⟩ - pcore_unit := ⟨Heap.core_empty, .rfl⟩ + unit_left_id {x} := fun n => ⟨(Algebra.MonoidOps.op_left_id : (∅ : H A) • x.data ≡ x.data) n, + (pcore_op_left' (OFE.Equiv.of_eq rfl)) n⟩ + pcore_unit := fun n => ⟨Heap.core_empty n, .rfl⟩ @[simp] theorem op_data (x y : DynReservationMap A H) : (x • y).data = x.data • y.data := rfl @@ -327,8 +317,9 @@ theorem op_token (x y : DynReservationMap A H) : (x • y).token = x.token • y @[rocq_alias dyn_reservation_map_included] theorem included {x y : DynReservationMap A H} : x ≼ y ↔ x.data ≼ y.data ∧ x.token ≼ y.token := by - refine ⟨fun ⟨z, hz⟩ => ⟨⟨z.data, hz.left⟩, ⟨z.token, hz.right⟩⟩, ?_⟩ - exact fun ⟨⟨z₁, hz₁⟩, ⟨z₂, hz₂⟩⟩ => ⟨mk z₁ z₂, hz₁, hz₂⟩ + refine ⟨fun ⟨z, hz⟩ => ⟨⟨z.data, fun n => (hz n).left⟩, + ⟨z.token, fun n => (hz n).right⟩⟩, ?_⟩ + exact fun ⟨⟨z₁, hz₁⟩, ⟨z₂, hz₂⟩⟩ => ⟨mk z₁ z₂, fun n => ⟨hz₁ n, hz₂ n⟩⟩ @[rocq_alias dyn_reservation_map_data_proj_validN] theorem data_proj_validN {n} {x : DynReservationMap A H} (h : ✓{n} x) : ✓{n} x.data := @@ -340,93 +331,68 @@ theorem token_proj_validN {n} {x : DynReservationMap A H} (h : ✓{n} x) : ✓{n @[rocq_alias dyn_reservation_map_cmra_discrete] instance [CMRA.Discrete A] : CMRA.Discrete (DynReservationMap A H) where - discrete_valid {_} v := by - refine valid_iff.mpr ⟨?_, ?_, ?_, ?_⟩ - · exact discrete_valid (validN_data_of_validN v) - · exact validN_token_of_validN v - · exact validN_infinite v - · exact validN_disj v + discrete_valid {_} v := valid_iff.mpr ⟨discrete_valid (validN_data_of_validN v), + validN_token_of_validN v, validN_infinite v, validN_disj v⟩ @[rocq_alias dyn_reservation_map_data_core_id] -instance instCoreIdSingleton {a : A} [CoreId a] : CoreId (singleton (H := H) k a) where +instance instCoreIdSingleton {a : A} [CoreId a] : CoreId (mkData (H := H) k a) where core_id := by - refine ⟨?_, rfl⟩ - simp [singleton, mkData, core_eqv_self (PartialMap.singleton k a)] - -theorem empty_infinite : setInfinite ((⊤ : CoPset) \ ∅) := by - rw [diff_empty]; exact top_infinite - -theorem split_valid {x : DynReservationMap A H} (vx : ✓ x) : - ∃ (d : H A) (t : CoPset), x ≡ mkData d • mkToken t := by - rcases x with ⟨xd, xt⟩ - match hh : xt with - | .error => - exact ((not_valid_invalid (S := CoPset)) (hh ▸ (valid_token_of_valid vx))).elim - | .valid t => - refine ⟨xd, t, ?_, ?_⟩ - · simp [mkData, mkToken, op_data, Algebra.MonoidOps.op_right_id.symm] - · simp only [mkData, mkToken, op_token, leibniz] - exact (pcore_op_left_L rfl).symm + refine OFE.some_eqv_some.mpr fun n => ⟨?_, .rfl⟩ + exact (core_eqv_self (PartialMap.singleton k a : H A)) n theorem split_validN {x : DynReservationMap A H} (vx : ✓{n} x) : - ∃ (d : H A) (t : CoPset), x ≡ mkData d • mkToken t := by + ∃ (d : H A) (t : CoPset), x ≡ mk d ∅ • mkToken t := by rcases x with ⟨xd, xt⟩ - have h := validN_token_of_validN vx - match hh : xt with - | .error => exact ((not_valid_invalid (S := CoPset)) (hh ▸ h)).elim - | .valid t => - refine ⟨xd, t, ?_, ?_⟩ - · simpa [mkData, mkToken, op_data] using Algebra.MonoidOps.op_right_id.symm - · exact (pcore_op_left' rfl).symm - -theorem valid_data {d : H A} : ✓ (mkData (H := H) d) ↔ ✓ d := - ⟨valid_data_of_valid, fun h => valid_iff.mpr ⟨h, valid_set, empty_infinite, + cases xt with + | error => exact (not_validN_invalid (S := CoPset) (validN_token_of_validN vx)).elim + | valid t => + refine ⟨xd, t, fun m => ⟨?_, ?_⟩⟩ + · exact (show xd ≡ xd • (∅ : H A) from Algebra.MonoidOps.op_right_id.symm) m + · exact ((pcore_op_left' (OFE.Equiv.of_eq rfl)).symm) m + +theorem valid_mkData_singleton : ✓ (mkData (H := H) k a) ↔ ✓ ({[k := a]} : H A) := + ⟨valid_data_of_valid, fun h => valid_iff.mpr ⟨h, valid_set, top_infinite, fun p => .inr (mem_empty p)⟩⟩ -theorem validN_data {d : H A} : ✓{n} (mkData (H := H) d) ↔ ✓{n} d := - ⟨validN_data_of_validN, fun h => validN_iff.mpr ⟨h, validN_set, empty_infinite, +theorem validN_mkData_singleton : ✓{n} (mkData (H := H) k a) ↔ ✓{n} ({[k := a]} : H A) := + ⟨validN_data_of_validN, fun h => validN_iff.mpr ⟨h, validN_set, top_infinite, fun p => .inr (mem_empty p)⟩⟩ @[rocq_alias dyn_reservation_map_data_valid] -theorem valid_singleton (k : Pos) (a : A) : ✓ (singleton (H := H) k a) ↔ ✓ a := - valid_data.trans Heap.singleton_valid_iff +theorem valid_mkData (k : Pos) (a : A) : ✓ (mkData (H := H) k a) ↔ ✓ a := + valid_mkData_singleton.trans Heap.singleton_valid_iff -theorem validN_singleton (k : Pos) (a : A) : ✓{n} (singleton (H := H) k a) ↔ ✓{n} a := - validN_data.trans Heap.singleton_validN_iff +theorem validN_mkData (k : Pos) (a : A) : ✓{n} (mkData (H := H) k a) ↔ ✓{n} a := + validN_mkData_singleton.trans Heap.singleton_validN_iff @[rocq_alias dyn_reservation_map_token_valid] theorem valid_token {e : CoPset} : - ✓ (mkToken (H := H) (A := A) e) ↔ setInfinite ((⊤ : CoPset) \ e) := by - refine ⟨fun h => valid_infinite h, fun hinf => - valid_iff.mpr ⟨Heap.valid_empty, valid_set, ?_, ?_⟩⟩ - · exact hinf - · exact fun i => .inl (get?_empty i) - -theorem data_op (a b : H A) : mkData (a • b) ≡ mkData a • mkData b := - ⟨.rfl, (pcore_op_right_L rfl).symm⟩ + ✓ (mkToken (H := H) (A := A) e) ↔ setInfinite ((⊤ : CoPset) \ e) := + ⟨valid_infinite, fun hinf => valid_iff.mpr + ⟨Heap.valid_empty, valid_set, hinf, fun i => .inl (get?_empty i)⟩⟩ @[rocq_alias dyn_reservation_map_data_op] -theorem singleton_op k (a b : A) : - singleton (H := H) k (a • b) ≡ singleton (H := H) k a • singleton k b := by - refine ((data_op _ _).symm.trans ?_).symm - exact NonExpansive.eqv (fun i => .of_eq (Heap.singleton_op_singleton i)) +theorem mkData_op k (a b : A) : + mkData (H := H) k (a • b) ≡ mkData k a • mkData k b := by + exact fun n => ⟨(fun i => Dist.of_eq (Heap.singleton_op_singleton i).symm), + Dist.of_eq (pcore_op_right_L rfl).symm⟩ @[rocq_alias dyn_reservation_map_data_mono] -theorem singleton_mono {k} {a b : A} (Hab : a ≼ b) : - singleton (H := H) k a ≼ singleton k b := +theorem mkData_mono {k} {a b : A} (Hab : a ≼ b) : + mkData (H := H) k a ≼ mkData k b := let ⟨z, hz⟩ := Hab - ⟨singleton k z, (NonExpansive.eqv hz).trans (singleton_op k a z)⟩ + ⟨mkData k z, (NonExpansive.eqv hz).trans (mkData_op k a z)⟩ set_option synthInstance.checkSynthOrder false in @[rocq_alias dyn_reservation_map_data_is_op] instance {ia ib₁ ib₂ : ProofMode.InOut} {a b₁ b₂ : A} [hv : IsOp ia a ib₁ b₁ ib₂ b₂] : - IsOp ia (singleton (H := H) k a) ib₁ (singleton k b₁) ib₂ (singleton k b₂) where - is_op := .trans (NonExpansive.eqv hv.is_op) (singleton_op k b₁ b₂) + IsOp ia (mkData (H := H) k a) ib₁ (mkData k b₁) ib₂ (mkData k b₂) where + is_op := .trans (NonExpansive.eqv hv.is_op) (mkData_op k b₁ b₂) @[rocq_alias dyn_reservation_map_token_union] theorem token_union {e₁ e₂} (he : e₁ ## e₂) : mkToken (H := H) (A := A) (e₁ ∪ e₂) ≡ mkToken e₁ • mkToken e₂ := by - refine ⟨fun i => ?_, ?_⟩ + refine fun n => ⟨fun i => ?_, ?_⟩ · simpa only [mkToken, get?_empty, op_data, Heap.get?_op] using .rfl · simp [mkToken, CMRA.op, he] @@ -452,60 +418,66 @@ theorem valid_token_op {e₁ e₂} : exact hinf · exact (Equiv.valid (token_union hdisj)).mp (valid_token.mpr hinf) -theorem disj_of_validN_data_op_token {a : H A} {b : CoPset} (h : ✓{n} mkData a • mkToken b) - (i : Pos) : get? a i = none ∨ i ∉ b := by +theorem disj_of_validN_data_op_token {a : H A} {b : CoPset} + (h : ✓{n} mk a ∅ • mkToken b) (i : Pos) : get? a i = none ∨ i ∉ b := by cases validN_disj h i with | inl h => - simp only [mkData, mkToken, op_data, Heap.get?_op, get?_empty] at h + simp only [mkToken, op_data, Heap.get?_op, get?_empty] at h exact .inl <| Option.eq_none_of_op_eq_none_left h | inr h' => - simp only [mkData, mkToken, op_token] at h' + simp only [mkToken, op_token] at h' rw [mem_iff_of_valid_union, not_or] at h' - · exact .inr <| h'.right - · exact valid_of_eqv (pcore_op_left' rfl).symm valid_set + · exact .inr h'.right + · exact valid_of_eqv (pcore_op_left' (OFE.Equiv.of_eq rfl)).symm valid_set -theorem infinite_data_op_token {a : H A} {b : CoPset} (h : ✓{n} mkData a • mkToken b) : +theorem infinite_data_op_token {a : H A} {b : CoPset} (h : ✓{n} mk a ∅ • mkToken b) : setInfinite ((⊤ : CoPset) \ b) := by - have hinf := validN_infinite h - have eo : (mkData a • mkToken b).token = .valid b := pcore_op_left_L rfl - rw [Infinite, eo] at hinf - exact hinf + simpa only [Infinite, show (mk a ∅ • mkToken b).token = .valid b from + pcore_op_left_L rfl] using validN_infinite h -theorem validN_data_op_token {n : Nat} (a : H A) (b : CoPset) (vd : ✓{n} mkData a) +theorem validN_data_op_token {n : Nat} {a : H A} {b : CoPset} (vd : ✓{n} a) (inf : setInfinite ((⊤ : CoPset) \ b)) (disj : ∀ i, get? a i = none ∨ i ∉ b) : - ✓{n} mkData a • mkToken b := by - have abdp : (mkData a • mkToken b).data ≡ a := + ✓{n} mk a ∅ • mkToken b := by + have abdp : (mk a ∅ • mkToken b).data ≡ a := show a • ∅ ≡ a from Algebra.MonoidOps.op_right_id have eo : ∅ • DisjointLeibnizSet.valid b = .valid b := pcore_op_left_L rfl refine validN_iff.mpr ⟨?_, ?_, ?_, fun i => ?_⟩ - · exact validN_of_eqv abdp.symm ((validN_data).mp vd) - · simp [mkData, mkToken, eo, validN_set] - · rw [Infinite, show (mkData a • mkToken b).token = .valid b from pcore_op_left_L rfl] + · exact validN_of_eqv abdp.symm vd + · simp [mkToken, eo, validN_set] + · rw [Infinite, show (mk a ∅ • mkToken b).token = .valid b from pcore_op_left_L rfl] exact inf - · simp [mkData, mkToken, op_data, Heap.get?_op, get?_empty, op_token] + · simp [mkToken, op_data, Heap.get?_op, get?_empty, op_token] cases disj i with - | inl h => simpa [h] using .inl <| rfl + | inl h => simpa [h] using .inl rfl | inr h => simpa [eo] using .inr h -theorem valid_op?_of_valid_singleton_op {a : A} {x : H A} (h : ✓{n} (singleton k a • mkData x)) : - ✓{n} a •? get? x k := by +theorem valid_op?_of_valid_mkData_op_data {a : A} {x : H A} + (h : ✓{n} (mkData k a • mk x ∅)) : ✓{n} a •? get? x k := by match h' : get? x k with - | none => simpa [op?] using (validN_singleton (H := H) k a).mp (validN_op_left h) + | none => simpa [op?] using (validN_mkData (H := H) k a).mp (validN_op_left h) | some g => simp only [op?] have vdp := (validN_data_of_validN h) k - simp only [CMRA.op, singleton, mkData, op_data', Heap.op, get?_merge, Option.merge, + simp only [CMRA.op, mkData, op_data', Heap.op, get?_merge, Option.merge, LawfulPartialMap.get?_singleton, ↓reduceIte, h'] at vdp exact vdp -theorem valid_singleton_op_of_valid_op? {a : A} {x : H A} (vx : ✓{n} x) (h : ✓{n} a •? get? x k) : - ✓{n} singleton k a • mkData x := by - refine validN_of_eqv (data_op (PartialMap.singleton k a) x) ?_ - refine (validN_data).mpr fun i => ?_ - rw [Heap.get?_op] - by_cases ki : k = i - · simp only [← ki, LawfulPartialMap.get?_singleton, ↓reduceIte, Option.some_op_opM]; exact h - · simp only [LawfulPartialMap.get?_singleton, ki, ↓reduceIte]; exact Heap.validN_get? vx +theorem valid_mkData_op_data_of_valid_op? {a : A} {x : H A} (vx : ✓{n} x) + (h : ✓{n} a •? get? x k) : ✓{n} mkData k a • mk x ∅ := by + have htok : (mkData k a • mk x ∅).token = .valid (∅ : CoPset) := pcore_op_left_L rfl + refine validN_iff.mpr ⟨?_, ?_, ?_, ?_⟩ + · show ✓{n} ({[k := a]} : H A) • x + intro i + rw [Heap.get?_op] + by_cases ki : k = i + · simp only [← ki, LawfulPartialMap.get?_singleton, ↓reduceIte, Option.some_op_opM] + exact h + · simp only [LawfulPartialMap.get?_singleton, ki, ↓reduceIte] + exact Heap.validN_get? vx + · exact htok ▸ validN_set + · rw [Infinite, htok] + exact top_infinite + · exact fun i => .inr (htok.symm ▸ mem_empty i) theorem validN_token_op_iff_disj {e₁ e₂} : ✓{n} (mkToken (H := H) (A := A) e₁ • mkToken e₂) ↔ @@ -523,60 +495,62 @@ theorem validN_token_op_iff_disj {e₁ e₂} : @[rocq_alias dyn_reservation_map_alloc] theorem alloc {e k} {a : A} (hke : k ∈ e) (va : ✓ a) : - mkToken (H := H) e ~~> singleton k a := by + mkToken (H := H) e ~~> mkData k a := by intro n mz vo match mz with - | none => exact Valid.validN <| (valid_singleton k a).mpr va + | none => exact Valid.validN <| (valid_mkData k a).mpr va | some z => have ⟨d, t, ze⟩ := split_validN (validN_op_right vo) - have vedt : ✓{n} mkToken e • (mkData d • mkToken t) := validN_of_eqv (op_right_eqv _ ze) vo - have disj : ∀ (i : Pos), get? d i = none ∨ ¬i ∈ e := - disj_of_validN_data_op_token (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt))) - have inf : setInfinite ((⊤ : CoPset) \ t) := - infinite_data_op_token (validN_of_eqv ze (validN_op_right vo)) + have vdt := validN_of_eqv ze (validN_op_right vo) + have vedt : ✓{n} mkToken e • (mk d ∅ • mkToken t) := + validN_of_eqv (op_right_eqv _ ze) vo + have disj : ∀ i : Pos, get? d i = none ∨ i ∉ e := + disj_of_validN_data_op_token + (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt))) refine validN_of_eqv (op_right_eqv _ ze.symm) ?_ refine validN_of_eqv CMRA.assoc.symm ?_ - refine validN_of_eqv (op_left_eqv (mkToken t) (data_op _ _)) ?_ - refine validN_data_op_token (PartialMap.singleton k a • d) t ?_ inf ?_ - · refine validN_of_eqv (data_op _ _).symm ?_ - apply valid_singleton_op_of_valid_op? - · exact validN_data.mp - (validN_op_left (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt)))) - · exact (disj k).elim (fun h => h ▸ Valid.validN va) (absurd hke) + refine validN_of_eqv (op_left_eqv (mkToken t) + (show mk ({[k := a]} • d) ∅ ≡ mkData k a • mk d ∅ from + fun n => ⟨.rfl, Dist.of_eq (pcore_op_right_L rfl).symm⟩)) ?_ + refine validN_data_op_token ?_ (infinite_data_op_token vdt) ?_ + · have vd : ✓{n} d := validN_data_of_validN + (validN_op_left (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt)))) + have vk : ✓{n} a •? get? d k := + (disj k).elim (fun h => h ▸ Valid.validN va) (absurd hke) + exact validN_data_of_validN (valid_mkData_op_data_of_valid_op? vd vk) · simp only [CMRA.op, Heap.op, get?_merge, LawfulPartialMap.get?_singleton, Option.merge_eq_none_iff, ite_eq_right_iff, reduceCtorEq, imp_false] intro i - grind [disj_of_validN_data_op_token (validN_of_eqv ze (validN_op_right vo)), + grind [disj_of_validN_data_op_token vdt, (validN_token_op_iff_disj.mp (validN_op_right (validN_of_eqv assoc.symm (validN_of_eqv comm vedt)))).left i] @[rocq_alias dyn_reservation_map_updateP] theorem updateP {P} {Q : DynReservationMap A H → Prop} k a (ap : a ~~>: P) - (apq : ∀ a', P a' → Q (singleton k a')) : singleton k a ~~>: Q := by + (apq : ∀ a', P a' → Q (mkData k a')) : mkData k a ~~>: Q := by intro n mz vaz match mz with | none => - obtain ⟨y, py, vy⟩ := ap n none ((validN_singleton k a).mp vaz) - exact ⟨_, (apq y py), (validN_singleton k y).mpr vy⟩ + obtain ⟨y, py, vy⟩ := ap n none ((validN_mkData k a).mp vaz) + exact ⟨_, apq y py, (validN_mkData k y).mpr vy⟩ | some z => obtain ⟨d, t, ze⟩ := split_validN (validN_op_right vaz) + have vdt := validN_of_eqv ze (validN_op_right vaz) obtain ⟨y, py, vy⟩ := ap n (get? d k) - (valid_op?_of_valid_singleton_op + (valid_op?_of_valid_mkData_op_data (validN_op_left (validN_of_eqv CMRA.assoc - (validN_of_eqv (op_right_eqv (singleton k a) ze) vaz)))) - refine ⟨singleton k y, apq y py, ?_⟩ + (validN_of_eqv (op_right_eqv (mkData k a) ze) vaz)))) + refine ⟨mkData k y, apq y py, ?_⟩ simp only [CMRA.op?] at vaz ⊢ - have inf : setInfinite ((⊤ : CoPset) \ t) := - infinite_data_op_token (validN_of_eqv ze (validN_op_right vaz)) - refine validN_of_eqv (op_right_eqv (singleton k y) ze).symm ?_ + refine validN_of_eqv (op_right_eqv (mkData k y) ze).symm ?_ refine validN_of_eqv CMRA.assoc.symm ?_ - refine validN_of_eqv (op_left_eqv (mkToken t) (data_op _ _)) ?_ - refine validN_data_op_token _ _ ?_ inf ?_ - · refine validN_of_eqv (data_op _ _).symm ?_ - refine valid_singleton_op_of_valid_op? ?_ vy - refine validN_data.mp ?_ - exact validN_op_left <| validN_of_eqv ze (validN_op_right vaz) - · have ddt := disj_of_validN_data_op_token (validN_of_eqv ze (validN_op_right vaz)) + refine validN_of_eqv (op_left_eqv (mkToken t) + (show mk ({[k := y]} • d) ∅ ≡ mkData k y • mk d ∅ from + fun n => ⟨.rfl, Dist.of_eq (pcore_op_right_L rfl).symm⟩)) ?_ + refine validN_data_op_token ?_ (infinite_data_op_token vdt) ?_ + · exact validN_data_of_validN <| valid_mkData_op_data_of_valid_op? + (validN_data_of_validN (validN_op_left vdt)) vy + · have ddt := disj_of_validN_data_op_token vdt have dde := disj_of_validN_data_op_token <| validN_of_eqv CMRA.comm (validN_op_right (validN_of_eqv CMRA.assoc.symm (validN_of_eqv CMRA.comm (validN_of_eqv (CMRA.cmra_op_ne2.eqv .rfl ze) vaz)))) @@ -586,13 +560,11 @@ theorem updateP {P} {Q : DynReservationMap A H → Prop} k a (ap : a ~~>: P) @[rocq_alias dyn_reservation_map_update] theorem update {k} {a b : A} (uab : a ~~> b) : - singleton (H := H) k a ~~> singleton k b := - Update.of_updateP <| updateP k a (.of_update uab) fun _ => congrArg (singleton k) + mkData (H := H) k a ~~> mkData k b := + Update.of_updateP <| updateP k a (.of_update uab) fun _ => congrArg (mkData k) end --- The dynamic reservation of a fresh infinite token set requires a finite map, so that its --- domain can be avoided when picking the fresh set. section variable [LawfulFiniteMap H Pos] @@ -603,8 +575,6 @@ def domCoPset (m : H A) : CoPset := FiniteMap.dom_set m theorem mem_domCoPset {m : H A} {i : Pos} : i ∈ domCoPset m ↔ get? m i ≠ none := (LawfulFiniteMap.mem_dom_set (S := CoPset)).trans (Option.isSome_iff_ne_none (o := get? m i)) -theorem domCoPset_finite {m : H A} : setFinite (domCoPset m) := ofList_finite - variable [CMRA A] @[rocq_alias dyn_reservation_map_reserve] @@ -613,21 +583,23 @@ theorem reserve (Q : DynReservationMap A H → Prop) (UCMRA.unit : DynReservationMap A H) ~~>: Q := by intro n mz vo have ⟨mf, Ef, hz, vmf, hinf, hdisj⟩ : - ∃ (mf : H A) (Ef : CoPset), (UCMRA.unit •? mz) ≡ mkData mf • mkToken Ef ∧ + ∃ (mf : H A) (Ef : CoPset), (UCMRA.unit •? mz) ≡ mk mf ∅ • mkToken Ef ∧ ✓{n} mf ∧ setInfinite ((⊤ : CoPset) \ Ef) ∧ ∀ i, get? mf i = none ∨ i ∉ Ef := by match mz with | none => - exact ⟨∅, ∅, ⟨show (∅ : H A) ≡ ∅ • ∅ from Algebra.MonoidOps.op_left_id.symm, - (pcore_op_left_L rfl).symm⟩, Heap.valid_empty.validN, empty_infinite, + exact ⟨∅, ∅, (fun n => + ⟨(show (∅ : H A) ≡ ∅ • ∅ from Algebra.MonoidOps.op_left_id.symm) n, + Dist.of_eq (pcore_op_left_L rfl).symm⟩), Heap.valid_empty.validN, top_infinite, fun i => .inl (get?_empty i)⟩ | some z => have vz : ✓{n} z := validN_of_eqv (unit_left_id (x := z)) vo obtain ⟨mf, Ef, hze⟩ := split_validN vz + have vze := validN_of_eqv hze vz refine ⟨mf, Ef, (unit_left_id (x := z)).trans hze, ?_, ?_, ?_⟩ - · exact validN_data.mp (validN_op_left (validN_of_eqv hze vz)) - · exact infinite_data_op_token (validN_of_eqv hze vz) - · exact disj_of_validN_data_op_token (validN_of_eqv hze vz) + · exact validN_data_of_validN (validN_op_left vze) + · exact infinite_data_op_token vze + · exact disj_of_validN_data_op_token vze obtain ⟨E₁, E₂, hEunion, hEdisj, hE₁inf, hE₂inf⟩ := CoPset.split_infinite ((⊤ : CoPset) \ (Ef ∪ domCoPset mf)) (setInfinite_mono @@ -635,12 +607,14 @@ theorem reserve (Q : DynReservationMap A H → Prop) have ⟨hiTEf, hiD⟩ := LawfulSet.mem_diff.mp hi LawfulSet.mem_diff.mpr ⟨CoPset.mem_full, fun hmem => (LawfulSet.mem_union.mp hmem).elim (LawfulSet.mem_diff.mp hiTEf).right hiD⟩) - (difference_infinite hinf domCoPset_finite)) + (difference_infinite hinf ofList_finite)) have hE₁Ef : E₁ ## Ef := fun i ⟨h₁, hEf⟩ => (LawfulSet.mem_diff.mp (hEunion ▸ LawfulSet.mem_union.mpr (.inl h₁))).right (LawfulSet.mem_union.mpr (.inl hEf)) - have hframe : mkToken E₁ •? mz ≡ mkToken E₁ • (mkData mf • mkToken Ef) := - (show mkToken E₁ •? mz ≡ mkToken E₁ • (UCMRA.unit •? mz) from + have hframe : (mkToken (H := H) (A := A) E₁) •? mz ≡ + mkToken E₁ • ((mk mf ∅ : DynReservationMap A H) • mkToken Ef) := + (show (mkToken (H := H) (A := A) E₁) •? mz ≡ + mkToken E₁ • (UCMRA.unit •? mz) from match mz with | none => (unit_right_id (x := mkToken E₁)).symm | some z => op_right_eqv (mkToken E₁) (unit_left_id (x := z)).symm).trans @@ -648,13 +622,15 @@ theorem reserve (Q : DynReservationMap A H → Prop) refine ⟨mkToken E₁, HQ E₁ hE₁inf, ?_⟩ refine validN_of_eqv hframe.symm ?_ have hrearrange : - mkToken E₁ • (mkData mf • mkToken Ef) ≡ mkData mf • (mkToken E₁ • mkToken Ef) := + (mkToken (H := H) (A := A) E₁) • ((mk mf ∅ : DynReservationMap A H) • mkToken Ef) ≡ + (mk mf ∅ : DynReservationMap A H) • (mkToken E₁ • mkToken Ef) := CMRA.assoc.trans - ((op_left_eqv (mkToken Ef) (CMRA.comm (x := mkToken E₁) (y := mkData mf))).trans + ((op_left_eqv (mkToken Ef) (CMRA.comm (x := mkToken E₁) (y := mk mf ∅))).trans CMRA.assoc.symm) refine validN_of_eqv hrearrange.symm ?_ - refine validN_of_eqv (op_right_eqv (mkData mf) (token_union hE₁Ef)) ?_ - refine validN_data_op_token mf (E₁ ∪ Ef) (validN_data.mpr vmf) ?_ ?_ + refine validN_of_eqv + (op_right_eqv (mk mf ∅ : DynReservationMap A H) (token_union hE₁Ef)) ?_ + refine validN_data_op_token vmf ?_ ?_ · refine setInfinite_mono (fun i hi => ?_) hE₂inf have hiX := hEunion ▸ LawfulSet.mem_union.mpr (.inr hi) refine LawfulSet.mem_diff.mpr ⟨(LawfulSet.mem_diff.mp hiX).left, fun hmem => ?_⟩ @@ -675,8 +651,7 @@ theorem reserve (Q : DynReservationMap A H → Prop) @[rocq_alias dyn_reservation_map_reserve'] theorem reserve' : - (UCMRA.unit : DynReservationMap A H) ~~>: - fun x => ∃ e : CoPset, setInfinite e ∧ x = mkToken e := + (UCMRA.unit : DynReservationMap A H) ~~>: fun x => ∃ e : CoPset, setInfinite e ∧ x = mkToken e := reserve _ fun e hinf => ⟨e, hinf, rfl⟩ end diff --git a/Iris/Iris/Std/GenSets.lean b/Iris/Iris/Std/GenSets.lean index 13fbc2d5f..67a2a0b3e 100644 --- a/Iris/Iris/Std/GenSets.lean +++ b/Iris/Iris/Std/GenSets.lean @@ -828,8 +828,8 @@ theorem difference_infinite {X Y : S} : simp only [mem_diff] grind -theorem setInfinite_mono {X Y : S} (H : X ⊆ Y) : setInfinite X → setInfinite Y := by - intro Hinf xs +theorem setInfinite_mono {X Y : S} (H : X ⊆ Y) (Hinf : setInfinite X) : setInfinite Y := by + intro xs obtain ⟨x, Hx, Hxs⟩ := Hinf xs exact ⟨x, H x Hx, Hxs⟩ From 59f1c0b05f9a83b2688e8967572a994a8189f7a9 Mon Sep 17 00:00:00 2001 From: Zongyuan Liu Date: Tue, 14 Jul 2026 13:19:43 +0200 Subject: [PATCH 3/3] Clean up --- Iris/Iris/Algebra/DynReservationMap.lean | 77 +++++++++++------------- 1 file changed, 34 insertions(+), 43 deletions(-) diff --git a/Iris/Iris/Algebra/DynReservationMap.lean b/Iris/Iris/Algebra/DynReservationMap.lean index fd947d019..f15aeb682 100644 --- a/Iris/Iris/Algebra/DynReservationMap.lean +++ b/Iris/Iris/Algebra/DynReservationMap.lean @@ -231,10 +231,8 @@ instance instUCMRADynReservationMap: UCMRA (DynReservationMap A H) where refine validN_iff.mpr ⟨?_, ?_, ?_, fun i => ?_⟩ · exact (Dist.validN h.left).mp (validN_data_of_validN v) · exact (Dist.validN h.right).mp (validN_token_of_validN v) - · have hinf := validN_infinite v - simp only [Infinite] at hinf ⊢ - rw [← h.right] - exact hinf + · rw [Infinite, ← h.right] + exact validN_infinite v · cases (validN_disj v) i with | inl gn => refine .inl <| ?_ @@ -284,10 +282,10 @@ instance instUCMRADynReservationMap: UCMRA (DynReservationMap A H) where exact (core_op x.data) n · simp [←Option.some_inj.mp h, op_token', core_token, core_op_L] pcore_idem {x cx} h := by - refine fun n => ⟨?_, ?_⟩ - · simp only [←Option.some_inj.mp h, core_data] - exact (core_idem x.data) n - · simp [←Option.some_inj.mp h, core_token, core_idem_L] + cases Option.some_inj.mp h.symm + rcases x with ⟨xd, xt⟩ + apply OFE.Equiv.of_eq + grind only [core, OFE.Equiv.to_eq, core_idem] pcore_op_mono {x cx} h y := by obtain ⟨z, hz⟩ := core_op_mono x.data y.data obtain ⟨w, hw⟩ := core_op_mono x.token y.token @@ -336,9 +334,8 @@ instance [CMRA.Discrete A] : CMRA.Discrete (DynReservationMap A H) where @[rocq_alias dyn_reservation_map_data_core_id] instance instCoreIdSingleton {a : A} [CoreId a] : CoreId (mkData (H := H) k a) where - core_id := by - refine OFE.some_eqv_some.mpr fun n => ⟨?_, .rfl⟩ - exact (core_eqv_self (PartialMap.singleton k a : H A)) n + core_id := OFE.Equiv.of_eq <| congrArg some <| congrArg (mk (token := ∅)) + (core_eqv_self (PartialMap.singleton k a : H A)).to_eq theorem split_validN {x : DynReservationMap A H} (vx : ✓{n} x) : ∃ (d : H A) (t : CoPset), x ≡ mk d ∅ • mkToken t := by @@ -373,8 +370,8 @@ theorem valid_token {e : CoPset} : @[rocq_alias dyn_reservation_map_data_op] theorem mkData_op k (a b : A) : - mkData (H := H) k (a • b) ≡ mkData k a • mkData k b := by - exact fun n => ⟨(fun i => Dist.of_eq (Heap.singleton_op_singleton i).symm), + mkData (H := H) k (a • b) ≡ mkData k a • mkData k b := + fun _ => ⟨(fun i => Dist.of_eq (Heap.singleton_op_singleton i).symm), Dist.of_eq (pcore_op_right_L rfl).symm⟩ @[rocq_alias dyn_reservation_map_data_mono] @@ -442,7 +439,7 @@ theorem validN_data_op_token {n : Nat} {a : H A} {b : CoPset} (vd : ✓{n} a) show a • ∅ ≡ a from Algebra.MonoidOps.op_right_id have eo : ∅ • DisjointLeibnizSet.valid b = .valid b := pcore_op_left_L rfl refine validN_iff.mpr ⟨?_, ?_, ?_, fun i => ?_⟩ - · exact validN_of_eqv abdp.symm vd + · exact abdp.symm.to_eq ▸ vd · simp [mkToken, eo, validN_set] · rw [Infinite, show (mk a ∅ • mkToken b).token = .valid b from pcore_op_left_L rfl] exact inf @@ -457,10 +454,9 @@ theorem valid_op?_of_valid_mkData_op_data {a : A} {x : H A} | none => simpa [op?] using (validN_mkData (H := H) k a).mp (validN_op_left h) | some g => simp only [op?] - have vdp := (validN_data_of_validN h) k - simp only [CMRA.op, mkData, op_data', Heap.op, get?_merge, Option.merge, - LawfulPartialMap.get?_singleton, ↓reduceIte, h'] at vdp - exact vdp + apply Option.some_validN.mp + simpa only [CMRA.op, mkData, op_data', Heap.op, get?_merge, Option.merge, + LawfulPartialMap.get?_singleton, ↓reduceIte, h'] using (validN_data_of_validN h) k theorem valid_mkData_op_data_of_valid_op? {a : A} {x : H A} (vx : ✓{n} x) (h : ✓{n} a •? get? x k) : ✓{n} mkData k a • mk x ∅ := by @@ -501,23 +497,22 @@ theorem alloc {e k} {a : A} (hke : k ∈ e) (va : ✓ a) : | none => exact Valid.validN <| (valid_mkData k a).mpr va | some z => have ⟨d, t, ze⟩ := split_validN (validN_op_right vo) - have vdt := validN_of_eqv ze (validN_op_right vo) + have vdt := ze.to_eq ▸ validN_op_right vo have vedt : ✓{n} mkToken e • (mk d ∅ • mkToken t) := - validN_of_eqv (op_right_eqv _ ze) vo + (op_right_eqv _ ze).to_eq ▸ vo have disj : ∀ i : Pos, get? d i = none ∨ i ∉ e := disj_of_validN_data_op_token (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt))) - refine validN_of_eqv (op_right_eqv _ ze.symm) ?_ - refine validN_of_eqv CMRA.assoc.symm ?_ - refine validN_of_eqv (op_left_eqv (mkToken t) + change ✓{n} mkData k a • z + rw [← (op_right_eqv _ ze.symm).to_eq, ← CMRA.assoc.symm.to_eq, + ← (op_left_eqv (mkToken t) (show mk ({[k := a]} • d) ∅ ≡ mkData k a • mk d ∅ from - fun n => ⟨.rfl, Dist.of_eq (pcore_op_right_L rfl).symm⟩)) ?_ + fun n => ⟨.rfl, Dist.of_eq (pcore_op_right_L rfl).symm⟩)).to_eq] refine validN_data_op_token ?_ (infinite_data_op_token vdt) ?_ - · have vd : ✓{n} d := validN_data_of_validN - (validN_op_left (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt)))) - have vk : ✓{n} a •? get? d k := - (disj k).elim (fun h => h ▸ Valid.validN va) (absurd hke) - exact validN_data_of_validN (valid_mkData_op_data_of_valid_op? vd vk) + · refine validN_data_of_validN <| valid_mkData_op_data_of_valid_op? ?_ ?_ + · exact validN_data_of_validN + (validN_op_left (validN_of_eqv comm (validN_op_left (validN_of_eqv assoc vedt)))) + · exact (disj k).elim (fun h => h ▸ Valid.validN va) (absurd hke) · simp only [CMRA.op, Heap.op, get?_merge, LawfulPartialMap.get?_singleton, Option.merge_eq_none_iff, ite_eq_right_iff, reduceCtorEq, imp_false] intro i @@ -535,18 +530,17 @@ theorem updateP {P} {Q : DynReservationMap A H → Prop} k a (ap : a ~~>: P) exact ⟨_, apq y py, (validN_mkData k y).mpr vy⟩ | some z => obtain ⟨d, t, ze⟩ := split_validN (validN_op_right vaz) - have vdt := validN_of_eqv ze (validN_op_right vaz) + have vdt := ze.to_eq ▸ validN_op_right vaz obtain ⟨y, py, vy⟩ := ap n (get? d k) (valid_op?_of_valid_mkData_op_data (validN_op_left (validN_of_eqv CMRA.assoc (validN_of_eqv (op_right_eqv (mkData k a) ze) vaz)))) refine ⟨mkData k y, apq y py, ?_⟩ simp only [CMRA.op?] at vaz ⊢ - refine validN_of_eqv (op_right_eqv (mkData k y) ze).symm ?_ - refine validN_of_eqv CMRA.assoc.symm ?_ - refine validN_of_eqv (op_left_eqv (mkToken t) + rw [← (op_right_eqv (mkData k y) ze).symm.to_eq, ← CMRA.assoc.symm.to_eq, + ← (op_left_eqv (mkToken t) (show mk ({[k := y]} • d) ∅ ≡ mkData k y • mk d ∅ from - fun n => ⟨.rfl, Dist.of_eq (pcore_op_right_L rfl).symm⟩)) ?_ + fun n => ⟨.rfl, Dist.of_eq (pcore_op_right_L rfl).symm⟩)).to_eq] refine validN_data_op_token ?_ (infinite_data_op_token vdt) ?_ · exact validN_data_of_validN <| valid_mkData_op_data_of_valid_op? (validN_data_of_validN (validN_op_left vdt)) vy @@ -593,9 +587,9 @@ theorem reserve (Q : DynReservationMap A H → Prop) Dist.of_eq (pcore_op_left_L rfl).symm⟩), Heap.valid_empty.validN, top_infinite, fun i => .inl (get?_empty i)⟩ | some z => - have vz : ✓{n} z := validN_of_eqv (unit_left_id (x := z)) vo + have vz : ✓{n} z := (unit_left_id (x := z)).to_eq ▸ vo obtain ⟨mf, Ef, hze⟩ := split_validN vz - have vze := validN_of_eqv hze vz + have vze := hze.to_eq ▸ vz refine ⟨mf, Ef, (unit_left_id (x := z)).trans hze, ?_, ?_, ?_⟩ · exact validN_data_of_validN (validN_op_left vze) · exact infinite_data_op_token vze @@ -620,16 +614,14 @@ theorem reserve (Q : DynReservationMap A H → Prop) | some z => op_right_eqv (mkToken E₁) (unit_left_id (x := z)).symm).trans (op_right_eqv (mkToken E₁) hz) refine ⟨mkToken E₁, HQ E₁ hE₁inf, ?_⟩ - refine validN_of_eqv hframe.symm ?_ have hrearrange : (mkToken (H := H) (A := A) E₁) • ((mk mf ∅ : DynReservationMap A H) • mkToken Ef) ≡ (mk mf ∅ : DynReservationMap A H) • (mkToken E₁ • mkToken Ef) := CMRA.assoc.trans ((op_left_eqv (mkToken Ef) (CMRA.comm (x := mkToken E₁) (y := mk mf ∅))).trans CMRA.assoc.symm) - refine validN_of_eqv hrearrange.symm ?_ - refine validN_of_eqv - (op_right_eqv (mk mf ∅ : DynReservationMap A H) (token_union hE₁Ef)) ?_ + rw [← hframe.symm.to_eq, ← hrearrange.symm.to_eq, + ← (op_right_eqv (mk mf ∅ : DynReservationMap A H) (token_union hE₁Ef)).to_eq] refine validN_data_op_token vmf ?_ ?_ · refine setInfinite_mono (fun i hi => ?_) hE₂inf have hiX := hEunion ▸ LawfulSet.mem_union.mpr (.inr hi) @@ -643,9 +635,8 @@ theorem reserve (Q : DynReservationMap A H → Prop) cases LawfulSet.mem_union.mp hmem with | inl h₁ => have hiX := hEunion ▸ LawfulSet.mem_union.mpr (.inl h₁) - have hnd : i ∉ domCoPset mf := - fun hd => (LawfulSet.mem_diff.mp hiX).right (LawfulSet.mem_union.mpr (.inr hd)) - exact Decidable.not_not.mp (mt mem_domCoPset.mpr hnd) + exact Decidable.not_not.mp <| mt mem_domCoPset.mpr fun hd => + (LawfulSet.mem_diff.mp hiX).right (LawfulSet.mem_union.mpr (.inr hd)) | inr hEf => exact (hdisj i).elim id fun h => absurd hEf h · exact .inr hmem