diff --git a/_CoqProject b/_CoqProject index aedb367b88fc3f7f6d1ecf4c6d28f0dabd7db2ea..861ba66eb382881b916d554b23c6901e150f819c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -54,6 +54,7 @@ algebra/upred.v algebra/upred_tactics.v algebra/upred_big_op.v algebra/frac.v +algebra/one_shot.v program_logic/model.v program_logic/adequacy.v program_logic/hoare_lifting.v diff --git a/algebra/frac.v b/algebra/frac.v index f504b0c13c71b4e22b8340a984c53f31eddcb9ec..f1ec2c20e0cd8a15fe32e644291bf9cbfe2b7b79 100644 --- a/algebra/frac.v +++ b/algebra/frac.v @@ -4,11 +4,10 @@ From iris.algebra Require Import upred. Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. -Inductive frac (A : Type) := - | Frac : Qp → A → frac A - | FracUnit : frac A. -Arguments Frac {_} _ _. -Arguments FracUnit {_}. +Inductive frac {A : Type} := + | Frac : Qp → A → frac + | FracUnit : frac. +Arguments frac _ : clear implicits. Instance maybe_Frac {A} : Maybe2 (@Frac A) := λ x, match x with Frac q a => Some (q,a) | _ => None end. Instance: Params (@Frac) 2. diff --git a/algebra/one_shot.v b/algebra/one_shot.v new file mode 100644 index 0000000000000000000000000000000000000000..65a96aa4dfb545ae030d80201e1af39b46ccaa00 --- /dev/null +++ b/algebra/one_shot.v @@ -0,0 +1,93 @@ +From iris.algebra Require Export cmra. +From iris.algebra Require Import upred. +Local Arguments validN _ _ _ !_ /. +Local Arguments valid _ _ !_ /. + +Inductive one_shot {A : Type} := + | OneShotPending : one_shot + | Shot : A → one_shot + | OneShotUnit : one_shot + | OneShotBot : one_shot. +Arguments one_shot _ : clear implicits. +Instance maybe_Shot {A} : Maybe (@Shot A) := λ x, + match x with Shot a => Some a | _ => None end. +Instance: Params (@Shot) 1. + +Section cofe. +Context {A : cofeT}. +Implicit Types a b : A. +Implicit Types x y : one_shot A. + +(* Cofe *) +Inductive one_shot_equiv : Equiv (one_shot A) := + | OneShotPending_equiv : OneShotPending ≡ OneShotPending + | OneShot_equiv a b : a ≡ b → Shot a ≡ Shot b + | OneShotUnit_equiv : OneShotUnit ≡ OneShotUnit + | OneShotBot_equiv : OneShotBot ≡ OneShotBot. +Existing Instance one_shot_equiv. +Inductive one_shot_dist : Dist (one_shot A) := + | OneShotPending_dist n : OneShotPending ≡{n}≡ OneShotPending + | OneShot_dist n a b : a ≡{n}≡ b → Shot a ≡{n}≡ Shot b + | OneShotUnit_dist n : OneShotUnit ≡{n}≡ OneShotUnit + | OneShotBot_dist n : OneShotBot ≡{n}≡ OneShotBot. +Existing Instance one_shot_dist. + +Global Instance One_Shot_ne n : Proper (dist n ==> dist n) (@Shot A). +Proof. by constructor. Qed. +Global Instance One_Shot_proper : Proper ((≡) ==> (≡)) (@Shot A). +Proof. by constructor. Qed. +Global Instance One_Shot_inj : Inj (≡) (≡) (@Shot A). +Proof. by inversion_clear 1. Qed. +Global Instance One_Shot_dist_inj n : Inj (dist n) (dist n) (@Shot A). +Proof. by inversion_clear 1. Qed. + +Program Definition one_shot_chain (c : chain (one_shot A)) (a : A) + (H : maybe Shot (c 0) = Some a) : chain A := + {| chain_car n := match c n return _ with Shot b => b | _ => a end |}. +Next Obligation. + intros c a ? n i ?; simpl. + destruct (c 0) eqn:?; simplify_eq/=. + by feed inversion (chain_cauchy c n i). +Qed. +Instance one_shot_compl : Compl (one_shot A) := λ c, + match Some_dec (maybe Shot (c 0)) with + | inleft (exist a H) => Shot (compl (one_shot_chain c a H)) + | inright _ => c 0 + end. +Definition one_shot_cofe_mixin : CofeMixin (one_shot A). +Proof. + split. + - intros mx my; split. + + by destruct 1; subst; constructor; try apply equiv_dist. + + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done. + apply equiv_dist=> n; by feed inversion (Hxy n). + - intros n; split. + + by intros [|a| |]; constructor. + + by destruct 1; constructor. + + destruct 1; inversion_clear 1; constructor; etrans; eauto. + - by inversion_clear 1; constructor; done || apply dist_S. + - intros n c; unfold compl, one_shot_compl. + destruct (Some_dec (maybe Shot (c 0))) as [[a Hx]|]. + { assert (c 0 = Shot a) by (by destruct (c 0); simplify_eq/=). + assert (∃ b, c n = Shot b) as [y Hy]. + { feed inversion (chain_cauchy c 0 n); + eauto with lia congruence f_equal. } + rewrite Hy; constructor; auto. + by rewrite (conv_compl n (one_shot_chain c a Hx)) /= Hy. } + feed inversion (chain_cauchy c 0 n); first lia; + constructor; destruct (c 0); simplify_eq/=. +Qed. +Canonical Structure one_shotC : cofeT := CofeT one_shot_cofe_mixin. +Global Instance one_shot_discrete : Discrete A → Discrete one_shotC. +Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. +Global Instance one_shot_leibniz : LeibnizEquiv A → LeibnizEquiv (one_shot A). +Proof. by destruct 2; f_equal; done || apply leibniz_equiv. Qed. + +Global Instance Shot_timeless (a : A) : Timeless a → Timeless (Shot a). +Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. +Global Instance OneShotUnit_timeless : Timeless (@OneShotUnit A). +Proof. by inversion_clear 1; constructor. Qed. +End cofe. + +Arguments one_shotC : clear implicits. +