diff --git a/Iris/Iris/Algebra/COFESolver.lean b/Iris/Iris/Algebra/COFESolver.lean index 9a84d8f57..447252440 100644 --- a/Iris/Iris/Algebra/COFESolver.lean +++ b/Iris/Iris/Algebra/COFESolver.lean @@ -6,6 +6,7 @@ Authors: Mario Carneiro module public import Iris.Algebra.OFE +public meta import Iris.Std.RocqPorting @[expose] public section @@ -19,31 +20,38 @@ variable [inh : Inhabited (F (ULift Unit) (ULift Unit))] namespace Fix.Impl variable (F) in +@[rocq_alias solver.A'] def A' : Nat → Σ α : Type u, COFE α | 0 => ⟨ULift Unit, inferInstance⟩ | n+1 => let ⟨A, _⟩ := A' n; ⟨F A A, inferInstance⟩ variable (F) in +@[rocq_alias solver.A] def A (n : Nat) : Type u := (A' F n).1 +@[rocq_alias solver.A_cofe] instance instA' (n) : COFE (A' F n).1 := (A' F n).2 instance instA (n) : COFE (A F n) := (A' F n).2 variable (F) in mutual +@[rocq_alias solver.f] def up : ∀ k, A F k -n> A F (k+1) | 0 => ⟨fun _ => inh.default, ⟨fun _ _ _ _ => .rfl⟩⟩ | k+1 => map (down k) (up k) +@[rocq_alias solver.g] def down : ∀ k, A F (k+1) -n> A F k | 0 => ⟨fun _ => ⟨()⟩, ⟨fun _ _ _ _ => .rfl⟩⟩ | k+1 => map (up k) (down k) end +@[rocq_alias solver.gf] theorem down_up : ∀ {k} x, down F k (up F k x) ≡ x | 0, ⟨()⟩ => .rfl | _+1, _ => (map_comp ..).symm.trans <| (map_ne.eqv down_up down_up _).trans (map_id _) +@[rocq_alias solver.fg] theorem up_down {k} (x) : up F (k+1) (down F (k+1) x) ≡{k}≡ x := by refine (map_comp ..).dist.symm.trans <| .trans ?_ (map_id _).dist open OFunctorContractive in exact match k with @@ -51,12 +59,14 @@ theorem up_down {k} (x) : up F (k+1) (down F (k+1) x) ≡{k}≡ x := by | k+1 => map_contractive.succ (x := (_, _)) (y := (_, _)) _ ⟨up_down, up_down⟩ _ variable (F) in -@[ext] structure Tower : Type u where +@[ext, rocq_alias solver.tower] +structure Tower : Type u where val k : A F k protected down {k} : down F k (val (k+1)) ≡ val k instance : CoeFun (Tower F) (fun _ => ∀ k, A F k) := ⟨Tower.val⟩ +@[rocq_alias solver.tower_ofe_mixin] instance : OFE (Tower F) where Equiv f g := ∀ k, f k ≡ g k Dist n f g := ∀ k, f k ≡{n}≡ g k @@ -68,10 +78,12 @@ instance : OFE (Tower F) where equiv_dist {_ _} := by simp [equiv_dist]; apply forall_comm dist_lt h1 h2 _ := dist_lt (h1 _) h2 +@[rocq_alias solver.tower_chain] def towerChain (c : Chain (Tower F)) (k : Nat) : Chain (A F k) where chain i := c.1 i k cauchy h := c.cauchy h k +@[rocq_alias solver.tower_cofe] instance : COFE (Tower F) where compl c := by refine ⟨fun k => compl ⟨fun i => c.1 i k, fun h => c.cauchy h k⟩, ?_⟩ @@ -81,22 +93,27 @@ instance : COFE (Tower F) where conv_compl _ := conv_compl variable (F) in +@[rocq_alias solver.ff] def upN {k} : ∀ n, A F k -n> A F (k + n) | 0 => .id | n+1 => (up F (k + n)).comp (upN n) variable (F) in +@[rocq_alias solver.gg] def downN {k} : ∀ n, A F (k + n) -n> A F k | 0 => .id | n+1 => (downN n).comp (down F (k + n)) +@[rocq_alias solver.ggff] theorem downN_upN {k} (x : A F k) : ∀ {i}, downN F i (upN F i x) ≡ x | 0 => .rfl | n+1 => ((downN F n).ne.eqv (down_up ..)).trans (downN_upN _) +@[rocq_alias solver.f_tower] protected theorem Tower.up (X : Tower F) : up F (k+1) (X (k+1)) ≡{k}≡ X (k+2) := ((up ..).ne.1 X.down.symm.dist).trans <| up_down _ +@[rocq_alias solver.ff_tower] protected theorem Tower.upN (X : Tower F) : ∀ i, upN F i (X (k+1)) ≡{k}≡ X (k+1+i) | 0 => .rfl | n+1 => by @@ -104,28 +121,36 @@ protected theorem Tower.upN (X : Tower F) : ∀ i, upN F i (X (k+1)) ≡{k}≡ X rintro _ rfl; exact X.up.le (Nat.le_add_right ..) exact ((up ..).ne.1 (X.upN _)).trans <| this _ (Nat.add_right_comm ..) +@[rocq_alias solver.gg_tower] protected theorem Tower.downN (X : Tower F) : ∀ i, downN F i (X (k+i)) ≡ X k | 0 => .rfl | _+1 => ((downN ..).ne.eqv X.down).trans (X.downN _) +@[rocq_alias solver.tower_car_ne] instance (k : Nat) : NonExpansive (fun X : Tower F => X.val k) := ⟨fun _ _ _ => (· _)⟩ +@[rocq_alias solver.project] def Tower.proj (k) : Tower F -n> A F k := ⟨(· k), ⟨fun _ _ _ => (· _)⟩⟩ +@[rocq_alias solver.coerce] def eqToHom (e : i = k) : A F i -n> A F k := e ▸ .id +@[rocq_alias solver.coerce_f] theorem eqToHom_up {k k'} {x : A F k} (e : k = k') : eqToHom (congrArg Nat.succ e) (up F k x) = up F k' (eqToHom e x) := by cases e; rfl +@[rocq_alias solver.g_coerce] theorem down_eqToHom {k k'} {x : A F (k+1)} (e : k = k') : down F k' (eqToHom (congrArg Nat.succ e) x) = eqToHom e (down F k x) := by cases e; rfl +@[rocq_alias solver.embed_coerce] def embed : A F k -n> A F i := if h : k ≤ i then (eqToHom (Nat.add_sub_cancel' h)).comp (upN ..) else (downN ..).comp (eqToHom (Nat.add_sub_cancel' (Nat.le_of_not_ge h)).symm) +@[rocq_alias solver.embed'] protected def Tower.embed (k) : A F k -n> Tower F := by refine ⟨fun n => ⟨fun _ => embed n, fun {i} => ?_⟩, ⟨fun _ _ _ h _ => embed.ne.1 h⟩⟩ dsimp [embed]; split <;> rename_i h₁ @@ -154,6 +179,7 @@ protected def Tower.embed (k) : A F k -n> Tower F := by rw [down_eqToHom (Nat.add_right_comm i a 1)] apply ih +@[rocq_alias solver.embed_f] theorem Tower.embed_up (x : A F k) : Tower.embed (k+1) (up F k x) ≡ Tower.embed k x := by refine equiv_dist.2 fun n i => ?_ @@ -183,6 +209,7 @@ theorem Tower.embed_up (x : A F k) : rintro a b eq rfl; cases Nat.add_left_cancel (m := b+1) eq exact (downN ..).ne.1 (down_up x).dist +@[rocq_alias solver.embed_tower] theorem Tower.embed_self (X : Tower F) : Tower.embed (k+1) (X (k+1)) ≡{k}≡ X := by refine fun i => ?_ @@ -196,8 +223,10 @@ theorem Tower.embed_self (X : Tower F) : · cases show k=i+a from Nat.succ.inj eq exact (X.downN _).dist +@[rocq_alias solver.tower_inhabited] instance : Inhabited (Tower F) := ⟨Tower.embed 0 ⟨()⟩⟩ +@[rocq_alias solver.unfold_chain] def unfoldChain (X : Tower F) : Chain (F (Tower F) (Tower F)) where chain n := map (Tower.proj _) (Tower.embed _) (X (n+1)) cauchy {n i} h := by @@ -257,14 +286,18 @@ end Fix.Impl open Fix.Impl variable (F) in +@[rocq_alias solver.T] def Fix : Type u := Tower F instance : Inhabited (Fix F) := inferInstanceAs (Inhabited (Tower F)) instance : COFE (Fix F) := inferInstanceAs (COFE (Tower F)) +@[rocq_alias solver.result] def Fix.iso : OFE.Iso (F (Fix F) (Fix F)) (Fix F) := Tower.iso +@[rocq_alias solver.fold] def Fix.fold : F (Fix F) (Fix F) -n> Fix F := Fix.iso.hom +@[rocq_alias solver.unfold] def Fix.unfold : Fix F -n> F (Fix F) (Fix F) := Fix.iso.inv theorem Fix.fold_unfold (X : Fix F) : Fix.fold (Fix.unfold X) ≡ X := Fix.iso.hom_inv theorem Fix.unfold_fold (X : F (Fix F) (Fix F)) : Fix.unfold (Fix.fold X) ≡ X := Fix.iso.inv_hom diff --git a/Iris/Iris/Algebra/Csum.lean b/Iris/Iris/Algebra/Csum.lean index 9b8855aed..4dcebd084 100644 --- a/Iris/Iris/Algebra/Csum.lean +++ b/Iris/Iris/Algebra/Csum.lean @@ -47,6 +47,7 @@ theorem dist_eqv [OFE α] [OFE β] {n} : Equivalence (Csum.Dist (α := α) (β : cases x <;> cases y <;> cases z <;> first | trivial | exact h₁.trans h₂ | exact h₂.elim | exact h₁.elim +@[rocq_alias csumO] instance [OFE α] [OFE β] : OFE (Csum α β) where Equiv := Csum.Equiv Dist := Csum.Dist @@ -181,6 +182,7 @@ private theorem pcore_map_inr_eq [CMRA β] {b : β} {cx : Csum α β} ∃ cb, CMRA.pcore b = some cb ∧ cx = inr cb := by cases _ : CMRA.pcore b <;> simp_all +@[rocq_alias csumR] instance [CMRA α] [CMRA β] : CMRA (Csum α β) where pcore := Csum.pcore op := Csum.op @@ -521,6 +523,7 @@ theorem oMap_ne [OFE α] [OFE α'] [OFE β] [OFE β'] : abbrev OF (Fa Fb : COFE.OFunctorPre) : COFE.OFunctorPre := fun A B _ _ => Csum (Fa A B) (Fb A B) +@[rocq_alias csum_map_cmra_morphism] def cMap [CMRA α] [CMRA α'] [CMRA β] [CMRA β'] (fa : α -C> α') (fb : β -C> β') : Csum α β -C> Csum α' β' where f := map fa fb diff --git a/Iris/Iris/Algebra/Excl.lean b/Iris/Iris/Algebra/Excl.lean index 4d7be15eb..504832af2 100644 --- a/Iris/Iris/Algebra/Excl.lean +++ b/Iris/Iris/Algebra/Excl.lean @@ -6,6 +6,7 @@ Authors: Oliver Soeser, Mario Carneiro module public import Iris.Algebra.CMRA +meta import Iris.Std.RocqPorting @[expose] public section @@ -13,6 +14,7 @@ namespace Iris section excl +@[rocq_alias excl] inductive Excl α where | excl : α → Excl α | invalid : Excl α @@ -58,6 +60,7 @@ instance [OFE α] : OFE (Excl α) where cases x <;> cases y <;> simp at * exact Dist.lt hn hlt +@[rocq_alias Excl_ne] instance [OFE α] : NonExpansive excl (α := α) where ne _ _ _ a := a @@ -72,22 +75,26 @@ theorem Excl.ne_match [OFE α] {B : Type _} [OFE B] | .invalid, .excl _, h => h.elim | .invalid, .invalid, _ => Dist.rfl⟩ +@[rocq_alias excl_ofe_discrete] instance [OFE α] [Discrete α] : Discrete (Excl α) where discrete_0 {x y} h' := by cases x <;> cases y <;> try exact h' exact discrete_0 (α := α) h' +@[rocq_alias excl_leibniz] instance [OFE α] [Leibniz α] : Leibniz (Excl α) where eq_of_eqv {x y} h' := by cases x <;> cases y <;> try trivial exact congrArg excl (eq_of_eqv h') +@[rocq_alias Excl_discrete] instance [OFE α] {a : α} [h : DiscreteE a] : DiscreteE (excl a) where discrete {x} h' := by cases x · exact h.discrete h' · exact h' +@[rocq_alias ExclInvalid_discrete] instance [OFE α] : DiscreteE (@invalid α) where discrete {x} h := by cases x <;> exact h @@ -98,7 +105,7 @@ instance [OFE α] : DiscreteE (@invalid α) where | excl a => a | invalid => dflt -@[simp] def Excl.map (f : α → β) : Excl α → Excl β +@[simp, rocq_alias excl_map] def Excl.map (f : α → β) : Excl α → Excl β | excl a => excl (f a) | invalid => invalid @@ -107,6 +114,7 @@ def exclChain [OFE α] (c : Chain (Excl α)) (a : α) : Chain α := by dsimp; have := c.cauchy H; revert this cases c.chain i <;> cases c.chain n <;> simp [Dist] +@[rocq_alias excl_cofe] instance [OFE α] [IsCOFE α] : IsCOFE (Excl α) where compl c := (c 0).map fun x => IsCOFE.compl (exclChain c x) conv_compl {n} c := by @@ -141,6 +149,7 @@ instance [OFE α] : CMRA (Excl α) where validN_op_left := by simp extend {n x y₁ y₂} h₁ h₂ := by cases x <;> trivial +@[rocq_alias excl_included] theorem excl_included [OFE α] {x y : Excl α} : x ≼ y ↔ y = invalid := by constructor · intro h @@ -150,41 +159,51 @@ theorem excl_included [OFE α] {x y : Excl α} : x ≼ y ↔ y = invalid := by exists invalid exact Equiv.of_eq h +@[rocq_alias excl_includedN] theorem excl_includedN [OFE α] {x y : Excl α} (n) : x ≼{n} y ↔ y = invalid := by constructor · intro ⟨z, hz⟩; cases x <;> cases y <;> trivial · rintro rfl; exists invalid +@[rocq_alias excl_exclusive] instance [OFE α] {x : Excl α} : CMRA.Exclusive x where exclusive0_l := fun _ a => a +@[rocq_alias excl_cmra_discrete] instance [OFE α] [OFE.Discrete α] : CMRA.Discrete (Excl α) where discrete_valid a := a +@[rocq_alias ExclInvalid_included] theorem invalid_included [OFE α] (ea : Excl α) : ea ≼ invalid := by exists invalid /-! ## Functors -/ +@[rocq_alias excl_map_id] theorem excl_map_id : map id x = x := by cases x <;> simp +@[rocq_alias excl_map_compose] theorem excl_map_compose (f : α → β) (g : β → γ) : map (g ∘ f) x = map g (map f x) := by cases x <;> simp +@[rocq_alias excl_map_ext] theorem excl_map_ext [OFE α] [OFE β] (f g : α → β) (h : ∀ x, f x ≡ g x) : map f x ≡ map g x := by cases x; apply h _; simp +@[rocq_alias excl_map_ne] theorem excl_map_ne [OFE α] [OFE β] (f : α -n> β) : NonExpansive (map f) where ne n x₁ x₂ h := by cases x₁ <;> cases x₂ <;> try trivial have ⟨hne⟩ := f.ne exact hne h +@[rocq_alias excl_map_morphism] def exclO_map [OFE α] [OFE β] (f : α -n> β) : Excl α -C> Excl β := by refine ⟨⟨map f, excl_map_ne f⟩, ?_, ?_, ?_⟩ · intro n x h; cases x <;> trivial · intro x; trivial · intro x y; trivial +@[rocq_alias exclRF] abbrev ExclOF (F : COFE.OFunctorPre) : COFE.OFunctorPre := fun A B _ _ => Excl (F A B) @@ -208,6 +227,7 @@ instance {F} [COFE.OFunctor F] : RFunctor (ExclOF F) where · apply COFE.OFunctor.map_comp · trivial +@[rocq_alias exclRF_contractive] instance {F} [COFE.OFunctorContractive F] : RFunctorContractive (ExclOF F) where map_contractive.1 {n x y} HKL z := by rewrite [RFunctor.map] diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 2ba970d54..1760b353f 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -7,6 +7,7 @@ module public import Iris.Algebra.CMRA public import Iris.Algebra.OFE +meta import Iris.Std.RocqPorting /-! # The Frac CMRA @@ -85,6 +86,7 @@ instance [Fraction α] : Coe α (Frac α) := ⟨(⟨·⟩)⟩ @[simp] instance [Fraction α] : Add (Frac α) := ⟨fun x y => x.1 + y.1⟩ instance : Leibniz (Frac α) := inferInstanceAs (Leibniz (LeibnizO α)) +@[rocq_alias fracR] instance Frac_CMRA [Fraction α] : CMRA (Frac α) where pcore _ := none op := Add.add @@ -103,6 +105,7 @@ instance Frac_CMRA [Fraction α] : CMRA (Frac α) where pcore_op_mono := by simp extend {_ _ y1 y2} _ _ := by exists y1; exists y2 +@[rocq_alias frac_cmra_discrete] instance [Fraction α] : CMRA.Discrete (Frac α) where discrete_0 := id discrete_valid := id @@ -110,11 +113,13 @@ instance [Fraction α] : CMRA.Discrete (Frac α) where instance [Fraction α] [CMRA α] {a : Frac α} (Hw : Whole a.1) : Exclusive a where exclusive0_l _ Hk := (not_exists.mp Hw.2) _ Hk +@[rocq_alias frac_cancelable] instance [Fraction α] {a : Frac α} : CMRA.Cancelable a where cancelableN {n x y} _ (H : a • x = a • y) := by refine Dist.of_eq <| LeibnizO.ext <| add_left_cancel (a := a.car) <| ?_ exact LeibnizO.eqv_inj H +@[rocq_alias frac_id_free] instance [Fraction α] {a : Frac α} : CMRA.IdFree a where id_free0_r b _ H := by suffices (b + a).car = a.car from add_ne this.symm diff --git a/Iris/Iris/Algebra/GenMap.lean b/Iris/Iris/Algebra/GenMap.lean index b2c7c092c..97abda1a0 100644 --- a/Iris/Iris/Algebra/GenMap.lean +++ b/Iris/Iris/Algebra/GenMap.lean @@ -8,6 +8,7 @@ module public import Iris.Algebra.OFE public import Iris.Algebra.CMRA public import Iris.Algebra.Updates +meta import Iris.Std.RocqPorting @[expose] public section diff --git a/Iris/Iris/Algebra/Heap.lean b/Iris/Iris/Algebra/Heap.lean index 158fea34b..7fa50e0a4 100644 --- a/Iris/Iris/Algebra/Heap.lean +++ b/Iris/Iris/Algebra/Heap.lean @@ -9,6 +9,7 @@ public import Iris.Algebra.CMRA public import Iris.Algebra.OFE public import Iris.Std.Set public import Iris.Std.PartialMap +meta import Iris.Std.RocqPorting @[expose] public section @@ -35,9 +36,11 @@ instance instOFE [PartialMap 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 [PartialMap 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,6 +55,7 @@ instance [LawfulPartialMap M K] [OFE V] (op : K → V → V → V) [∀ k, NonEx ne _ {_ _} Ht {_ _} Hs k := by simp only [get?_merge]; exact NonExpansive₂.ne (Ht k) (Hs k) /-- Project a chain of stores through its kth coordinate to a chain of values. -/ +@[rocq_alias gmap_chain] def chain [PartialMap 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 @@ -61,6 +65,7 @@ theorem chain_get [PartialMap M K] [OFE V] (k : K) (c : Chain (M V)) : end PartialMap +@[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 @@ -88,6 +93,7 @@ variable [LawfulPartialMap M K] [CMRA V] @[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 +@[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 @@ -103,6 +109,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 @@ -240,43 +247,51 @@ variable {K V : Type _} [LawfulPartialMap M K] [CMRA V] open CMRA +@[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 exact OFE.Dist.validN He |>.mp +@[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) 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) @@ -289,6 +304,7 @@ theorem insert_equiv_singleton_op_singleton {m : M V} (Hemp : get? m i = none) : · rw [← He, Hemp] · cases (get? m k) <;> rfl +@[rocq_alias insert_singleton_op] theorem insert_eq_singleton_op_singleton [IsoFunMap M K] {m : M V} (Hemp : get? m i = none) : insert m i x = singleton i x • m := IsoFunMap.ext (insert_equiv_singleton_op_singleton Hemp) @@ -300,11 +316,13 @@ theorem core_singleton_equiv {i : K} {x : V} {cx : V} (Hpcore : CMRA.pcore x = s simp [← Hpcore, core, CMRA.pcore, get?_singleton, get?_bindAlter] split <;> rfl +@[rocq_alias singleton_core] theorem singleton_core_eq [IsoFunMap M K] {i : K} {x : V} {cx} (Hpcore : CMRA.pcore x = some cx) : core (singleton i x : M V) = singleton i cx := IsoFunMap.ext (core_singleton_equiv Hpcore) open Classical in +@[rocq_alias singleton_core'] theorem singleton_core_eqv {i : K} {x : V} {cx} (Hpcore : CMRA.pcore x ≡ some cx) : core (singleton i x : M V) ≡ singleton i cx := by intro k @@ -315,6 +333,7 @@ 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) +@[rocq_alias singleton_core_total] theorem singleton_core_total_eq [IsTotal V] [IsoFunMap M K] {i : K} {x : V} : core (singleton i x : M V) = singleton i (core x) := IsoFunMap.ext singleton_core_total @@ -326,10 +345,12 @@ theorem singleton_op_singleton {i : K} {x y : V} : simp only [CMRA.op, Heap.op, get?_merge, get?_singleton] split <;> simp [Option.merge] +@[rocq_alias singleton_op] 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 +@[rocq_alias gmap_core_id'] instance {m : M V} [I : ∀ x : V, CoreId x] : CoreId m where core_id i := by rw [get?_bindAlter] @@ -337,6 +358,7 @@ instance {m : M V} [I : ∀ x : V, CoreId x] : CoreId m where exact core_id open Classical in +@[rocq_alias gmap_singleton_core_id] instance [CoreId (x : V)] : CoreId (singleton i x : M V) where core_id k := by simp [get?_bindAlter, get?_singleton] @@ -344,6 +366,7 @@ instance [CoreId (x : V)] : CoreId (singleton i x : M V) where exact core_id 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⟩ => ?_⟩ @@ -376,6 +399,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⟩ => ?_⟩ @@ -407,6 +431,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 _ => ?_⟩ @@ -414,6 +439,7 @@ 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 => ?_⟩ · refine inc_of_inc_of_eqv Hxz ?_ @@ -422,15 +448,18 @@ theorem singleton_inc_singleton_iff : (singleton i x : M V) ≼ (singleton i y : · refine ⟨y, ?_, H⟩ exact .of_eq <| 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_isTotal +@[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 @@ -444,6 +473,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) @@ -461,6 +491,7 @@ theorem insert_op_equiv {m1 m2 : M V} : · simp [CMRA.op, get?_insert_eq He, get?_merge] · simp [CMRA.op, get?_insert_ne He, get?_merge] +@[rocq_alias insert_op] 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 @@ -473,10 +504,12 @@ theorem disjoint_op_equiv_union {m1 m2 : M V} (Hd : Set.Disjoint (dom m1) (dom m refine (Hd j ?_).elim simp_all [dom] +@[rocq_alias gmap_op_union] theorem disjoint_op_eq_union [IsoFunMap M K] {m1 m2 : M V} (H : Set.Disjoint (dom m1) (dom m2)) : 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 @@ -487,14 +520,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 @@ -502,6 +538,7 @@ theorem inc_dom_inc {m1 m2 : M V} (Hinc : m1 ≼ m2) : Set.Included (dom m1) (do revert Hz cases get? m1 i <;> cases get? m2 i <;> cases z <;> simp [CMRA.op, optionOp] +@[rocq_alias gmap_cmra_discrete] nonrec instance [HD : CMRA.Discrete V] [PartialMap M K] : Discrete (M V) where discrete_0 {_ _} H := (OFE.Discrete.discrete_0 <| H ·) discrete_valid {_} := (CMRA.Discrete.discrete_valid <| · ·) @@ -516,6 +553,7 @@ namespace PartialMap def map (f : α → β) : H α → H β := PartialMap.bindAlter (fun _ a => some <| f a) +@[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] @@ -529,6 +567,7 @@ def map_id [OFE α] (a : H α): intro x 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 @@ -551,6 +590,7 @@ def 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 @@ -578,6 +618,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 cofe := inferInstance map f g := mapO H (COFE.OFunctor.map f g) @@ -597,6 +638,7 @@ 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' _ +@[rocq_alias gmapURF] instance {F} [RFunctor F] : URFunctor (PartialMapOF H F) where map f g := mapC H (RFunctor.map f g) map_ne {_} _ _ _ _ _ _ _ := by @@ -615,6 +657,7 @@ instance {F} [RFunctor F] : URFunctor (PartialMapOF H F) where cases get? m x <;> simp exact (RFunctor.map_comp ..) +@[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/HeapView.lean b/Iris/Iris/Algebra/HeapView.lean index 06bd0845e..40308a65e 100644 --- a/Iris/Iris/Algebra/HeapView.lean +++ b/Iris/Iris/Algebra/HeapView.lean @@ -9,6 +9,7 @@ public import Iris.Algebra.Heap public import Iris.Algebra.View public import Iris.Algebra.DFrac public import Iris.Algebra.Frac +meta import Iris.Std.RocqPorting /-! # Heap Views @@ -40,10 +41,12 @@ open Std PartialMap Heap OFE CMRA variable (F K V : Type _) (H : Type _ → Type _) [UFraction F] [LawfulPartialMap H K] [CMRA V] /-- The view relation for heaps: relates a model heap to a fragment heap at step index `n`. -/ +@[rocq_alias gmap_view_rel_raw] def HeapR (n : Nat) (m : H V) (f : H (DFrac F × V)) : Prop := ∀ k fv, get? f k = some fv → ∃ (v : V) (dq : DFrac F), get? m k = some v ∧ ✓{n} (dq, v) ∧ (some fv ≼{n} some (dq, v)) +@[rocq_alias gmap_view_rel] instance : IsViewRel (HeapR F K V H) where mono {n1 m1 f1 n2 m2 f2 Hrel Hm Hf Hn k} vk Hk := by obtain Hf' : ∃ z, get? f1 k ≡{n2}≡ some vk • z := by @@ -74,9 +77,11 @@ instance : IsViewRel (HeapR F K V H) where namespace HeapR +@[rocq_alias gmap_view_rel_unit] theorem unit : HeapR F K V H n m UCMRA.unit := by simp [HeapR, UCMRA.unit, Heap.unit, get?_empty] +@[rocq_alias gmap_view_rel_exists] theorem exists_iff_validN {n f} : (∃ m, HeapR F K V H n m f) ↔ ✓{n} f := by refine ⟨fun ⟨m, Hrel⟩ => IsViewRel.rel_validN _ _ _ Hrel, fun Hv => ?_⟩ let FF : K → (DFrac F × V) → Option V := fun k _ => get? f k |>.bind (·.2) @@ -89,6 +94,7 @@ theorem exists_iff_validN {n f} : (∃ m, HeapR F K V H n m f) ↔ ✓{n} f := b simp only [get?_bindAlter, h, Option.bind_some, true_and, FF] exact ⟨dq, (h ▸ Hv k : ✓{n} some (dq, v)), incN_refl _⟩ +@[rocq_alias gmap_view_rel_lookup] theorem singleton_get_iff n m k dq v : HeapR F K V H n m (PartialMap.singleton k (dq, v)) ↔ ∃ (v' : V) (dq' : DFrac F), @@ -104,6 +110,7 @@ theorem singleton_get_iff n m k dq v : · rw [PartialMap.singleton, get?_insert_ne h, get?_empty] at Hfv cases Hfv +@[rocq_alias gmap_view_rel_discrete] instance [CMRA.Discrete V] : IsViewRelDiscrete (HeapR F K V H) where discrete n _ _ H k v He := by have ⟨v, Hv1, ⟨x, Hx1, Hx2⟩⟩ := H k v He @@ -124,17 +131,21 @@ open Heap OFE View One DFrac CMRA UFraction PartialMap Std LawfulPartialMap variable {F K V : Type _} {H : Type _ → Type _} [UFraction F] [LawfulPartialMap H K] [CMRA V] /-- Authoritative (fractional) ownership over an entire heap. -/ +@[rocq_alias gmap_view_auth] def Auth (dq : DFrac F) (m : H V) : HeapView F K V H := ●V{dq} m /-- Fragmental (fractional) ownership over an allocated element in the heap. -/ +@[rocq_alias gmap_view_frag] def Frag (k : K) (dq : DFrac F) (v : V) : HeapView F K V H := ◯V (Std.PartialMap.singleton k (dq, v)) /-- Fragmental (fractional) ownership over an element in the heap. -/ def Elem (k : K) (v : DFrac F × V) : HeapView F K V H := ◯V (Std.PartialMap.singleton k v) -- TODO: Do we need this? +@[rocq_alias gmap_view_auth_ne] instance : NonExpansive (Auth dq : _ → HeapView F K V H) := View.auth_ne +@[rocq_alias gmap_view_frag_ne] instance : NonExpansive (Frag k dq : _ → HeapView F K V H) where ne _ _ _ Hx := by refine frag_ne.ne (fun k' => ?_) @@ -145,49 +156,62 @@ instance : NonExpansive (Frag k dq : _ → HeapView F K V H) where variable {dp dq : DFrac F} {n : Nat} {m1 m2 : H V} {k : K} {v1 v2 : V} +@[rocq_alias gmap_view_auth_dfrac_op] theorem auth_dfrac_op_equiv : Auth (dp • dq) m1 ≡ Auth dp m1 • Auth dq m1 := View.auth_op_auth_eqv +@[rocq_alias gmap_view_auth_dfrac_op_invN] theorem dist_of_validN_auth_op : ✓{n} Auth dp m1 • Auth dq m2 → m1 ≡{n}≡ m2 := dist_of_validN_auth +@[rocq_alias gmap_view_auth_dfrac_op_inv] theorem equiv_of_valid_auth_op : ✓ Auth dp m1 • Auth dq m2 → m1 ≡ m2 := eqv_of_valid_auth +@[rocq_alias gmap_view_auth_dfrac_validN] nonrec theorem auth_validN_iff : ✓{n} Auth dq m1 ↔ ✓ dq := auth_validN_iff.trans <| and_iff_left_of_imp (fun _ => HeapR.unit _ _ _ _) +@[rocq_alias gmap_view_auth_dfrac_valid] nonrec theorem auth_valid_iff : ✓ Auth dq m1 ↔ ✓ dq := auth_valid_iff.trans <| and_iff_left_of_imp (fun _ _ => HeapR.unit _ _ _ _) +@[rocq_alias gmap_view_auth_valid] theorem auth_one_valid : ✓ Auth (.own (F := F) one) m1 := auth_valid_iff.mpr valid_own_one +@[rocq_alias gmap_view_auth_dfrac_op_validN] nonrec theorem auth_op_auth_validN_iff : ✓{n} Auth dp m1 • Auth dq m2 ↔ ✓ dp • dq ∧ m1 ≡{n}≡ m2 := auth_op_auth_validN_iff.trans <| and_congr_right <| fun _ => and_iff_left_of_imp <| fun _ => HeapR.unit _ _ _ _ +@[rocq_alias gmap_view_auth_dfrac_op_valid] nonrec theorem auth_op_auth_valid_iff : ✓ Auth dp m1 • Auth dq m2 ↔ ✓ dp • dq ∧ m1 ≡ m2 := auth_op_auth_valid_iff.trans <| and_congr_right <| fun _ => and_iff_left_of_imp <| fun _ _ => HeapR.unit _ _ _ _ +@[rocq_alias gmap_view_auth_op_validN] nonrec theorem auth_one_op_auth_one_validN_iff : ✓{n} Auth (F := F) (.own one) m1 • Auth (.own one) m2 ↔ False := auth_one_op_auth_one_validN_iff +@[rocq_alias gmap_view_auth_op_valid] nonrec theorem auth_one_op_auth_one_valid_iff : ✓ Auth (F := F) (.own one) m1 • Auth (.own one) m2 ↔ False := auth_one_op_auth_one_valid_iff +@[rocq_alias gmap_view_frag_op] theorem frag_op_equiv : Frag (H := H) k (dp • dq) (v1 • v2) ≡ Frag k dp v1 • Frag k dq v2 := by refine frag_ne.eqv ?_ refine .trans ?_ (eqv_of_Equiv <| Heap.singleton_op_singleton).symm exact .rfl +@[rocq_alias gmap_view_frag_add] theorem frag_add_op_equiv {q1 q2 : F} : Frag (H := H) k (.own (q1 + q2)) (v1 • v2) ≡ Frag k (.own q1) v1 • Frag k (.own q2) v2 := frag_op_equiv +@[rocq_alias gmap_view_both_dfrac_validN] nonrec theorem auth_op_frag_validN_iff : ✓{n} Auth dp m1 • Frag k dq v ↔ ∃ v' dq', ✓ dp ∧ (Std.PartialMap.get? m1 k = some v') ∧ ✓{n} (dq', v') ∧ some (dq, v) ≼{n} some (dq', v') := @@ -195,6 +219,7 @@ nonrec theorem auth_op_frag_validN_iff : (and_congr_right fun _ => (HeapR.singleton_get_iff ..).trans <| exists_congr fun _ => exists_and_left).trans (by grind) +@[rocq_alias gmap_view_both_validN] theorem auth_op_frag_one_validN_iff : ✓{n} (Auth dp m1 • Frag k (.own one) v1) ↔ ✓ dp ∧ ✓{n} v1 ∧ Std.PartialMap.get? m1 k ≡{n}≡ some v1 := by refine auth_op_frag_validN_iff.trans ⟨fun ⟨Hp, v', dq', Hl, Hv, Hi⟩ => ?_, fun ⟨Hp, Hv, Hl⟩ => ?_⟩ @@ -208,6 +233,7 @@ theorem auth_op_frag_one_validN_iff : · exact ⟨one_whole (α := F) |>.1, Dist.validN (h ▸ Hl).symm |>.mp Hv⟩ · exact Option.some_incN_some_iff.mpr <| .inl <| dist_prod_ext rfl (h.symm ▸ Hl).symm +@[rocq_alias gmap_view_both_dfrac_validN_total] theorem auth_op_frag_validN_total_iff [IsTotal V] (H : ✓{n} Auth dp m1 • Frag k dq v1) : ∃ v', ✓ dp ∧ ✓ dq ∧ Std.PartialMap.get? m1 k = some v' ∧ ✓{n} v' ∧ v1 ≼{n} v' := by obtain ⟨v', dq', Hdp, Hl, Hv, ⟨x, Hx⟩⟩ := auth_op_frag_validN_iff.mp H @@ -222,6 +248,7 @@ theorem auth_op_frag_validN_total_iff [IsTotal V] (H : ✓{n} Auth dp m1 • Fra | none => exact incN_of_incN_of_dist (incN_refl _) Hx.2.symm | some x => exact ⟨x.2, Hx.2⟩ +@[rocq_alias gmap_view_both_dfrac_valid_discrete] theorem auth_op_frag_discrete_valid_iff [CMRA.Discrete V] : ✓ Auth dp m1 • Frag k dq v1 ↔ ∃ v' dq', ✓ dp ∧ Std.PartialMap.get? m1 k = some v' ∧ ✓ (dq', v') ∧ some (dq, v1) ≼ some (dq', v') := by @@ -233,6 +260,7 @@ theorem auth_op_frag_discrete_valid_iff [CMRA.Discrete V] : exact ⟨discrete_valid Hv.1, discrete_valid Hv.2⟩ · exact fun ⟨v', dq', Hdp, Hl, Hv, Hi⟩ n => ⟨v', dq', Hdp, Hl, Hv.validN, inc_iff_incN n |>.mp Hi⟩ +@[rocq_alias gmap_view_both_dfrac_valid_discrete_total] theorem auth_op_frag_valid_total_discrete_iff [IsTotal V] [CMRA.Discrete V] (H : ✓ Auth dp m1 • Frag k dq v1) : ∃ v', ✓ dp ∧ ✓ dq ∧ Std.PartialMap.get? m1 k = some v' ∧ ✓ v' ∧ v1 ≼ v' := by @@ -247,6 +275,7 @@ theorem auth_op_frag_valid_total_discrete_iff [IsTotal V] [CMRA.Discrete V] · exact inc_of_inc_of_eqv (inc_refl _) Hz.symm · exists z +@[rocq_alias gmap_view_both_valid] theorem auth_op_frag_one_valid_iff : ✓ Auth dp m1 • Frag k (.own one) v1 ↔ ✓ dp ∧ ✓ v1 ∧ Std.PartialMap.get? m1 k ≡ some v1 := by refine valid_iff_validN.trans ?_ @@ -255,6 +284,7 @@ theorem auth_op_frag_one_valid_iff : · exact ⟨Hv 0 |>.1, valid_iff_validN.mpr (Hv · |>.2.1), equiv_dist.mpr (Hv · |>.2.2)⟩ · exact fun ⟨Hdp, Hv, Hl⟩ n => ⟨Hdp, Hv.validN, Hl.dist⟩ +@[rocq_alias gmap_view_frag_core_id] instance [Hdq : CoreId dq] [Hv1 : CoreId v1] : CoreId (Frag (H := H) k dq v1) where core_id := by obtain ⟨H⟩ := Hdq @@ -267,21 +297,25 @@ instance [Hdq : CoreId dq] [Hv1 : CoreId v1] : CoreId (Frag (H := H) k dq v1) wh · simp only [Option.bind_some, H] exact ⟨rfl, some_eqv_some.mp (h ▸ Hv1.core_id)⟩ +@[rocq_alias gmap_view_frag_validN] nonrec theorem frag_validN_iff : ✓{n} Frag (H := H) k dq v1 ↔ ✓ dq ∧ ✓{n} v1 := frag_validN_iff.trans <| (HeapR.exists_iff_validN ..).trans singleton_validN_iff +@[rocq_alias gmap_view_frag_valid] theorem frag_valid_iff : ✓ Frag (H := H) k dq v1 ↔ ✓ dq ∧ ✓ v1 := by refine (forall_congr' (fun _ => frag_validN_iff)).trans ?_ refine ⟨fun H => ?_, fun ⟨H1, H2⟩ n => ?_⟩ · exact ⟨valid_iff_validN.mpr (H · |>.1), valid_iff_validN.mpr (H · |>.2)⟩ · exact ⟨valid_iff_validN.mp H1 n, valid_iff_validN.mp H2 n⟩ +@[rocq_alias gmap_view_frag_op_validN] theorem frag_op_validN_iff : ✓{n} Frag (H := H) k dp v1 • Frag k dq v2 ↔ ✓ (dp • dq) ∧ ✓{n} (v1 • v2) := by refine View.frag_validN_iff.trans <| (HeapR.exists_iff_validN ..).trans ?_ refine (validN_iff <| equiv_dist.mp (eqv_of_Equiv singleton_op_singleton) _).trans ?_ exact singleton_validN_iff +@[rocq_alias gmap_view_frag_op_valid] theorem frag_op_valid_iff : ✓ (Frag (H := H) k dp v1 • Frag k dq v2) ↔ ✓ (dp • dq) ∧ ✓ (v1 • v2) := by @@ -296,6 +330,7 @@ theorem frag_op_valid_iff : section heapUpdates +@[rocq_alias gmap_view_alloc] theorem update_one_alloc (Hfresh : Std.PartialMap.get? m1 k = none) (Hdq : ✓ dq) (Hval : ✓ v1) : Auth (.own one) m1 ~~> Auth (H := H) (.own one) (Std.PartialMap.insert m1 k v1) • Frag k dq v1 := by refine auth_one_alloc (fun n bf Hrel j => ?_) @@ -311,6 +346,7 @@ theorem update_one_alloc (Hfresh : Std.PartialMap.get? m1 k = none) (Hdq : ✓ d · grind exact (Hrel j · · <| · ▸ Hbf) +@[rocq_alias gmap_view_delete] theorem update_one_delete : Auth (F := F) (.own one) m1 • Frag k (.own one) v1 ~~> Auth (.own one) (Std.PartialMap.delete m1 k) := by refine auth_one_op_frag_dealloc <| fun n bf Hrel j => ?_ @@ -336,6 +372,7 @@ theorem update_one_delete : obtain ⟨v, H, q, H'⟩ := Hrel a b rfl exact ⟨v, q, H.symm ▸ get?_delete_ne h, H'⟩ +@[rocq_alias gmap_view_update] theorem update_auth_op_frag (Hup : ∀ (n : Nat) (mv : V) (f : Option (DFrac F × V)), (Std.PartialMap.get? m1 k = some mv) → @@ -406,6 +443,7 @@ theorem update_auth_op_frag rw [← Hbf] simp [get?_singleton_ne h] +@[rocq_alias gmap_view_update_local] theorem update_of_local_update (Hl : Std.PartialMap.get? m1 k = some mv) (Hup : (mv, v) ~l~> (mv', v')) : Auth (F := F) (.own one) m1 • Frag k dq v ~~> Auth (.own one) (Std.PartialMap.insert m1 k mv') • Frag k dq v' := by @@ -418,6 +456,7 @@ theorem update_of_local_update (Hl : Std.PartialMap.get? m1 k = some mv) (Hup : cases _ : f <;> simp_all [op?, CMRA.op] cases f <;> exact ⟨⟨Hv1, validN_ne Hup'.2 Hup'.1⟩, Hup'.2⟩ +@[rocq_alias gmap_view_replace] theorem update_replace (Hval' : ✓ v2) : Auth (.own one) m1 • Frag (F := F) k (.own one) v1 ~~> Auth (.own one) (Std.PartialMap.insert m1 k v2) • Frag k (.own one) v2 := by @@ -428,12 +467,15 @@ theorem update_replace (Hval' : ✓ v2) : · simp_all [CMRA.op?, CMRA.op, Prod.op] exact (own_whole_exclusive one_whole |>.exclusive0_l _ (valid0_of_validN Hval.1)).elim +@[rocq_alias gmap_view_auth_persist] theorem auth_dfrac_discard : Auth dq m1 ~~> Auth .discard m1 := auth_discard +@[rocq_alias gmap_view_auth_unpersist] theorem auth_dfrac_acquire [IsSplitFraction F] : Auth (F := F) .discard m1 ~~>: fun a => ∃ q, a = Auth (.own q) m1 := auth_acquire +@[rocq_alias gmap_view_frag_dfrac] theorem update_of_dfrac_update P (Hdq : dq ~~>: P) : Frag (H := H) k dq v1 ~~>: fun a => ∃ dq', a = Frag k dq' v1 ∧ P dq' := by apply UpdateP.weaken @@ -466,9 +508,11 @@ theorem update_of_dfrac_update P (Hdq : dq ~~>: P) : · rintro y ⟨b, rfl, q, _, _⟩ exists q +@[rocq_alias gmap_view_frag_persist] theorem update_frag_discard : Frag (H := H) k dq v1 ~~> Frag k .discard v1 := .lift_updateP (Frag k · v1) _ _ update_of_dfrac_update DFrac.update_discard +@[rocq_alias gmap_view_frag_unpersist] theorem update_frag_acquire [IsSplitFraction F] : (Frag k .discard v1 : HeapView F K V H) ~~>: fun a => ∃ q, a = Frag k (.own q) v1 := by apply UpdateP.weaken (update_of_dfrac_update _ DFrac.update_acquire) @@ -513,6 +557,7 @@ theorem heapR_map_eq [OFE A] [OFE B] [OFE A'] [OFE B'] [RFunctor T] (f : A' -n> · simp_all · exact (Hom.monoN _ _ he) +@[rocq_alias gmap_viewURF] abbrev HeapViewURF T [RFunctor T] : COFE.OFunctorPre := fun A B _ _ => HeapView F K (T A B) H @@ -552,6 +597,7 @@ instance {T} [RFunctor T] : URFunctor (HeapViewURF (F := F) (H := H) T) where apply (fun _ => Prod.map_ext _ _) <;> simp exact (fun _ => RFunctor.map_comp _ _ _ _) +@[rocq_alias gmap_viewURF_contractive] instance {T} [RFunctorContractive T] : URFunctorContractive (HeapViewURF (F := F) (H := H) T) where map_contractive.1 H _ := by apply View.map_ne <;> intros <;> apply PartialMap.map_ne diff --git a/Iris/Iris/Algebra/IProp.lean b/Iris/Iris/Algebra/IProp.lean index cb2b5ccd8..4d4469a56 100644 --- a/Iris/Iris/Algebra/IProp.lean +++ b/Iris/Iris/Algebra/IProp.lean @@ -11,6 +11,7 @@ public import Iris.Algebra.UPred public import Iris.Algebra.GenMap public import Iris.Algebra.COFESolver public import Init.Data.Vector +meta import Iris.Std.RocqPorting @[expose] public section @@ -30,6 +31,7 @@ def BundledGFunctors.set (GF : BundledGFunctors) (i : Nat) (FB : Σ F, RFunctorC abbrev GName := Nat +@[rocq_alias iResF] abbrev IResF (GF : BundledGFunctors) : OFunctorPre := DiscreteFunOF (fun i => GenMapOF (GF i).fst) @@ -39,20 +41,26 @@ section IProp variable (GF : BundledGFunctors) +@[rocq_alias iPrePropO] def IPre : Type _ := OFunctor.Fix (UPredOF (IResF GF)) +@[rocq_alias iPreProp_cofe] instance : COFE (IPre GF) := inferInstanceAs (COFE (OFunctor.Fix _)) +@[rocq_alias iResUR] def IResUR : Type := (i : GType) → GenMap (GF i |>.fst (IPre GF) (IPre GF)) instance : UCMRA (IResUR GF) := ucmraDiscreteFunO (β := fun (i : GType) => GenMap (GF i |>.fst (IPre GF) (IPre GF))) +@[rocq_alias iProp] abbrev IProp := UPred (IResUR GF) +@[rocq_alias iProp_unfold] def IProp.unfold : IProp GF -n> IPre GF := OFE.Iso.hom <| OFunctor.Fix.iso (F := (UPredOF (IResF GF))) +@[rocq_alias iProp_fold] def IProp.fold : IPre GF -n> IProp GF := OFE.Iso.inv <| OFunctor.Fix.iso (F := (UPredOF (IResF GF))) diff --git a/Iris/Iris/Algebra/LeibnizSet.lean b/Iris/Iris/Algebra/LeibnizSet.lean index d6385adfb..f47e3b654 100644 --- a/Iris/Iris/Algebra/LeibnizSet.lean +++ b/Iris/Iris/Algebra/LeibnizSet.lean @@ -10,6 +10,7 @@ public import Iris.Algebra.LocalUpdates public import Iris.Algebra.Updates public import Iris.Std.GenSets public import Iris.Std.Infinite +meta import Iris.Std.RocqPorting @[expose] public section @@ -22,6 +23,7 @@ OFE/CMRA on the element type. open Iris Std CMRA OFE LawfulSet +@[rocq_alias gset_disj] inductive DisjointLeibnizSet (S : Type _) where | valid : S → DisjointLeibnizSet S | error : DisjointLeibnizSet S @@ -85,6 +87,7 @@ instance : CMRA (DisjointLeibnizSet S) where simp [disjoint_empty_left] extend {_ _ y₁ y₂} _ h := ⟨y₁, y₂, ⟨h, rfl, rfl⟩⟩ +@[rocq_alias gset_disj_cmra_discrete] instance : CMRA.Discrete (DisjointLeibnizSet S) where discrete_0 := id discrete_valid := id @@ -95,6 +98,7 @@ instance : UCMRA (DisjointLeibnizSet S) where unit_left_id {x} := by rcases x <;> simp [disjoint_empty_left, op] pcore_unit := by simp [pcore] +@[rocq_alias gset_disj_included] theorem included_iff_subset {X Y : S} : valid X ≼ valid Y ↔ X ⊆ Y := by refine ⟨?_, ?_⟩ · rintro ⟨(Z|_), HZ⟩ @@ -111,19 +115,23 @@ theorem included_iff_subset {X Y : S} : valid X ≼ valid Y ↔ X ⊆ Y := by ext p; rw [mem_union, mem_diff] refine ⟨by grind, (·.casesOn (Hsub _) (·.left))⟩ +@[rocq_alias gset_disj_union] theorem disj_op_union {X Y : S} (Hdisj : X ## Y) : (valid X) • (valid Y) ≡ valid (X ∪ Y) := by simp [op, Hdisj] +@[rocq_alias gset_disj_valid_op] theorem valid_op_iff_disj {X Y : S} : ✓ ((valid X) • (valid Y)) ↔ X ## Y := by by_cases H : X ## Y <;> simp [H, op, Valid] +@[rocq_alias gset_disj_valid_inv_l] theorem valid_inv_l {X : S} {Y : DisjointLeibnizSet S} : ✓ (valid X) • Y → ∃ Y', Y = valid Y' ∧ X ## Y' := by simp only [op, Valid] rcases Y with (Y|_) <;> try (· simp) by_cases H : X ## Y <;> simp [H] +@[rocq_alias gset_disj_dealloc_local_update] theorem localUpdate_dealloc {X Y : S} : (valid X, valid Y) ~l~> (valid (X \ Y), valid ∅) := by refine LocalUpdate.total_valid fun vx vy inc => ?_ refine (local_update_unital_discrete ..).mpr fun z hx heq => ⟨valid_mapN (fun _ _ => vx) vx, ?_⟩ @@ -137,6 +145,7 @@ theorem localUpdate_dealloc {X Y : S} : (valid X, valid Y) ~l~> (valid (X \ Y), grind · cases heq +@[rocq_alias gset_disj_dealloc_empty_local_update] theorem localUpdate_dealloc_empty {X Z : S} : (valid Z • valid X, valid Z) ~l~> (valid X, valid ∅) := by refine LocalUpdate.total_valid fun Hdisj _ _ => ?_ @@ -148,16 +157,19 @@ theorem localUpdate_dealloc_empty {X Z : S} : conv => rhs; rw [Heq] exact localUpdate_dealloc +@[rocq_alias gset_disj_dealloc_op_local_update] theorem localUpdate_op_l {X Y Z : S} : (valid Z • valid X, valid Z • valid Y) ~l~> (valid X, valid Y) := by suffices (valid Z • valid X, valid Z • valid Y) ~l~> (valid X, unit • valid Y) by rwa [show UCMRA.unit • valid Y ≡ valid Y by apply unit_left_id] at this exact LocalUpdate.op_frame _ _ _ _ _ localUpdate_dealloc_empty +@[rocq_alias gset_disj_alloc_op_local_update] theorem localUpdate_op_r {X Y Z : S} (Hdisj : Z ## X) : (valid X, valid Y) ~l~> (valid Z • valid X, valid Z • valid Y) := LocalUpdate.op_discrete _ _ _ fun _ => valid_op_iff_disj.mpr Hdisj +@[rocq_alias gset_disj_alloc_local_update] theorem localUpdate_union_r_of_disj (X Y Z : S) (Hdisj : Z ## X) : (valid X, valid Y) ~l~> (valid (Z ∪ X), valid (Z ∪ Y)) := by refine LocalUpdate.total_valid fun vx vy inc => ?_ @@ -165,12 +177,14 @@ theorem localUpdate_union_r_of_disj (X Y Z : S) (Hdisj : Z ## X) : rw [←disj_op_union Hdisj, ←disj_op_union HdisjY] exact localUpdate_op_r Hdisj +@[rocq_alias gset_disj_alloc_empty_local_update] theorem localUpdate_alloc_empty_of_disj (X Z : S) (Hdisj : Z ## X) : (valid X, valid ∅) ~l~> (valid (Z ∪ X), valid Z) := by rw [show valid Z ≡ valid (Z ∪ ∅) by simp [union_empty_right]] exact localUpdate_union_r_of_disj X ∅ Z Hdisj +@[rocq_alias gset_disj_alloc_updateP_strong] theorem alloc_updateP_strong {P : A → Prop} {Q : DisjointLeibnizSet S → Prop} {X : S} (Hfresh : ∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) (HQ : ∀ {i}, i ∉ X → P i → Q (valid ({i} ∪ X))) : valid X ~~>: Q := by @@ -185,10 +199,12 @@ theorem alloc_updateP_strong {P : A → Prop} {Q : DisjointLeibnizSet S → Prop · exact (Hnotin <| mem_union.mpr <| .inr ·) · grind [Hdisj i] +@[rocq_alias gset_disj_alloc_updateP_strong'] theorem alloc_updateP_strong' {P : A → Prop} {X : S} (H : ∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) : valid X ~~>: fun Y => ∃ i, Y = valid ({i} ∪ X) ∧ i ∉ X ∧ P i := alloc_updateP_strong H (by grind) +@[rocq_alias gset_disj_alloc_empty_updateP_strong] theorem alloc_empty_updateP_strong {P : A → Prop} {Q : DisjointLeibnizSet S → Prop} (Hfresh : ∀ Y : S, ∃ j, j ∉ Y ∧ P j) (Hvalid : ∀ {i}, P i → Q (valid {i})) : valid ∅ ~~>: Q := by @@ -196,6 +212,7 @@ theorem alloc_empty_updateP_strong {P : A → Prop} {Q : DisjointLeibnizSet S rw [union_empty_right] exact Hvalid HP +@[rocq_alias gset_disj_alloc_empty_updateP_strong'] theorem alloc_empty_updateP_strong' {P : A → Prop} (Hfresh : ∀ Y : S, ∃ j, j ∉ Y ∧ P j) : valid (∅ : S) ~~>: fun Y => ∃ i, Y = valid {i} ∧ P i := by refine alloc_updateP_strong (fun _ => Hfresh ·) ?_ @@ -208,26 +225,31 @@ namespace DisjointLeibnizSet variable {S : Type _} [LawfulFiniteSet S A] [DecidableDisj S] [InfiniteType A] +@[rocq_alias gset_disj_alloc_updateP] theorem alloc_updateP {Q : DisjointLeibnizSet S → Prop} {X} (Hv : ∀ {i}, i ∉ X → Q (valid ({i} ∪ X))) : valid X ~~>: Q := by refine alloc_updateP_strong (P := fun _ => True) (fun Y H => ?_) (fun _ => Hv ·) obtain ⟨a, _⟩ := FiniteSet.fresh Y exists a +@[rocq_alias gset_disj_alloc_updateP'] theorem alloc_updateP' {X : S} : valid X ~~>: fun Y => ∃ i : A, Y = valid ({i} ∪ X) ∧ i ∉ X := alloc_updateP (by grind) +@[rocq_alias gset_disj_alloc_empty_updateP] theorem alloc_empty_updateP {Q : DisjointLeibnizSet S → Prop} (Hv : ∀ {i}, Q (valid {i})) : valid ∅ ~~>: Q := by refine alloc_updateP (fun i => ?_) rw [union_empty_right] exact Hv +@[rocq_alias gset_disj_alloc_empty_updateP'] theorem alloc_empty_updateP' : valid (∅ : S) ~~>: fun Y => ∃ i, Y = valid {i} := alloc_empty_updateP (by grind) end DisjointLeibnizSet +@[rocq_alias gsetR] inductive LeibnizSet (S : Type _) where | valid (s : S) @@ -262,12 +284,15 @@ instance : UCMRA (LeibnizSet S) where unit_left_id := by simp [op, union_empty_left] pcore_unit := by simp [pcore, pcore] +@[rocq_alias gset_op] theorem op_union (X Y : S) : (valid X) • (valid Y) ≡ valid (X ∪ Y) := by simp [op] +@[rocq_alias gset_core] theorem core_equiv (X : LeibnizSet S) : core X ≡ X := by change (pcore X).getD X ≡ X simp [pcore] +@[rocq_alias gset_included] theorem included_iff_subset (X Y : S) : valid X ≼ valid Y ↔ X ⊆ Y := by simp only [Included, op] refine ⟨fun ⟨_, H⟩ => ?_, fun Hsub => ?_⟩ diff --git a/Iris/Iris/Algebra/LocalUpdates.lean b/Iris/Iris/Algebra/LocalUpdates.lean index 1888c892c..06ef04ce0 100644 --- a/Iris/Iris/Algebra/LocalUpdates.lean +++ b/Iris/Iris/Algebra/LocalUpdates.lean @@ -6,11 +6,13 @@ Authors: Сухарик (@suhr), Mario Carneiro module public import Iris.Algebra.CMRA +meta import Iris.Std.RocqPorting @[expose] public section namespace Iris +@[rocq_alias local_update] def LocalUpdate [CMRA α] (x y : α × α) : Prop := ∀n mz, ✓{n} x.1 → x.1 ≡{n}≡ x.2 •? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 •? mz @@ -48,12 +50,14 @@ theorem LocalUpdate.equiv_right (x : α × α) {y z : α × α} (h : y ≡ z) : -- Global Instance local_update_preorder : PreOrder (@local_update SI A). -- Proof. split; unfold local_update; red; naive_solver. Qed. +@[rocq_alias exclusive_local_update] theorem LocalUpdate.exclusive [CMRA.Exclusive y] {x x' : α} (vx' : ✓ x') : (x, y) ~l~> (x', x') := by intro n mz vx e cases CMRA.none_of_excl_valid_op ((OFE.Dist.validN e).mp vx) exact ⟨vx'.validN, .rfl⟩ +@[rocq_alias op_local_update] theorem LocalUpdate.op {x y z : α} (h : ∀ n, ✓{n} x → ✓{n} (z • x)) : (x, y) ~l~> (z • x, z • y) := by refine fun n mz vx e => ⟨h n vx, ?_⟩ @@ -61,10 +65,12 @@ theorem LocalUpdate.op {x y z : α} (z • x) ≡{n}≡ z • (y •? mz) := e.op_r _ ≡{n}≡ (z • y) •? mz := OFE.Dist.symm (CMRA.op_opM_assoc_dist z y mz) +@[rocq_alias op_local_update_discrete] theorem LocalUpdate.op_discrete [CMRA.Discrete α] (x y z : α) (h : ✓ x → ✓ (z • x)) : (x, y) ~l~> (z • x, z • y) := .op fun n vx => (h ((CMRA.valid_iff_validN' n).mpr vx)).validN +@[rocq_alias op_local_update_frame] theorem LocalUpdate.op_frame (x y x' y' yf : α) (h : (x, y) ~l~> (x', y')) : (x, y • yf) ~l~> (x', y' • yf) := by intro n mz vx e @@ -76,15 +82,18 @@ theorem LocalUpdate.op_frame (x y x' y' yf : α) x' ≡{n}≡ y' •? (some yf • mz) := h2 _ ≡{n}≡ (y' • yf) •? mz := Option.op_some_opM_assoc_dist.symm +@[rocq_alias cancel_local_update] theorem LocalUpdate.cancel (x y z : α) [CMRA.Cancelable x] : (x • y, x • z) ~l~> (y, z) := fun _ _ vx e => ⟨CMRA.validN_op_right vx, CMRA.op_opM_cancel_dist vx e⟩ +@[rocq_alias replace_local_update] theorem LocalUpdate.replace (x y : α) [CMRA.IdFree x] (h : ✓ y) : (x, x) ~l~> (y, y) := by intro _ mz vx e match mz with | none => exact ⟨h.validN, .rfl⟩ | some _ => cases CMRA.id_freeN_r vx e.symm +@[rocq_alias core_id_local_update] theorem LocalUpdate.core_id (x y z : α) [CMRA.CoreId y] (inc : y ≼ x) : (x, z) ~l~> (x, z • y) := by refine fun n mz vx e => ⟨vx, ?_⟩ refine (CMRA.op_core_right_of_inc inc).symm.dist.trans ?_ @@ -97,6 +106,7 @@ theorem LocalUpdate.core_id (x y z : α) [CMRA.CoreId y] (inc : y ≼ x) : (x, z _ ≡{n}≡ (y • z) • w := CMRA.op_assocN _ ≡{n}≡ (z • y) • w := CMRA.op_commN.op_l +@[rocq_alias local_update_discrete] theorem LocalUpdate.discrete [CMRA.Discrete α] (x y x' y' : α) : (x, y) ~l~> (x', y') ↔ ∀ mz, ✓ x → x ≡ y •? mz → (✓ x' ∧ x' ≡ y' •? mz) := by refine ⟨fun h mz vx e => ?_, fun h n mz vx e => ?_⟩ @@ -105,6 +115,7 @@ theorem LocalUpdate.discrete [CMRA.Discrete α] (x y x' y' : α) : · have ⟨vx', e'⟩ := h mz ((CMRA.valid_iff_validN' n).mpr vx) (OFE.discrete e) exact ⟨vx'.validN, e'.dist⟩ +@[rocq_alias local_update_valid0] theorem LocalUpdate.valid0 {x y x' y' : α} (h : ✓{0} x → ✓{0} y → some y ≼{0} some x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') := by @@ -113,15 +124,18 @@ theorem LocalUpdate.valid0 {x y x' y' : α} have : some y ≼{0} some x := CMRA.inc0_of_incN (Option.some_inc_some_of_dist_opM e) exact h (CMRA.valid0_of_validN vx) v0y this n mz vx e +@[rocq_alias local_update_valid] theorem LocalUpdate.valid [CMRA.Discrete α] {x y x' y' : α} (h : ✓ x → ✓ y → some y ≼ some x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') := .valid0 fun vx0 vy0 mz => h (CMRA.discrete_valid vx0) (CMRA.discrete_valid vy0) ((CMRA.inc_iff_incN 0).mpr mz) +@[rocq_alias local_update_total_valid0] theorem LocalUpdate.total_valid0 [CMRA.IsTotal α] {x y x' y' : α} (h : ✓{0} x → ✓{0} y → y ≼{0} x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') := .valid0 fun vx0 vy0 mz => h vx0 vy0 (Option.some_incN_some_iff_isTotal.mp mz) +@[rocq_alias local_update_total_valid] theorem LocalUpdate.total_valid [CMRA.IsTotal α] [CMRA.Discrete α] {x y x' y' : α} (h : ✓ x → ✓ y → y ≼ x → (x, y) ~l~> (x', y')) : (x, y) ~l~> (x', y') := .valid fun vx vy inc => h vx vy (Option.inc_of_some_inc_some inc) @@ -132,6 +146,7 @@ section UCMRA variable [UCMRA α] +@[rocq_alias local_update_unital] theorem local_update_unital {x y x' y' : α} : (x, y) ~l~> (x', y') ↔ ∀ n z, ✓{n} x → x ≡{n}≡ y • z → (✓{n} x' ∧ x' ≡{n}≡ y' • z) where mp h n z := h n (some z) @@ -142,6 +157,7 @@ theorem local_update_unital {x y x' y' : α} : ⟨h1, h2.trans (CMRA.unit_right_id_dist y')⟩ | some z => h n z vx e +@[rocq_alias local_update_unital_discrete] theorem local_update_unital_discrete [CMRA.Discrete α] (x y x' y' : α) : (x, y) ~l~> (x', y') ↔ ∀ z, ✓ x → x ≡ y • z → (✓ x' ∧ x' ≡ y' • z) where mp h z vx e := @@ -152,6 +168,7 @@ theorem local_update_unital_discrete [CMRA.Discrete α] (x y x' y' : α) : have ⟨vx', e'⟩ := h z ((CMRA.valid_iff_validN' n).mpr vnx) (OFE.discrete e) exact ⟨vx'.validN, e'.dist⟩ +@[rocq_alias cancel_local_update_unit] theorem cancel_local_update_unit (x y : α) [CMRA.Cancelable x] : (x • y, x) ~l~> (y, CMRA.unit) := have e : (x • y, x • CMRA.unit) ≡ (x • y, x) := ⟨.rfl, CMRA.unit_right_id⟩ .equiv_left _ e (.cancel x y CMRA.unit) @@ -167,8 +184,10 @@ theorem leibniz_discrete_unital_triv_local_update [OFE.Leibniz α] [CMRA.Discret end UCMRA +@[rocq_alias unit_local_update] theorem LocalUpdate.unit {x y x' y' : Unit} : (x, y) ~l~> (x', y') := .id ((), ()) +@[rocq_alias discrete_fun_local_update] theorem LocalUpdate.discrete_fun {β : α → Type _} [∀ x, UCMRA (β x)] {f g f' g' : ∀ x, β x} (h : ∀ x : α, (f x, g x) ~l~> (f' x, g' x)) : (f, g) ~l~> (f', g') := by @@ -182,6 +201,7 @@ theorem LocalUpdate.discrete_fun {β : α → Type _} [∀ x, UCMRA (β x)] variable [CMRA α] [CMRA β] +@[rocq_alias prod_local_update] theorem LocalUpdate.prod {x y x' y' : α × β} (hl : (x.1, y.1) ~l~> (x'.1, y'.1)) (hr : (x.2, y.2) ~l~> (x'.2, y'.2)) : (x, y) ~l~> (x', y') := by @@ -196,19 +216,23 @@ theorem LocalUpdate.prod {x y x' y' : α × β} have ⟨v₂, e₂⟩ := hr n (some z.snd) vx.right e.right exact ⟨⟨v₁, v₂⟩, ⟨e₁, e₂⟩⟩ +@[rocq_alias prod_local_update'] theorem LocalUpdate.prod' {x1 y1 x1' y1' : α} {x2 y2 x2' y2' : β} (hl : (x1, y1) ~l~> (x1', y1')) (hr : (x2, y2) ~l~> (x2', y2')) : ((x1, x2), (y1, y2)) ~l~> ((x1', x2'), (y1', y2')) := .prod hl hr +@[rocq_alias prod_local_update_1] theorem LocalUpdate.prod_1 {x1 y1 x1' y1' : α} (x2 y2 : β) (h : (x1, y1) ~l~> (x1', y1')) : ((x1, x2), (y1, y2)) ~l~> ((x1', x2), (y1', y2)) := .prod' h (.id _) +@[rocq_alias prod_local_update_2] theorem LocalUpdate.prod_2 (x1 y1 : α) {x2 y2 x2' y2' : β} (h : (x2, y2) ~l~> (x2', y2')) : ((x1, x2), (y1, y2)) ~l~> ((x1, x2'), (y1, y2')) := .prod' (.id _) h +@[rocq_alias option_local_update] theorem LocalUpdate.option {x y x' y' : α} (h : (x, y) ~l~> (x', y')) : (some x, some y) ~l~> (some x', some y') := by intro n mz @@ -216,12 +240,14 @@ theorem LocalUpdate.option {x y x' y' : α} | none | some none => exact h n none | some (some z) => exact h n (some z) +@[rocq_alias option_local_update_None] theorem LocalUpdate.option_none {α} [UCMRA α] {x x' y' : α} (h : (x, CMRA.unit) ~l~> (x', y')) : (some x, none) ~l~> (some x', some y') := by intro n mz vx e let .some (some z) := mz exact h n (some z) vx (.trans e (CMRA.unit_left_id_dist z).symm) +@[rocq_alias alloc_option_local_update] theorem LocalUpdate.alloc_option {x : α} (y : Option α) (vx : ✓ x) : (none, y) ~l~> (some x, some x) := by intro n mz _ e @@ -231,6 +257,7 @@ theorem LocalUpdate.alloc_option {x : α} (y : Option α) have ⟨_, hw⟩ := Option.exists_op_some_dist_some (n := n) y z cases e.trans hw +@[rocq_alias delete_option_local_update] theorem LocalUpdate.delete_option (x : Option α) (y : α) [CMRA.Exclusive y] : (x, some y) ~l~> (none, none) := by intro n mz vx e @@ -238,6 +265,7 @@ theorem LocalUpdate.delete_option (x : Option α) (y : α) [CMRA.Exclusive y] : | none | some none => exact ⟨trivial, .rfl⟩ | some (some z) => cases Option.not_valid_some_exclN_op_left <| (OFE.Dist.validN e).mp vx +@[rocq_alias delete_option_local_update_cancelable] theorem LocalUpdate.delete_option_cancelable (mx : Option α) [CMRA.Cancelable mx] : (mx, mx) ~l~> (none, none) := by intro _ mz vx e diff --git a/Iris/Iris/Algebra/Monoid.lean b/Iris/Iris/Algebra/Monoid.lean index 5ed8029cc..cb5fd2bf8 100644 --- a/Iris/Iris/Algebra/Monoid.lean +++ b/Iris/Iris/Algebra/Monoid.lean @@ -6,6 +6,7 @@ Authors: Zongyuan Liu module public import Iris.Algebra.OFE +meta import Iris.Std.RocqPorting public section @@ -21,6 +22,7 @@ open OFE /-- A commutative monoid on an OFE, used for big operators. The operation must be non-expansive, associative, commutative, and have a left identity. -/ +@[rocq_alias Monoid] class MonoidOps {M : Type u} [OFE M] (op : M → M → M) (unit : outParam M) where /-- The operation is non-expansive in both arguments -/ op_ne : NonExpansive₂ op @@ -39,11 +41,13 @@ attribute [instance] op_ne variable {M : Type u} [OFE M] {unit : M} {op : M → M → M} /-- The operation is proper with respect to equivalence. -/ +@[rocq_alias monoid_proper] theorem op_proper [MonoidOps op unit] (ha : a ≡ a') (hb : b ≡ b') : op a b ≡ op a' b' := NonExpansive₂.eqv ha hb /-- Right identity follows from commutativity and left identity. -/ -@[simp] theorem op_right_id [MonoidOps op unit] : op a unit ≡ a := +@[simp, rocq_alias monoid_right_id] +theorem op_right_id [MonoidOps op unit] : op a unit ≡ a := op_comm.trans op_left_id /-- Congruence on the left argument. -/ @@ -81,6 +85,7 @@ end MonoidOps /-! ## Monoid Homomorphisms -/ /-- A weak monoid homomorphism preserves the operation but not necessarily the unit. -/ +@[rocq_alias WeakMonoidHomomorphism] class WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂] @@ -99,6 +104,7 @@ class WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M map_op : ∀ {x y}, R (f (op₁ x y)) (op₂ (f x) (f y)) /-- A monoid homomorphism preserves both the operation and the unit. -/ +@[rocq_alias MonoidHomomorphism] class MonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂] diff --git a/Iris/Iris/Algebra/Numbers.lean b/Iris/Iris/Algebra/Numbers.lean index 302f549fc..a5c7b9e39 100644 --- a/Iris/Iris/Algebra/Numbers.lean +++ b/Iris/Iris/Algebra/Numbers.lean @@ -8,6 +8,7 @@ module public import Iris.Algebra.CMRA public import Iris.Algebra.OFE public import Iris.Algebra.LocalUpdates +meta import Iris.Std.RocqPorting /-! ## Numbers CMRA Simple CMRA's for commutative monoids. diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean index cba558a9b..9b529a422 100644 --- a/Iris/Iris/Algebra/OFE.lean +++ b/Iris/Iris/Algebra/OFE.lean @@ -12,6 +12,7 @@ public meta import Iris.Std.RocqPorting namespace Iris /-- Ordered family of equivalences -/ +@[rocq_alias ofe] class OFE (α : Type _) where Equiv : α → α → Prop Dist : Nat → α → α → Prop @@ -26,8 +27,10 @@ scoped notation:40 x " ≡{" n "}≡ " y:41 => OFE.Dist n x y namespace OFE +@[rocq_alias dist_lt] theorem Dist.lt [OFE α] {m n} {x y : α} : x ≡{n}≡ y → m < n → x ≡{m}≡ y := dist_lt +@[rocq_alias dist_le] theorem Dist.le [OFE α] {m n} {x y : α} (h : x ≡{n}≡ y) (h' : m ≤ n) : x ≡{m}≡ y := if hm : m = n then hm ▸ h else h.lt (Nat.lt_of_le_of_ne h' hm) @@ -36,6 +39,7 @@ theorem Dist.le [OFE α] {m n} {x y : α} (h : x ≡{n}≡ y) (h' : m ≤ n) : x theorem Dist.trans [OFE α] {n} {x : α} : x ≡{n}≡ y → y ≡{n}≡ z → x ≡{n}≡ z := dist_eqv.3 theorem Dist.of_eq [OFE α] {x y : α} : x = y → x ≡{n}≡ y := (· ▸ .rfl) +@[rocq_alias ofe_equivalence] theorem equiv_eqv [ofe : OFE α] : Equivalence ofe.Equiv := by constructor · rintro x; rw [ofe.equiv_dist]; rintro n; exact Dist.rfl @@ -55,25 +59,30 @@ instance [OFE α] {n : Nat} : Trans (OFE.Dist n) (OFE.Dist n) (OFE.Dist n : α trans := Dist.trans /-- A function `f : α → β` is non-expansive if it preserves `n`-equivalence. -/ +@[rocq_alias NonExpansive] class NonExpansive [OFE α] [OFE β] (f : α → β) where ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → f x₁ ≡{n}≡ f x₂ instance id_ne [OFE α] : NonExpansive (@id α) := ⟨fun _ _ _ h => h⟩ /-- Note: Not an instance, as any function can be decomposed as a composition in multiple ways. -/ +@[rocq_alias ccompose_ne] theorem NonExpansive.comp [OFE α] [OFE β] [OFE γ] {g : β → γ} {f : α → β} (hg : NonExpansive g) (hf : NonExpansive f) : NonExpansive (g ∘ f) := ⟨fun {_ _ _} h => hg.ne (hf.ne h)⟩ /-- A non-expansive function preserves equivalence. -/ +@[rocq_alias ne_proper] theorem NonExpansive.eqv [OFE α] [OFE β] {f : α → β} [NonExpansive f] ⦃x₁ x₂⦄ (h : x₁ ≡ x₂) : f x₁ ≡ f x₂ := equiv_dist.2 fun _ => ne (equiv_dist.1 h _) /-- A function `f : α → β → γ` is non-expansive if it preserves `n`-equivalence in each argument. -/ +@[rocq_alias NonExpansive2] class NonExpansive₂ [OFE α] [OFE β] [OFE γ] (f : α → β → γ) where ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → f x₁ y₁ ≡{n}≡ f x₂ y₂ +@[rocq_alias ne_proper_2] theorem NonExpansive₂.eqv [OFE α] [OFE β] [OFE γ] {f : α → β → γ} [NonExpansive₂ f] ⦃x₁ x₂⦄ (hx : x₁ ≡ x₂) ⦃y₁ y₂⦄ (hy : y₁ ≡ y₂) : f x₁ y₁ ≡ f x₂ y₂ := equiv_dist.2 fun _ => ne hx.dist hy.dist @@ -89,6 +98,7 @@ theorem NonExpansive₂.ne_left [OFE α] [OFE β] [OFE γ] (f : α → β → γ ⟨fun {_ _ _} h => ne h Dist.rfl⟩ /-- `DistLater n x y` means that `x` and `y` are `m`-equivalent for all `m < n`. -/ +@[rocq_alias dist_later] def DistLater [OFE α] (n : Nat) (x y : α) : Prop := ∀ m, m < n → x ≡{m}≡ y @[simp, refl] theorem DistLater.rfl [OFE α] {n} {x : α} : DistLater n x x := fun _ _ => .rfl @@ -98,53 +108,62 @@ theorem DistLater.trans [OFE α] {n} {x : α} (h1 : DistLater n x y) (h2 : DistL DistLater n x z := fun _ hm => (h1 _ hm).trans (h2 _ hm) /-- `DistLater n`-equivalence is an equivalence relation. -/ +@[rocq_alias dist_later_equivalence] theorem distLater_eqv [OFE α] {n} : Equivalence (α := α) (DistLater n) where refl _ := DistLater.rfl symm h := h.symm trans h1 := h1.trans /-- `n`-equivalence implies `DistLater n`-equivalence. -/ +@[rocq_alias dist_dist_later] theorem Dist.distLater [OFE α] {n} {x y : α} (h : x ≡{n}≡ y) : DistLater n x y := fun _ => dist_lt h /-- `DistLater n`-equivalence implies `m`-equivalence for all `m < n`. -/ +@[rocq_alias dist_later_dist_lt] theorem DistLater.dist_lt [OFE α] {m n} {x y : α} (h : DistLater n x y) (hm : m < n) : x ≡{m}≡ y := h _ hm /-- `DistLater 0`-equivalence is trivial. -/ -@[simp] theorem distLater_zero [OFE α] {x y : α} : DistLater 0 x y := nofun +@[simp, rocq_alias dist_later_0] theorem distLater_zero [OFE α] {x y : α} : DistLater 0 x y := nofun /-- `DistLater n`-equivalence is equivalent to `(n + 1)`-equivalence. -/ +@[rocq_alias dist_later_S] theorem distLater_succ [OFE α] {n} {x y : α} : DistLater n.succ x y ↔ x ≡{n}≡ y := ⟨(·.dist_lt (Nat.lt_succ_self _)), fun h1 _ h2 => h1.le (Nat.le_of_lt_succ h2)⟩ /-- A function `f : α → β` is contractive if it sends `DistLater n`-equivalent inputs to `n`-equivalent outputs. -/ +@[rocq_alias Contractive] class Contractive [OFE α] [OFE β] (f : α → β) where distLater_dist : DistLater n x y → f x ≡{n}≡ f y -@[simp] theorem Contractive.zero [OFE α] [OFE β] (f : α → β) [Contractive f] {x y} : - f x ≡{0}≡ f y := +@[simp, rocq_alias contractive_0] theorem Contractive.zero [OFE α] [OFE β] (f : α → β) + [Contractive f] {x y} : f x ≡{0}≡ f y := Contractive.distLater_dist distLater_zero +@[rocq_alias contractive_S] theorem Contractive.succ [OFE α] [OFE β] (f : α → β) [Contractive f] {n x y} (h : x ≡{n}≡ y) : f x ≡{n.succ}≡ f y := Contractive.distLater_dist (distLater_succ.2 h) /-- A contractive function is non-expansive. -/ +@[rocq_alias contractive_ne] instance ne_of_contractive [OFE α] [OFE β] (f : α → β) [Contractive f] : NonExpansive f where ne := fun _ _ _ h => Contractive.distLater_dist (Dist.distLater h) /-- A contractive function preserves equivalence. -/ +@[rocq_alias contractive_proper] theorem Contractive.eqv [OFE α] [OFE β] (f : α → β) [Contractive f] ⦃x y : α⦄ (h : x ≡ y) : f x ≡ f y := NonExpansive.eqv h /-- Constant functions are contractive. -/ +@[rocq_alias const_contractive] instance [OFE α] [OFE β] {x : β} : Contractive (fun _ : α => x) where distLater_dist := fun _ => Dist.rfl /-- The discrete OFE obtained from an equivalence relation `Equiv` -/ -@[reducible] +@[reducible, rocq_alias discrete_ofe_mixin] def ofDiscrete (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : OFE α where Equiv := Equiv Dist _ := Equiv @@ -153,24 +172,29 @@ def ofDiscrete (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : OF dist_lt h _ := h /-- A discrete element in an OFE -/ +@[rocq_alias Discrete] class DiscreteE {α : Type _} [OFE α] (x : α) : Prop where discrete : x ≡{0}≡ y → x ≡ y /-- A discrete OFE is one where equivalence is implied by `0`-equivalence. -/ +@[rocq_alias OfeDiscrete] class Discrete (α : Type _) [OFE α] where discrete_0 {x y : α} : x ≡{0}≡ y → x ≡ y export OFE.Discrete (discrete_0) /-- For discrete OFEs, `n`-equivalence implies equivalence for any `n`. -/ +@[rocq_alias discrete] theorem Discrete.discrete [OFE α] [Discrete α] {n} {x y : α} (h : x ≡{n}≡ y) : x ≡ y := discrete_0 (h.le (Nat.zero_le _)) export OFE.Discrete (discrete) /-- For discrete OFEs, `n`-equivalence implies equivalence for any `n`. -/ +@[rocq_alias discrete_iff_0] theorem Discrete.discrete_n [OFE α] [Discrete α] {n} {x y : α} (h : x ≡{0}≡ y) : x ≡{n}≡ y := (discrete h).dist export OFE.Discrete (discrete_n) +@[rocq_alias LeibnizEquiv] class Leibniz (α : Type _) [OFE α] where eq_of_eqv {x y : α} : x ≡ y → x = y export OFE.Leibniz (eq_of_eqv) @@ -181,7 +205,7 @@ export OFE.Leibniz (leibniz) /-- A morphism between OFEs, written `α -n> β`, is defined to be a function that is non-expansive. -/ -@[ext] structure Hom (α β : Type _) [OFE α] [OFE β] where +@[ext, rocq_alias ofe_mor] structure Hom (α β : Type _) [OFE α] [OFE β] where f : α → β ne : NonExpansive f @@ -192,11 +216,13 @@ instance [OFE α] [OFE β] : CoeFun (α -n> β) (fun _ => α → β) := ⟨Hom.f instance [OFE α] [OFE β] (f : α -n> β) : NonExpansive f := f.ne /-- The identity morphism on an OFE. -/ +@[rocq_alias cid] protected def Hom.id [OFE α] : α -n> α where f := id ne.ne _ _ _ := id /-- The composition of two morphisms between OFEs. -/ +@[rocq_alias ccompose] protected def Hom.comp [OFE α] [OFE β] [OFE γ] (g : β -n> γ) (f : α -n> β) : α -n> γ where f := g.f ∘ f.f ne.1 _ _ _ h := g.ne.1 (f.ne.1 h) @@ -230,6 +256,7 @@ theorem InvImage.equivalence {α : Sort u} {β : Sort v} symm := H.symm trans := H.trans +@[rocq_alias unit_ofe_mixin] instance : OFE Unit where Equiv _ _ := True Dist _ _ _ := True @@ -265,6 +292,7 @@ theorem _root_.Option.Forall₂.equivalence {R : α → α → Prop} symm {x y} := by cases x <;> cases y <;> simp [Option.Forall₂]; apply H.2 trans {x y z} := by cases x <;> cases y <;> cases z <;> simp [Option.Forall₂]; apply H.3 +@[rocq_alias option_ofe_mixin] instance [OFE α] : OFE (Option α) where Equiv := Option.Forall₂ Equiv Dist n := Option.Forall₂ (Dist n) @@ -272,6 +300,7 @@ instance [OFE α] : OFE (Option α) where equiv_dist {x y} := by cases x <;> cases y <;> simp [Option.Forall₂]; apply equiv_dist dist_lt {_ x y _} := by cases x <;> cases y <;> simp [Option.Forall₂]; apply dist_lt +@[rocq_alias option_ofe_discrete] instance [OFE α] [OFE.Discrete α] : OFE.Discrete (Option α) where discrete_0 {mx my} e := match mx, my with @@ -284,7 +313,8 @@ instance [OFE α] [OFE.Discrete α] : OFE.Discrete (Option α) where @[simp] theorem not_some_eqv_none [OFE α] {x : α} : ¬some x ≡ none := id @[simp] theorem not_none_eqv_some [OFE α] {x : α} : ¬none ≡ some x := id -@[simp] theorem some_dist_some [OFE α] {n} {x y : α} : (some x ≡{n}≡ some y) ↔ x ≡{n}≡ y := .rfl +@[simp, rocq_alias dist_Some] +theorem some_dist_some [OFE α] {n} {x y : α} : (some x ≡{n}≡ some y) ↔ x ≡{n}≡ y := .rfl @[simp] theorem not_some_dist_none [OFE α] {n} {x : α} : ¬some x ≡{n}≡ none := id @[simp] theorem not_none_dist_some [OFE α] {n} {x : α} : ¬none ≡{n}≡ some x := id @@ -293,9 +323,11 @@ theorem equiv_some [OFE α] {o : Option α} {y : α} (e : o ≡ some y) : let .some x := o exact ⟨x, rfl, e⟩ +@[rocq_alias dist_None] theorem equiv_none [OFE α] {o : Option α} : o ≡ none ↔ o = none := ⟨fun _ => let .none := o; rfl, (· ▸ .rfl)⟩ +@[rocq_alias dist_Some_inv_l] theorem dist_some [OFE α] {n mx y} (h : mx ≡{n}≡ some y) : ∃ z : α, mx = some z ∧ y ≡{n}≡ z := suffices hh : ∀ mx my y, mx ≡{n}≡ my → my = some y → ∃ t, mx = some t ∧ t ≡{n}≡ y from @@ -317,8 +349,10 @@ instance [OFE α] [Discrete α] : Discrete (Option α) where | none, none => H | some _, some _ => some_eqv_some.mpr (discrete_0 H) +@[rocq_alias Some_ne] instance OFE.Option.some.ne [OFE α] : OFE.NonExpansive (some : α → Option α) := ⟨fun _ _ _ => id⟩ +@[rocq_alias Some_discrete] theorem Option.some_is_discrete [OFE α] {a : α} (Ha : DiscreteE a) : DiscreteE (some a) := by constructor rintro (_|_) H @@ -332,6 +366,7 @@ theorem Option.ne_match [OFE α] {B : Type _} [OFE B] ⟨fun {n x' y'} (h : Option.Forall₂ (Dist n) x' y') => match x', y', h with | some _, some _, h => hf.ne h | none, none, _ => Dist.rfl⟩ +@[rocq_alias None_discrete] theorem Option.none_is_discrete [OFE α] : DiscreteE (none : Option α) := by constructor; rintro (_|_) <;> simp @@ -343,6 +378,7 @@ instance Option.merge_ne [OFE α] {op : α → α → α} [NonExpansive₂ op] : abbrev OFEFun {α : Type _} (β : α → Type _) := ∀ a, OFE (β a) +@[rocq_alias discrete_fun_ofe_mixin] instance [OFEFun (β : α → _)] : OFE ((x : α) → β x) where Equiv f g := ∀ x, f x ≡ g x Dist n f g := ∀ x, f x ≡{n}≡ g x @@ -354,6 +390,7 @@ instance [OFEFun (β : α → _)] : OFE ((x : α) → β x) where equiv_dist {_ _} := by simp [equiv_dist]; apply forall_comm dist_lt h1 h2 _ := dist_lt (h1 _) h2 +@[rocq_alias ofe_mor_ofe_mixin] instance [OFE α] [OFE β] : OFE (α -n> β) where Equiv f g := f.f ≡ g.f Dist n f g := f.f ≡{n}≡ g.f @@ -385,6 +422,7 @@ def mapCodHom [OFEFun (β₁ : α → _)] [OFEFun β₂] f f x := F x (f x) ne.1 _ _ _ H x := (F x).ne.1 (H x) +@[rocq_alias prod_ofe_mixin] instance [OFE α] [OFE β] : OFE (α × β) where Equiv a b := a.1 ≡ b.1 ∧ a.2 ≡ b.2 Dist n a b := a.1 ≡{n}≡ b.1 ∧ a.2 ≡{n}≡ b.2 @@ -414,9 +452,11 @@ theorem prod_mk_ne_left [OFE α] [OFE β] (b : β) : NonExpansive (β := α × theorem prod_mk_ne_right [OFE α] [OFE β] (a : α) : NonExpansive (β := α × β) (a, ·) := ⟨fun {_ _ _} h => dist_prod_ext Dist.rfl h⟩ +@[rocq_alias fst_ne] instance [OFE α] [OFE β] : NonExpansive (Prod.fst (α := α) (β := β)) := ⟨fun {_ _ _} h => dist_fst h⟩ +@[rocq_alias snd_ne] instance [OFE α] [OFE β] : NonExpansive (Prod.snd (α := α) (β := β)) := ⟨fun {_ _ _} h => dist_snd h⟩ @@ -425,11 +465,13 @@ theorem NonExpansive₂.uncurry [OFE α] [OFE β] [OFE γ] {f : α → β → γ NonExpansive (Function.uncurry f) := ⟨fun {_ _ _} (h : _ ∧ _) => hf.ne h.1 h.2⟩ +@[rocq_alias prod_discrete] theorem prod.is_discrete [OFE α] [OFE β] {a : α} {b : β} (Ha : DiscreteE a) (Hb : DiscreteE b) : DiscreteE (a, b) := by constructor intro y H; refine ⟨Ha.discrete H.1, Hb.discrete H.2⟩ +@[rocq_alias prod_ofe_discrete] instance [OFE α] [OFE β] [Discrete α] [Discrete β] : Discrete (α × β) where discrete_0 H := by constructor @@ -466,7 +508,7 @@ instance Hom.toSubtype_ne [OFE α] [OFE β] : NonExpansive (Hom.toSubtype (α := /-- An isomorphism between two OFEs is a pair of morphisms whose composition is equivalent to the identity morphism. -/ -@[ext] structure Iso (α β : Type _) [OFE α] [OFE β] where +@[ext, rocq_alias ofe_iso] structure Iso (α β : Type _) [OFE α] [OFE β] where hom : α -n> β inv : β -n> α hom_inv : hom (inv x) ≡ x @@ -511,6 +553,7 @@ theorem Iso.inv_dist [OFE α] [OFE β] (iso : Iso α β) {n} ⦃x y⦄ : Dist.trans (NonExpansive.ne h) (iso.hom_inv_dist)⟩ /-- The identity OFE isomorphism -/ +@[rocq_alias iso_ofe_refl] def Iso.id [OFE α] : Iso α α where hom := Hom.id inv := Hom.id @@ -520,6 +563,7 @@ def Iso.id [OFE α] : Iso α α where @[simp] theorem Iso.id_apply [OFE α] {x} : ((Iso.id : Iso α α) : α -n> α) x = x := rfl /-- The inverse of an OFE isomorphism -/ +@[rocq_alias iso_ofe_sym] def Iso.symm [OFE α] [OFE β] (iso : Iso α β) : Iso β α where hom := iso.inv inv := iso.hom @@ -527,6 +571,7 @@ def Iso.symm [OFE α] [OFE β] (iso : Iso α β) : Iso β α where inv_hom := by intro x; simp /-- Composition of OFE isomorphisms -/ +@[rocq_alias iso_ofe_trans] def Iso.comp [OFE α] [OFE β] [OFE γ] (iso1 : Iso β γ) (iso2 : Iso α β) : Iso α γ where hom := iso1.hom.comp iso2.hom inv := iso2.inv.comp iso1.inv @@ -541,7 +586,7 @@ end OFE /-- A chain in an OFE is a `Nat`-indexed sequence of elements that is upward-closed in terms of `n`-equivalence. -/ -structure Chain (α : Type _) [OFE α] where +@[rocq_alias chain] structure Chain (α : Type _) [OFE α] where chain : Nat → α cauchy : n ≤ i → chain i ≡{n}≡ chain n @@ -550,6 +595,7 @@ instance [OFE α] : CoeFun (Chain α) (fun _ => Nat → α) := ⟨Chain.chain⟩ namespace Chain /-- The constant chain. -/ +@[rocq_alias chain_const] def const [OFE α] (a : α) : Chain α where chain := fun _ => a cauchy _ := OFE.Dist.rfl @@ -557,6 +603,7 @@ def const [OFE α] (a : α) : Chain α where @[simp] theorem const_apply [OFE α] {a : α} {n} : const a n = a := rfl /-- Mapping a chain through a non-expansive function. -/ +@[rocq_alias chain_map] def map [OFE α] [OFE β] (f : α -n> β) (c : Chain α) : Chain β where chain n := f (c n) cauchy h := f.ne.1 (c.cauchy h) @@ -608,6 +655,7 @@ def chain_option_some [OFE V] {c : Chain (Option V)} (H : c n = some v) : simp [hcc] /-- Complete ordered family of equivalences -/ +@[rocq_alias Cofe] class IsCOFE (α : Type _) [OFE α] where compl : Chain α → α conv_compl {c : Chain α} : compl c ≡{n}≡ c n @@ -618,17 +666,20 @@ class abbrev COFE (α : Type _) := OFE α, IsCOFE α namespace COFE export IsCOFE (compl conv_compl) +@[rocq_alias conv_compl_le] theorem conv_compl' [COFE α] {c : Chain α} {n i} (h : n ≤ i) : compl c ≡{n}≡ c i := conv_compl.trans (c.cauchy h).symm /-- Chain maps commute with completion. -/ +@[rocq_alias compl_chain_map] theorem compl_map [COFE α] [COFE β] (f : α -n> β) (c : Chain α) : compl (Chain.map f c) ≡ f (compl c) := by refine OFE.equiv_dist.mpr (fun n => ?_) exact Dist.trans conv_compl (NonExpansive.ne (Dist.symm conv_compl)) /-- Constant chains complete to their constant value -/ -@[simp] theorem compl_const [COFE α] (a : α) : compl (Chain.const a) ≡ a := +@[simp, rocq_alias compl_chain_const] +theorem compl_const [COFE α] (a : α) : compl (Chain.const a) ≡ a := OFE.equiv_dist.mpr (fun _ => conv_compl) /-- Completion of discrete COFEs is the constant value. -/ @@ -636,7 +687,7 @@ theorem compl_map [COFE α] [COFE β] (f : α -n> β) (c : Chain α) : Discrete.discrete_0 conv_compl /-- The discrete COFE obtained from an equivalence relation `Equiv` -/ -@[reducible] +@[reducible, rocq_alias discrete_cofe] def ofDiscrete (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : COFE α := let _ := OFE.ofDiscrete Equiv equiv_eqv { compl := fun c => c 0 @@ -655,12 +706,14 @@ instance : COFE Unit where abbrev IsCOFEFun {α : Type _} (β : α → Type _) [OFEFun β] := ∀ x : α, IsCOFE (β x) +@[rocq_alias discrete_fun_cofe] instance {α : Type _} (β : α → Type _) [∀ x, COFE (β x)] : COFE ((x : α) → β x) where compl c x := compl (c.map (applyHom x)) conv_compl _ := IsCOFE.conv_compl abbrev OFunctorPre := ∀ α β [OFE α] [OFE β], Type _ +@[rocq_alias oFunctor] class OFunctor (F : OFunctorPre) where -- EXPERIMENT: Replacing COFE in this definition with OFE -- https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean/topic/OFunctor.20definition @@ -675,12 +728,14 @@ class OFunctor (F : OFunctorPre) where (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) : map (f.comp g) (g'.comp f') x ≡ map g g' (map f f' x) +@[rocq_alias oFunctorContractive] class OFunctorContractive (F : OFunctorPre) extends OFunctor F where map_contractive [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : Contractive (Function.uncurry (@map α₁ α₂ β₁ β₂ _ _ _ _)) attribute [reducible, instance] OFunctor.cofe +@[rocq_alias constOF] abbrev constOF (B : Type) : OFunctorPre := fun _ _ _ _ => B instance oFunctorConstOF [OFE B] : OFunctor (constOF B) where @@ -690,13 +745,14 @@ instance oFunctorConstOF [OFE B] : OFunctor (constOF B) where map_id := by simp map_comp := by simp +@[rocq_alias constOF_contractive] instance OFunctor.constOF_contractive [OFE B] : OFunctorContractive (constOF B) where map_contractive.1 := by simp [map] end COFE /- Leibniz OFE structure on a type -/ -@[ext] structure LeibnizO (α : Type _) where +@[ext, rocq_alias leibnizO] structure LeibnizO (α : Type _) where car : α -- Move? @@ -708,6 +764,7 @@ instance : COFE (LeibnizO α) := COFE.ofDiscrete _ Eq_Equivalence instance : Leibniz (LeibnizO α) := ⟨(·)⟩ instance {α : Type _} : OFE.Discrete (LeibnizO α) := ⟨congrArg id⟩ +@[rocq_alias leibnizO_leibniz] instance {α : Type _} : OFE.Leibniz (LeibnizO α) := ⟨congrArg id⟩ theorem LeibnizO.eqv_inj {x y : α} (H : LeibnizO.mk x ≡ LeibnizO.mk y) : x = y := @@ -719,6 +776,7 @@ theorem LeibnizO.dist_inj {x y : α} {n} (H : LeibnizO.mk x ≡{n}≡ LeibnizO.m section DiscreteFunOF open COFE +@[rocq_alias discrete_funOF] abbrev DiscreteFunOF {C : Type _} (F : C → OFunctorPre) : OFunctorPre := fun A B _ _ => (c : C) → F c A B @@ -735,11 +793,13 @@ end DiscreteFunOF section Option variable [OFE α] +@[rocq_alias option_chain] def optionChain (c : Chain (Option α)) (x : α) : Chain α := by refine ⟨fun n => (c n).getD x, fun {n i} H => ?_⟩ dsimp; have := c.cauchy H; revert this cases c.chain i <;> cases c.chain n <;> simp [Dist, Option.Forall₂] +@[rocq_alias option_cofe] instance isCOFE_option [IsCOFE α] : IsCOFE (Option α) where compl c := (c 0).map fun x => IsCOFE.compl (optionChain c x) conv_compl {n} c := by @@ -748,6 +808,7 @@ instance isCOFE_option [IsCOFE α] : IsCOFE (Option α) where refine fun _ => OFE.dist_eqv.trans IsCOFE.conv_compl ?_ simp [optionChain, e] +@[rocq_alias optionO_map] def optionMap {α β : Type _} [OFE α] [OFE β] (f : α -n> β) : Option α -n> Option β := by refine ⟨Option.map f, ⟨?_⟩⟩ rintro _ ⟨⟩ ⟨⟩ H <;> simp_all [Dist, Option.Forall₂] @@ -763,6 +824,7 @@ end Option section OptionOF open COFE +@[rocq_alias optionOF] abbrev OptionOF (F : OFunctorPre) : OFunctorPre := fun A B _ _ => Option (F A B) @@ -781,6 +843,7 @@ instance oFunctorOption [OFunctor F] : OFunctor (OptionOF F) where cases z <;> simp [optionMap, Equiv, Option.Forall₂] apply OFunctor.map_comp +@[rocq_alias optionOF_contractive] instance [OFunctorContractive F] : OFunctorContractive (OptionOF F) where map_contractive.1 H z := by have := (OFunctorContractive.map_contractive (F := F)).distLater_dist H @@ -790,30 +853,37 @@ end OptionOF section Fixpoint +@[rocq_alias LimitPreserving] def LimitPreserving [COFE α] (P : α → Prop) : Prop := ∀ (c : Chain α), (∀ n, P (c n)) → P (COFE.compl c) +@[rocq_alias limit_preserving_const] theorem LimitPreserving.const [COFE α] {P : Prop} : LimitPreserving fun (_ : α) => P := by simp [LimitPreserving] +@[rocq_alias limit_preserving_discrete] theorem LimitPreserving.discrete [COFE α] {P : α → Prop} : (∀ {x y : α}, x ≡{0}≡ y → (P x → P y)) → LimitPreserving P := fun Hdisc _ H => Hdisc COFE.conv_compl.symm (H _) +@[rocq_alias limit_preserving_and] theorem LimitPreserving.and [COFE α] {P Q : α → Prop} (HP : LimitPreserving P) (HQ : LimitPreserving Q) : LimitPreserving fun a => P a ∧ Q a := fun _ HPQ => ⟨HP _ (fun n => (HPQ n).left), HQ _ (fun n => (HPQ n).right)⟩ +@[rocq_alias limit_preserving_forall] theorem LimitPreserving.forall [COFE α] (P : β → α → Prop) (Hlim : ∀ y, LimitPreserving (P y)) : LimitPreserving (∀ y, P y ·) := fun c H y => Hlim y c (H · y) +@[rocq_alias limit_preserving_impl] theorem LimitPreserving.impl [COFE α] (P1 P2 : α → Prop) (HP1 : ∀ {x y : α}, x ≡{0}≡ y → P1 x → P1 y) (Hcompl : LimitPreserving P2) : LimitPreserving (fun x => P1 x → P2 x) := fun _ Hc HP1c => Hcompl _ <| fun n => Hc _ (HP1 (COFE.conv_compl' (Nat.zero_le n)) HP1c) +@[rocq_alias limit_preserving_equiv] theorem LimitPreserving.equiv [COFE α] [COFE β] (f g : α -n> β) : LimitPreserving (fun x => f x ≡ g x) := by intro c Hfg @@ -827,6 +897,7 @@ theorem LimitPreserving.equiv [COFE α] [COFE β] (f g : α -n> β) : theorem LimitPreserving.ext {α}[COFE α] {P Q : α -> Prop} (he : ∀ {x}, (P x ↔ Q x)) (hp : LimitPreserving P) : LimitPreserving Q := fun _ => (he.1 <| hp _ <| fun _ => he.2 <| · _) +@[rocq_alias fixpoint_chain] def Fixpoint.chain [OFE α] [Inhabited α] (f : α → α) [Contractive f] : Chain α where chain n := Nat.repeat f (n + 1) default cauchy {n} := by @@ -838,11 +909,13 @@ def Fixpoint.chain [OFE α] [Inhabited α] (f : α → α) [Contractive f] : Cha exact (IH H).le (Nat.le_of_lt_succ Hm) /-- Fixpoints inside of a COFE -/ +@[rocq_alias fixpoint] def fixpoint [COFE α] [Inhabited α] (f : α → α) [Contractive f] : α := COFE.compl <| Fixpoint.chain f nonrec abbrev OFE.ContractiveHom.fixpoint [COFE α] [Inhabited α] (f : α -c> α) : α := fixpoint f.f +@[rocq_alias fixpoint_unfold] theorem fixpoint_unfold [COFE α] [Inhabited α] (f : α -c> α) : fixpoint f ≡ f (fixpoint f) := by refine equiv_dist.mpr fun n => ?_ @@ -852,6 +925,7 @@ theorem fixpoint_unfold [COFE α] [Inhabited α] (f : α -c> α) : | zero => exact Contractive.zero f.f | succ _ IH => exact (Contractive.succ f.f IH.symm).symm +@[rocq_alias fixpoint_unique] theorem fixpoint_unique [COFE α] [Inhabited α] {f : α -c> α} {x : α} (H : x ≡ f x) : x ≡ fixpoint f := by refine equiv_dist.mpr fun n => ?_ @@ -859,6 +933,7 @@ theorem fixpoint_unique [COFE α] [Inhabited α] {f : α -c> α} {x : α} (H : x | zero => exact Contractive.zero f.f | succ _ IH => exact Contractive.succ f.f IH +@[rocq_alias fixpoint_ne] instance OFE.ContractiveHom.fixpoint_ne [COFE α] [Inhabited α] : NonExpansive (ContractiveHom.fixpoint (α := α)) where ne n f1 f2 H := by @@ -868,7 +943,7 @@ instance OFE.ContractiveHom.fixpoint_ne [COFE α] [Inhabited α] : | zero => exact H _ | succ _ IH => exact (H _).trans <| Contractive.succ _ <| IH <| Dist.lt H (Nat.lt_add_one _) -@[elab_as_elim] +@[elab_as_elim, rocq_alias fixpoint_ind] theorem OFE.ContractiveHom.fixpoint_ind [COFE α] [Inhabited α] (f : α -c> α) (P : α → Prop) (HProper : ∀ A B : α, A ≡ B → P A → P B) (x : α) (Hbase : P x) (Hind : ∀ x, P x → P (f x)) (Hlim : LimitPreserving P) : @@ -913,6 +988,7 @@ instance ne₂_of_contractive [OFE α] [OFE β] [OFE γ] (fB : α -c> β -c> γ) refine .trans ?_ ((fB.f x₂).ne.ne Hy) apply fB.ne.ne Hx +@[rocq_alias fixpoint_AB] def fixpointAB [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fB : α -c> β -c> β) (x : α) : β := by let con_hom : β -c> β := { f := fB x, @@ -920,6 +996,7 @@ def fixpointAB [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fB : α -c> β } exact con_hom.fixpoint +@[rocq_alias fixpoint_AB_contractive] theorem fixpointAB_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fB : α -c> β -c> β) : Contractive (fixpointAB fB) where distLater_dist {n _ _} Dl := by @@ -927,10 +1004,12 @@ theorem fixpointAB_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β] apply fB.contractive.distLater_dist exact Dl +@[rocq_alias fixpoint_AA] def fixpointAA [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) (x : α) : α := fA x (fixpointAB fB x) +@[rocq_alias fixpoint_AA_contractive] theorem fixpointAA_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : Contractive (fixpointAA fA fB) where distLater_dist {_ _ x₂} Dl := by @@ -938,6 +1017,7 @@ theorem fixpointAA_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β] apply fA.contractive.distLater_dist exact Dl +@[rocq_alias fixpoint_A] def fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : α := by let con_hom : α -c> α := { @@ -946,20 +1026,24 @@ def fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β } exact con_hom.fixpoint +@[rocq_alias fixpoint_B] def fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : β := fixpointAB fB <| fixpointA fA fB +@[rocq_alias fixpoint_A_unfold] theorem fixpointA_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : fA (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointA fA fB) := by exact .symm (fixpoint_unfold _) +@[rocq_alias fixpoint_B_unfold] theorem fixpointB_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : fB (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointB fA fB) := by exact .symm (fixpoint_unfold _) +@[rocq_alias fixpoint_A_unique] theorem fixpointA_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) (Hp : fA p q ≡ p) (Hq : fB p q ≡ q) : p ≡ (fixpointA fA fB) := by @@ -971,6 +1055,7 @@ theorem fixpointA_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β] have := ne₂_of_contractive fB exact Hq.symm.trans (NonExpansive₂.eqv (f := fB) Hp.symm .rfl) +@[rocq_alias fixpoint_B_unique] theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) (Hp : fA p q ≡ p) (Hq : fB p q ≡ q) : q ≡ (fixpointB fA fB) := by @@ -979,6 +1064,7 @@ theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β] refine Hq.symm.trans (NonExpansive₂.eqv (f := fB) ?_ .rfl) exact fixpointA_unique fA fB Hp Hq +@[rocq_alias fixpoint_A_ne] instance fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] : NonExpansive₂ (fixpointA (α := α) (β := β)) where ne n fA fA' HfA fB fB' HfB := by @@ -987,6 +1073,7 @@ instance fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] : refine ((ne₂_of_contractive_ne fA).ne .rfl ?_).trans (HfA z₁ _) exact ContractiveHom.fixpoint_ne.ne (HfB z₁) +@[rocq_alias fixpoint_B_ne] instance fixpointB_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] : NonExpansive₂ (fixpointB (α := α) (β := β)) where ne n fA fA' HfA fB fB' HfB := by @@ -999,9 +1086,11 @@ end FixpointAB section Later +@[rocq_alias later] structure Later (A : Type u) : Type u where next :: car : A +@[rocq_alias later_ofe_mixin] instance isOFE_later [OFE A] : OFE (Later A) where Equiv x y := x.car ≡ y.car Dist n x y := DistLater n x.car y.car @@ -1011,13 +1100,16 @@ instance isOFE_later [OFE A] : OFE (Later A) where exact ⟨by simp +contextual, fun H n => H (Nat.succ n) n (by simp)⟩ dist_lt Hxy Hmn _ Hkm := Hxy _ (Nat.lt_trans Hkm Hmn) +@[rocq_alias Next_contractive] instance NextContractive {A : Type _} [OFE A] : Contractive (@Later.next A) where distLater_dist := id +@[rocq_alias later_chain] def laterChain [OFE A] (c : Chain (Later A)) : Chain A where chain n := (c (Nat.succ n)).car cauchy Hle := c.cauchy (Nat.succ_le_succ Hle) _ (Nat.lt_succ_self _) +@[rocq_alias later_cofe] instance isCOFE_later [OFE A] [IsCOFE A] : IsCOFE (Later A) where compl c := Later.next (IsCOFE.compl (laterChain c)) conv_compl {n} c := by @@ -1025,6 +1117,7 @@ instance isCOFE_later [OFE A] [IsCOFE A] : IsCOFE (Later A) where intros m Hlt exact (IsCOFE.conv_compl (n := n') (c := laterChain c)).le (Nat.le_of_lt_succ Hlt) +@[rocq_alias laterO_map] def laterMap [OFE A] [OFE B] (f : A -n> B) : Later A -n> Later B := by refine ⟨fun x => Later.next (f x.car), ⟨?_⟩⟩ rintro _ ⟨⟩ ⟨⟩ H <;> simp_all only [Dist, DistLater] @@ -1035,6 +1128,7 @@ end Later section LaterOF open COFE +@[rocq_alias laterOF] abbrev LaterOF (F : OFunctorPre) : OFunctorPre := fun A B _ _ => Later (F A B) @@ -1047,6 +1141,7 @@ instance oFunctorLater [OFunctor F] : OFunctor (LaterOF F) where map_id _ := OFunctor.map_id _ map_comp _ _ _ _ _ := OFunctor.map_comp .. +@[rocq_alias laterOF_contractive] instance [OFunctorContractive F] : OFunctorContractive (LaterOF F) where map_contractive.1 H z m := Dist.lt <| by have := (OFunctorContractive.map_contractive (F := F)).distLater_dist H diff --git a/Iris/Iris/Algebra/UPred.lean b/Iris/Iris/Algebra/UPred.lean index 806e9b599..b9d6b2147 100644 --- a/Iris/Iris/Algebra/UPred.lean +++ b/Iris/Iris/Algebra/UPred.lean @@ -7,6 +7,7 @@ module public import Iris.Algebra.CMRA public import Iris.Algebra.OFE +meta import Iris.Std.RocqPorting @[expose] public section @@ -14,7 +15,7 @@ namespace Iris open CMRA /-- The data of a UPred object is an indexed proposition over M (Bundled version) -/ -@[ext] +@[ext, rocq_alias uPred] structure UPred (M : Type _) [UCMRA M] where holds : Nat → M → Prop mono {n1 n2 x1 x2} : holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → holds n2 x2 @@ -31,6 +32,7 @@ variable [UCMRA M] open UPred +@[rocq_alias uPredO] instance : OFE (UPred M) where Equiv P Q := ∀ n x, ✓{n} x → (P n x ↔ Q n x) Dist n P Q := ∀ n' x, n' ≤ n → ✓{n'} x → (P n' x ↔ Q n' x) @@ -44,17 +46,21 @@ instance : OFE (UPred M) where dist_lt Hdist Hlt _ _ Hle Hvalid := Hdist _ _ (Nat.le_trans Hle (Nat.le_of_succ_le Hlt)) Hvalid +@[rocq_alias uPred_ne] theorem uPred_ne {P : UPred M} {n} {m₁ m₂} (H : m₁ ≡{n}≡ m₂) : P n m₁ ↔ P n m₂ := ⟨fun H' => P.mono H' H.to_incN (Nat.le_refl _), fun H' => P.mono H' H.symm.to_incN (Nat.le_refl _)⟩ +@[rocq_alias uPred_proper] theorem uPred_proper {P : UPred M} {n} {m₁ m₂} (H : m₁ ≡ m₂) : P n m₁ ↔ P n m₂ := uPred_ne H.dist +@[rocq_alias uPred_holds_ne] theorem uPred_holds_ne {P Q : UPred M} {n₁ n₂ x} (HPQ : P ≡{n₂}≡ Q) (Hn : n₂ ≤ n₁) (Hx : ✓{n₂} x) (HQ : Q n₁ x) : P n₂ x := (HPQ _ _ (Nat.le_refl _) Hx).mpr (Q.mono HQ .rfl Hn) +@[rocq_alias uPred_cofe] instance : IsCOFE (UPred M) where compl c := { holds n x := ∀ n', n' ≤ n → ✓{n'} x → (c n') n' x @@ -66,9 +72,11 @@ instance : IsCOFE (UPred M) where refine ⟨fun H => H _ (Nat.le_refl _) Hv, fun H n' Hn' Hv' => ?_⟩ exact (c.cauchy Hn' _ _ (Nat.le_refl _) Hv').mp (mono _ H .rfl Hn') +@[rocq_alias uPredOF] abbrev UPredOF (F : COFE.OFunctorPre) [URFunctor F] : COFE.OFunctorPre := fun A B _ _ => UPred (F B A) +@[rocq_alias uPredO_map] def uPred_map [UCMRA α] [UCMRA β] (f : β -C> α) : UPred α -n> UPred β := by refine ⟨fun P => ⟨fun n x => P n (f x), ?_⟩, ⟨?_⟩⟩ · intro n1 n2 x1 x2 HP Hm Hn @@ -84,6 +92,7 @@ instance [URFunctor F] : COFE.OFunctor (UPredOF F) where map_id _ _ z _ := uPred_proper <| URFunctor.map_id z map_comp f g f' g' _ _ H _ := uPred_proper <| URFunctor.map_comp g' f' g f H +@[rocq_alias uPredOF_contractive] instance instUPredOFunctorContractive [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where map_contractive.1 {_ x y} HKL _ _ _ Hn _ := by refine uPred_ne <| (URFunctorContractive.map_contractive.1 diff --git a/Iris/Iris/Algebra/Updates.lean b/Iris/Iris/Algebra/Updates.lean index 688b6622c..c790d8878 100644 --- a/Iris/Iris/Algebra/Updates.lean +++ b/Iris/Iris/Algebra/Updates.lean @@ -6,15 +6,18 @@ Authors: Сухарик (@suhr) module public import Iris.Algebra.CMRA +meta import Iris.Std.RocqPorting @[expose] public section namespace Iris +@[rocq_alias cmra_updateP] def UpdateP [CMRA α] (x : α) (P : α → Prop) := ∀ n mz, ✓{n} (x •? mz) → ∃ y, P y ∧ ✓{n} (y •? mz) infixr:50 " ~~>: " => UpdateP +@[rocq_alias cmra_update] def Update [CMRA α] (x y : α) := ∀ n mz, ✓{n} (x •? mz) → ✓{n} (y •? mz) infixr:50 " ~~> " => Update @@ -49,12 +52,14 @@ instance [CMRA α] : Trans OFE.Equiv Update Update (α := α) where instance [CMRA α] : Trans Update OFE.Equiv Update (α := α) where trans u e := Update.equiv_right e u +@[rocq_alias cmra_update_updateP] theorem Update.of_updateP {x y : α} (h : x ~~>: (y = ·)) : x ~~> y := fun n mz v => let ⟨_, e, v⟩ := (h n mz v); e ▸ v theorem UpdateP.of_update {x y : α} (h : x ~~> y) : x ~~>: (y = ·) := fun n mz v => ⟨y, rfl, h n mz v⟩ +@[rocq_alias cmra_updateP_id] theorem UpdateP.id {P : α → Prop} {x} (h : P x) : x ~~>: P := fun _ _ v => ⟨x, h, v⟩ @@ -63,15 +68,19 @@ theorem Update.id {x : α} : x ~~> x := fun _ _ h => h theorem Update.trans {x y z : α} (uxy : x ~~> y) (uyz : y ~~> z) : x ~~> z := fun n mz v => uyz n mz (uxy n mz v) +@[rocq_alias cmra_updateP_compose] theorem UpdateP.trans {x : α} (ux : x ~~>: P) (upq : ∀ y, P y → y ~~>: Q) : x ~~>: Q := fun n mz v => let ⟨y, py, vy⟩ := ux n mz v; upq y py n mz vy +@[rocq_alias cmra_updateP_compose_l] theorem Update.transP {x y : α} (uxy : x ~~> y) (uyq : y ~~>: Q) : x ~~>: Q := fun n mz v => uyq n mz (uxy n mz v) +@[rocq_alias cmra_updateP_weaken] theorem UpdateP.weaken {x : α} (uxp : x ~~>: P) (pq : ∀ y, P y → Q y) : x ~~>: Q := fun n mz v => let ⟨y, py, vy⟩ := uxp n mz v; ⟨y, pq y py, vy⟩ +@[rocq_alias cmra_update_exclusive] theorem Update.exclusive {x y : α} [CMRA.Exclusive x] (vy : ✓ y) : x ~~> y := fun _ _ P => CMRA.none_of_excl_valid_op P ▸ vy.validN @@ -100,6 +109,7 @@ instance [CMRA α] : Trans Update UpdateP UpdateP (α := α) where -- Proper (cmra_update ==> flip cmra_update ==> flip impl) (@cmra_update SI A). -- Proof. Admitted. *) +@[rocq_alias cmra_updateP_op] theorem UpdateP.op {P Q R : α → Prop} {x y} (uxp : x ~~>: P) (uyq : y ~~>: Q) (pqr : ∀z w, P z → Q w → R (z • w)) : x • y ~~>: R := by intro n mz v @@ -113,10 +123,12 @@ theorem UpdateP.op {P Q R : α → Prop} {x y} let ⟨z, pz, vz⟩ := uxp n (some (w •? mz)) (CMRA.validN_ne e₂ vw) exact ⟨z • w, pqr z w pz pw, CMRA.validN_ne (CMRA.op_opM_assoc_dist z w mz).symm vz⟩ +@[rocq_alias cmra_updateP_op'] theorem UpdateP.op' {P Q : α → Prop} {x y : α} (uxp : x ~~>: P) (uyq : y ~~>: Q) : (x • y : α) ~~>: λ t ↦ ∃ z w, t = (z • w : α) ∧ P z ∧ Q w := .op uxp uyq fun z w pz qw => ⟨z, w, rfl, pz, qw⟩ +@[rocq_alias cmra_update_op] theorem Update.op {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x₂ ~~> y₂) : x₁ • x₂ ~~> y₁ • y₂ := .of_updateP <| .op (.of_update xy₁) (.of_update xy₂) fun _ _ ez ew => ez ▸ ew ▸ rfl @@ -136,17 +148,22 @@ theorem Update.op {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x -- Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)). -- Proof. Admitted. *) +@[rocq_alias cmra_update_op_l] theorem Update.op_l {x y : α} : x • y ~~> x := fun _ _ => CMRA.validN_op_opM_left +@[rocq_alias cmra_update_op_r] theorem Update.op_r {x y : α} : x • y ~~> y := fun _ _ => CMRA.validN_op_opM_right +@[rocq_alias cmra_update_included] theorem Update.included {x y : α} : x ≼ y → y ~~> x := fun ⟨_, ez⟩ => .equiv_left ez.symm .op_l +@[rocq_alias cmra_update_valid0] theorem Update.valid0 {x y : α} : (✓{0} x → x ~~> y) → x ~~> y := fun h n mz v => h (CMRA.valid0_of_validN (CMRA.validN_opM v)) n mz v /-! ## Frame preserving updates for total and discete CMRAs -/ +@[rocq_alias cmra_total_updateP] theorem UpdateP.total [CMRA.IsTotal α] : x ~~>: P ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ∃ y, P y ∧ ✓{n} (y • z) where mp uxp := fun n z v => uxp n (some z) v @@ -157,6 +174,7 @@ theorem UpdateP.total [CMRA.IsTotal α] : ⟨y, py, CMRA.validN_op_opM_left vy⟩ | some z => h n z v +@[rocq_alias cmra_total_update] theorem Update.total [CMRA.IsTotal α] : x ~~> y ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ✓{n} (y • z) where mp uxy := fun n z v => uxy n (some z) v @@ -166,6 +184,7 @@ theorem Update.total [CMRA.IsTotal α] : CMRA.validN_op_opM_left $ h n (CMRA.core x) (CMRA.validN_ne (CMRA.op_core_dist x).symm v) | some z => h n z v +@[rocq_alias cmra_discrete_updateP] theorem UpdateP.discrete [CMRA.Discrete α] : x ~~>: P ↔ ∀ (mz : Option α), ✓ (x •? mz) → ∃ y, P y ∧ ✓ (y •? mz) where mp uxp := fun mz v => @@ -175,11 +194,13 @@ theorem UpdateP.discrete [CMRA.Discrete α] : let ⟨y, py, vy⟩ := h mz ((CMRA.valid_iff_validN' n).mpr v) ⟨y, py, CMRA.Valid.validN vy⟩ +@[rocq_alias cmra_discrete_update] theorem Update.discrete [CMRA.Discrete α] {x y : α} : x ~~> y ↔ ∀ (mz : Option α), ✓ (x •? mz) → ✓ (y •? mz) where mp uxp := fun mz v => CMRA.discrete_valid $ uxp 0 mz (CMRA.Valid.validN v) mpr h := fun n mz v => CMRA.Valid.validN $ h mz ((CMRA.valid_iff_validN' n).mpr v) +@[rocq_alias cmra_discrete_total_updateP] theorem UpdateP.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] : x ~~>: P ↔ ∀ (z : α), ✓ (x • z) → ∃ y, P y ∧ ✓ (y • z) where mp uxp := fun z vz => @@ -190,6 +211,7 @@ theorem UpdateP.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] : let ⟨y, py, vy⟩ := h z ((CMRA.valid_iff_validN' n).mpr v) ⟨y, py, CMRA.Valid.validN vy⟩ +@[rocq_alias cmra_discrete_total_update] theorem Update.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] : x ~~> y ↔ ∀ (z : α), ✓ (x • z) → ✓ (y • z) where mp uxp := fun z vz => @@ -211,6 +233,7 @@ theorem Update.discrete_total [CMRA.Discrete α] [CMRA.IsTotal α] : -- End cmra_transport. /-! ## Isomorphism -/ +@[rocq_alias iso_cmra_updateP] theorem UpdateP.iso (gf : ∀ x, g (f x) ≡ x) (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2) @@ -233,6 +256,7 @@ theorem UpdateP.iso | some z => (g_op x (f z)).trans (CMRA.op_right_eqv (g x) (gf z)) exact ⟨g x, pq x px, CMRA.validN_ne this.dist ((g_validN n _).mpr vx)⟩ +@[rocq_alias iso_cmra_updateP'] theorem UpdateP.iso' (gf : ∀ x, g (f x) ≡ x) (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2) @@ -242,6 +266,7 @@ theorem UpdateP.iso' .iso f g gf g_op g_validN uyp fun z pz => ⟨z, rfl, pz⟩ /-! ## Lift -/ +@[rocq_alias cmra_update_lift_updateP] theorem Update.lift_updateP (x y : β) (H : ∀ P, x ~~>: P → g x ~~>: λ a' ↦ ∃ b', a' = g b' ∧ P b') (uxy : x ~~> y) : g x ~~> g y := @@ -251,6 +276,7 @@ theorem Update.lift_updateP (x y : β) ⟨z, hz.symm, vz⟩ /-! ## Product -/ +@[rocq_alias prod_updateP] theorem UpdateP.prod {P : α → Prop} {Q : β → Prop} {R : α × β → Prop} {x : α × β} (uxp : x.fst ~~>: P) (uxq : x.snd ~~>: Q) (pq : ∀ a b, P a → Q b → R (a, b)) : x ~~>: R := by @@ -265,14 +291,17 @@ theorem UpdateP.prod {P : α → Prop} {Q : β → Prop} {R : α × β → Prop} have ⟨y₂, qy, vy₂⟩ := uxq n (some z.snd) v.2 exact ⟨(y₁, y₂), pq y₁ y₂ py qy, ⟨vy₁, vy₂⟩⟩ +@[rocq_alias prod_updateP'] theorem UpdateP.prod' (P : α → Prop) (Q : β → Prop) (x : α × β) (uxp : x.fst ~~>: P) (uxq : x.snd ~~>: Q) : x ~~>: λ y ↦ P (y.fst) ∧ Q (y.snd) := .prod uxp uxq fun _ _ px qy => ⟨px, qy⟩ +@[rocq_alias prod_update] theorem Update.prod (x : α × β) (uxy₁ : x.fst ~~> y.fst) (uxy₂ : x.snd ~~> y.snd) : x ~~> y := .of_updateP <| .prod (.of_update uxy₁) (.of_update uxy₂) fun _ _ ya yb => Prod.ext ya yb /-! ## Option -/ +@[rocq_alias option_updateP] theorem UpdateP.option {P : α → Prop} {Q : Option α → Prop} {x : α} (uxp : x ~~>: P) (pq : ∀ y, P y → Q (some y)) : some x ~~>: Q := by intro n mz v @@ -280,8 +309,10 @@ theorem UpdateP.option {P : α → Prop} {Q : Option α → Prop} {x : α} | none | some none => let ⟨w, pw, vw⟩ := uxp n none v; exact ⟨w, pq w pw, vw⟩ | some (some z) => let ⟨w, pw, vw⟩ := uxp n (some z) v; exact ⟨w, pq w pw, vw⟩ +@[rocq_alias option_updateP'] theorem UpdateP.option' (P : α → Prop) (x : α) (uxp : x ~~>: P) : some x ~~>: Option.rec False P := .option uxp fun _ py => py +@[rocq_alias option_update] theorem Update.option (x y : α) (uxy : x ~~> y) : some x ~~> some y := .of_updateP <| .option (.of_update uxy) fun _ => congrArg some diff --git a/Iris/Iris/Algebra/View.lean b/Iris/Iris/Algebra/View.lean index ee563a2e3..1d5c2ab15 100644 --- a/Iris/Iris/Algebra/View.lean +++ b/Iris/Iris/Algebra/View.lean @@ -12,11 +12,13 @@ public import Iris.Algebra.DFrac public import Iris.Algebra.Agree public import Iris.Algebra.Updates public import Iris.Algebra.LocalUpdates +meta import Iris.Std.RocqPorting @[expose] public section open Iris +@[rocq_alias view_rel] abbrev ViewRel (A B : Type _) := Nat → A → B → Prop class IsViewRel [OFE A] [UCMRA B] (R : ViewRel A B) where @@ -24,6 +26,7 @@ class IsViewRel [OFE A] [UCMRA B] (R : ViewRel A B) where rel_validN n a b : R n a b → ✓{n} b rel_unit n : ∃ a, R n a UCMRA.unit +@[rocq_alias ViewRelDiscrete] class IsViewRelDiscrete [OFE A] [UCMRA B] (R : ViewRel A B) extends IsViewRel R where discrete n a b : R 0 a b → R n a b @@ -32,21 +35,26 @@ open IsViewRel DFrac variable [OFE A] [UCMRA B] {R : ViewRel A B} [IsViewRel R] +@[rocq_alias view_rel_ne] theorem iff_of_dist (Ha : a1 ≡{n}≡ a2) (Hb : b1 ≡{n}≡ b2) : R n a1 b1 ↔ R n a2 b2 := ⟨(mono · Ha Hb.symm.to_incN n.le_refl), (mono · Ha.symm Hb.to_incN n.le_refl)⟩ +@[rocq_alias view_rel_proper] theorem iff_of_equiv (Ha : a1 ≡ a2) (Hb : b1 ≡ b2) : R n a1 b1 ↔ R n a2 b2 := iff_of_dist Ha.dist Hb.dist end ViewRel +@[rocq_alias view] structure View (F : Type _) {A B : Type _} (R : ViewRel A B) where auth : Option ((DFrac F) × Agree A) frag : B +@[rocq_alias view_auth] abbrev View.Auth [UCMRA B] {R : ViewRel A B} (dq : DFrac F) (a : A) : View F R := ⟨some (dq, toAgree a), UCMRA.unit⟩ +@[rocq_alias view_frag] abbrev View.Frag {R : ViewRel A B} (b : B) : View F R := ⟨none, b⟩ notation "●V{" dq "} " a => View.Auth dq a @@ -58,9 +66,12 @@ section OFE open OFE UCMRA variable [OFE A] [OFE B] {R : ViewRel A B} +@[rocq_alias view_equiv] def equiv (x y : View F R) : Prop := x.auth ≡ y.auth ∧ x.frag ≡ y.frag +@[rocq_alias view_dist] def dist (n : Nat) (x y : View F R) : Prop := x.auth ≡{n}≡ y.auth ∧ x.frag ≡{n}≡ y.frag +@[rocq_alias viewO] instance : OFE (View F R) where Equiv := equiv Dist := dist @@ -74,25 +85,33 @@ instance : OFE (View F R) where fun H => ⟨equiv_dist.mpr (H · |>.1), equiv_dist.mpr (H · |>.2)⟩⟩ dist_lt H Hn := ⟨dist_lt H.1 Hn, dist_lt H.2 Hn⟩ +@[rocq_alias View_ne] instance mk.ne : NonExpansive₂ (mk : _ → _ → View F R) := ⟨fun _ _ _ Ha _ _ Hb => ⟨Ha, Hb⟩⟩ +@[rocq_alias view_auth_proj_ne] instance auth.ne : NonExpansive (auth : View F R → _) := ⟨fun _ _ _ H => H.1⟩ +@[rocq_alias view_frag_proj_ne] instance frag.ne : NonExpansive (frag : View F R → _) := ⟨fun _ _ _ H => H.2⟩ +@[rocq_alias View_discrete] theorem discrete {ag : Option ((DFrac F) × Agree A)} (Ha : DiscreteE ag) (Hb : DiscreteE b) : DiscreteE (α := View F R) (mk ag b) := ⟨fun H => ⟨Ha.discrete H.1, Hb.discrete H.2⟩⟩ +@[rocq_alias view_ofe_discrete] instance [Discrete A] [Discrete B] : Discrete (View F R) where discrete_0 H := ⟨discrete_0 H.1, discrete_0 H.2⟩ +@[rocq_alias view_auth_dist_inj] theorem auth_inj_frac [UCMRA B] {q1 q2 : DFrac F} {a1 a2 : A} {n} (H : (●V{q1} a1 : View F R) ≡{n}≡ ●V{q2} a2) : q1 = q2 := H.1.1 theorem dist_of_auth_dist [UCMRA B] {q1 q2 : DFrac F} {a1 a2 : A} {n} (H : (●V{q1} a1 : View F R) ≡{n}≡ ●V{q2} a2) : a1 ≡{n}≡ a2 := toAgree.inj H.1.2 +@[rocq_alias view_frag_dist_inj] theorem dist_of_frag_dist [UCMRA B] {b1 b2 : B} {n} (H : (◯V b1 : View F R) ≡{n}≡ ◯V b2) : b1 ≡{n}≡ b2 := H.2 +@[rocq_alias view_auth_discrete] theorem auth_discrete [UFraction F] [UCMRA B] {dq a} (Ha : DiscreteE a) (He : DiscreteE (unit : B)) : DiscreteE (●V{dq} a : View F R) := by refine discrete ?_ He @@ -100,6 +119,7 @@ theorem auth_discrete [UFraction F] [UCMRA B] {dq a} (Ha : DiscreteE a) (He : Di refine prod.is_discrete DFrac.is_discrete ?_ exact Agree.toAgree.is_discrete Ha +@[rocq_alias view_frag_discrete] theorem frag_discrete [UCMRA B] (Hb : DiscreteE b) : (DiscreteE (◯V b : View F R)) := discrete Option.none_is_discrete Hb @@ -117,6 +137,7 @@ theorem IsViewRel.of_agree_dist_iff (Hb : b' ≡{n}≡ b) : exact mono HR (inj HA.symm) Hb.symm.to_incN n.le_refl · exact ⟨a, .rfl, mono H .rfl Hb.to_incN n.le_refl⟩ +@[rocq_alias view_auth_ne] instance auth_ne {dq : DFrac F} : NonExpansive (Auth dq : A → View F R) where ne _ _ _ H := by refine mk.ne.ne ?_ .rfl @@ -131,25 +152,31 @@ instance auth_ne₂ : NonExpansive₂ (Auth : DFrac F → A → View F R) where refine NonExpansive.ne ?_ exact dist_prod_ext Hq (NonExpansive.ne Hf) +@[rocq_alias view_frag_ne] instance frag_ne : NonExpansive (Frag : B → View F R) where ne _ _ _ H := mk.ne.ne .rfl H -@[simp] def Valid (v : View F R) : Prop := +@[rocq_alias view_valid_instance, simp] +def Valid (v : View F R) : Prop := match v.auth with | some (dq, ag) => ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ toAgree a ∧ R n a (frag v)) | none => ∀ n, ∃ a, R n a (frag v) -@[simp] def ValidN (n : Nat) (v : View F R) : Prop := +@[rocq_alias view_validN_instance, simp] +def ValidN (n : Nat) (v : View F R) : Prop := match v.auth with | some (dq, ag) => ✓{n} dq ∧ (∃ a, ag ≡{n}≡ toAgree a ∧ R n a (frag v)) | none => ∃ a, R n a (frag v) -@[simp] def Pcore (v : View F R) : Option (View F R) := +@[rocq_alias view_pcore_instance, simp] +def Pcore (v : View F R) : Option (View F R) := some <| mk (CMRA.core v.auth) (CMRA.core v.frag) -@[simp] def Op (v1 v2 : View F R) : View F R := +@[rocq_alias view_op_instance, simp] +def Op (v1 v2 : View F R) : View F R := mk (v1.auth • v2.auth) (v1.frag • v2.frag) +@[rocq_alias viewR] instance : CMRA (View F R) where pcore := Pcore op := Op @@ -244,6 +271,7 @@ instance : CMRA (View F R) where exists ⟨z1.1, z1.2⟩ exists ⟨z2.1, z2.2⟩ +@[rocq_alias view_cmra_discrete] instance [Discrete A] [CMRA.Discrete B] [IsViewRelDiscrete R] : CMRA.Discrete (View F R) where discrete_valid {x} := by simp only [CMRA.ValidN, ValidN, CMRA.Valid, Valid] @@ -254,37 +282,47 @@ instance [Discrete A] [CMRA.Discrete B] [IsViewRelDiscrete R] : CMRA.Discrete (V · exact IsViewRelDiscrete.discrete _ _ _ H3 · exact fun ⟨a, H⟩ _ => ⟨a, IsViewRelDiscrete.discrete _ _ _ H⟩ +@[rocq_alias viewUR] instance : UCMRA (View F R) where unit := ⟨UCMRA.unit, UCMRA.unit⟩ unit_valid := IsViewRel.rel_unit unit_left_id := ⟨UCMRA.unit_left_id, UCMRA.unit_left_id⟩ pcore_unit := ⟨.rfl, CMRA.core_eqv_self UCMRA.unit⟩ +@[rocq_alias view_auth_dfrac_op] theorem auth_op_auth_eqv : (●V{dq1 • dq2} a : View F R) ≡ (●V{dq1} a) • ●V{dq2} a := ⟨⟨rfl, Agree.idemp.symm⟩, UCMRA.unit_left_id.symm⟩ +@[rocq_alias view_frag_op] theorem frag_op_eq : (◯V (b1 • b2) : View F R) = ((◯V b1) • ◯V b2 : View F R) := rfl +@[rocq_alias view_frag_mono] theorem frag_inc_of_inc (H : b1 ≼ b2) : (◯V b1 : View F R) ≼ ◯V b2 := by rcases H with ⟨c, H⟩ refine CMRA.inc_of_inc_of_eqv ?_ (NonExpansive.eqv H.symm) rw [frag_op_eq] exact CMRA.inc_op_left _ _ +@[rocq_alias view_frag_core] theorem frag_core : CMRA.core (◯V b : View F R) = ◯V (CMRA.core b) := rfl +@[rocq_alias view_both_core_discarded] theorem auth_discard_op_frag_core : CMRA.core ((●V{.discard} a) • ◯V b : View F R) ≡ (●V{.discard} a) • ◯V (CMRA.core b) := ⟨.rfl, (CMRA.core_ne.eqv UCMRA.unit_left_id).trans UCMRA.unit_left_id.symm⟩ +@[rocq_alias view_both_core_frac] theorem auth_own_op_frag_core : CMRA.core ((●V{.own q} a) • ◯V b : View F R) ≡ ◯V (CMRA.core b) := ⟨trivial, CMRA.core_ne.eqv UCMRA.unit_left_id⟩ +@[rocq_alias view_auth_core_id] instance : CMRA.CoreId (●V{.discard} a : View F R) where core_id := ⟨.rfl, CMRA.core_eqv_self UCMRA.unit⟩ +@[rocq_alias view_frag_core_id] instance [CMRA.CoreId b] : CMRA.CoreId (◯V b : View F R) where core_id := ⟨.rfl, CMRA.coreId_iff_core_eqv_self.mp (by trivial)⟩ +@[rocq_alias view_both_core_id] instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View F R) • ◯V b) where core_id := by refine ⟨.rfl, ?_⟩ @@ -292,20 +330,25 @@ instance [CMRA.CoreId b] : CMRA.CoreId ((●V{.discard} a : View F R) • ◯V b refine (CMRA.coreId_iff_core_eqv_self.mp (by trivial)).trans ?_ refine UCMRA.unit_left_id.symm +@[rocq_alias view_auth_dfrac_op_invN] theorem dist_of_validN_auth (H : ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡{n}≡ a2 := by rcases H with ⟨_, _, H, _⟩ refine toAgree.inj (Agree.op_invN ?_) exact Agree.validN_ne H.symm trivial +@[rocq_alias view_auth_dfrac_op_inv] theorem eqv_of_valid_auth (H : ✓ ((●V{dq1} a1 : View F R) • ●V{dq2} a2)) : a1 ≡ a2 := equiv_dist.mpr fun _ => dist_of_validN_auth H.validN +@[rocq_alias view_auth_dfrac_validN] theorem auth_validN_iff : ✓{n} (●V{dq} a : View F R) ↔ ✓{n}dq ∧ R n a UCMRA.unit := and_congr_right fun _ => IsViewRel.of_agree_dist_iff .rfl +@[rocq_alias view_auth_validN] theorem auth_one_validN_iff n a : ✓{n} (●V a : View F R) ↔ R n a UCMRA.unit := ⟨(auth_validN_iff.mp · |>.2), (auth_validN_iff.mpr ⟨UFraction.one_whole.1, ·⟩)⟩ +@[rocq_alias view_auth_dfrac_op_validN] theorem auth_op_auth_validN_iff : ✓{n} ((●V{dq1} a1 : View F R) • ●V{dq2} a2) ↔ ✓(dq1 • dq2) ∧ a1 ≡{n}≡ a2 ∧ R n a1 UCMRA.unit := by refine ⟨fun H => ?_, fun H => ?_⟩ @@ -323,26 +366,33 @@ theorem auth_op_auth_validN_iff : · refine mono H.2.2 .rfl ?_ n.le_refl exact OFE.Dist.to_incN <| CMRA.unit_left_id_dist UCMRA.unit +@[rocq_alias view_auth_op_validN] theorem auth_one_op_auth_one_validN_iff : ✓{n} ((●V a1 : View F R) • ●V a2) ↔ False := by refine auth_op_auth_validN_iff.trans ?_ simp only [iff_false, not_and] refine fun _ => (UFraction.one_whole (α := F)).2 ?_ |>.elim exists 1 +@[rocq_alias view_frag_validN] theorem frag_validN_iff : ✓{n} (◯V b : View F R) ↔ ∃ a, R n a b := by rfl +@[rocq_alias view_both_dfrac_validN] theorem auth_op_frag_validN_iff : ✓{n} ((●V{dq} a : View F R) • ◯V b) ↔ ✓dq ∧ R n a b := and_congr_right (fun _ => IsViewRel.of_agree_dist_iff <| CMRA.unit_left_id_dist b) +@[rocq_alias view_both_validN] theorem auth_one_op_frag_validN_iff : ✓{n} ((●V a : View F R) • ◯V b) ↔ R n a b := auth_op_frag_validN_iff.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one) +@[rocq_alias view_auth_dfrac_valid] theorem auth_valid_iff : ✓ (●V{dq} a : View F R) ↔ ✓dq ∧ ∀ n, R n a UCMRA.unit := and_congr_right (fun _=> forall_congr' fun _ => IsViewRel.of_agree_dist_iff .rfl) +@[rocq_alias view_auth_valid] theorem auth_one_valid_iff : ✓ (●V a : View F R) ↔ ∀ n, R n a UCMRA.unit := auth_valid_iff.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one) +@[rocq_alias view_auth_dfrac_op_valid] theorem auth_op_auth_valid_iff : ✓ ((●V{dq1} a1 : View F R) • ●V{dq2} a2) ↔ ✓(dq1 • dq2) ∧ a1 ≡ a2 ∧ ∀ n, R n a1 UCMRA.unit := by refine CMRA.valid_iff_validN.trans ?_ refine ⟨fun H => ?_, fun H n => ?_⟩ @@ -355,21 +405,26 @@ theorem auth_op_auth_valid_iff : ✓ ((●V{dq1} a1 : View F R) • ●V{dq2} a2 exact (CMRA.op_ne.ne <| toAgree.ne.ne (Hn _).symm).trans Agree.idemp.dist · exact auth_op_auth_validN_iff.mpr ⟨H.1, H.2.1.dist, H.2.2 n⟩ +@[rocq_alias view_auth_op_valid] theorem auth_one_op_auth_one_valid_iff : ✓ ((●V a1 : View F R) • ●V a2) ↔ False := by refine auth_op_auth_valid_iff.trans ?_ simp [CMRA.op, op, CMRA.Valid, op, valid] refine fun _ => (UFraction.one_whole (α := F)).2 ?_ |>.elim exists 1 +@[rocq_alias view_frag_valid] theorem frag_valid_iff : ✓ (◯V b : View F R) ↔ ∀ n, ∃ a, R n a b := by rfl +@[rocq_alias view_both_dfrac_valid] theorem auth_op_frag_valid_iff : ✓ ((●V{dq} a : View F R) • ◯V b) ↔ ✓dq ∧ ∀ n, R n a b := and_congr_right (fun _ => forall_congr' fun _ => IsViewRel.of_agree_dist_iff <| CMRA.unit_left_id_dist b) +@[rocq_alias view_both_valid] theorem auth_one_op_frag_valid_iff : ✓ ((●V a : View F R) • ◯V b) ↔ ∀ n, R n a b := auth_op_frag_valid_iff.trans <| and_iff_right_iff_imp.mpr (fun _ => valid_own_one) open CMRA in +@[rocq_alias view_auth_dfrac_includedN] theorem auth_incN_auth_op_frag_iff : (●V{dq1} a1 : View F R) ≼{n} ((●V{dq2} a2) • ◯V b) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 := by refine ⟨?_, fun H => ?_⟩ · simp only [Auth, Frag, CMRA.IncludedN, CMRA.op] @@ -394,6 +449,7 @@ theorem auth_incN_auth_op_frag_iff : (●V{dq1} a1 : View F R) ≼{n} ((●V{dq2 exact HRa2 ▸NonExpansive₂.ne rfl HRb.symm open CMRA in +@[rocq_alias view_auth_dfrac_included] theorem auth_inc_auth_op_frag_iff : ((●V{dq1} a1 : View F R) ≼ (●V{dq2} a2 : View F R) • ◯V b) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 := by refine ⟨fun H => ⟨?_, ?_⟩, fun H => ?_⟩ · exact auth_incN_auth_op_frag_iff (n := 0) |>.mp (CMRA.incN_of_inc _ H) |>.1 @@ -414,13 +470,16 @@ theorem auth_inc_auth_op_frag_iff : ((●V{dq1} a1 : View F R) ≼ (●V{dq2} a2 apply CMRA.op_ne.eqv exact Hq ▸ NonExpansive₂.eqv rfl Ha.symm +@[rocq_alias view_auth_includedN] theorem auth_one_incN_auth_one_op_frag_iff : (●V a1 : View F R) ≼{n} ((●V a2) • ◯V b) ↔ a1 ≡{n}≡ a2 := auth_incN_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl +@[rocq_alias view_auth_included] theorem auth_one_inc_auth_one_op_frag_iff : (●V a1 : View F R) ≼ ((●V a2) • ◯V b) ↔ a1 ≡ a2 := auth_inc_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl open CMRA in +@[rocq_alias view_frag_includedN] theorem frag_incN_auth_op_frag_iff : (◯V b1 : View F R) ≼{n} ((●V{p} a) • ◯V b2) ↔ b1 ≼{n} b2 := by refine ⟨?_, ?_⟩ · rintro ⟨xf, ⟨_, Hb⟩⟩ @@ -436,6 +495,7 @@ theorem frag_incN_auth_op_frag_iff : (◯V b1 : View F R) ≼{n} ((●V{p} a) _ ≼{n} (●V{p} a) • ◯V b2 := incN_of_incN_of_dist .rfl (op_ne.ne (NonExpansive.ne Hbf.symm)) open CMRA in +@[rocq_alias view_frag_included] theorem frag_inc_auth_op_frag_iff : (◯V b1 : View F R) ≼ ((●V{p} a) • ◯V b2) ↔ b1 ≼ b2 := by constructor · rintro ⟨xf, ⟨_, Hb⟩⟩ @@ -451,6 +511,7 @@ theorem frag_inc_auth_op_frag_iff : (◯V b1 : View F R) ≼ ((●V{p} a) • _ ≼ (●V{p} a) • ◯V b2 := inc_of_inc_of_eqv .rfl (op_ne.eqv (NonExpansive.eqv Hbf.symm)) open CMRA in +@[rocq_alias view_both_dfrac_includedN] theorem auth_op_frag_incN_auth_op_frag_iff : ((●V{dq1} a1 : View F R) • ◯V b1) ≼{n} ((●V{dq2} a2) • ◯V b2) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2 := by @@ -472,6 +533,7 @@ theorem auth_op_frag_incN_auth_op_frag_iff : exact H2.trans (equiv_dist.mp comm _) |>.symm open CMRA in +@[rocq_alias view_both_dfrac_included] theorem auth_op_frag_inc_auth_op_frag_iff : ((●V{dq1} a1 : View F R) • ◯V b1) ≼ ((●V{dq2} a2) • ◯V b2) ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡ a2 ∧ b1 ≼ b2 := by refine ⟨fun H => ?_, fun ⟨H0, H1, ⟨bf, H2⟩⟩ => ?_⟩ @@ -493,9 +555,11 @@ theorem auth_op_frag_inc_auth_op_frag_iff : ((●V{dq1} a1 : View F R) • ◯V refine op_ne.eqv (NonExpansive.eqv ?_) exact (H2.trans comm).symm +@[rocq_alias view_both_includedN] theorem auth_one_op_frag_incN_auth_one_op_frag_iff : ((●V a1 : View F R) • ◯V b1) ≼{n} ((●V a2) • ◯V b2) ↔ (a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2) := auth_op_frag_incN_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl +@[rocq_alias view_both_included] theorem auth_one_op_frag_inc_auth_one_op_frag_iff : ((●V a1 : View F R) • ◯V b1) ≼ ((●V a2) • ◯V b2) ↔ a1 ≡ a2 ∧ b1 ≼ b2 := auth_op_frag_inc_auth_op_frag_iff.trans <| and_iff_right_iff_imp.mpr <| fun _ => .inr rfl @@ -507,6 +571,7 @@ variable [UFraction F] [OFE A] [IB : UCMRA B] {R : ViewRel A B} [IsViewRel R] open CMRA DFrac +@[rocq_alias view_updateP] theorem auth_one_op_frag_updateP {Pab : A → B → Prop} (Hup : ∀ n bf, R n a (b • bf) → ∃ a' b', Pab a' b' ∧ R n a' (b' • bf)) : ((●V a) • ◯V b : View F R) ~~>: fun k => ∃ a' b', k = ((●V a') • ◯V b' : View F R) ∧ Pab a' b' := by @@ -531,6 +596,7 @@ theorem auth_one_op_frag_updateP {Pab : A → B → Prop} · letI _ := own_whole_exclusive <| (UFraction.one_whole (α := F)) exact (not_valid_exclN_op_left ·.1 |>.elim) +@[rocq_alias view_update] theorem auth_one_op_frag_update (Hup : ∀ n bf, R n a (b • bf) → R n a' (b' • bf)) : ((●V a) • ◯V b : View F R) ~~> (●V a') • ◯V b' := by apply Update.of_updateP @@ -540,12 +606,14 @@ theorem auth_one_op_frag_update (Hup : ∀ n bf, R n a (b • bf) → R n a' (b' · rintro y ⟨a', b', H, rfl, rfl⟩ exact H.symm +@[rocq_alias view_update_alloc] theorem auth_one_alloc (Hup : ∀ n bf, R n a bf → R n a' (b' • bf)) : ((●V a) ~~> ((●V a' : View F R) • ◯V b')) := by refine Update.equiv_left CMRA.unit_right_id ?_ refine auth_one_op_frag_update (fun n bf H => Hup n bf <| IsViewRel.mono H .rfl ?_ n.le_refl) exact incN_op_right n unit bf +@[rocq_alias view_update_dealloc] theorem auth_one_op_frag_dealloc (Hup : (∀ n bf, R n a (b • bf) → R n a' bf)) : ((●V a : View F R) • ◯V b) ~~> ●V a' := by refine Update.equiv_right CMRA.unit_right_id ?_ @@ -553,6 +621,7 @@ theorem auth_one_op_frag_dealloc (Hup : (∀ n bf, R n a (b • bf) → R n a' b refine IsViewRel.mono (Hup n bf H) .rfl ?_ n.le_refl exact (unit_left_id_dist bf).to_incN +@[rocq_alias view_update_auth] theorem auth_one_update (Hup : ∀ n bf, R n a bf → R n a' bf) : (●V a : View F R) ~~> ●V a' := by refine Update.equiv_right unit_right_id ?_ @@ -560,6 +629,7 @@ theorem auth_one_update (Hup : ∀ n bf, R n a bf → R n a' bf) : refine auth_one_op_frag_update (fun n bf H => ?_) exact IsViewRel.mono (Hup n _ H) .rfl .rfl n.le_refl +@[rocq_alias view_updateP_auth_dfrac] theorem auth_updateP (Hupd : dq ~~>: P) : (●V{dq} a : View F R) ~~>: (fun k => ∃ dq', (k = ●V{dq'} a) ∧ P dq') := by refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_) @@ -569,11 +639,13 @@ theorem auth_updateP (Hupd : dq ~~>: P) : · obtain ⟨dr, Hdr, Heq⟩ := Hupd n (some dq') Hv refine ⟨●V{dr} a, (by exists dr), ⟨Heq, (by exists a')⟩⟩ +@[rocq_alias view_update_auth_persist] theorem auth_discard : (●V{dq} a : View F R) ~~> ●V{.discard} a := by apply Update.lift_updateP (g := fun dq => ●V{dq} a) · exact fun _ => auth_updateP · exact DFrac.update_discard +@[rocq_alias view_updateP_auth_unpersist] theorem auth_acquire [IsSplitFraction F] : (●V{.discard} a : View F R) ~~>: fun k => ∃ q, k = ●V{.own q} a := by apply UpdateP.weaken @@ -582,6 +654,7 @@ theorem auth_acquire [IsSplitFraction F] : · rintro y ⟨dq, rfl, q', rfl⟩ exists q' +@[rocq_alias view_updateP_both_unpersist] theorem auth_op_frag_acquire [IsSplitFraction F] : ((●V{.discard} a : View F R) • ◯V b) ~~>: fun k => ∃ q, k = ((●V{.own q} a : View F R) • ◯V b ):= by apply UpdateP.op @@ -589,6 +662,7 @@ theorem auth_op_frag_acquire [IsSplitFraction F] : apply UpdateP.id rfl rintro z1 z2 ⟨q, rfl⟩ rfl; exists q +@[rocq_alias view_updateP_frag] theorem frag_updateP {P : B → Prop} (Hupd : ∀ a n bf, R n a (b • bf) → ∃ b', P b' ∧ R n a (b' • bf)) : (◯V b : View F R) ~~>: (fun k => ∃ b', (k = (◯V b' : View F R)) ∧ P b') := by refine UpdateP.total.mpr (fun n ⟨ag, bf⟩ => ?_) @@ -606,6 +680,7 @@ theorem frag_updateP {P : B → Prop} (Hupd : ∀ a n bf, R n a (b • bf) → simp [CMRA.ValidN, ValidN, CMRA.op, optionOp] exact ⟨Hq, ⟨a, Hae, Hp⟩⟩ +@[rocq_alias view_update_frag] theorem frag_update (Hupd : ∀ a n bf, R n a (b • bf) → R n a (b' • bf)) : (◯V b : View F R) ~~> (◯V b' : View F R) := by refine Update.total.mpr (fun n ⟨ag, bf⟩ => ?_) @@ -620,6 +695,7 @@ theorem frag_update (Hupd : ∀ a n bf, R n a (b • bf) → R n a (b' • bf)) exists a exact ⟨He, Hupd _ _ _ Hr⟩ +@[rocq_alias view_update_dfrac_alloc] theorem auth_alloc (Hup : ∀ n bf, R n a bf → R n a (b • bf)) : (●V{dq} a : View F R) ~~> ((●V{dq} a) • ◯V b) := by refine Update.total.mpr (fun n ⟨ag', bf⟩ => ?_) @@ -645,6 +721,7 @@ theorem auth_alloc (Hup : ∀ n bf, R n a bf → R n a (b • bf)) : refine CMRA.op_ne.ne ?_ exact (CMRA.unit_left_id_dist _) +@[rocq_alias view_local_update] theorem view_local_update {a a' : A} {b0 b1 b0' b1' : B} (Hup : (b0, b1) ~l~> (b0', b1')) (Hrel : ∀ n, R n a b0 → R n a' b0') : @@ -664,14 +741,17 @@ end Updates section ViewMap +@[rocq_alias view_map] def map {R : ViewRel A B} (R' : ViewRel A' B') (f : A → A') (g : B → B') (v : View F R) : View F R' where auth := match v.auth with | none => none | some (fr, a) => (fr, a.map' f) frag := g v.frag +@[rocq_alias view_map_id] theorem map_id {R : ViewRel A B} (v : View F R) : View.map R id id v = v := by rcases v with ⟨a, b⟩ cases a <;> simp [View.map, Agree.map'] +@[rocq_alias view_map_compose] theorem map_compose {R : ViewRel A B} {R' : ViewRel A' B'} {R'' : ViewRel A'' B''} f g (f' : A' → A'') (g' : B' → B'') (v : View F R) : View.map R'' (f' ∘ f) (g' ∘ g) v = View.map R'' f' g' (View.map R' f g v) := by @@ -688,6 +768,7 @@ theorem map_compose' [OFE A''] [OFE B''] {R'' : ViewRel A'' B''} map_compose f.f g.f f'.f g'.f v omit [OFE B] in +@[rocq_alias view_map_ext] theorem map_ext {f1 f2 : A → A'} {g1 g2 : B → B'} [OFE.NonExpansive f1] [OFE.NonExpansive f2] (v : View F R) (h1 : ∀ a, f1 a ≡ f2 a) (h2 : ∀ b, g1 b ≡ g2 b) : View.map R' f1 g1 v ≡ View.map R' f2 g2 v := by @@ -707,6 +788,7 @@ theorem map_ne {f1 f2 : A → A'} {g1 g2 : B → B'} [OFE.NonExpansive f1] [OFE. · rfl · exact ⟨rfl, Agree.map_ne h1⟩ +@[rocq_alias view_map_ne] instance (f : A → A') (g : B → B') [OFE.NonExpansive f] [hne : OFE.NonExpansive g] : OFE.NonExpansive (View.map R' f g : (View F R → _)) where ne := by @@ -716,12 +798,14 @@ instance (f : A → A') (g : B → B') [OFE.NonExpansive f] [hne : OFE.NonExpans split <;> split <;> simp_all exact ⟨h1.1, Agree.map f |>.ne.ne h1.2⟩ +@[rocq_alias viewO_map] instance mapO (f : A -n> A') (g : B -n> B') : View F R -n> View F R' where f := View.map R' f g ne := inferInstance end mapO +@[rocq_alias view_map_cmra_morphism] instance mapC [UFraction F] [OFE A] [UCMRA B] [OFE A'] [UCMRA B'] {R : ViewRel A B} [IsViewRel R] {R' : ViewRel A' B'} [IsViewRel R'] (f : A -n> A') (g : B -C> B') (H : ∀ n a b, R n a b → R' n (f a) (g b)) :