Alternative definition for CMRA

src/Iris/Algebra/CMRA.lean

@@ -8,46 +8,63 @@ import Iris.Algebra.OFE
 namespace Iris
 open OFE
 
-class CMRA (α : Type _) extends OFE α where
-  pcore : α → Option α
+class PreCMRA (α : Type _) extends OFE α where
   op : α → α → α
   validN : Nat → α → Prop
   valid : α → Prop
 
-  op_ne : NonExpansive (op x)
-  pcore_ne : x ≡{n}≡ y → pcore x = some cx →
-    ∃ y, pcore y = some cy ∧ cx ≡{n}≡ cy
-  validN_ne : x ≡{n}≡ y → validN n x → validN n y
+export PreCMRA (op validN valid)
+
+namespace CMRA
+
+infix:60 " • " => op
+
+def included [PreCMRA α] (x y : α)  : Prop := ∃ z, y ≡ x • z
+infix:50 " ≼ " => included
+
+def includedN [PreCMRA α] (n : Nat) (x y : α) : Prop := ∃ z, y ≡{n}≡ x • z
+notation:50 x " ≼{" n "} " y:51 => includedN n x y
+
+prefix:50 "✓" => valid
+notation:50 "✓{" n "}" x:51 => validN n x
+
+abbrev is_idempotentN_lb [PreCMRA α] (x : α) (n : Nat) (y : α) : Prop :=
+  y ≼{n} x ∧ y • y ≡{n}≡ y
+
+abbrev is_maximal_idempotentN_lb [PreCMRA α] (x : α) (n : Nat) (cx : α) : Prop :=
+  is_idempotentN_lb x n cx ∧ ∀ m y, m ≤ n -> is_idempotentN_lb x m y -> y ≼{m} cx
+
+abbrev no_maximal_idempotentN [PreCMRA α] (x : α) : Prop :=
+  ∀ y, ¬ is_idempotentN_lb x 0 y
 
+inductive MI [PreCMRA α] (x : α) (n : Nat) : Type _ where
+| HasMI (cx : α) : is_maximal_idempotentN_lb x n cx -> MI x n
+| NoMI : no_maximal_idempotentN x -> MI x n
+
+end CMRA
+
+class CMRA (α : Type _) extends PreCMRA α where
+  op_ne : NonExpansive (op x)
+  valid_imp_eqv : x₁ ≡{n}≡ x₂ -> validN n x₁ -> validN n x₂
   valid_validN : valid x ↔ ∀ n, validN n x
   validN_succ : validN n.succ x → validN n x
   assoc : op x (op y z) = op (op x y) z
   comm : op x y = op y x
-  pcore_l : pcore x = some cx → op cx x ≡ x
-  pcore_idem : pcore x = some cx → pcore cx ≡ some cx
-  pcore_mono' : pcore x = some cx → ∃ cy, pcore (op x y) = some (op cx cy)
-  validN_op_l : validN n (op x y) → validN n x
+  validN_l : validN n (op x y) -> validN n x
   extend : validN n x → x ≡{n}≡ op y₁ y₂ →
     Σ' z₁ z₂, x ≡ op z₁ z₂ ∧ z₁ ≡{n}≡ y₁ ∧ z₂ ≡{n}≡ y₂
+  mi : validN n x -> CMRA.MI x n
 
 namespace CMRA
 variable [CMRA α]
 
-infix:60 " • " => op
-
-def included (x y : α) : Prop := ∃ z, y ≡ x • z
-infix:50 " ≼ " => included
-
 def op? [CMRA α] (x : α) : Option α → α
   | some y => x • y
   | none => x
 infix:60 " •? " => op?
 
-prefix:50 "✓" => valid
-notation:50 "✓{" n "}" x:51 => validN n x
-
 class CoreId (x : α) : Prop where
-  core_id : pcore x ≡ some x
+  core_id : x ≡ x • x
 
 class Exclusive (x : α) : Prop where
   exclusive0_l : ¬✓{0} x • y
@@ -59,9 +76,7 @@ class IdFree (x : α) : Prop where
   id_free0_r : ✓{0} x → ¬x • y ≡{0}≡ x
 
 class IsTotal (α : Type _) [CMRA α] where
-  total (x : α) : ∃ cx, pcore x = some cx
-
-def core (x : α) := (pcore x).getD x
+  total (x : α) : ∃ cx, cx ≼ x ∧ cx ≡ cx • cx
 
 class Discrete (α : Type _) [CMRA α] extends OFE.Discrete α where
   discrete_valid {x : α} : ✓{0} x → ✓ x
@@ -72,4 +87,6 @@ class UCMRA (α : Type _) extends CMRA α where
   unit : α
   unit_valid : ✓ unit
   unit_left_id : unit • x ≡ x
-  pcore_unit : pcore unit ≡ some unit
+
+class CMRATotal (α : Type _) extends CMRA α where
+  total : ∀ x, ∃ (cx : α), cx ≼ x ∧ cx • cx ≡ cx