Commit 7fc5808c by Ralf Jung

### complete one_shot

parent a26a3367
 ... ... @@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!