Add updates

Author: suhr

src/Iris/Algebra/Updates.lean

@@ -0,0 +1,195 @@
+import Iris.Algebra.CMRA
+
+namespace Iris
+
+def cmra_updateP [CMRA A] (x : A) (P : A → Prop) := ∀ n mz,
+  ✓{n} (x •? mz) → ∃ y, P y ∧ ✓{n} (y •? mz)
+infixr:50 " ~~>: " => cmra_updateP
+
+def cmra_update [CMRA A] (x y : A) := ∀ n mz,
+  ✓{n} (x •? mz) → ✓{n} (y •? mz)
+infixr:50 " ~~> " => cmra_update
+
+section updates
+variable [CMRA α]
+
+-- (* Global Instance cmra_updateP_proper :
+--   Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP SI A).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_proper :
+--   Proper ((≡) ==> (≡) ==> iff) (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+theorem cmra_update_updateP {x y: α} : x ~~> y ↔ x ~~>: (y =.) := sorry
+
+theorem cmra_updateP_id (P : α → Prop) x : P x → x ~~>: P := sorry
+
+theorem cmra_updateP_compose (P Q : α → Prop) x :
+  x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q := sorry
+
+theorem cmra_updateP_compose_l (Q : α → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q := sorry
+
+theorem cmra_updateP_weaken (P Q : α → Prop) x :
+  x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q := sorry
+
+theorem cmra_update_exclusive {x y: α} [CMRA.Exclusive x] y:
+  ✓ y → x ~~> y := sorry
+
+-- (** Updates form a preorder. *)
+-- (** We set this rewrite relation's cost above the stdlib's
+--   ([impl], [iff], [eq], ...) and [≡] but below [⊑].
+--   [eq] (at 100) < [≡] (at 150) < [cmra_update] (at 170) < [⊑] (at 200) *)
+
+-- (* Global Instance cmra_update_rewrite_relation :
+--   RewriteRelation (@cmra_update SI A) | 170 := {}. *)
+
+-- (* Global Instance cmra_update_preorder : PreOrder (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_proper_update :
+--   Proper (flip cmra_update ==> cmra_update ==> impl) (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_flip_proper_update :
+--   Proper (cmra_update ==> flip cmra_update ==> flip impl) (@cmra_update SI A).
+-- Proof. Admitted. *)
+
+theorem cmra_updateP_op (P1 P2 Q : α → Prop) x1 x2 :
+  x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 • y2)) →
+  x1 • x2 ~~>: Q := sorry
+
+theorem cmra_updateP_op' (P1 P2 : α → Prop) {x1 x2: α} :
+  x1 ~~>: P1 → x2 ~~>: P2 →
+  x1 • x2 ~~>: λ y ↦ ∃ y1 y2, y = y1 • y2 ∧ P1 y1 ∧ P2 y2 := sorry
+
+theorem cmra_update_op {x1 x2 y1 y2 : α} : x1 ~~> y1 → x2 ~~> y2 → x1 • x2 ~~> y1 • y2 := sorry
+
+-- (* Global Instance cmra_update_op_proper :
+--   Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_op_flip_proper :
+--   Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+
+-- (* Global Instance cmra_update_op_proper :
+--   Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+-- (* Global Instance cmra_update_op_flip_proper :
+--   Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
+-- Proof. Admitted. *)
+
+
+theorem cmra_update_op_l [CMRA α] (x y : α) : x • y ~~> x := by admit
+
+theorem cmra_update_op_r [CMRA α] (x y : α) : x • y ~~> y := by admit
+
+theorem cmra_update_included [CMRA α] (x y : α) : x ≼ y → y ~~> x := by admit
+
+theorem cmra_update_valid0 [CMRA α] (x y : α) : (∀ (h₀ : ✓{0} x), x ~~> y) → x ~~> y := by admit
+
+-- (** ** Frame preserving updates for total and discete CMRAs *)
+
+theorem cmra_total_updateP [CMRA α] [CMRA.IsTotal α] (x : α) (P : α → Prop) :
+  x ~~>: P ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ∃ y, P y ∧ ✓{n} (y • z) := by admit
+
+theorem cmra_total_update [CMRA α] [CMRA.IsTotal α] (x y : α) :
+  x ~~> y ↔ ∀ (n : Nat) (z : α), ✓{n} (x • z) → ✓{n} (y • z) := by admit
+
+
+theorem cmra_discrete_updateP [CMRA α] [CMRA.Discrete α] (x : α) (P : α → Prop) :
+  x ~~>: P ↔ ∀ (mz : Option α), ✓ (x •? mz) → ∃ y, P y ∧ ✓ (y •? mz) := by admit
+
+theorem cmra_discrete_update [CMRA α] [CMRA.Discrete α] (x y : α) :
+  x ~~> y ↔ ∀ (mz : Option α), ✓ (x •? mz) → ✓ (y •? mz) := by admit
+
+theorem cmra_discrete_total_updateP [CMRA α] [CMRA.Discrete α] [CMRA.IsTotal α]
+  (x : α) (P : α → Prop) :
+  x ~~>: P ↔ ∀ (z : α), ✓ (x • z) → ∃ y, P y ∧ ✓ (y • z) := by admit
+
+theorem cmra_discrete_total_update [CMRA α] [CMRA.Discrete α] [CMRA.IsTotal α]
+  (x y : α) :
+  x ~~> y ↔ ∀ (z : α), ✓ (x • z) → ✓ (y • z) := by admit
+
+end updates
+
+-- (** * Transport *)
+-- Section cmra_transport.
+--   Context {SI : sidx} {A B : cmra} (H : A = B).
+--   Notation T := (cmra_transport H).
+--   Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
+--     x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
+--   Proof. Admitted.
+
+--   Lemma cmra_transport_updateP' (P : A → Prop) x :
+--     x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
+--   Proof. Admitted.
+
+-- End cmra_transport.
+
+-- (** * Isomorphism *)
+section iso_cmra
+  variable [CMRA α] [CMRA β] (f : α → β) (g : β → α)
+
+  theorem iso_cmra_updateP (P : β → Prop) (Q : α → Prop) (y : β)
+    (gf : ∀ x, g (f x) ≡ x)
+    (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2)
+    (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
+    y ~~>: P →
+    (∀ y', P y' → Q (g y')) →
+    g y ~~>: Q :=
+  sorry
+
+  theorem iso_cmra_updateP' (P : β → Prop) (y : β)
+    (gf : ∀ x, g (f x) ≡ x)
+    (g_op : ∀ y1 y2, g (y1 • y2) ≡ g y1 • g y2)
+    (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
+    y ~~>: P →
+    g y ~~>: λ x ↦ ∃ y, x = g y ∧ P y :=
+  sorry
+end iso_cmra
+
+section update_lift_cmra
+  variable  [CMRA α] [CMRA β]
+
+  theorem cmra_update_lift_updateP (f : β → α) (b : β) (b' : β)
+    (H : ∀ P, b ~~>: P → f b ~~>: λ a' ↦ ∃ b', a' = f b' ∧ P b') :
+    b ~~> b' →
+    f b ~~> f b' :=
+  sorry
+end update_lift_cmra
+
+section prod
+  variable [CMRA α] [CMRA β]
+
+  theorem prod_updateP (P1 : α → Prop) (P2 : β → Prop) (Q : α × β → Prop) (x : α × β) :
+    x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a, b)) → x ~~>: Q :=
+    sorry
+
+  theorem prod_updateP' (P1 : α → Prop) (P2 : β → Prop) (x : α × β) :
+     x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y ↦ P1 (y.1) ∧ P2 (y.2) :=
+    sorry
+
+  theorem prod_update (x : α × β) :
+    x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y :=
+    sorry
+end prod
+
+section option
+  variable [CMRA α]
+
+  theorem option_updateP (P : α → Prop) (x : α) :
+    x ~~>: P → (∀ y, P y → Q (some y)) → some x ~~>: Q :=
+    sorry
+
+  theorem option_updateP' (P : α → Prop) (x : α) :
+    x ~~>: P → some x ~~>: Option.rec False P :=
+    sorry
+
+  theorem option_update (x y : α) :
+    x ~~> y → some x ~~> some y :=
+    sorry
+end option