From 0c8251ad496a091ab1ee0c0318e32e9308d0ded8 Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 16 Jul 2026 10:17:52 +0200 Subject: [PATCH 1/4] Add notation for `internalCmraValid` and documentation --- Iris/Iris/Algebra/CMRA.lean | 11 +++++++++-- Iris/Iris/BI/Cmra.lean | 8 +++++++- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/Algebra/CMRA.lean b/Iris/Iris/Algebra/CMRA.lean index a6e4180b9..7a43610f0 100644 --- a/Iris/Iris/Algebra/CMRA.lean +++ b/Iris/Iris/Algebra/CMRA.lean @@ -59,23 +59,30 @@ theorem pcore_op_mono_of_core_op_mono [OFE α] (op : α → α → α) (pcore : namespace CMRA variable [CMRA α] +/-- The CMRA composition operation. -/ infix:60 " • " => op +/-- The inclusion order on a CMRA. -/ @[rocq_alias included] def Included (x y : α) : Prop := ∃ z, y ≡ x • z +@[inherit_doc] infix:50 " ≼ " => Included +/-- The step-indexed inclusion order on a CMRA. -/ @[rocq_alias includedN] def IncludedN (n : Nat) (x y : α) : Prop := ∃ z, y ≡{n}≡ x • z -notation:50 x " ≼{" n "} " y:51 => IncludedN n x y +@[inherit_doc] notation:50 x " ≼{" n "} " y:51 => IncludedN n x y +/-- The CMRA composition operation with an optional right argument. -/ @[rocq_alias opM] def op? [CMRA α] (x : α) : Option α → α | some y => x • y | none => x -infix:60 " •? " => op? +@[inherit_doc] infix:60 " •? " => op? +/-- The validity of a CMRA element. -/ prefix:50 "✓ " => Valid +/-- The step-indexed validity of a CMRA element. -/ notation:50 "✓{" n "} " x:51 => ValidN n x @[rocq_alias CoreId] diff --git a/Iris/Iris/BI/Cmra.lean b/Iris/Iris/BI/Cmra.lean index ad9e96d2d..d5b0cde72 100644 --- a/Iris/Iris/BI/Cmra.lean +++ b/Iris/Iris/BI/Cmra.lean @@ -29,6 +29,12 @@ variable [Sbi PROP] [CMRA A] @[rocq_alias internal_cmra_valid] def internalCmraValid (a : A) : PROP := siPure (cmraValid a) +macro_rules +| `(iprop(✓ $a)) => ``(internalCmraValid $a) + +delab_rule internalCmraValid +| `($_ $a) => ``(iprop(✓ $a)) + @[rocq_alias internal_cmra_valid_ne] instance internalCmraValid_ne : NonExpansive (internalCmraValid (PROP := PROP) (A := A)) where ne _ _ _ h := siPure_ne.ne (instNonExpansiveCmraValid.ne h) @@ -37,7 +43,7 @@ instance internalCmraValid_ne : NonExpansive (internalCmraValid (PROP := PROP) ( @[rocq_alias internal_cmra_valid_intro] theorem internalCmraValid_intro {P : PROP} {a : A} (h : Valid a) : - P ⊢ internalCmraValid a := + P ⊢ ✓ a := calc (P : PROP) _ ⊢ True := true_intro _ ⊢ True := siPure_pure.mpr From 0243b6739c39829497e8aacac5b285cbfd85297f Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 16 Jul 2026 10:25:29 +0200 Subject: [PATCH 2/4] =?UTF-8?q?Use=20`=E2=9C=93`=20for=20`internalCmraVali?= =?UTF-8?q?d`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Iris/Iris/BI/Algebra.lean | 46 ++++++++++++------------- Iris/Iris/BI/Cmra.lean | 26 +++++++------- Iris/Iris/Instances/IProp/Instance.lean | 10 +++--- Iris/Iris/Instances/Lib/GhostMap.lean | 4 +-- Iris/Iris/Instances/UPred/Instance.lean | 2 +- Iris/Iris/ProofMode/InstancesCmra.lean | 4 +-- 6 files changed, 46 insertions(+), 46 deletions(-) diff --git a/Iris/Iris/BI/Algebra.lean b/Iris/Iris/BI/Algebra.lean index 32fb70df9..b8c7b1aeb 100644 --- a/Iris/Iris/BI/Algebra.lean +++ b/Iris/Iris/BI/Algebra.lean @@ -20,7 +20,7 @@ open BI Std BIBase.BiEntails @[rocq_alias prod_validI] theorem prod_validI [Sbi PROP] [CMRA A] [CMRA B] (x : A × B) : - internalCmraValid x ⊣⊢@{PROP} internalCmraValid x.1 ∧ internalCmraValid x.2 := by + ✓ x ⊣⊢@{PROP} ✓ x.1 ∧ ✓ x.2 := by simp only [internalCmraValid] refine .trans ?_ siPure_and refine siPure_mono_bi ?_ @@ -53,7 +53,7 @@ open BI Std BIBase.BiEntails @[rocq_alias option_validI] theorem option_validI [Sbi PROP] [CMRA A] {mx : Option A} : - internalCmraValid mx ⊣⊢@{PROP} mx.elim iprop(True) internalCmraValid := + ✓ mx ⊣⊢@{PROP} mx.elim iprop(True) internalCmraValid := match mx with | none => ⟨true_intro, internalCmraValid_intro trivial⟩ | some _ => .rfl @@ -122,8 +122,8 @@ variable [LawfulPartialMap H K] [CMRA V] @[rocq_alias gmap_view_both_dfrac_validI] theorem auth_op_frag_validI [Sbi PROP] (dp : DFrac) (m : H V) k dq v : - internalCmraValid (Auth dp m • Frag k dq v) ⊣⊢@{PROP} - ∃ v' dq', ⌜✓ dp⌝ ∧ ⌜get? m k = .some v'⌝ ∧ internalCmraValid (dq', v') ∧ + ✓ (Auth dp m • Frag k dq v) ⊣⊢@{PROP} + ∃ v' dq', ⌜✓ dp⌝ ∧ ⌜get? m k = .some v'⌝ ∧ ✓ (dq', v') ∧ internalCmraIncluded (Option.some (dq, v)) (Option.some (dq', v')) := by suffices H : ( SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊣⊢@{PROP} @@ -156,8 +156,8 @@ theorem auth_op_frag_validI [Sbi PROP] (dp : DFrac) (m : H V) k dq v : @[rocq_alias gmap_view_both_validI] theorem auth_op_frag_one_validI [Sbi PROP] (dp : DFrac) (m : H V) k v : - internalCmraValid (Auth dp m • Frag k (.own One.one) v) ⊣⊢@{PROP} - ⌜✓ dp⌝ ∧ internalCmraValid v ∧ internalEq (get? m k) (.some v) := by + ✓ (Auth dp m • Frag k (.own One.one) v) ⊣⊢@{PROP} + ⌜✓ dp⌝ ∧ ✓ v ∧ internalEq (get? m k) (.some v) := by simp only [internalCmraValid, internalEq, ←siPure_and.to_eq] rw [←siPure_pure.to_eq, ←siPure_and.to_eq] constructor @@ -170,9 +170,9 @@ theorem auth_op_frag_one_validI [Sbi PROP] (dp : DFrac) (m : H V) k v : @[rocq_alias gmap_view_both_validI_total] theorem auth_op_frag_validI_total [Sbi PROP] [CMRA.IsTotal V] (dp : DFrac) (m : H V) k dq v : - internalCmraValid (Auth dp m • Frag k dq v) ⊢@{PROP} + ✓ (Auth dp m • Frag k dq v) ⊢@{PROP} ∃ v', ⌜✓ dp⌝ ∧ ⌜✓ dq⌝ ∧ ⌜get? m k = .some v'⌝ ∧ - internalCmraValid v' ∧ internalCmraIncluded v v' := by + ✓ v' ∧ internalCmraIncluded v v' := by suffices H : ( SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊢@{PROP} (∃ v', ⌜✓ dp⌝ ∧ ⌜✓ dq⌝ ∧ ⌜get? m k = some v'⌝ ∧ SiProp.cmraValid v' ∧ ∃ c, internalEq v' (v • c))) by @@ -190,8 +190,8 @@ theorem auth_op_frag_validI_total [Sbi PROP] [CMRA.IsTotal V] (dp : DFrac) (m : @[rocq_alias gmap_view_frag_op_validI] theorem frag_op_frag_validI [Sbi PROP] k dq1 dq2 v1 v2 : - internalCmraValid (Frag (H := H) (V := V) k dq1 v1 • Frag k dq2 v2) ⊣⊢@{PROP} - ⌜✓ (dq1 • dq2)⌝ ∧ internalCmraValid (v1 • v2) := by + ✓ (Frag (H := H) (V := V) k dq1 v1 • Frag k dq2 v2) ⊣⊢@{PROP} + ⌜✓ (dq1 • dq2)⌝ ∧ ✓ (v1 • v2) := by simp only [←(and_congr_left siPure_pure).to_eq, internalCmraValid, ←siPure_and.to_eq] constructor · refine siPure_mono fun n => ?_ @@ -216,24 +216,24 @@ theorem agree_equivI {a b : A} : internalEq (toAgree a) (toAgree b) ⊣⊢@{PROP apply NonExpansive.ne @[rocq_alias agree_op_invI] -theorem agree_op_invI {x y : Agree A} : internalCmraValid (x • y) ⊢@{PROP} internalEq x y := +theorem agree_op_invI {x y : Agree A} : ✓ (x • y) ⊢@{PROP} internalEq x y := siPure_mono (fun _ => op_invN) @[rocq_alias to_agree_validI] theorem toAgree_validI (a : A) : - ⊢@{PROP} internalCmraValid (toAgree a) := by + ⊢@{PROP} ✓ (toAgree a) := by refine internalCmraValid_intro fun n => ?_ simp @[rocq_alias to_agree_op_validI] theorem toAgree_op_validI (a b : A) : - internalCmraValid (toAgree a • toAgree b) ⊣⊢@{PROP} internalEq a b := + ✓ (toAgree a • toAgree b) ⊣⊢@{PROP} internalEq a b := ⟨siPure_mono fun _ => toAgree_op_validN_iff_dist.mp, siPure_mono fun _ => toAgree_op_validN_iff_dist.mpr⟩ @[rocq_alias to_agree_uninjI] theorem toAgree_uninjI (x : Agree A) : - internalCmraValid x ⊢@{PROP} ∃ a, internalEq (toAgree a) x := by + ✓ x ⊢@{PROP} ∃ a, internalEq (toAgree a) x := by refine .trans (siPure_mono fun n hvalid => ?_) siPure_exist.mp have ⟨a, heq⟩ := toAgree_uninjN hvalid apply SiProp.instBI.sExists_intro @@ -293,20 +293,20 @@ variable [Sbi PROP] [UCMRA A] @[rocq_alias auth_auth_dfrac_validI] theorem auth_dfrac_validI (dq : DFrac) (a : A) : - internalCmraValid (●{dq} a : Auth A) ⊣⊢@{PROP} ⌜✓ dq⌝ ∧ internalCmraValid a := by + ✓ (●{dq} a : Auth A) ⊣⊢@{PROP} ⌜✓ dq⌝ ∧ ✓ a := by simp only [←(and_congr_left siPure_pure).to_eq, internalCmraValid, ←siPure_and.to_eq] refine ⟨siPure_mono fun n => ?_, siPure_mono fun n => ?_⟩ all_goals simp only [SiProp.cmraValid, auth_dfrac_validN]; exact id @[rocq_alias auth_auth_validI] -theorem auth_validI (a : A) : internalCmraValid (● a : Auth A) ⊣⊢@{PROP} internalCmraValid a := by +theorem auth_validI (a : A) : ✓ (● a : Auth A) ⊣⊢@{PROP} ✓ a := by refine ⟨siPure_mono fun n => ?_, siPure_mono fun n => ?_⟩ all_goals simpa only [SiProp.cmraValid, auth_validN] using id @[rocq_alias auth_auth_dfrac_op_validI] theorem auth_dfrac_op_validI (dq1 dq2 : DFrac) (a1 a2 : A) : - internalCmraValid ((●{dq1} a1) • (●{dq2} a2)) ⊣⊢@{PROP} - ⌜✓ (dq1 • dq2)⌝ ∧ internalEq a1 a2 ∧ internalCmraValid a1 := by + ✓ ((●{dq1} a1) • (●{dq2} a2)) ⊣⊢@{PROP} + ⌜✓ (dq1 • dq2)⌝ ∧ internalEq a1 a2 ∧ ✓ a1 := by simp only [←(and_congr_left siPure_pure).to_eq, internalEq, internalCmraValid , ←(siPure_and.trans (and_congr_right siPure_and)).to_eq] refine ⟨siPure_mono fun n => ?_, siPure_mono fun n => ?_⟩ @@ -314,14 +314,14 @@ theorem auth_dfrac_op_validI (dq1 dq2 : DFrac) (a1 a2 : A) : @[rocq_alias auth_frag_validI] theorem frag_validI (a : A) : - internalCmraValid (◯ a : Auth A) ⊣⊢@{PROP} internalCmraValid a := by + ✓ (◯ a : Auth A) ⊣⊢@{PROP} ✓ a := by refine ⟨siPure_mono fun n => ?_, siPure_mono fun n => ?_⟩ all_goals simpa only [SiProp.cmraValid, frag_validN] using id @[rocq_alias auth_both_dfrac_validI] theorem both_dfrac_validI (dq : DFrac) (a b : A) : - internalCmraValid ((●{dq} a) • ◯ b) ⊣⊢@{PROP} - ⌜✓ dq⌝ ∧ internalCmraIncluded b a ∧ internalCmraValid a := by + ✓ ((●{dq} a) • ◯ b) ⊣⊢@{PROP} + ⌜✓ dq⌝ ∧ internalCmraIncluded b a ∧ ✓ a := by simp only [internalCmraValid, internalCmraIncluded, ←(and_congr siPure_pure siPure_and).to_eq] simp only [←siPure_and.to_eq, BI.and_exists_right.to_eq, BI.and_exists_left.to_eq] refine siPure_mono_bi ?_ @@ -337,8 +337,8 @@ theorem both_dfrac_validI (dq : DFrac) (a b : A) : @[rocq_alias auth_both_validI] theorem auth_both_validI (a b : A) : - internalCmraValid ((● a : Auth A) • ◯ b) ⊣⊢@{PROP} - internalCmraIncluded b a ∧ internalCmraValid a := by + ✓ ((● a : Auth A) • ◯ b) ⊣⊢@{PROP} + internalCmraIncluded b a ∧ ✓ a := by simp only [internalCmraIncluded, internalCmraValid, ←siPure_and.to_eq, BI.and_exists_right.to_eq] refine siPure_mono_bi ?_ simp only [SiProp.cmraValid, both_dfrac_validN] diff --git a/Iris/Iris/BI/Cmra.lean b/Iris/Iris/BI/Cmra.lean index d5b0cde72..d14d703a7 100644 --- a/Iris/Iris/BI/Cmra.lean +++ b/Iris/Iris/BI/Cmra.lean @@ -47,67 +47,67 @@ theorem internalCmraValid_intro {P : PROP} {a : A} (h : Valid a) : calc (P : PROP) _ ⊢ True := true_intro _ ⊢ True := siPure_pure.mpr - _ ⊢ internalCmraValid a := siPure_mono (cmraValid_intro h) + _ ⊢ ✓ a := siPure_mono (cmraValid_intro h) @[rocq_alias internal_cmra_valid_elim] -theorem internalCmraValid_elim (a : A) : internalCmraValid a ⊢@{PROP} ⌜✓{0} a⌝ := +theorem internalCmraValid_elim (a : A) : ✓ a ⊢@{PROP} ⌜✓{0} a⌝ := calc internalCmraValid a _ ⊢ ⌜✓{0} a⌝ := siPure_mono cmraValid_elim _ ⊢ ⌜✓{0} a⌝ := siPure_pure.mp @[rocq_alias internal_cmra_valid_weaken] theorem internalCmraValid_weaken {a b : A} : - internalCmraValid (a • b) ⊢@{PROP} internalCmraValid a := + ✓ (a • b) ⊢@{PROP} ✓ a := siPure_mono cmraValid_weaken @[rocq_alias internal_cmra_valid_entails] theorem internalCmraValid_entails [CMRA B] {a : A} {b : B} : - (internalCmraValid a ⊢@{PROP} internalCmraValid b) ↔ ∀ n, ✓{n} a → ✓{n} b := + (✓ a ⊢@{PROP} ✓ b) ↔ ∀ n, ✓{n} a → ✓{n} b := siPure_entails.trans cmraValid_entails_iff @[rocq_alias si_pure_internal_cmra_valid] -theorem siPure_internalCmraValid {a : A} : cmraValid a ⊣⊢@{PROP} internalCmraValid a := +theorem siPure_internalCmraValid {a : A} : cmraValid a ⊣⊢@{PROP} ✓ a := .rfl @[rocq_alias persistently_internal_cmra_valid] theorem persistently_internalCmraValid {a : A} : - internalCmraValid a ⊣⊢@{PROP} internalCmraValid a := + ✓ a ⊣⊢@{PROP} ✓ a := persistently_siPure @[rocq_alias plainly_internal_cmra_valid] theorem plainly_internalCmraValid (a : A) : - ■ internalCmraValid a ⊣⊢@{PROP} internalCmraValid a := + ■ ✓ a ⊣⊢@{PROP} ✓ a := plainly_siPure @[rocq_alias intuitionistically_internal_cmra_valid] theorem intuitionistically_internalCmraValid [BIAffine PROP] {a : A} : - □ internalCmraValid a ⊣⊢@{PROP} internalCmraValid a := + □ ✓ a ⊣⊢@{PROP} ✓ a := intuitionistically_iff_persistently.trans persistently_internalCmraValid @[rocq_alias internal_cmra_valid_discrete] theorem internalCmraValid_discrete [CMRA.Discrete A] {a : A} : - internalCmraValid a ⊣⊢@{PROP} ⌜✓ a⌝ := + ✓ a ⊣⊢@{PROP} ⌜✓ a⌝ := ⟨(internalCmraValid_elim a).trans <| pure_mono (discrete_valid ·), pure_elim' internalCmraValid_intro⟩ @[rocq_alias internal_cmra_valid_persistent] instance internalCmraValid_persistent (a : A) : - Persistent (PROP := PROP) (internalCmraValid a) where + Persistent (PROP := PROP) iprop(✓ a) where persistent := persistently_internalCmraValid.mpr @[rocq_alias internal_cmra_valid_absorbing] instance internalCmraValid_absorbing (a : A) : - Absorbing (PROP := PROP) (internalCmraValid a) := + Absorbing (PROP := PROP) iprop(✓ a) := siPure_absorbing _ @[rocq_alias internal_cmra_valid_plain] instance internalCmraValid_plain (a : A) : - Plain (PROP := PROP) (internalCmraValid a) where + Plain (PROP := PROP) iprop(✓ a) where plain := plainly_internalCmraValid a |>.mpr @[rocq_alias internal_cmra_valid_timeless] instance internalCmraValid_timeless [CMRA.Discrete A] (a : A) : - Timeless (PROP := PROP) (internalCmraValid a) := by + Timeless (PROP := PROP) iprop(✓ a) := by unfold internalCmraValid; infer_instance end CmraValid diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index 2d0cab892..3036228da 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/Iris/Iris/Instances/IProp/Instance.lean @@ -516,19 +516,19 @@ theorem iOwn_mono {a1 a2 : F.ap (IProp GF)} (H : a2 ≼ a1) : iOwn γ a1 ⊢ iOw next => simp [GenMap.empty_map_lookup]; exact Dist.op_l Dist.rfl @[rocq_alias own_valid] -theorem iOwn_cmraValid {a : F.ap (IProp GF)} : iOwn γ a ⊢ internalCmraValid a := +theorem iOwn_cmraValid {a : F.ap (IProp GF)} : iOwn γ a ⊢ ✓ a := (UPred.ownM_valid _).trans (internalCmraValid_entails.mpr fun _ => validN_of_iSingleton) @[rocq_alias own_valid_2] theorem iOwn_cmraValid_op {a1 a2 : F.ap (IProp GF)} : - iOwn γ a1 ∗ iOwn γ a2 ⊢ internalCmraValid (a1 • a2) := + iOwn γ a1 ∗ iOwn γ a2 ⊢ ✓ (a1 • a2) := iOwn_op.mpr.trans iOwn_cmraValid @[rocq_alias own_valid_r] -theorem iOwn_valid_r {a : F.ap (IProp GF)} : iOwn γ a ⊢ iOwn γ a ∗ internalCmraValid a := +theorem iOwn_valid_r {a : F.ap (IProp GF)} : iOwn γ a ⊢ iOwn γ a ∗ ✓ a := BI.persistent_entails_left iOwn_cmraValid @[rocq_alias own_valid_l] -theorem iOwn_valid_l {a : F.ap (IProp GF)} : iOwn γ a ⊢ internalCmraValid a ∗ iOwn γ a := +theorem iOwn_valid_l {a : F.ap (IProp GF)} : iOwn γ a ⊢ ✓ a ∗ iOwn γ a := BI.persistent_entails_right iOwn_cmraValid @[rocq_alias own_core_persistent] @@ -798,7 +798,7 @@ instance combineSepAs_iOwn {γ} {a b1 b2 : F.ap (IProp GF)} [h : IsOpMerge a b1 @[rocq_alias combine_sep_gives_own] instance combineSepGives_iOwn {γ} {a1 a2 : F.ap (IProp GF)} : - CombineSepGives (iOwn γ a1) (iOwn γ a2) (internalCmraValid (a1 • a2)) where + CombineSepGives (iOwn γ a1) (iOwn γ a2) iprop(✓ (a1 • a2)) where combine_sep_gives := iOwn_cmraValid_op set_option synthInstance.checkSynthOrder false in diff --git a/Iris/Iris/Instances/Lib/GhostMap.lean b/Iris/Iris/Instances/Lib/GhostMap.lean index 71f376681..87d848f01 100644 --- a/Iris/Iris/Instances/Lib/GhostMap.lean +++ b/Iris/Iris/Instances/Lib/GhostMap.lean @@ -106,7 +106,7 @@ theorem ghost_map_elems_unseal [DecidableEq K] γ (m : H V) dq : @[rocq_alias ghost_map_elem_valid] theorem ghost_map_elem_valid (γ : GName) (k : K) (dq : DFrac) (v : V) : - (γ ↪◯MAP[k]{dq} v) ⊢@{IProp GF} internalCmraValid dq := by + (γ ↪◯MAP[k]{dq} v) ⊢@{IProp GF} ✓ dq := by refine iOwn_cmraValid.trans ?_ iintro %h ipureintro @@ -115,7 +115,7 @@ theorem ghost_map_elem_valid (γ : GName) (k : K) (dq : DFrac) (v : V) : @[rocq_alias ghost_map_elem_valid_2] theorem ghost_map_elem_valid_2 (γ : GName) (k : K) (dq1 dq2 : DFrac) (v1 v2 : V) : (γ ↪◯MAP[k]{dq1} v1) ∗ (γ ↪◯MAP[k]{dq2} v2) ⊢@{IProp GF} - internalCmraValid (dq1 • dq2) ∧ ⌜v1 = v2⌝ := by + ✓ (dq1 • dq2) ∧ ⌜v1 = v2⌝ := by unfold ghost_map_elem iintro ⟨H1, H2⟩ icombine H1 H2 gives %H diff --git a/Iris/Iris/Instances/UPred/Instance.lean b/Iris/Iris/Instances/UPred/Instance.lean index 3e63dc321..05c64c011 100644 --- a/Iris/Iris/Instances/UPred/Instance.lean +++ b/Iris/Iris/Instances/UPred/Instance.lean @@ -619,7 +619,7 @@ theorem plainly_eq_uPred_plainly (P : UPred M) : iprop(■ P) = UPred.plainly P /-- The Sbi-derived `internalCmraValid` on UPred unfolds to `UPred.cmraValid`. -/ theorem internalCmraValid_eq_uPred_cmraValid [CMRA A] (a : A) : - (internalCmraValid a : UPred M) = UPred.cmraValid a := rfl + iprop(✓ a : UPred M) = UPred.cmraValid a := rfl instance : BUpd (UPred M) := ⟨bupd⟩ diff --git a/Iris/Iris/ProofMode/InstancesCmra.lean b/Iris/Iris/ProofMode/InstancesCmra.lean index e4b9e3273..6084e0517 100644 --- a/Iris/Iris/ProofMode/InstancesCmra.lean +++ b/Iris/Iris/ProofMode/InstancesCmra.lean @@ -20,12 +20,12 @@ variable {PROP} [Sbi PROP] @[rocq_alias into_pure_internal_cmra_valid] instance intoPure_internalCmraValid α [CMRA α] [CMRA.Discrete α] (a : α) : - IntoPure (PROP:=PROP) (internalCmraValid a) (✓ a) where + IntoPure (PROP:=PROP) iprop(✓ a) (✓ a) where into_pure := internalCmraValid_discrete.1 @[rocq_alias from_pure_internal_cmra_valid] instance fromPure_internalCmraValid io α [CMRA α] (a : α) : - FromPure (PROP:=PROP) false (internalCmraValid a) io (✓ a) where + FromPure (PROP:=PROP) false iprop(✓ a) io (✓ a) where from_pure := BI.pure_elim' internalCmraValid_intro @[rocq_alias into_pure_internal_included] From b9cd0eb663815ef3f51b9884d5e3b7685979af4e Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 16 Jul 2026 10:33:44 +0200 Subject: [PATCH 3/4] =?UTF-8?q?Use=20`=E2=89=BC`=20for=20`internalCmraIncl?= =?UTF-8?q?uded`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Iris/Iris/BI/Algebra.lean | 26 +++++++++---------- Iris/Iris/BI/Cmra.lean | 36 +++++++++++++++----------- Iris/Iris/ProofMode/InstancesCmra.lean | 8 +++--- 3 files changed, 38 insertions(+), 32 deletions(-) diff --git a/Iris/Iris/BI/Algebra.lean b/Iris/Iris/BI/Algebra.lean index b8c7b1aeb..8a776ed16 100644 --- a/Iris/Iris/BI/Algebra.lean +++ b/Iris/Iris/BI/Algebra.lean @@ -29,8 +29,8 @@ theorem prod_validI [Sbi PROP] [CMRA A] [CMRA B] (x : A × B) : @[rocq_alias prod_includedI] theorem prod_includedI [Sbi PROP] [CMRA A] [CMRA B] (x y : A × B) : - internalCmraIncluded x y ⊣⊢@{PROP} internalCmraIncluded x.1 y.1 ∧ internalCmraIncluded x.2 y.2 := by - simp only [internalCmraIncluded, internalEq] + x ≼ y ⊣⊢@{PROP} x.1 ≼ y.1 ∧ x.2 ≼ y.2 := by + simp only [internalCmraIncluded, internalEq] refine .trans (siPure_mono_bi ?_) siPure_and refine siPure_exist.symm.trans ?_ refine .trans ?_ (and_congr_left siPure_exist) @@ -60,9 +60,9 @@ theorem option_validI [Sbi PROP] [CMRA A] {mx : Option A} : @[rocq_alias option_includedI] theorem option_includedI [Sbi PROP] [CMRA A] {mx my : Option A} : - internalCmraIncluded mx my ⊣⊢@{PROP} + mx ≼ my ⊣⊢@{PROP} match mx, my with - | some x, some y => iprop((internalCmraIncluded x y) ∨ (internalEq x y)) + | some x, some y => iprop((x ≼ y) ∨ (internalEq x y)) | none, _ => iprop(True) | some _, none => iprop(False) := by rcases mx with _ | x <;> rcases my with _ | y @@ -86,9 +86,9 @@ theorem option_includedI [Sbi PROP] [CMRA A] {mx my : Option A} : @[rocq_alias option_included_totalI] theorem option_included_totalI [Sbi PROP] [CMRA A] [CMRA.IsTotal A] {mx my : Option A} : - internalCmraIncluded mx my ⊣⊢@{PROP} + mx ≼ my ⊣⊢@{PROP} match mx, my with - | some x, some y => internalCmraIncluded x y + | some x, some y => iprop(x ≼ y) | none, _ => iprop(True) | some _, none => iprop(False) := by rcases mx with _ | x <;> rcases my with _ | y @@ -108,7 +108,7 @@ theorem option_included_totalI [Sbi PROP] [CMRA A] [CMRA.IsTotal A] {mx my : Opt @[rocq_alias Some_included_totalI] theorem Some_included_totalI [Sbi PROP] [CMRA A] [CMRA.IsTotal A] {x y : A} : - internalCmraIncluded (some x) (some y) ⊣⊢@{PROP} internalCmraIncluded x y := + some x ≼ some y ⊣⊢@{PROP} x ≼ y := option_included_totalI end option @@ -124,7 +124,7 @@ variable [LawfulPartialMap H K] [CMRA V] theorem auth_op_frag_validI [Sbi PROP] (dp : DFrac) (m : H V) k dq v : ✓ (Auth dp m • Frag k dq v) ⊣⊢@{PROP} ∃ v' dq', ⌜✓ dp⌝ ∧ ⌜get? m k = .some v'⌝ ∧ ✓ (dq', v') ∧ - internalCmraIncluded (Option.some (dq, v)) (Option.some (dq', v')) := by + some (dq, v) ≼ some (dq', v') := by suffices H : ( SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊣⊢@{PROP} ( ∃ x x_1, ⌜✓ dp⌝ ∧ ⌜get? m k = some x⌝ ∧ SiProp.cmraValid (x_1, x) ∧ @@ -172,7 +172,7 @@ theorem auth_op_frag_one_validI [Sbi PROP] (dp : DFrac) (m : H V) k v : theorem auth_op_frag_validI_total [Sbi PROP] [CMRA.IsTotal V] (dp : DFrac) (m : H V) k dq v : ✓ (Auth dp m • Frag k dq v) ⊢@{PROP} ∃ v', ⌜✓ dp⌝ ∧ ⌜✓ dq⌝ ∧ ⌜get? m k = .some v'⌝ ∧ - ✓ v' ∧ internalCmraIncluded v v' := by + ✓ v' ∧ v ≼ v' := by suffices H : ( SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊢@{PROP} (∃ v', ⌜✓ dp⌝ ∧ ⌜✓ dq⌝ ∧ ⌜get? m k = some v'⌝ ∧ SiProp.cmraValid v' ∧ ∃ c, internalEq v' (v • c))) by @@ -265,7 +265,7 @@ theorem agree_op_equiv_toAgreeI (x y : Agree A) (a : A) : @[rocq_alias agree_includedI] theorem agree_includedI (x y : Agree A) : - internalCmraIncluded x y ⊣⊢@{PROP} internalEq y (x • y) := by + x ≼ y ⊣⊢@{PROP} internalEq y (x • y) := by constructor · refine siPure_mono (exists_elim (fun c => ?_)) exact (fun n Heq => (includedN.mp ⟨c, Heq⟩).trans op_commN) @@ -274,7 +274,7 @@ theorem agree_includedI (x y : Agree A) : @[rocq_alias to_agree_includedI] theorem toAgree_includedI (a b : A) : - internalCmraIncluded (toAgree a) (toAgree b) ⊣⊢@{PROP} internalEq a b := by + toAgree a ≼ toAgree b ⊣⊢@{PROP} internalEq a b := by constructor · refine siPure_mono (exists_elim (fun c => ?_)) exact (fun n Heq => toAgree_includedN.mp ⟨c, Heq⟩) @@ -321,7 +321,7 @@ theorem frag_validI (a : A) : @[rocq_alias auth_both_dfrac_validI] theorem both_dfrac_validI (dq : DFrac) (a b : A) : ✓ ((●{dq} a) • ◯ b) ⊣⊢@{PROP} - ⌜✓ dq⌝ ∧ internalCmraIncluded b a ∧ ✓ a := by + ⌜✓ dq⌝ ∧ b ≼ a ∧ ✓ a := by simp only [internalCmraValid, internalCmraIncluded, ←(and_congr siPure_pure siPure_and).to_eq] simp only [←siPure_and.to_eq, BI.and_exists_right.to_eq, BI.and_exists_left.to_eq] refine siPure_mono_bi ?_ @@ -338,7 +338,7 @@ theorem both_dfrac_validI (dq : DFrac) (a b : A) : @[rocq_alias auth_both_validI] theorem auth_both_validI (a b : A) : ✓ ((● a : Auth A) • ◯ b) ⊣⊢@{PROP} - internalCmraIncluded b a ∧ ✓ a := by + b ≼ a ∧ ✓ a := by simp only [internalCmraIncluded, internalCmraValid, ←siPure_and.to_eq, BI.and_exists_right.to_eq] refine siPure_mono_bi ?_ simp only [SiProp.cmraValid, both_dfrac_validN] diff --git a/Iris/Iris/BI/Cmra.lean b/Iris/Iris/BI/Cmra.lean index d14d703a7..5c49a9fa1 100644 --- a/Iris/Iris/BI/Cmra.lean +++ b/Iris/Iris/BI/Cmra.lean @@ -30,10 +30,10 @@ variable [Sbi PROP] [CMRA A] def internalCmraValid (a : A) : PROP := siPure (cmraValid a) macro_rules -| `(iprop(✓ $a)) => ``(internalCmraValid $a) + | `(iprop(✓ $a)) => ``(internalCmraValid $a) delab_rule internalCmraValid -| `($_ $a) => ``(iprop(✓ $a)) + | `($_ $a) => ``(iprop(✓ $a)) @[rocq_alias internal_cmra_valid_ne] instance internalCmraValid_ne : NonExpansive (internalCmraValid (PROP := PROP) (A := A)) where @@ -119,6 +119,12 @@ variable [Sbi PROP] [CMRA A] @[rocq_alias internal_included] def internalCmraIncluded (a b : A) : PROP := siPure (∃ c, internalEq b (a • c)) +macro_rules + | `(iprop($a ≼ $b)) => ``(internalCmraIncluded $a $b) + +delab_rule internalCmraIncluded + | `($_ $a $b) => ``(iprop($a ≼ $b)) + @[rocq_alias internal_included_nonexpansive] instance internalCmraIncluded_ne : NonExpansive₂ (internalCmraIncluded (PROP := PROP) (A := A)) where @@ -130,36 +136,36 @@ instance internalCmraIncluded_ne : @[rocq_alias internal_included_intro] theorem internalCmraIncluded_intro {P : PROP} {a b : A} (h : a ≼ b) : - P ⊢ internalCmraIncluded a b := by + P ⊢ a ≼ b := by obtain ⟨c, hc⟩ := h calc (P : PROP) _ ⊢ True := true_intro _ ⊢ True := siPure_pure.mpr - _ ⊢ internalCmraIncluded a b := siPure_mono (BI.exists_intro_trans c (internalEq.of_equiv hc)) + _ ⊢ a ≼ b := siPure_mono (BI.exists_intro_trans c (internalEq.of_equiv hc)) @[rocq_alias si_pure_internal_included] theorem siPure_internalCmraIncluded {a b : A} : - internalCmraIncluded a b ⊣⊢@{PROP} internalCmraIncluded a b := + a ≼ b ⊣⊢@{PROP} a ≼ b := persistently_iff.symm.trans persistently_siPure @[rocq_alias persistently_internal_included] theorem persistently_internalCmraIncluded {a b : A} : - internalCmraIncluded a b ⊣⊢@{PROP} internalCmraIncluded a b := + a ≼ b ⊣⊢@{PROP} a ≼ b := persistently_siPure @[rocq_alias plainly_internal_included] theorem plainly_internalCmraIncluded {a b : A} : - ■ internalCmraIncluded a b ⊣⊢@{PROP} internalCmraIncluded a b := + ■ a ≼ b ⊣⊢@{PROP} a ≼ b := plainly_siPure @[rocq_alias intuitionistically_internal_included] theorem intuitionistically_internalCmraIncluded [BIAffine PROP] {a b : A} : - □ internalCmraIncluded a b ⊣⊢@{PROP} internalCmraIncluded a b := + □ a ≼ b ⊣⊢@{PROP} a ≼ b := intuitionistically_iff_persistently.trans persistently_internalCmraIncluded @[rocq_alias internal_included_discrete] theorem internalCmraIncluded_discrete {a b : A} [CMRA.Discrete A] : - internalCmraIncluded a b ⊣⊢@{PROP} ⌜a ≼ b⌝ := by + a ≼ b ⊣⊢@{PROP} ⌜a ≼ b⌝ := by haveI : ∀ x : A, DiscreteE x := fun x => ⟨OFE.Discrete.discrete⟩ refine ⟨?_, pure_elim' internalCmraIncluded_intro⟩ calc internalCmraIncluded a b @@ -170,12 +176,12 @@ theorem internalCmraIncluded_discrete {a b : A} [CMRA.Discrete A] : _ ⊢ ⌜a ≼ b⌝ := pure_mono fun ⟨c, h⟩ => ⟨c, h⟩ @[rocq_alias internal_included_refl] -theorem internalCmraIncluded_refl {a : A} [IsTotal A] : ⊢@{PROP} internalCmraIncluded a a := +theorem internalCmraIncluded_refl {a : A} [IsTotal A] : ⊢@{PROP} a ≼ a := internalCmraIncluded_intro .rfl @[rocq_alias internal_included_trans] theorem internalCmraIncluded_trans {a b c : A} : - ⊢@{PROP} internalCmraIncluded a b -∗ internalCmraIncluded b c -∗ internalCmraIncluded a c := by + ⊢@{PROP} a ≼ b -∗ b ≼ c -∗ a ≼ c := by refine BI.entails_wand (siPure_exist.mp.trans ?_) refine BI.exists_elim (fun a' => ?_) refine BI.wand_intro ((BI.sep_mono_right siPure_exist.mp).trans (BI.sep_exists_left.mp.trans ?_)) @@ -189,24 +195,24 @@ theorem internalCmraIncluded_trans {a b c : A} : @[rocq_alias internal_included_timeless] instance internalCmraIncluded_timeless {a b : A} [CMRA.Discrete A] : - Timeless (PROP := PROP) (internalCmraIncluded a b) := by + Timeless (PROP := PROP) iprop(a ≼ b) := by haveI : ∀ x : A, DiscreteE x := fun x => ⟨OFE.Discrete.discrete⟩ unfold internalCmraIncluded infer_instance @[rocq_alias internal_included_plain] instance internalCmraIncluded_plain {a b : A} : - Plain (PROP := PROP) (internalCmraIncluded a b) where + Plain (PROP := PROP) iprop(a ≼ b) where plain := plainly_internalCmraIncluded.mpr @[rocq_alias internal_included_persistent] instance internalCmraIncluded_persistent {a b : A} : - Persistent (PROP := PROP) (internalCmraIncluded a b) where + Persistent (PROP := PROP) iprop(a ≼ b) where persistent := persistently_internalCmraIncluded.mpr @[rocq_alias internal_included_absorbing] instance internalCmraIncluded_absorbing {a b : A} : - Absorbing (PROP := PROP) (internalCmraIncluded a b) := + Absorbing (PROP := PROP) iprop(a ≼ b) := siPure_absorbing _ end CmraIncluded diff --git a/Iris/Iris/ProofMode/InstancesCmra.lean b/Iris/Iris/ProofMode/InstancesCmra.lean index 6084e0517..f7a53f983 100644 --- a/Iris/Iris/ProofMode/InstancesCmra.lean +++ b/Iris/Iris/ProofMode/InstancesCmra.lean @@ -30,22 +30,22 @@ instance fromPure_internalCmraValid io α [CMRA α] (a : α) : @[rocq_alias into_pure_internal_included] instance intoPure_internalCmraIncluded α [CMRA α] [CMRA.Discrete α] (a b : α) : - IntoPure (PROP:=PROP) (internalCmraIncluded a b) (a ≼ b) where + IntoPure (PROP:=PROP) iprop(a ≼ b) (a ≼ b) where into_pure := internalCmraIncluded_discrete.1 @[rocq_alias from_pure_internal_included] instance fromPure_internalCmraIncluded io α [CMRA α] (a b : α) : - FromPure (PROP:=PROP) false (internalCmraIncluded a b) io (a ≼ b) where + FromPure (PROP:=PROP) false iprop(a ≼ b) io (a ≼ b) where from_pure := BI.pure_elim' internalCmraIncluded_intro @[rocq_alias into_exist_internal_included] instance intoExists_internalCmraIncluded α [CMRA α] (a b : α) : - IntoExists (PROP:=PROP) (internalCmraIncluded a b) (λ c => internalEq b (a • c)) where + IntoExists (PROP:=PROP) iprop(a ≼ b) (λ c => internalEq b (a • c)) where into_exists := siPure_exist.1 @[rocq_alias from_exist_internal_included] instance fromExists_internalCmraIncluded α [CMRA α] (a b : α) : - FromExists (PROP:=PROP) (internalCmraIncluded a b) (λ c => internalEq b (a • c)) where + FromExists (PROP:=PROP) iprop(a ≼ b) (λ c => internalEq b (a • c)) where from_exists := siPure_exist.2 end cmra From a1bb217b76551a7664e175c639a0e3307afe15be Mon Sep 17 00:00:00 2001 From: Alvin Tang Date: Thu, 16 Jul 2026 11:01:05 +0200 Subject: [PATCH 4/4] =?UTF-8?q?Use=20`=E2=89=A1`=20for=20`internalEq`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Iris/Iris/BI/Algebra.lean | 32 ++--- Iris/Iris/BI/Cmra.lean | 4 +- Iris/Iris/BI/Embedding.lean | 4 +- Iris/Iris/BI/InternalEq.lean | 144 ++++++++++--------- Iris/Iris/BI/MonPred.lean | 10 +- Iris/Iris/BI/Plainly.lean | 40 +++--- Iris/Iris/Instances/Lib/Boxes.lean | 8 +- Iris/Iris/Instances/Lib/WSat.lean | 2 +- Iris/Iris/ProofMode/Classes.lean | 2 +- Iris/Iris/ProofMode/InstancesCmra.lean | 12 +- Iris/Iris/ProofMode/InstancesInternalEq.lean | 14 +- Iris/Iris/ProofMode/Tactics/Rewrite.lean | 10 +- Iris/Iris/Tests/Tactics.lean | 28 ++-- 13 files changed, 157 insertions(+), 153 deletions(-) diff --git a/Iris/Iris/BI/Algebra.lean b/Iris/Iris/BI/Algebra.lean index 8a776ed16..84b52ee57 100644 --- a/Iris/Iris/BI/Algebra.lean +++ b/Iris/Iris/BI/Algebra.lean @@ -62,7 +62,7 @@ theorem option_validI [Sbi PROP] [CMRA A] {mx : Option A} : theorem option_includedI [Sbi PROP] [CMRA A] {mx my : Option A} : mx ≼ my ⊣⊢@{PROP} match mx, my with - | some x, some y => iprop((x ≼ y) ∨ (internalEq x y)) + | some x, some y => iprop((x ≼ y) ∨ (x ≡ y)) | none, _ => iprop(True) | some _, none => iprop(False) := by rcases mx with _ | x <;> rcases my with _ | y @@ -128,7 +128,7 @@ theorem auth_op_frag_validI [Sbi PROP] (dp : DFrac) (m : H V) k dq v : suffices H : ( SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊣⊢@{PROP} ( ∃ x x_1, ⌜✓ dp⌝ ∧ ⌜get? m k = some x⌝ ∧ SiProp.cmraValid (x_1, x) ∧ - ∃ c, internalEq (some (x_1, x)) (some (dq, v) • c))) by + ∃ c, some (x_1, x) ≡ some (dq, v) • c)) by simp only [internalCmraValid, internalCmraIncluded, H.to_eq, siPure_exist.to_eq, siPure_and.to_eq, siPure_pure.to_eq, BIBase.BiEntails.rfl] constructor @@ -157,7 +157,7 @@ theorem auth_op_frag_validI [Sbi PROP] (dp : DFrac) (m : H V) k dq v : @[rocq_alias gmap_view_both_validI] theorem auth_op_frag_one_validI [Sbi PROP] (dp : DFrac) (m : H V) k v : ✓ (Auth dp m • Frag k (.own One.one) v) ⊣⊢@{PROP} - ⌜✓ dp⌝ ∧ ✓ v ∧ internalEq (get? m k) (.some v) := by + ⌜✓ dp⌝ ∧ ✓ v ∧ get? m k ≡ .some v := by simp only [internalCmraValid, internalEq, ←siPure_and.to_eq] rw [←siPure_pure.to_eq, ←siPure_and.to_eq] constructor @@ -175,7 +175,7 @@ theorem auth_op_frag_validI_total [Sbi PROP] [CMRA.IsTotal V] (dp : DFrac) (m : ✓ v' ∧ v ≼ v' := by suffices H : ( SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊢@{PROP} (∃ v', ⌜✓ dp⌝ ∧ ⌜✓ dq⌝ ∧ ⌜get? m k = some v'⌝ ∧ SiProp.cmraValid v' ∧ - ∃ c, internalEq v' (v • c))) by + ∃ c, v' ≡ v • c)) by simp only [internalCmraValid, internalCmraIncluded, siPure_exist.to_eq, siPure_and.to_eq, siPure_pure.to_eq] at H ⊢ exact H @@ -210,13 +210,13 @@ open Iris BI Agree OFE variable [Sbi PROP] [OFE A] @[rocq_alias agree_equivI] -theorem agree_equivI {a b : A} : internalEq (toAgree a) (toAgree b) ⊣⊢@{PROP} internalEq a b := by +theorem agree_equivI {a b : A} : toAgree a ≡ toAgree b ⊣⊢@{PROP} a ≡ b := by refine ⟨siPure_mono fun _ => Agree.toAgree_injN, ?_⟩ refine siPure_mono fun n => ?_ apply NonExpansive.ne @[rocq_alias agree_op_invI] -theorem agree_op_invI {x y : Agree A} : ✓ (x • y) ⊢@{PROP} internalEq x y := +theorem agree_op_invI {x y : Agree A} : ✓ (x • y) ⊢@{PROP} x ≡ y := siPure_mono (fun _ => op_invN) @[rocq_alias to_agree_validI] @@ -227,13 +227,13 @@ theorem toAgree_validI (a : A) : @[rocq_alias to_agree_op_validI] theorem toAgree_op_validI (a b : A) : - ✓ (toAgree a • toAgree b) ⊣⊢@{PROP} internalEq a b := + ✓ (toAgree a • toAgree b) ⊣⊢@{PROP} a ≡ b := ⟨siPure_mono fun _ => toAgree_op_validN_iff_dist.mp, siPure_mono fun _ => toAgree_op_validN_iff_dist.mpr⟩ @[rocq_alias to_agree_uninjI] theorem toAgree_uninjI (x : Agree A) : - ✓ x ⊢@{PROP} ∃ a, internalEq (toAgree a) x := by + ✓ x ⊢@{PROP} ∃ a, toAgree a ≡ x := by refine .trans (siPure_mono fun n hvalid => ?_) siPure_exist.mp have ⟨a, heq⟩ := toAgree_uninjN hvalid apply SiProp.instBI.sExists_intro @@ -245,19 +245,19 @@ theorem toAgree_uninjI (x : Agree A) : @[rocq_alias agree_op_equiv_to_agreeI] theorem agree_op_equiv_toAgreeI (x y : Agree A) (a : A) : - internalEq (x • y) (toAgree a) ⊢@{PROP} internalEq x y ∧ internalEq y (toAgree a) := by - have H1 : internalEq (x • y) (toAgree a) ⊢@{PROP} internalEq x y := by + x • y ≡ toAgree a ⊢@{PROP} x ≡ y ∧ y ≡ toAgree a := by + have H1 : x • y ≡ toAgree a ⊢@{PROP} x ≡ y := by refine absorbingly_internalEq (x • y) (toAgree a) |>.mpr.trans ?_ refine (absorbingly_mono ?_).trans absorbing refine internalEq.rewrite' internalCmraValid internalEq.symm ?_ |>.trans agree_op_invI refine emp_sep.2.trans ?_ refine (sep_mono_left (toAgree_validI a)) |>.trans ?_ exact sep_elim_left - have H2 : internalEq (x • y) (toAgree a) ⊢@{PROP} internalEq x (toAgree a) := by + have H2 : x • y ≡ toAgree a ⊢@{PROP} x ≡ toAgree a := by letI : NonExpansive (x • ·) := CMRA.op_ne - have H21 : internalEq (x • y) (toAgree a) ⊢@{PROP} internalEq (x • x) (toAgree a) := by + have H21 : x • y ≡ toAgree a ⊢@{PROP} x • x ≡ toAgree a := by exact (and_intro (H1.trans (internalEq.of_internalEquiv_ne (x • ·))) .rfl).trans internalEq.trans - have H22 : internalEq (x • y) (toAgree a) ⊢@{PROP} internalEq (x • x) x := by + have H22 : x • y ≡ toAgree a ⊢@{PROP} x • x ≡ x := by exact emp_sep.2.trans (sep_mono_left (internalEq.of_equiv Agree.idemp)) |>.trans sep_elim_left refine (and_intro (H22.trans internalEq.symm) H21).trans internalEq.trans apply and_intro H1 @@ -265,7 +265,7 @@ theorem agree_op_equiv_toAgreeI (x y : Agree A) (a : A) : @[rocq_alias agree_includedI] theorem agree_includedI (x y : Agree A) : - x ≼ y ⊣⊢@{PROP} internalEq y (x • y) := by + x ≼ y ⊣⊢@{PROP} y ≡ x • y := by constructor · refine siPure_mono (exists_elim (fun c => ?_)) exact (fun n Heq => (includedN.mp ⟨c, Heq⟩).trans op_commN) @@ -274,7 +274,7 @@ theorem agree_includedI (x y : Agree A) : @[rocq_alias to_agree_includedI] theorem toAgree_includedI (a b : A) : - toAgree a ≼ toAgree b ⊣⊢@{PROP} internalEq a b := by + toAgree a ≼ toAgree b ⊣⊢@{PROP} a ≡ b := by constructor · refine siPure_mono (exists_elim (fun c => ?_)) exact (fun n Heq => toAgree_includedN.mp ⟨c, Heq⟩) @@ -306,7 +306,7 @@ theorem auth_validI (a : A) : ✓ (● a : Auth A) ⊣⊢@{PROP} ✓ a := by @[rocq_alias auth_auth_dfrac_op_validI] theorem auth_dfrac_op_validI (dq1 dq2 : DFrac) (a1 a2 : A) : ✓ ((●{dq1} a1) • (●{dq2} a2)) ⊣⊢@{PROP} - ⌜✓ (dq1 • dq2)⌝ ∧ internalEq a1 a2 ∧ ✓ a1 := by + ⌜✓ (dq1 • dq2)⌝ ∧ a1 ≡ a2 ∧ ✓ a1 := by simp only [←(and_congr_left siPure_pure).to_eq, internalEq, internalCmraValid , ←(siPure_and.trans (and_congr_right siPure_and)).to_eq] refine ⟨siPure_mono fun n => ?_, siPure_mono fun n => ?_⟩ diff --git a/Iris/Iris/BI/Cmra.lean b/Iris/Iris/BI/Cmra.lean index 5c49a9fa1..f1d3fe55c 100644 --- a/Iris/Iris/BI/Cmra.lean +++ b/Iris/Iris/BI/Cmra.lean @@ -117,7 +117,7 @@ section CmraIncluded variable [Sbi PROP] [CMRA A] @[rocq_alias internal_included] -def internalCmraIncluded (a b : A) : PROP := siPure (∃ c, internalEq b (a • c)) +def internalCmraIncluded (a b : A) : PROP := siPure (∃ c, iprop(b ≡ (a • c))) macro_rules | `(iprop($a ≼ $b)) => ``(internalCmraIncluded $a $b) @@ -169,7 +169,7 @@ theorem internalCmraIncluded_discrete {a b : A} [CMRA.Discrete A] : haveI : ∀ x : A, DiscreteE x := fun x => ⟨OFE.Discrete.discrete⟩ refine ⟨?_, pure_elim' internalCmraIncluded_intro⟩ calc internalCmraIncluded a b - _ ⊢ (∃ c, internalEq b (a • c)) := siPure_internalCmraIncluded.mp + _ ⊢ (∃ c, b ≡ (a • c)) := siPure_internalCmraIncluded.mp _ ⊢ (∃ c, ⌜b ≡ a • c⌝) := siPure_mono <| exists_mono fun _ => discrete_eq_mp _ ⊢ ⌜∃ c, b ≡ a • c⌝ := siPure_mono pure_exists.mp _ ⊢ ⌜∃ c, b ≡ a • c⌝ := siPure_pure.mp diff --git a/Iris/Iris/BI/Embedding.lean b/Iris/Iris/BI/Embedding.lean index bee649f74..1b45a98f2 100644 --- a/Iris/Iris/BI/Embedding.lean +++ b/Iris/Iris/BI/Embedding.lean @@ -429,7 +429,7 @@ theorem embed_si_pure (Pi : SiProp) : @[rocq_alias embed_internal_eq] theorem embed_internal_eq {A : Type _} [OFE A] (x y : A) : - (embed (internalEq x y : P1) : P2) ⊣⊢ internalEq x y := + (embed (iprop(x ≡ y) : P1) : P2) ⊣⊢ x ≡ y := embed_si_pure (SiProp.internalEq x y) @[rocq_alias embed_plainly] @@ -453,7 +453,7 @@ instance embed_plain (P : P1) [Plain P] : Plain (embed P : P2) where /-- `⎡·⎤` reflects internal equality. -/ @[rocq_alias embed_internal_inj] theorem embed_internal_inj {P3 : Type _} [Sbi P3] (P Q : P1) : - (internalEq (embed P : P2) (embed Q) : P3) ⊢ internalEq P Q := by + ((embed P : P2) ≡ embed Q : P3) ⊢ P ≡ Q := by refine siPure_mono ?_ refine (prop_ext_siEmpValid_equiv (embed P) (embed Q)).mp.trans ?_ refine (siEmpValid_and.mp.trans ?_).trans (prop_ext_siEmpValid_equiv P Q).mpr diff --git a/Iris/Iris/BI/InternalEq.lean b/Iris/Iris/BI/InternalEq.lean index 570f0440b..51a49f4c1 100644 --- a/Iris/Iris/BI/InternalEq.lean +++ b/Iris/Iris/BI/InternalEq.lean @@ -20,6 +20,12 @@ open BI OFE Iris.Std def internalEq [Sbi PROP] {A : Type _} [OFE A] (a b : A) : PROP := iprop( (SiProp.internalEq a b)) +macro_rules + | `(iprop($a ≡ $b)) => ``(internalEq $a $b) + +delab_rule internalEq + | `($_ $a $b) => ``(iprop($a ≡ $b)) + namespace BI section internalEqLaws @@ -28,7 +34,6 @@ variable {PROP : Type u} [Sbi PROP] {P Q : PROP} namespace internalEq - @[rocq_alias internal_eq_ne] instance instInternalEq_ne (A : Type _) [OFE A] : NonExpansive₂ (internalEq (PROP := PROP) (A := A)) where @@ -45,21 +50,21 @@ theorem ne_r {A : Type _} [OFE A] (a : A) : NonExpansive₂.ne_right internalEq a @[rocq_alias internal_eq_refl] -theorem refl {A : Type _} [OFE A] {P : PROP} {a : A} : P ⊢ internalEq a a := +theorem refl {A : Type _} [OFE A] {P : PROP} {a : A} : P ⊢ a ≡ a := true_intro.trans <| siPure_pure.mpr.trans <| siPure_mono (SiProp.internalEq_refl _ _) @[rocq_alias equiv_internal_eq] theorem of_equiv {A : Type _} [OFE A] {P : PROP} {a b : A} (h : a ≡ b) : - P ⊢ internalEq a b := + P ⊢ a ≡ b := refl.trans (equiv_iff.mp (NonExpansive₂.eqv Equiv.rfl h)).1 @[rocq_alias pure_internal_eq] -theorem of_pure {A : Type _} [OFE A] {x y : A} : ⌜x ≡ y⌝ ⊢ internalEq (PROP := PROP) x y := +theorem of_pure {A : Type _} [OFE A] {x y : A} : ⌜x ≡ y⌝ ⊢ (iprop(x ≡ y) : PROP) := pure_elim' of_equiv @[rocq_alias internal_eq_rewrite] theorem rewrite {A : Type _} [OFE A] {a b : A} (Ψ : A → PROP) [hΨ : NonExpansive Ψ] : - internalEq a b ⊢ Ψ a → Ψ b := by + a ≡ b ⊢ Ψ a → Ψ b := by let Φ : A → SiProp := fun a' => iprop( (True -∗ Ψ a → Ψ a')) letI _ : NonExpansive Φ := ⟨fun {_ _ _} h => Sbi.siEmpValid_ne.ne (wand_ne.ne .rfl (imp_ne.ne .rfl (hΨ.ne h)))⟩ @@ -76,25 +81,25 @@ theorem rewrite {A : Type _} [OFE A] {a b : A} (Ψ : A → PROP) [hΨ : NonExpan @[rocq_alias internal_eq_rewrite'] theorem rewrite' {A : Type _} [OFE A] {a b : A} (Ψ : A → PROP) [NonExpansive Ψ] - (Heq : P ⊢ internalEq a b) (HΨa : P ⊢ Ψ a) : P ⊢ Ψ b := + (Heq : P ⊢ a ≡ b) (HΨa : P ⊢ Ψ a) : P ⊢ Ψ b := (and_intro .rfl HΨa).trans <| (and_mono_left Heq).trans <| imp_elim (rewrite Ψ) @[rocq_alias internal_eq_sym] -theorem symm {A : Type _} [OFE A] {a b : A} : internalEq a b ⊢@{PROP} internalEq b a := +theorem symm {A : Type _} [OFE A] {a b : A} : a ≡ b ⊢@{PROP} b ≡ a := letI _ := ne_l (PROP := PROP) a rewrite' (internalEq · a) .rfl refl @[rocq_alias internal_eq_trans] theorem trans {A : Type _} [OFE A] {a b c : A} : - internalEq a b ∧ internalEq b c ⊢@{PROP} internalEq a c := + a ≡ b ∧ b ≡ c ⊢@{PROP} a ≡ c := letI _ := ne_l (PROP := PROP) c rewrite' (internalEq · c) (and_elim_l.trans symm) and_elim_r @[rocq_alias f_equivI] theorem of_internalEquiv_ne {A B : Type _} [OFE A] [OFE B] (f : A → B) [hf : NonExpansive f] {x y : A} : - internalEq x y ⊢@{PROP} internalEq (f x) (f y) := - letI _ : NonExpansive (fun y => internalEq (PROP := PROP) (f x) (f y)) := (ne_r (f x)).comp hf - rewrite' (fun y => internalEq (f x) (f y)) .rfl refl + x ≡ y ⊢@{PROP} f x ≡ f y := + letI _ : NonExpansive (fun y => (iprop(f x ≡ f y) : PROP)) := (ne_r (f x)).comp hf + rewrite' (fun y => iprop(f x ≡ f y)) .rfl refl end internalEq @@ -104,27 +109,27 @@ open internalEq @[rocq_alias discrete_eq_1] theorem discrete_eq_mp {A : Type _} [OFE A] {a b : A} [TCOr (DiscreteE a) (DiscreteE b)] : - internalEq a b ⊢@{PROP} ⌜a ≡ b⌝ := + a ≡ b ⊢@{PROP} ⌜a ≡ b⌝ := siPure_mono (SiProp.discrete_eq_internalEq _ _)|>.trans siPure_pure.mp @[rocq_alias discrete_eq] theorem discrete_eq {A : Type _} [OFE A] {a b : A} [TCOr (DiscreteE a) (DiscreteE b)] : - internalEq a b ⊣⊢@{PROP} ⌜a ≡ b⌝ := + a ≡ b ⊣⊢@{PROP} ⌜a ≡ b⌝ := ⟨discrete_eq_mp, of_pure⟩ @[rocq_alias fun_extI] theorem fun_extI {A : Type _} {B : A → Type _} [OFEFun B] {f g : (x : A) → B x} : - (∀ x, internalEq (f x) (g x)) ⊢ internalEq (PROP := PROP) f g := + (∀ x, (f x) ≡ (g x)) ⊢@{PROP} f ≡ g := siPure_forall_mpr.trans <| siPure_mono (SiProp.fun_ext_internalEq f g) @[rocq_alias sig_equivI_1] theorem sig_equivI_mp {A : Type _} [OFE A] {P : A → Prop} {x y : Subtype P} : - internalEq x.val y.val ⊢@{PROP} internalEq x y := + x.val ≡ y.val ⊢@{PROP} x ≡ y := siPure_mono (SiProp.sig_equiv_internalEq P x y) @[rocq_alias sig_equivI] theorem sig_equivI {A : Type _} [OFE A] (P : A → Prop) (x y : Subtype P) : - internalEq x.val y.val ⊣⊢@{PROP} internalEq x y := + x.val ≡ y.val ⊣⊢@{PROP} x ≡ y := ⟨sig_equivI_mp, of_internalEquiv_ne Subtype.val⟩ -- TODO: sum_equivI (requires Sum OFE) @@ -132,31 +137,31 @@ theorem sig_equivI {A : Type _} [OFE A] (P : A → Prop) (x y : Subtype P) : @[rocq_alias prod_equivI] theorem prod_equivI {A B : Type _} [OFE A] [OFE B] (x y : A × B) : - internalEq x y ⊣⊢@{PROP} internalEq x.1 y.1 ∧ internalEq x.2 y.2 := by + x ≡ y ⊣⊢@{PROP} x.1 ≡ y.1 ∧ x.2 ≡ y.2 := by constructor · exact and_intro (of_internalEquiv_ne Prod.fst) (of_internalEquiv_ne Prod.snd) - · letI _ : NonExpansive (fun a => internalEq (PROP := PROP) x (a, y.2)) := + · letI _ : NonExpansive (fun a => (iprop(x ≡ (a, y.2)) : PROP)) := (ne_r x).comp (prod_mk_ne_left y.2) - letI _ : NonExpansive (fun b => internalEq (PROP := PROP) x (x.1, b)) := + letI _ : NonExpansive (fun b => (iprop(x ≡ (x.1, b)) : PROP)) := (ne_r x).comp (prod_mk_ne_right x.1) - refine rewrite' (fun a => internalEq x (a, y.2)) and_elim_l ?_ - exact rewrite' (fun b => internalEq x (x.1, b)) and_elim_r refl + refine rewrite' (fun a => iprop(x ≡ (a, y.2))) and_elim_l ?_ + exact rewrite' (fun b => iprop(x ≡ (x.1, b))) and_elim_r refl @[rocq_alias option_equivI] theorem option_some_equivI {A : Type _} [OFE A] (a b : A) : - internalEq (some a) (some b) ⊣⊢@{PROP} internalEq a b := by + some a ≡ some b ⊣⊢@{PROP} a ≡ b := by refine ⟨?_, of_internalEquiv_ne some⟩ let Ψ : Option A → PROP := fun y => - match y with | some b => internalEq a b | none => iprop(⌜False⌝) + match y with | some b => iprop(a ≡ b) | none => iprop(⌜False⌝) have : NonExpansive Ψ := Option.ne_match _ (ne_r a) _ exact rewrite' Ψ .rfl refl theorem option_none_equivI (A : Type _) [OFE A] : - internalEq (none : Option A) none ⊣⊢@{PROP} True := + (none : Option A) ≡ none ⊣⊢@{PROP} True := ⟨true_intro, refl⟩ theorem option_some_none_equivI {A : Type _} [OFE A] (a : A) : - internalEq (some a) (none : Option A) ⊣⊢@{PROP} False := by + some a ≡ (none : Option A) ⊣⊢@{PROP} False := by refine ⟨?_, false_elim⟩ let Ψ : Option A → PROP := fun y => match y with | some _ => iprop(⌜True⌝) | none => iprop(⌜False⌝) @@ -164,24 +169,24 @@ theorem option_some_none_equivI {A : Type _} [OFE A] (a : A) : exact rewrite' Ψ .rfl true_intro theorem option_none_some_equivI {A : Type _} [OFE A] (a : A) : - internalEq (none : Option A) (some a) ⊣⊢@{PROP} False := + (none : Option A) ≡ some a ⊣⊢@{PROP} False := ⟨symm.trans (option_some_none_equivI a).1, false_elim⟩ @[rocq_alias excl_equivI] theorem excl_equivI_excl {O : Type _} [OFE O] (a b : O) : - internalEq (Excl.excl a) (Excl.excl b) ⊣⊢@{PROP} internalEq a b := by + Excl.excl a ≡ Excl.excl b ⊣⊢@{PROP} a ≡ b := by refine ⟨?_, of_internalEquiv_ne Excl.excl⟩ let Ψ : Excl O → PROP := fun y => - match y with | Excl.excl b => internalEq a b | Excl.invalid => iprop(⌜False⌝) + match y with | Excl.excl b => iprop(a ≡ b) | Excl.invalid => iprop(⌜False⌝) have : NonExpansive Ψ := Excl.ne_match _ (ne_r a) _ exact rewrite' Ψ .rfl refl theorem excl_equivI_invalid (O : Type _) [OFE O] : - internalEq (Excl.invalid : Excl O) Excl.invalid ⊣⊢@{PROP} True := + (Excl.invalid : Excl O) ≡ Excl.invalid ⊣⊢@{PROP} True := ⟨true_intro, refl⟩ theorem excl_equivI_excl_invalid {O : Type _} [OFE O] (a : O) : - internalEq (Excl.excl a) (Excl.invalid : Excl O) ⊣⊢@{PROP} False := by + Excl.excl a ≡ (Excl.invalid : Excl O) ⊣⊢@{PROP} False := by refine ⟨?_, false_elim⟩ let Ψ : Excl O → PROP := fun y => match y with | Excl.excl _ => iprop(⌜True⌝) | Excl.invalid => iprop(⌜False⌝) @@ -189,22 +194,22 @@ theorem excl_equivI_excl_invalid {O : Type _} [OFE O] (a : O) : exact rewrite' Ψ .rfl true_intro theorem excl_equivI_invalid_excl {O : Type _} [OFE O] (a : O) : - internalEq (Excl.invalid : Excl O) (Excl.excl a) ⊣⊢@{PROP} False := + (Excl.invalid : Excl O) ≡ Excl.excl a ⊣⊢@{PROP} False := ⟨symm.trans (excl_equivI_excl_invalid a).1, false_elim⟩ @[rocq_alias csum_equivI] theorem csum_equivI {A B : Type _} [OFE A] [OFE B] (sx sy : Csum A B) : - internalEq sx sy ⊣⊢@{PROP} + sx ≡ sy ⊣⊢@{PROP} match sx, sy with - | .inl x, .inl y => internalEq x y - | .inr x, .inr y => internalEq x y + | .inl x, .inl y => iprop(x ≡ y) + | .inr x, .inr y => iprop(x ≡ y) | .invalid, .invalid => iprop(⌜True⌝) | _, _ => iprop(⌜False⌝) := by constructor · let Ψ : Csum A B → PROP := fun sy' => match sx, sy' with - | .inl x, .inl y => internalEq x y - | .inr x, .inr y => internalEq x y + | .inl x, .inl y => iprop(x ≡ y) + | .inr x, .inr y => iprop(x ≡ y) | .invalid, .invalid => iprop(⌜True⌝) | _, _ => iprop(⌜False⌝) have : NonExpansive Ψ := by @@ -221,8 +226,8 @@ theorem csum_equivI {A B : Type _} [OFE A] [OFE B] (sx sy : Csum A B) : | exact false_elim theorem discreteFun_equivI_mp {A : Type _} {B : A → Type _} [OFEFun B] (f g : (x : A) → B x) : - internalEq f g ⊢@{PROP} ∀ x, internalEq (f x) (g x) := by - let Ψ : ((x : A) → B x) → PROP := fun g => iprop(∀ x, internalEq (A := B x) (f x) (g x)) + f ≡ g ⊢@{PROP} ∀ x, f x ≡ g x := by + let Ψ : ((x : A) → B x) → PROP := fun g => iprop(∀ x, f x ≡ g x) have : NonExpansive Ψ := ⟨fun {_ _ _} h => sForall_ne ⟨ fun p ⟨a, ha⟩ => ⟨_, ⟨a, rfl⟩, ha ▸ (ne_r (f a)).ne (h a)⟩, fun p ⟨a, ha⟩ => ⟨_, ⟨a, rfl⟩, ha ▸ (ne_r (f a)).ne (h a)⟩⟩⟩ @@ -230,113 +235,113 @@ theorem discreteFun_equivI_mp {A : Type _} {B : A → Type _} [OFEFun B] (f g : @[rocq_alias discrete_fun_equivI] theorem discreteFun_equivI {A : Type _} {B : A → Type _} [OFEFun B] (f g : (x : A) → B x) : - internalEq f g ⊣⊢@{PROP} ∀ x, internalEq (f x) (g x) := + f ≡ g ⊣⊢@{PROP} ∀ x, f x ≡ g x := ⟨discreteFun_equivI_mp f g, fun_extI⟩ theorem ofeMorO_equivI_mp {A B : Type _} [OFE A] [OFE B] (f g : A -n> B) : - internalEq f g ⊢@{PROP} ∀ x, internalEq (f x) (g x) := by - let Ψ : (A -n> B) → PROP := fun g => iprop(∀ x, internalEq (A := B) (f x) (g x)) + f ≡ g ⊢@{PROP} ∀ x, f x ≡ g x := by + let Ψ : (A -n> B) → PROP := fun g => iprop(∀ x, f x ≡ g x) have : NonExpansive Ψ := ⟨fun {_ _ _} h => sForall_ne ⟨ fun p ⟨a, ha⟩ => ⟨_, ⟨a, rfl⟩, ha ▸ (ne_r (f a)).ne (h a)⟩, fun p ⟨a, ha⟩ => ⟨_, ⟨a, rfl⟩, ha ▸ (ne_r (f a)).ne (h a)⟩⟩⟩ exact rewrite' Ψ .rfl (forall_intro fun _ => refl) theorem ofeMorO_equivI_mpr {A B : Type _} [OFE A] [OFE B] (f g : A -n> B) : - (∀ x, internalEq (f x) (g x)) ⊢@{PROP} internalEq f g := by + (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g := by refine (discreteFun_equivI (PROP := PROP) f.f g.f).2 |>.trans ?_ refine (sig_equivI_mp (x := f.toSubtype) (y := g.toSubtype)).trans ?_ exact of_internalEquiv_ne Hom.ofSubtype @[rocq_alias ofe_morO_equivI] theorem ofeMorO_equivI {A B : Type _} [OFE A] [OFE B] (f g : A -n> B) : - internalEq f g ⊣⊢@{PROP} ∀ x, internalEq (f x) (g x) := + f ≡ g ⊣⊢@{PROP} ∀ x, f x ≡ g x := ⟨ofeMorO_equivI_mp f g, ofeMorO_equivI_mpr f g⟩ /-! ## Modalities -/ @[rocq_alias absorbingly_internal_eq] theorem absorbingly_internalEq {A : Type _} [OFE A] (x y : A) : - internalEq x y ⊣⊢@{PROP} internalEq x y := + x ≡ y ⊣⊢@{PROP} x ≡ y := absorbingly_siPure @[rocq_alias persistently_internal_eq] theorem persistently_internalEq {A : Type _} [OFE A] (a b : A) : - internalEq a b ⊣⊢@{PROP} internalEq a b := + a ≡ b ⊣⊢@{PROP} a ≡ b := persistently_siPure @[rocq_alias internal_eq_absorbing] instance internalEq_absorbing {A : Type _} [OFE A] (x y : A) : - Absorbing (PROP := PROP) (internalEq x y) where + Absorbing (PROP := PROP) iprop(x ≡ y) where absorbing := (absorbingly_internalEq x y).1 @[rocq_alias internal_eq_persistent] instance internalEq_persistent {A : Type _} [OFE A] (a b : A) : - Persistent (PROP := PROP) (internalEq a b) where + Persistent (PROP := PROP) iprop(a ≡ b) where persistent := (persistently_internalEq a b).2 /-! ## Equality under a later -/ @[rocq_alias later_equivI_1] theorem later_equivI_mp {A : Type _} [OFE A] (x y : A) : - internalEq (PROP := PROP) (Later.next x) (Later.next y) ⊢ ▷ internalEq x y := + Later.next x ≡ Later.next y ⊢@{PROP} ▷ x ≡ y := (siPure_mono (SiProp.later_equiv_internalEq_mp x y)).trans siPure_later.mp @[rocq_alias later_equivI_2] theorem later_equivI_mpr {A : Type _} [OFE A] (x y : A) : - ▷ internalEq x y ⊢@{PROP} internalEq (Later.next x) (Later.next y) := + ▷ x ≡ y ⊢@{PROP} Later.next x ≡ Later.next y := siPure_later.mpr.trans (siPure_mono (SiProp.later_equiv_internalEq_mpr x y)) @[rocq_alias later_equivI] theorem later_equivI {A : Type _} [OFE A] (x y : A) : - internalEq (PROP := PROP) (Later.next x) (Later.next y) ⊣⊢ ▷ internalEq x y := + Later.next x ≡ Later.next y ⊣⊢@{PROP} ▷ x ≡ y := ⟨later_equivI_mp x y, later_equivI_mpr x y⟩ @[rocq_alias f_equivI_contractive] theorem f_equivI_contractive {A B : Type _} [OFE A] [OFE B] (f : A → B) [hf : Contractive f] - (x y : A) : ▷ internalEq x y ⊢@{PROP} internalEq (f x) (f y) := by + (x y : A) : ▷ x ≡ y ⊢@{PROP} f x ≡ f y := by letI _ : NonExpansive (f ∘ Later.car) := ⟨fun {_ _ _} h => hf.distLater_dist h⟩ exact (later_equivI_mpr x y).trans <| of_internalEquiv_ne (f ∘ Later.car) @[rocq_alias internal_eq_rewrite_contractive] theorem internalEq_rewrite_contractive {A : Type _} [OFE A] (a b : A) (Ψ : A → PROP) [Contractive Ψ] : - ▷ internalEq a b ⊢ Ψ a → Ψ b := + ▷ a ≡ b ⊢ Ψ a → Ψ b := (f_equivI_contractive Ψ a b).trans (rewrite id) @[rocq_alias internal_eq_rewrite_contractive'] theorem internalEq_rewrite_contractive' {A : Type _} [OFE A] (a b : A) (Ψ : A → PROP) - [Contractive Ψ] (Heq : P ⊢ ▷ internalEq a b) (HΨa : P ⊢ Ψ a) : P ⊢ Ψ b := + [Contractive Ψ] (Heq : P ⊢ ▷ a ≡ b) (HΨa : P ⊢ Ψ a) : P ⊢ Ψ b := (and_intro .rfl HΨa).trans <| (and_mono_left Heq).trans <| imp_elim (internalEq_rewrite_contractive a b Ψ) @[rocq_alias eq_timeless] instance eq_timeless {A : Type _} [OFE A] (a b : A) [TCOr (DiscreteE a) (DiscreteE b)] : - Timeless (PROP := PROP) (internalEq a b) where + Timeless (PROP := PROP) iprop(a ≡ b) where timeless := - calc iprop(▷ internalEq a b) + calc iprop(▷ a ≡ b) _ ⊢ ▷ ⌜a ≡ b⌝ := later_mono discrete_eq.1 _ ⊢ ◇ ⌜a ≡ b⌝ := Timeless.timeless (P := iprop(⌜a ≡ b⌝)) - _ ⊢ ◇ internalEq a b := except0_mono discrete_eq.2 + _ ⊢ ◇ a ≡ b := except0_mono discrete_eq.2 /-! ## Equality of propositions -/ @[rocq_alias internal_eq_iff] -theorem internalEq_iff (P Q : PROP) : internalEq P Q ⊢ iprop(P ↔ Q) := +theorem internalEq_iff (P Q : PROP) : P ≡ Q ⊢ iprop(P ↔ Q) := letI _ := NonExpansive₂.ne_right (BIBase.iff (PROP := PROP)) P rewrite' (BIBase.iff P) .rfl (and_intro (imp_intro and_elim_r) (imp_intro and_elim_r)) @[rocq_alias affinely_internal_eq_wand_iff] -theorem affinely_internalEq_wandIff (P Q : PROP) : internalEq P Q ⊢ P ∗-∗ Q := +theorem affinely_internalEq_wandIff (P Q : PROP) : (P ≡ Q) ⊢ P ∗-∗ Q := letI _ := NonExpansive₂.ne_right (wandIff (PROP := PROP)) P rewrite' (wandIff P) (affinely_elim.trans .rfl) (affinely_elim_emp.trans wandIff_refl) @[rocq_alias internal_eq_wand_iff] -theorem internalEq_wandIff (P Q : PROP) : internalEq P Q ⊢ (P ∗-∗ Q) := +theorem internalEq_wandIff (P Q : PROP) : P ≡ Q ⊢ (P ∗-∗ Q) := absorbingly_affinely_intro_of_persistent.trans (absorbingly_mono (affinely_internalEq_wandIff P Q)) @[rocq_alias si_pure_internal_eq] theorem siPure_internalEq {A : Type _} [OFE A] (x y : A) : - (SiProp.internalEq x y) ⊣⊢@{PROP} internalEq x y := .rfl + SiProp.internalEq x y ⊣⊢@{PROP} x ≡ y := .rfl @[rocq_alias prop_ext_si_emp_valid_2] theorem prop_ext_siEmpValid_mpr (P Q : PROP) : @@ -350,7 +355,7 @@ theorem prop_ext_siEmpValid_equiv (P Q : PROP) : ((Sbi.siPure_ne (PROP := PROP)).comp Sbi.siEmpValid_ne).comp (NonExpansive₂.ne_right wandIff P) refine ⟨?_, prop_ext_siEmpValid⟩ rw [← siPure_entails (PROP := PROP)] - change internalEq P Q ⊢@{PROP} (P ∗-∗ Q) + change P ≡ Q ⊢@{PROP} (P ∗-∗ Q) refine rewrite' (fun Q => iprop( (P ∗-∗ Q))) .rfl ?_ refine (pure_intro trivial).trans <| ?_ refine siPure_pure.mpr.trans (siPure_mono ?_) @@ -358,40 +363,39 @@ theorem prop_ext_siEmpValid_equiv (P Q : PROP) : @[rocq_alias later_equivI_prop_2] theorem later_equivI_prop_mpr (P Q : PROP) : - ▷ internalEq P Q ⊢ internalEq (PROP := PROP) (BIBase.later P) (BIBase.later Q) := by - show iprop(▷ (SiProp.internalEq P Q) ⊢ (SiProp.internalEq (BIBase.later P) (BIBase.later Q))) + ▷ P ≡ Q ⊢ (iprop(▷ P) ≡ iprop(▷ Q) : PROP) := by + show iprop(▷ (SiProp.internalEq P Q) ⊢ (SiProp.internalEq iprop(▷ P) iprop(▷ Q))) calc iprop(▷ (SiProp.internalEq P Q)) _ ⊢ ▷ (SiProp.internalEq P Q) := siPure_later.mpr _ ⊢ ▷ ( (P ∗-∗ Q)) := siPure_mono (later_mono (prop_ext_siEmpValid_equiv P Q).mp) _ ⊢ ▷ (P ∗-∗ Q) := siPure_mono siEmpValid_later.mpr _ ⊢ (▷ P ∗-∗ ▷ Q) := siPure_mono (siEmpValid_mono later_wand_iff) - _ ⊢ (SiProp.internalEq (BIBase.later P) (BIBase.later Q)) := + _ ⊢ (iprop(▷ P) ≡ iprop(▷ Q)) := siPure_mono (prop_ext_siEmpValid_equiv _ _).mpr @[rocq_alias internal_eq_soundness] theorem internalEq_soundness {A : Type _} [OFE A] (x y : A) : - (⊢@{PROP} internalEq x y) → x ≡ y := + (⊢@{PROP} x ≡ y) → x ≡ y := (SiProp.internalEq_soundness <| siPure_emp_valid.mp ·) /-! ## Derive NonExpansive/Contractive from internal statements -/ @[rocq_alias internal_eq_entails] theorem internalEq_entails {A B : Type _} [OFE A] [OFE B] {a₁ a₂ : A} {b₁ b₂ : B} : - (internalEq a₁ a₂ ⊢@{PROP} internalEq b₁ b₂) ↔ (∀ n, a₁ ≡{n}≡ a₂ → b₁ ≡{n}≡ b₂) := + (a₁ ≡ a₂ ⊢@{PROP} b₁ ≡ b₂) ↔ (∀ n, a₁ ≡{n}≡ a₂ → b₁ ≡{n}≡ b₂) := siPure_entails.trans (SiProp.internalEq_entails ..) @[rocq_alias ne_internal_eq] theorem ne_internalEq {A B : Type _} [OFE A] [OFE B] (f : A → B) : - NonExpansive f ↔ (∀ {x₁ x₂}, internalEq x₁ x₂ ⊢@{PROP} internalEq (f x₁) (f x₂)) := + NonExpansive f ↔ (∀ {x₁ x₂}, x₁ ≡ x₂ ⊢@{PROP} (f x₁) ≡ (f x₂)) := ⟨fun ⟨hne⟩ _ _ => internalEq_entails.mpr (fun _ h => hne h), fun h => ⟨fun {_ _ _} hx => internalEq_entails.mp h _ hx⟩⟩ @[rocq_alias ne_2_internal_eq] theorem ne_2_internalEq {A B C : Type _} [OFE A] [OFE B] [OFE C] (f : A → B → C) : NonExpansive₂ f ↔ - (∀ x₁ x₂ y₁ y₂, internalEq x₁ x₂ ∧ internalEq y₁ y₂ ⊢@{PROP} - internalEq (f x₁ y₁) (f x₂ y₂)) := by + (∀ x₁ x₂ y₁ y₂, x₁ ≡ x₂ ∧ y₁ ≡ y₂ ⊢@{PROP} f x₁ y₁ ≡ f x₂ y₂) := by constructor · intro hf x₁ x₂ y₁ y₂ letI _ := hf.uncurry @@ -402,7 +406,7 @@ theorem ne_2_internalEq {A B C : Type _} [OFE A] [OFE B] [OFE C] (f : A → B @[rocq_alias contractive_internal_eq] theorem contractive_internalEq {A B : Type _} [OFE A] [OFE B] (f : A → B) : - Contractive f ↔ (∀ x₁ x₂, ▷ internalEq x₁ x₂ ⊢@{PROP} internalEq (f x₁) (f x₂)) := + Contractive f ↔ (∀ x₁ x₂, ▷ (x₁ ≡ x₂) ⊢@{PROP} f x₁ ≡ f x₂) := ⟨fun _ x₁ x₂ => f_equivI_contractive f x₁ x₂, fun hf => ⟨fun {n x y} h => internalEq_entails.mp ((later_equivI_mp x y).trans (hf x y)) n h⟩⟩ diff --git a/Iris/Iris/BI/MonPred.lean b/Iris/Iris/BI/MonPred.lean index a48d9d63b..71a753ce5 100644 --- a/Iris/Iris/BI/MonPred.lean +++ b/Iris/Iris/BI/MonPred.lean @@ -1469,7 +1469,7 @@ instance instSbiMonPred : Sbi (MonPred I PROP) where iprop(P.monPred_at i ∗-∗ Q.monPred_at i) := fun i => and_mono (monPred_wand_force i P Q) (monPred_wand_force i Q P) have hstep : SiEmpValid.siEmpValid (iprop(∀ i, (iprop(P ∗-∗ Q) : MonPred I PROP).monPred_at i)) - ⊢@{SiProp} ∀ i, internalEq (PROP := SiProp) (P.monPred_at i) (Q.monPred_at i) := + ⊢@{SiProp} ∀ i, P.monPred_at i ≡ Q.monPred_at i := siEmpValid_forall.mp.trans <| forall_mono fun i => (siEmpValid_mono (hforce i)).trans (BI.prop_ext_siEmpValid_mpr _ _) refine hstep.trans ?_ @@ -1485,11 +1485,11 @@ instance instSbiMonPred : Sbi (MonPred I PROP) where @[rocq_alias monPred_internal_eq_unfold] theorem monPred_internal_eq_unfold {A : Type _} [OFE A] : (internalEq : A → A → MonPred I PROP) = - fun x y => (iprop(⎡(internalEq x y : PROP)⎤) : MonPred I PROP) := rfl + fun x y => (iprop(⎡(x ≡ y : PROP)⎤) : MonPred I PROP) := rfl @[rocq_alias monPred_at_internal_eq] theorem monPred_at_internal_eq {A : Type _} [OFE A] (i : I.car) (a b : A) : - (internalEq a b : MonPred I PROP).monPred_at i ⊣⊢ internalEq a b := + (iprop(a ≡ b) : MonPred I PROP).monPred_at i ⊣⊢ a ≡ b := BIBase.BiEntails.of_eq rfl @[rocq_alias monPred_at_plainly] @@ -1507,7 +1507,7 @@ theorem monPred_at_plainly (i : I.car) (P : MonPred I PROP) : @[rocq_alias monPred_equivI] theorem monPred_equivI {PROP' : Type _} [Sbi PROP'] (P Q : MonPred I PROP) : - (internalEq P Q : PROP') ⊣⊢ iprop(∀ i, internalEq (P.monPred_at i) (Q.monPred_at i)) := by + (P ≡ Q : PROP') ⊣⊢ iprop(∀ i, P.monPred_at i ≡ Q.monPred_at i) := by refine ⟨?_, ?_⟩ · refine forall_intro fun i => ?_ letI _ := MonPred.monPred_at_ne (PROP := PROP) i @@ -1525,7 +1525,7 @@ instance si_pure_objective (Pi : SiProp) : Objective (iprop( Pi) : MonP @[rocq_alias internal_eq_objective] instance internal_eq_objective {A : Type _} [OFE A] (x y : A) : - Objective (internalEq x y : MonPred I PROP) where + Objective (iprop(x ≡ y) : MonPred I PROP) where objective_at _ _ := .rfl @[rocq_alias plainly_objective] diff --git a/Iris/Iris/BI/Plainly.lean b/Iris/Iris/BI/Plainly.lean index 4e6546dbd..4744465bf 100644 --- a/Iris/Iris/BI/Plainly.lean +++ b/Iris/Iris/BI/Plainly.lean @@ -722,34 +722,34 @@ instance plainly_timeless (P : PROP) [Timeless P] : Timeless iprop(■ P) := @[rocq_alias plainly_internal_eq] theorem plainly_internalEq {A} [OFE A] {a b : A} : - iprop(■ (internalEq a b) ⊣⊢@{PROP} internalEq a b) := by + iprop(■ (a ≡ b) ⊣⊢@{PROP} a ≡ b) := by refine ⟨plainly_elim, ?_⟩ - have : OFE.NonExpansive (β := PROP) (λ x ↦ iprop(■ (internalEq a x))) := { + have : OFE.NonExpansive (β := PROP) (λ x ↦ iprop(■ (a ≡ x))) := { ne n x x' xx' := instPlainly_ne.ne ((internalEq.ne_r a).ne xx') } - refine .trans ?_ (imp_elim <| internalEq.rewrite (a := a) (fun x ↦ iprop(■ internalEq a x))) + refine .trans ?_ (imp_elim <| internalEq.rewrite (a := a) (fun x ↦ iprop(■ a ≡ x))) refine and_intro .rfl ?_ - calc iprop(internalEq a b) + calc iprop(a ≡ b) _ ⊢ True := true_intro _ ⊢ ■ (True) := plainly_pure.2 - _ ⊢ ■ (internalEq a a) := plainly_mono internalEq.refl + _ ⊢ ■ (a ≡ a) := plainly_mono internalEq.refl @[rocq_alias internal_eq_plain] -instance internalEq_plain {A} [OFE A] (a b : A) : Plain (PROP := PROP) iprop(internalEq a b) where +instance internalEq_plain {A} [OFE A] (a b : A) : Plain (PROP := PROP) iprop(a ≡ b) where plain := plainly_internalEq |>.2 @[rocq_alias prop_ext] -theorem prop_ext (P Q : PROP) : iprop(internalEq P Q ⊣⊢ ■ (P ∗-∗ Q)) := +theorem prop_ext (P Q : PROP) : iprop(P ≡ Q ⊣⊢ ■ (P ∗-∗ Q)) := have ⟨mp, mpr⟩:= prop_ext_siEmpValid_equiv P Q ⟨siPure_mono mp, siPure_mono mpr⟩ #rocq_ignore prop_ext_2 "Subsumed by `prop_ext_symm`" -theorem prop_ext_symm (P Q : PROP) : iprop(■ (P ∗-∗ Q) ⊣⊢ internalEq P Q) := +theorem prop_ext_symm (P Q : PROP) : iprop(■ (P ∗-∗ Q) ⊣⊢ P ≡ Q) := prop_ext P Q |>.symm @[rocq_alias plainly_alt] -theorem plainly_alt (P : PROP) : ■ P ⊣⊢ internalEq iprop( P) iprop(emp) := by +theorem plainly_alt (P : PROP) : ■ P ⊣⊢ iprop( P) ≡ emp := by apply plainly_affinely_elim.symm.trans refine ⟨?_, ?_⟩ · refine .trans ?_ (prop_ext (affinely P) iprop(emp) |>.2) @@ -757,34 +757,34 @@ theorem plainly_alt (P : PROP) : ■ P ⊣⊢ internalEq iprop( P) iprop refine and_intro (wand_intro_left ?_) (wand_intro_left ?_) · exact affinely_sep_mpr.trans affinely_elim_emp · exact emp_sep.1 - · calc iprop(internalEq _ _) - _ ⊢ internalEq _ _ := internalEq.symm + · calc iprop(_ ≡ _) + _ ⊢ _ ≡ _ := internalEq.symm _ ⊢ ■ iprop(emp) → ■ ( P) := internalEq.rewrite BIBase.plainly _ ⊢ True → ■ ( P) := imp_mono_left (plainly_pure.2.trans plainly_true_emp.1) _ ⊢ ■ P := true_imp.1 @[rocq_alias plainly_alt_absorbing] -theorem plainly_alt_absorbing (P : PROP)[Absorbing P] : ■ P ⊣⊢ internalEq iprop(P) iprop(True) := by +theorem plainly_alt_absorbing (P : PROP)[Absorbing P] : ■ P ⊣⊢ P ≡ iprop(True) := by refine ⟨?_, ?_⟩ · refine .trans ?_ (prop_ext P iprop(True) |>.2) refine plainly_mono ?_ exact and_intro (wand_intro_left true_intro) (wand_intro_left true_sep.1) - · calc iprop(internalEq _ _) - _ ⊢ internalEq _ _ := internalEq.symm + · calc iprop(_ ≡ _) + _ ⊢ _ ≡ _ := internalEq.symm _ ⊢ ■ True → ■ iprop(P) := internalEq.rewrite BIBase.plainly _ ⊢ True → ■ iprop(P) := imp_mono_left plainly_pure.2 _ ⊢ ■ P := true_imp.1 @[rocq_alias plainly_True_alt] -theorem plainly_true_alt (P : PROP) : ■ (True -∗ P) ⊣⊢ internalEq P iprop(True) := by +theorem plainly_true_alt (P : PROP) : ■ (True -∗ P) ⊣⊢ P ≡ iprop(True) := by refine ⟨?_, ?_⟩ · refine .trans ?_ (prop_ext P iprop(True) |>.2) refine plainly_mono ?_ exact and_intro (wand_intro_left true_intro) (wand_intro_left wand_elim_right) · let Ψ P : PROP := iprop(■ (True -∗ P)) haveI : OFE.NonExpansive Ψ := OFE.NonExpansive.comp (inferInstance) (wand_ne.ne_right _ _) - calc iprop(internalEq _ _) - _ ⊢ internalEq _ _ := internalEq.symm + calc iprop(_ ≡ _) + _ ⊢ _ ≡ _ := internalEq.symm _ ⊢ ■ (True -∗ True) → (■ (True -∗ P)) := internalEq.rewrite Ψ _ ⊢ ■ emp → (■ (True -∗ P)) := imp_mono_left <| plainly_mono <| wand_intro <| true_intro _ ⊢ True → (■ (True -∗ P)) := imp_mono_left (plainly_emp_intro) @@ -793,13 +793,13 @@ theorem plainly_true_alt (P : PROP) : ■ (True -∗ P) ⊣⊢ internalEq P ipro /-- Timeless instance for InternalEq based on a Plainly construction. -/ @[rocq_alias internal_eq_timeless] instance internalEq_timeless {P Q : PROP} [Timeless P] [Timeless Q] : - Timeless (PROP := PROP) (internalEq P Q) where + Timeless (PROP := PROP) iprop(P ≡ Q) where timeless := have ⟨mp, mpr⟩:= prop_ext P Q - calc iprop(▷ internalEq P Q) + calc iprop(▷ P ≡ Q) _ ⊢ ▷ ■ (P ∗-∗ Q) := later_mono mp _ ⊢ ◇ ■ (P ∗-∗ Q) := Timeless.timeless - _ ⊢ ◇ internalEq P Q := except0_mono mpr + _ ⊢ ◇ P ≡ Q := except0_mono mpr @[rocq_alias later_plainly_1] theorem later_plainly_mp {P : PROP} : ▷ ■ P ⊢ ■ ▷ P := later_plainly.1 diff --git a/Iris/Iris/Instances/Lib/Boxes.lean b/Iris/Iris/Instances/Lib/Boxes.lean index 96c39a072..51d2e94db 100644 --- a/Iris/Iris/Instances/Lib/Boxes.lean +++ b/Iris/Iris/Instances/Lib/Boxes.lean @@ -74,7 +74,7 @@ def slice (N : Namespace) (γ : SliceName) (P : IProp GF) : IProp GF := def box {M : Type _ → Type _} [LawfulFiniteMap M SliceName] (N : Namespace) (f : M Bool) (P : IProp GF) : IProp GF := iprop% ∃ Φ : SliceName → IProp GF, - ▷ internalEq P ([∗map] γ ↦ _x ∈ f, Φ γ) ∗ + ▷ (P ≡ ([∗map] γ ↦ _x ∈ f, Φ γ)) ∗ [∗map] γ ↦ b ∈ f, box_own_auth γ (◯E (⟨b⟩ : BoolO)) ∗ box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)) @[rocq_alias box_inv_ne] @@ -123,7 +123,7 @@ theorem box_own_auth_update {γ : SliceName} {b1 b2: Bool} (b3 : Bool) : @[rocq_alias box_own_agree] theorem box_own_agree (γ : SliceName) (Q1 Q2 : IProp GF) : - box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ internalEq Q1 Q2 := by + box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2) := by simp only [box_own_prop, ←iOwn_op.to_eq] iintro H icases iOwn_cmraValid $$ H with H @@ -180,7 +180,7 @@ theorem slice_delete_empty {M : Type _ → Type _} [LawfulFiniteMap M SliceName] {γ : SliceName} {N : Namespace} (Hf : get? f γ = some false) : slice N γ Q ∗ ▷?q box N f P ⊢ - |={E}=> ∃ P', ▷?q (▷ internalEq P iprop(Q ∗ P')) ∗ ▷?q (box N (delete f γ) P') := by + |={E}=> ∃ P', ▷?q (▷ (P ≡ iprop(Q ∗ P'))) ∗ ▷?q (box N (delete f γ) P') := by unfold slice box iintro ⟨⟨#Hprop, #Hinv⟩, %Φ, #Heq, Hbig⟩ iexists iprop([∗map] γ' ↦ _x ∈ delete f γ, Φ γ') @@ -281,7 +281,7 @@ theorem slice_delete_full {M : Type _ → Type _} [LawfulFiniteMap M SliceName] (HE : ↑N ⊆ E) (Hf : PartialMap.get? f γ = some true) : slice N γ Q ∗ (▷?q box N f P) ⊢ |={E}=> ∃ P', ▷ Q ∗ - (▷?q ▷ internalEq P iprop(Q ∗ P')) ∗ (▷?q box N (delete f γ) P') := by + (▷?q ▷ (P ≡ iprop(Q ∗ P'))) ∗ (▷?q box N (delete f γ) P') := by iintro ⟨#Hslice, Hbox⟩ imod slice_empty HE Hf $$ [$Hslice $Hbox] with ⟨HQ, Hbox⟩ imod slice_delete_empty (get?_insert_eq rfl) $$ [$Hslice $Hbox] with ⟨%P', #Heq, Hbox⟩ diff --git a/Iris/Iris/Instances/Lib/WSat.lean b/Iris/Iris/Instances/Lib/WSat.lean index dea55be69..23b5c87ae 100644 --- a/Iris/Iris/Instances/Lib/WSat.lean +++ b/Iris/Iris/Instances/Lib/WSat.lean @@ -198,7 +198,7 @@ variable {GF : BundledGFunctors} [W : WsatGS GF] @[rocq_alias invariant_lookup] theorem invariant_lookup (I : InvMap (IProp GF)) (i : Pos) (P : IProp GF) : iOwn (E := W.inv) W.invariant_name (invMap I) ∗ ownI i P - ⊢@{IProp GF} ∃ Q, ⌜get? I i = .some Q⌝ ∗ ▷ internalEq Q P := by + ⊢@{IProp GF} ∃ Q, ⌜get? I i = .some Q⌝ ∗ ▷ (Q ≡ P) := by unfold ownI iintro H ihave H := iOwn_cmraValid_op $$ H diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean index ac2ca161b..4c8608ad7 100644 --- a/Iris/Iris/ProofMode/Classes.lean +++ b/Iris/Iris/ProofMode/Classes.lean @@ -115,7 +115,7 @@ export IntoOr (into_or) @[ipm_class, rocq_alias IntoInternalEq] class IntoInternalEq {PROP} [BI PROP] [Sbi PROP] {A : outParam $ Type _} [ofe : outParam $ OFE A] (P : PROP) (x y : outParam A) where - into_internal_eq : P ⊢@{PROP} internalEq x y + into_internal_eq : P ⊢@{PROP} x ≡ y export IntoInternalEq (into_internal_eq) @[ipm_class, rocq_alias IntoPersistent] diff --git a/Iris/Iris/ProofMode/InstancesCmra.lean b/Iris/Iris/ProofMode/InstancesCmra.lean index f7a53f983..870b41917 100644 --- a/Iris/Iris/ProofMode/InstancesCmra.lean +++ b/Iris/Iris/ProofMode/InstancesCmra.lean @@ -20,32 +20,32 @@ variable {PROP} [Sbi PROP] @[rocq_alias into_pure_internal_cmra_valid] instance intoPure_internalCmraValid α [CMRA α] [CMRA.Discrete α] (a : α) : - IntoPure (PROP:=PROP) iprop(✓ a) (✓ a) where + IntoPure (PROP := PROP) iprop(✓ a) (✓ a) where into_pure := internalCmraValid_discrete.1 @[rocq_alias from_pure_internal_cmra_valid] instance fromPure_internalCmraValid io α [CMRA α] (a : α) : - FromPure (PROP:=PROP) false iprop(✓ a) io (✓ a) where + FromPure (PROP := PROP) false iprop(✓ a) io (✓ a) where from_pure := BI.pure_elim' internalCmraValid_intro @[rocq_alias into_pure_internal_included] instance intoPure_internalCmraIncluded α [CMRA α] [CMRA.Discrete α] (a b : α) : - IntoPure (PROP:=PROP) iprop(a ≼ b) (a ≼ b) where + IntoPure (PROP := PROP) iprop(a ≼ b) (a ≼ b) where into_pure := internalCmraIncluded_discrete.1 @[rocq_alias from_pure_internal_included] instance fromPure_internalCmraIncluded io α [CMRA α] (a b : α) : - FromPure (PROP:=PROP) false iprop(a ≼ b) io (a ≼ b) where + FromPure (PROP := PROP) false iprop(a ≼ b) io (a ≼ b) where from_pure := BI.pure_elim' internalCmraIncluded_intro @[rocq_alias into_exist_internal_included] instance intoExists_internalCmraIncluded α [CMRA α] (a b : α) : - IntoExists (PROP:=PROP) iprop(a ≼ b) (λ c => internalEq b (a • c)) where + IntoExists (PROP := PROP) iprop(a ≼ b) (λ c => iprop(b ≡ (a • c))) where into_exists := siPure_exist.1 @[rocq_alias from_exist_internal_included] instance fromExists_internalCmraIncluded α [CMRA α] (a b : α) : - FromExists (PROP:=PROP) iprop(a ≼ b) (λ c => internalEq b (a • c)) where + FromExists (PROP := PROP) iprop(a ≼ b) (λ c => iprop(b ≡ (a • c))) where from_exists := siPure_exist.2 end cmra diff --git a/Iris/Iris/ProofMode/InstancesInternalEq.lean b/Iris/Iris/ProofMode/InstancesInternalEq.lean index fd2753a28..31fbb6ed0 100644 --- a/Iris/Iris/ProofMode/InstancesInternalEq.lean +++ b/Iris/Iris/ProofMode/InstancesInternalEq.lean @@ -21,33 +21,33 @@ variable {PROP} [Sbi PROP] @[rocq_alias from_pure_internal_eq] instance fromPure_internalEq [Sbi PROP] [OFE A] (a b : A) : - FromPure (PROP := PROP) false (internalEq a b) io (a ≡ b) where + FromPure (PROP := PROP) false iprop(a ≡ b) io (a ≡ b) where from_pure := internalEq.of_pure @[ipm_backtrack, rocq_alias into_pure_eq] instance intoPure_internalEq [Sbi PROP] [OFE A] (a b : A) [TCOr (OFE.DiscreteE a) (OFE.DiscreteE b)] : - IntoPure (PROP := PROP) (internalEq a b) (a ≡ b) where + IntoPure (PROP := PROP) iprop(a ≡ b) (a ≡ b) where into_pure := discrete_eq_mp @[ipm_backtrack] instance (priority := default + 10) intoPure_internalEq_leibniz [Sbi PROP] [OFE A] (a b : A) [TCOr (OFE.DiscreteE a) (OFE.DiscreteE b)] : - IntoPure (PROP := PROP) (internalEq a b) (a = b) where + IntoPure (PROP := PROP) iprop(a ≡ b) (a = b) where into_pure := discrete_eq_mp.trans (pure_mono OFE.Equiv.to_eq) @[rocq_alias from_modal_Next] instance fromModal_internalEq_next [Sbi PROP] [OFE A] (x y : A) : FromModal (PROP1 := PROP) (PROP2 := PROP) True (modality_laterN 1) - iprop(▷ internalEq x y) (internalEq (Later.next x) (Later.next y)) (internalEq x y) where + iprop(▷ (x ≡ y)) iprop(Later.next x ≡ Later.next y) iprop(x ≡ y) where from_modal _ := later_equivI_mpr x y @[rocq_alias into_laterN_Next] instance intoLaterN_internalEq_next [Sbi PROP] [OFE A] (x y : A) only_head n n' [h : NatCancel n 1 n' 0] : - IntoLaterN (PROP := PROP) only_head n (internalEq (Later.next x) (Later.next y)) - (internalEq x y) where + IntoLaterN (PROP := PROP) only_head n iprop(Later.next x ≡ Later.next y) + iprop(x ≡ y) where into_laterN := (later_equivI_mp x y).trans (by have hcancel : n' + 1 = n := by have := h.nat_cancel; omega rw [← hcancel] @@ -56,7 +56,7 @@ instance intoLaterN_internalEq_next [Sbi PROP] [OFE A] (x y : A) -- IntoInternalEq @[rocq_alias into_internal_eq_internal_eq] instance intoInternalEq_internalEq [Sbi PROP] [OFE A] (x y : A) : - IntoInternalEq (PROP := PROP) (internalEq x y) x y where + IntoInternalEq (PROP := PROP) iprop(x ≡ y) x y where into_internal_eq := .rfl @[rocq_alias into_internal_eq_affinely] diff --git a/Iris/Iris/ProofMode/Tactics/Rewrite.lean b/Iris/Iris/ProofMode/Tactics/Rewrite.lean index 8e8e2d4f1..000ac373d 100644 --- a/Iris/Iris/ProofMode/Tactics/Rewrite.lean +++ b/Iris/Iris/ProofMode/Tactics/Rewrite.lean @@ -23,11 +23,11 @@ theorem rewrite_tac [Sbi PROP] {P P' Q : PROP} {A : Type _} [OFE A] {a b : A} {p (h1 : P ⊢ P' ∗ □?p Q) : P ⊢ (Ψ a ∗-∗ Ψ b) := calc P - _ ⊢ P' ∗ internalEq a b := h1.trans (sep_mono_right (intuitionisticallyIf_elim.trans heq.1)) - _ ⊢ internalEq a b := sep_elim_right - _ ⊢ internalEq (Ψ a) (Ψ b) := internalEq.of_internalEquiv_ne Ψ - _ ⊢ internalEq (Ψ a) (Ψ b) := persistent - _ ⊢ internalEq (Ψ a) (Ψ b) := persistently_affinely.2 + _ ⊢ P' ∗ a ≡ b := h1.trans (sep_mono_right (intuitionisticallyIf_elim.trans heq.1)) + _ ⊢ a ≡ b := sep_elim_right + _ ⊢ Ψ a ≡ Ψ b := internalEq.of_internalEquiv_ne Ψ + _ ⊢ (Ψ a ≡ Ψ b) := persistent + _ ⊢ Ψ a ≡ Ψ b := persistently_affinely.2 _ ⊢ (Ψ a ∗-∗ Ψ b) := persistently_mono (affinely_internalEq_wandIff _ _) theorem rewrite_tac_symm [Sbi PROP] {P P' Q : PROP} {A : Type _} [OFE A] {a b : A} {p} diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index fb8509a5f..19671f5cd 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2082,21 +2082,21 @@ variable {A B : Type _} [OFE A] [OFE B] /- Tests `irewrite` rewriting in goal -/ example (a b : A) (P : A → PROP) [OFE.NonExpansive P] [Absorbing (P a)] : - internalEq b a ∗ P a ⊢ P b := by + b ≡ a ∗ P a ⊢ P b := by iintro ⟨Heq, Ha⟩ irewrite [Heq] iexact Ha /- Tests `irewrite` rewriting in goal explicitly -/ example (a b : A) (P : A → PROP) [OFE.NonExpansive P] [Absorbing (P a)] : - internalEq b a ∗ P a ⊢ P b := by + b ≡ a ∗ P a ⊢ P b := by iintro ⟨Heq, Ha⟩ irewrite [Heq] at ⊢ iexact Ha /- Tests `irewrite` rewriting in goal in backward direction -/ example (a b : A) (P : A → PROP) [OFE.NonExpansive P] [Absorbing (P b)] : - internalEq b a ∗ P b ⊢ P a := by + b ≡ a ∗ P b ⊢ P a := by iintro ⟨Heq, Hb⟩ irewrite [← Heq] iexact Hb @@ -2104,7 +2104,7 @@ example (a b : A) (P : A → PROP) [OFE.NonExpansive P] [Absorbing (P b)] : /- Tests `irewrite` rewriting in hypothesis -/ example (a b : A) (P Q R : A → PROP) [OFE.NonExpansive P] [OFE.NonExpansive Q] [OFE.NonExpansive R] [Absorbing iprop(P b ∗ Q b ∗ R b)] : - internalEq a b ∗ (P a ∗ Q a ∗ R a) ⊢ P b ∗ Q b ∗ R b := by + a ≡ b ∗ (P a ∗ Q a ∗ R a) ⊢ P b ∗ Q b ∗ R b := by iintro ⟨Heq, H⟩ irewrite [Heq] at H · refine ⟨fun _ _ _ h => ?_⟩ @@ -2115,7 +2115,7 @@ example (a b : A) (P Q R : A → PROP) /- Tests `irewrite` rewriting in same hypothesis -/ example (a b : A) (P : A → PROP) [OFE.NonExpansive P] [Absorbing (P b)] : - internalEq b a ⊢@{PROP} internalEq a a := by + b ≡ a ⊢@{PROP} a ≡ a := by iintro Heq irewrite [Heq] at Heq · apply internalEq.ne_l @@ -2123,7 +2123,7 @@ example (a b : A) (P : A → PROP) [OFE.NonExpansive P] [Absorbing (P b)] : /- Tests `irewrite` with proof mode terms -/ example (a b : A) (P Q : A → PROP) [OFE.NonExpansive P] [OFE.NonExpansive Q] [Absorbing (P a)] : - (∀ c, internalEq a c) ∗ P a ∗ (P b -∗ Q b) ⊢ Q b := by + (∀ c, a ≡ c) ∗ P a ∗ (P b -∗ Q b) ⊢ Q b := by iintro ⟨Heq, Ha, Himpl⟩ iapply Himpl irewrite [← Heq $$ %b, ← Heq $$ %a] @@ -2131,14 +2131,14 @@ example (a b : A) (P Q : A → PROP) [OFE.NonExpansive P] [OFE.NonExpansive Q] [ /- Tests `irewrite` with multiple rewrites -/ example (a b c : A) (P : A → PROP) [OFE.NonExpansive P] [Absorbing (P a)] : - internalEq a b ∗ internalEq b c ∗ P a ⊢ P c := by + a ≡ b ∗ b ≡ c ∗ P a ⊢ P c := by iintro ⟨Hab, Hbc, Ha⟩ irewrite [←Hbc, ←Hab] iexact Ha /- Tests `irewrite` with manual nonexpansive proof -/ example (f : A → B) [OFE.NonExpansive f] (a b : A) (P : B → PROP) [OFE.NonExpansive P] [Absorbing (P (f a))] : - internalEq a b ∗ P (f a) ⊢ P (f b) := by + a ≡ b ∗ P (f a) ⊢ P (f b) := by iintro ⟨Heq, Ha⟩ irewrite [←Heq] · exact (OFE.NonExpansive.comp (g := P) (f := f) inferInstance inferInstance) @@ -2147,7 +2147,7 @@ example (f : A → B) [OFE.NonExpansive f] (a b : A) (P : B → PROP) [OFE.NonEx /- Tests `irewrite` under separating conjunction -/ example (a b : A) (P Q R : A → PROP) [OFE.NonExpansive P] [OFE.NonExpansive Q] [OFE.NonExpansive R] [Absorbing (P a)] : - internalEq a b ∗ (P a ∗ Q a ∗ R a) ⊢ P b ∗ Q b ∗ R b := by + a ≡ b ∗ (P a ∗ Q a ∗ R a) ⊢ P b ∗ Q b ∗ R b := by iintro ⟨Heq, H⟩ irewrite [←Heq] · refine ⟨fun _ _ _ h => ?_⟩ @@ -2158,7 +2158,7 @@ example (a b : A) (P Q R : A → PROP) /- Tests `irewrite` under more connectives -/ example (x y : A) P : - ⊢@{PROP} □ (∀ z, P -∗ (internalEq z y)) -∗ (P -∗ P ∧ (internalEq (x,x) (y,x))) := by + ⊢@{PROP} □ (∀ z, P -∗ (z ≡ y)) -∗ (P -∗ P ∧ ((x, x) ≡ (y, x))) := by iintro #H1 H2 irewrite [H1 $$ %x H2] · refine ⟨fun _ _ _ h => and_ne.ne .rfl ?_⟩ @@ -2170,7 +2170,7 @@ example (x y : A) P : /- Tests `irewrite` with Later.next -/ example (f : A -n> A) x y : - ⊢@{PROP} internalEq (Later.next x) (Later.next y) -∗ internalEq (Later.next (f x)) (Later.next (f y)) := by + ⊢@{PROP} (Later.next x ≡ Later.next y) -∗ (Later.next (f x) ≡ Later.next (f y)) := by iintro H -- FIXME: inext iapply later_equivI_mpr @@ -2182,7 +2182,7 @@ example (f : A -n> A) x y : /- Tests `irewrite` under affine and later -/ example (P Q : PROP) : - ▷ (internalEq Q P) -∗ ▷ Q -∗ ▷ P := by + ▷ (Q ≡ P) -∗ ▷ Q -∗ ▷ P := by iintro #HPQ HQ !> inext irewrite [HPQ] at HQ @@ -2191,7 +2191,7 @@ example (P Q : PROP) : /- Tests `irewrite` under affine and later backwards -/ example (P Q : PROP) : - ▷ (internalEq Q P) -∗ ▷ P -∗ ▷ Q := by + ▷ (Q ≡ P) -∗ ▷ P -∗ ▷ Q := by iintro #HPQ HQ !> inext irewrite [←HPQ] at HQ @@ -2207,7 +2207,7 @@ in the target expression -/ #guard_msgs in example (P Q : PROP) : - internalEq P Q -∗ Q := by + P ≡ Q -∗ Q := by iintro HPQ irewrite [HPQ]