Skip to content

feat: notations for internalCmraValid, internalEq, internalIncluded #519

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
alvinylt wants to merge 4 commits into
base: master
Choose a base branch
from
Open

feat: notations for internalCmraValid, internalEq, internalIncluded #519

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0c8251a
Add notation for `internalCmraValid` and documentation
alvinylt Jul 16, 2026
0243b67
Use `✓` for `internalCmraValid`
alvinylt Jul 16, 2026
b9cd0eb
Use `≼` for `internalCmraIncluded`
alvinylt Jul 16, 2026
a1bb217
Use `≡` for `internalEq`
alvinylt Jul 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions Iris/Iris/Algebra/CMRA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
82 changes: 41 additions & 41 deletions Iris/Iris/BI/Algebra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ?_
Expand All @@ -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)
Expand All @@ -53,16 +53,16 @@ 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

@[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) ∨ (x ≡ y))
| none, _ => iprop(True)
| some _, none => iprop(False) := by
rcases mx with _ | x <;> rcases my with _ | y
Expand All @@ -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
Expand All @@ -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
Expand All @@ -122,13 +122,13 @@ 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') ∧
internalCmraIncluded (Option.some (dq, v)) (Option.some (dq', v')) := by
✓ (Auth dp m • Frag k dq v) ⊣⊢@{PROP}
∃ v' dq', ⌜✓ dp⌝ ∧ ⌜get? m k = .some v'⌝ ∧ ✓ (dq', v') ∧
some (dq, v) ≼ some (dq', v') := by
suffices H :
(<si_pure> SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊣⊢@{PROP}
(<si_pure> ∃ 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
Expand Down Expand Up @@ -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 ∧ get? m k ≡ .some v := by
simp only [internalCmraValid, internalEq, ←siPure_and.to_eq]
rw [←siPure_pure.to_eq, ←siPure_and.to_eq]
constructor
Expand All @@ -170,12 +170,12 @@ 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' ∧ v ≼ v' := by
suffices H : (<si_pure> SiProp.cmraValid (HeapView.Auth dp m • Frag k dq v) ⊢@{PROP}
<si_pure> (∃ 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
Expand All @@ -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 => ?_
Expand All @@ -210,30 +210,30 @@ 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} : internalCmraValid (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]
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} 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, 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
Expand All @@ -245,27 +245,27 @@ 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
exact (and_intro (H1.trans internalEq.symm) H2).trans internalEq.trans

@[rocq_alias agree_includedI]
theorem agree_includedI (x y : Agree A) :
internalCmraIncluded 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)
Expand All @@ -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} a ≡ b := by
constructor
· refine siPure_mono (exists_elim (fun c => ?_))
exact (fun n Heq => toAgree_includedN.mp ⟨c, Heq⟩)
Expand All @@ -293,35 +293,35 @@ 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)⌝ ∧ 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 => ?_⟩
all_goals simp only [SiProp.cmraValid, auth_dfrac_op_validN]; exact id

@[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⌝ ∧ 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 ?_
Expand All @@ -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}
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]
Expand Down
Loading