feat: View CMRA

src/Iris/Algebra.lean

@@ -4,3 +4,4 @@ import Iris.Algebra.COFESolver
 import Iris.Algebra.OFE
 import Iris.Algebra.Frac
 import Iris.Algebra.Heap
+import Iris.Algebra.View

src/Iris/Algebra/Agree.lean

@@ -233,6 +233,41 @@ theorem Agree.includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x :=
 theorem Agree.included {x y : Agree α} : x ≼ y ↔ y ≡ y • x :=
   ⟨fun ⟨z, h⟩ n => includedN.mp ⟨z, h n⟩, fun h => ⟨y, h.trans op_comm⟩⟩
 
+theorem Agree.toAgree.is_discrete {a : α} (Ha : OFE.DiscreteE a) : OFE.DiscreteE (toAgree a) := by
+  refine ⟨fun ⟨Hal, Har⟩ _ => ?_⟩
+  constructor <;> simp_all [toAgree]
+  · rcases Hal with ⟨b, Hb1, Hb2⟩
+    exact ⟨b, ⟨Hb1, Ha.discrete (Har b Hb1) |>.dist⟩⟩
+  · intro H Hb
+    exact Ha.discrete (Har H Hb) |>.dist
+
+open OFE OFE.Discrete in
+instance [OFE α] [Discrete α] : Discrete (Agree α) where
+  discrete_0 {x y} H := by
+    refine fun n => ⟨fun a Ha => ?_, fun b Hb => ?_⟩
+    · rcases H.1 a Ha with ⟨c, Hc⟩
+      refine ⟨c, ⟨Hc.1, ?_⟩⟩
+      apply equiv_dist.mp <| discrete_0 (Hc.2.le <| Nat.zero_le 0)
+    · rcases H.2 b Hb with ⟨c, Hc⟩
+      refine ⟨c, ⟨Hc.1, ?_⟩⟩
+      apply equiv_dist.mp <| discrete_0 (Hc.2.le <| Nat.zero_le 0)
+
+instance toAgree.ne [OFE α] : OFE.NonExpansive (toAgree : α → Agree α) where
+  ne n x y H := by
+    refine ⟨?_, ?_⟩
+    · intro a Ha; exists y; revert Ha
+      simp [toAgree]; exact (·▸H)
+    · intro b Hb; exists x; revert Hb
+      simp [toAgree]; exact (·▸H)
+
+theorem toAgree.inj {a1 a2 : α} {n} (H : toAgree a1 ≡{n}≡ toAgree a2) : a1 ≡{n}≡ a2 := by
+  have Hinc : a1 ∈ (toAgree a1).car := by simp [toAgree]
+  rcases H.1 a1 Hinc with ⟨_, ⟨_, _⟩⟩
+  simp_all [toAgree]
+
+instance : CMRA.IsTotal (Agree α) where
+  total := by simp [CMRA.pcore]
+
 theorem Agree.valid_includedN {x y : Agree α} : ✓{n} y → x ≼{n} y → x ≡{n}≡ y := by
   intro hval ⟨z, heq⟩
   have : ✓{n} (x • z) := heq.validN.mp hval
@@ -354,4 +389,9 @@ theorem Agree.agree_map_ext {g : α → β} [OFE.NonExpansive g] (heq : ∀ a, f
   · exact ⟨g a, ⟨a, ha, rfl⟩, (heq a).dist⟩
   · exact ⟨f a, ⟨a, ha, rfl⟩, (heq a).dist⟩
 
+theorem toAgree.incN {a b : α} {n} : toAgree a ≼{n} toAgree b ↔ a ≡{n}≡ b := by
+  refine ⟨?_, fun H => (CMRA.incN_iff_right <| toAgree.ne.ne H).mp <| CMRA.incN_refl _⟩
+  intro H
+  apply toAgree.inj
+  exact Agree.valid_includedN trivial H
 end agree_map

src/Iris/Algebra/CMRA.lean

@@ -183,6 +183,7 @@ theorem op_opM_assoc (x y : α) (mz : Option α) : (x • y) •? mz ≡ x • (
 theorem op_opM_assoc_dist (x y : α) (mz : Option α) : (x • y) •? mz ≡{n}≡ x • (y •? mz) := by
   unfold op?; cases mz <;> simp [assoc.dist, Dist.symm]
 
+
 /-! ## Validity -/
 
 theorem Valid.validN : ✓ (x : α) → ✓{n} x := (valid_iff_validN.1 · _)
@@ -1253,10 +1254,12 @@ theorem some_incN_some_iff_opM {a b : α} : some a ≼{n} some b ↔ ∃ mc, b 
     · exact .inl H.symm
     · right; exists z
 
+
+
 instance [CMRA.Discrete α] : CMRA.Discrete (Option α) where
   discrete_valid {x} := by
-    cases x <;> simp [Valid]
-    exact (discrete_valid ·)
+    cases x <;> simp [CMRA.Valid, optionValid]
+    exact (CMRA.discrete_valid ·)
 
 end Option
 end option

src/Iris/Algebra/Heap.lean

@@ -72,7 +72,6 @@ instance Heap.instCOFE [Heap T K V] [COFE V] : COFE T where
 
 end OFE
 
-
 section CMRA
 open CMRA