From 7fc5808cafd9bbb636523c6b80394f4783d6b2b7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Mar 2016 13:13:30 +0100
Subject: [PATCH] complete one_shot
---
algebra/one_shot.v | 197 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 197 insertions(+)
diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 14cb69b26..2cefc59b7 100644
--- a/algebra/one_shot.v
+++ b/algebra/one_shot.v
@@ -2,6 +2,8 @@ From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
+Local Arguments cmra_validN _ _ !_ /.
+Local Arguments cmra_valid _ !_ /.
(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *)
Inductive one_shot {A : Type} :=
@@ -92,3 +94,198 @@ End cofe.
Arguments one_shotC : clear implicits.
+(* Functor on COFEs *)
+Definition one_shot_map {A B} (f : A → B) (x : one_shot A) : one_shot B :=
+ match x with
+ | OneShotPending => OneShotPending
+ | Shot a => Shot (f a)
+ | OneShotUnit => OneShotUnit
+ | OneShotBot => OneShotBot
+ end.
+Instance: Params (@one_shot_map) 2.
+
+Lemma one_shot_map_id {A} (x : one_shot A) : one_shot_map id x = x.
+Proof. by destruct x. Qed.
+Lemma one_shot_map_compose {A B C} (f : A → B) (g : B → C) (x : one_shot A) :
+ one_shot_map (g ∘ f) x = one_shot_map g (one_shot_map f x).
+Proof. by destruct x. Qed.
+Lemma one_shot_map_ext {A B : cofeT} (f g : A → B) x :
+ (∀ x, f x ≡ g x) → one_shot_map f x ≡ one_shot_map g x.
+Proof. by destruct x; constructor. Qed.
+Instance one_shot_map_cmra_ne {A B : cofeT} n :
+ Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@one_shot_map A B).
+Proof. intros f f' Hf; destruct 1; constructor; by try apply Hf. Qed.
+Definition one_shotC_map {A B} (f : A -n> B) : one_shotC A -n> one_shotC B :=
+ CofeMor (one_shot_map f).
+Instance one_shotC_map_ne A B n : Proper (dist n ==> dist n) (@one_shotC_map A B).
+Proof. intros f f' Hf []; constructor; by try apply Hf. Qed.
+
+Section cmra.
+Context {A : cmraT}.
+Implicit Types a b : A.
+Implicit Types x y : one_shot A.
+
+(* CMRA *)
+Instance one_shot_valid : Valid (one_shot A) := λ x,
+ match x with
+ | OneShotPending => True
+ | Shot a => ✓ a
+ | OneShotUnit => True
+ | OneShotBot => False
+ end.
+Instance one_shot_validN : ValidN (one_shot A) := λ n x,
+ match x with
+ | OneShotPending => True
+ | Shot a => ✓{n} a
+ | OneShotUnit => True
+ | OneShotBot => False
+ end.
+Global Instance one_shot_empty : Empty (one_shot A) := OneShotUnit.
+Instance one_shot_core : Core (one_shot A) := λ x,
+ match x with
+ | Shot a => Shot (core a)
+ | OneShotBot => OneShotBot
+ | _ => ∅
+ end.
+Instance one_shot_op : Op (one_shot A) := λ x y,
+ match x, y with
+ | Shot a, Shot b => Shot (a â‹… b)
+ | Shot a, OneShotUnit | OneShotUnit, Shot a => Shot a
+ | OneShotUnit, OneShotPending | OneShotPending, OneShotUnit => OneShotPending
+ | OneShotUnit, OneShotUnit => OneShotUnit
+ | _, _ => OneShotBot
+ end.
+
+Lemma Shot_op a b : Shot a â‹… Shot b = Shot (a â‹… b).
+Proof. done. Qed.
+Lemma Shot_incl a b : Shot a ≼ Shot b ↔ a ≼ b.
+Proof.
+ split; intros [c H].
+ - destruct c; inversion_clear H; first by eexists.
+ by rewrite (_ : b ≡ a).
+ - exists (Shot c). constructor. done.
+Qed.
+
+Definition one_shot_cmra_mixin : CMRAMixin (one_shot A).
+Proof.
+ split.
+ - intros n []; destruct 1; constructor; by cofe_subst.
+ - intros ? [|a| |] [|b| |] H; inversion_clear H; constructor; by f_equiv.
+ - intros ? [|a| |] [|b| |] H; inversion_clear H; cofe_subst; done.
+ - intros [|a| |]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
+ - intros n [|a| |]; simpl; auto using cmra_validN_S.
+ - intros [|a1| |] [|a2| |] [|a3| |]; constructor; by rewrite ?assoc.
+ - intros [|a1| |] [|a2| |]; constructor; by rewrite 1?comm.
+ - intros [|a| |]; constructor; []. exact: cmra_core_l.
+ - intros [|a| |]; constructor; []. exact: cmra_core_idemp.
+ - intros [|a1| |] [|a2| |]; simpl;
+ try solve [ by exists OneShotUnit; constructor
+ | by exists OneShotBot; constructor
+ | by intros [[|a3| |] H]; inversion_clear H ].
+ + intros H%Shot_incl. apply Shot_incl, cmra_core_preserving. done.
+ + intros _. exists (Shot (core a2)). by constructor.
+ - intros n [|a1| |] [|a2| |]; simpl; eauto using cmra_validN_op_l; done.
+ - intros n [|a| |] y1 y2 Hx Hx'; last 2 first.
+ + by exists (∅, ∅); destruct y1, y2; inversion_clear Hx'.
+ + by exists (OneShotBot, OneShotBot); destruct y1, y2; inversion_clear Hx'.
+ + destruct y1, y2; try (exfalso; by inversion_clear Hx').
+ * by exists (OneShotPending, OneShotUnit).
+ * by exists (OneShotUnit, OneShotPending).
+ + destruct y1 as [|b1 | |], y2 as [|b2| |]; try (exfalso; by inversion_clear Hx').
+ * apply (inj Shot) in Hx'.
+ destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto.
+ exists (Shot z1, Shot z2). by repeat constructor.
+ * exists (Shot a, ∅). inversion_clear Hx'. by repeat constructor.
+ * exists (∅, Shot a). inversion_clear Hx'. by repeat constructor.
+Qed.
+Canonical Structure one_shotR : cmraT := CMRAT one_shot_cofe_mixin one_shot_cmra_mixin.
+Global Instance one_shot_cmra_unit : CMRAUnit one_shotR.
+Proof. split. done. by intros []. apply _. Qed.
+Global Instance one_shot_cmra_discrete : CMRADiscrete A → CMRADiscrete one_shotR.
+Proof.
+ split; first apply _.
+ intros [|a| |]; simpl; auto using cmra_discrete_valid.
+Qed.
+
+Lemma one_shot_validN_inv_l n y : ✓{n} (OneShotPending ⋅ y) → y = ∅.
+Proof.
+ destruct y as [|b| |]; [done| |done|done]. destruct 1.
+Qed.
+Lemma one_shot_valid_inv_l y : ✓ (OneShotPending ⋅ y) → y = ∅.
+Proof. intros. by apply one_shot_validN_inv_l with 0, cmra_valid_validN. Qed.
+Lemma one_shot_bot_largest y : y ≼ OneShotBot.
+Proof.
+ destruct y; exists OneShotBot; constructor.
+Qed.
+
+(** Internalized properties *)
+Lemma one_shot_equivI {M} (x y : one_shot A) :
+ (x ≡ y) ⊣⊢ (match x, y with
+ | OneShotPending, OneShotPending => True
+ | Shot a, Shot b => a ≡ b
+ | OneShotUnit, OneShotUnit => True
+ | OneShotBot, OneShotBot => True
+ | _, _ => False
+ end : uPred M).
+Proof.
+ uPred.unseal; do 2 split; first by destruct 1.
+ by destruct x, y; try destruct 1; try constructor.
+Qed.
+Lemma one_shot_validI {M} (x : one_shot A) :
+ (✓ x) ⊣⊢ (match x with
+ | Shot a => ✓ a
+ | OneShotBot => False
+ | _ => True
+ end : uPred M).
+Proof. uPred.unseal. by destruct x. Qed.
+
+(** Updates *)
+Lemma one_shot_update_shoot (a : A) : ✓ a → OneShotPending ~~> Shot a.
+Proof.
+ move=> ? n y /one_shot_validN_inv_l ->. by apply cmra_valid_validN.
+Qed.
+Lemma one_shot_update (a1 a2 : A) : a1 ~~> a2 → Shot a1 ~~> Shot a2.
+Proof.
+ intros Ha n [|b| |] ?; simpl; auto.
+ apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
+Qed.
+
+End cmra.
+
+Arguments one_shotR : clear implicits.
+
+(* Functor *)
+Instance one_shot_map_cmra_monotone {A B : cmraT} (f : A → B) :
+ CMRAMonotone f → CMRAMonotone (one_shot_map f).
+Proof.
+ split; try apply _.
+ - intros n [|a| |]; simpl; auto using validN_preserving.
+ - intros [|a1| |] [|a2| |] [[|a3| |] Hx];
+ inversion Hx; setoid_subst; try apply cmra_unit_least;
+ try apply one_shot_bot_largest; auto; [].
+ destruct (included_preserving f a1 (a1 â‹… a3)) as [b ?].
+ { by apply cmra_included_l. }
+ by exists (Shot b); constructor.
+Qed.
+
+Program Definition one_shotRF (F : rFunctor) : rFunctor := {|
+ rFunctor_car A B := one_shotR (rFunctor_car F A B);
+ rFunctor_map A1 A2 B1 B2 fg := one_shotC_map (rFunctor_map F fg)
+|}.
+Next Obligation.
+ by intros F A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+ intros F A B x. rewrite /= -{2}(one_shot_map_id x).
+ apply one_shot_map_ext=>y; apply rFunctor_id.
+Qed.
+Next Obligation.
+ intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -one_shot_map_compose.
+ apply one_shot_map_ext=>y; apply rFunctor_compose.
+Qed.
+
+Instance one_shotRF_contractive F :
+ rFunctorContractive F → rFunctorContractive (one_shotRF F).
+Proof.
+ by intros ? A1 A2 B1 B2 n f g Hfg; apply one_shotC_map_ne, rFunctor_contractive.
+Qed.
--
GitLab