diff --git a/algebra/cofe.v b/algebra/cofe.v index dfd10fcbdabe7d1f75e71864072911f05bdc0143..99586fb523374eb57c1b5e207ac836263c4ba42c 100644 --- a/algebra/cofe.v +++ b/algebra/cofe.v @@ -248,7 +248,6 @@ Section cofe_mor. Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _. Lemma cofe_mor_ext (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x. Proof. done. Qed. - End cofe_mor. Arguments cofe_mor : clear implicits. diff --git a/algebra/excl.v b/algebra/excl.v index 89b4f40878f3659702c1fe6a420dde1e4d01514e..bca3134c9eb555876245fe10760c990aa2212e89 100644 --- a/algebra/excl.v +++ b/algebra/excl.v @@ -39,18 +39,11 @@ Proof. by inversion_clear 1. Qed. Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A). Proof. by inversion_clear 1. Qed. -Program Definition excl_chain - (c : chain (excl A)) (a : A) (H : maybe Excl (c 0) = Some a) : chain A := +Program Definition excl_chain (c : chain (excl A)) (a : A) : chain A := {| chain_car n := match c n return _ with Excl y => y | _ => 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. +Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Instance excl_compl : Compl (excl A) := λ c, - match Some_dec (maybe Excl (c 0)) with - | inleft (exist a H) => Excl (compl (excl_chain c a H)) | inright _ => c 0 - end. + match c 0 with Excl a => Excl (compl (excl_chain c a)) | x => x end. Definition excl_cofe_mixin : CofeMixin (excl A). Proof. split. @@ -62,15 +55,9 @@ Proof. + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; apply dist_S. - - intros n c; unfold compl, excl_compl. - destruct (Some_dec (maybe Excl (c 0))) as [[a Ha]|]. - { assert (c 0 = Excl a) by (by destruct (c 0); simplify_eq/=). - assert (∃ b, c n = Excl b) as [b Hb]. - { feed inversion (chain_cauchy c 0 n); eauto with lia congruence. } - rewrite Hb; constructor. - by rewrite (conv_compl n (excl_chain c a Ha)) /= Hb. } - feed inversion (chain_cauchy c 0 n); first lia; - constructor; destruct (c 0); simplify_eq/=. + - intros n c; rewrite /compl /excl_compl. + feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. + rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver. Qed. Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin. Global Instance excl_discrete : Discrete A → Discrete exclC. diff --git a/algebra/one_shot.v b/algebra/one_shot.v index 6be12c47706a1e0474ac287ff87d6442793408e7..18db970bb868e745a38ff20ba404629ff2959f54 100644 --- a/algebra/one_shot.v +++ b/algebra/one_shot.v @@ -44,19 +44,11 @@ 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 := +Program Definition one_shot_chain (c : chain (one_shot A)) (a : 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. +Next Obligation. intros c a n i ?; simpl. by destruct (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. + match c 0 with Shot a => Shot (compl (one_shot_chain c a)) | x => x end. Definition one_shot_cofe_mixin : CofeMixin (one_shot A). Proof. split. @@ -69,16 +61,9 @@ Proof. + 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/=. + - intros n c; rewrite /compl /one_shot_compl. + feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. + rewrite (conv_compl n (one_shot_chain c _)) /=. destruct (c n); naive_solver. Qed. Canonical Structure one_shotC : cofeT := CofeT one_shot_cofe_mixin. Global Instance one_shot_discrete : Discrete A → Discrete one_shotC. diff --git a/algebra/option.v b/algebra/option.v index d9241aba530c5c13ec7608e6a49761d49e949c26..1a34c48279e2ec41d5f11c0ff2c43d5a6c7a85e8 100644 --- a/algebra/option.v +++ b/algebra/option.v @@ -8,18 +8,11 @@ Inductive option_dist : Dist (option A) := | Some_dist n x y : x ≡{n}≡ y → Some x ≡{n}≡ Some y | None_dist n : None ≡{n}≡ None. Existing Instance option_dist. -Program Definition option_chain - (c : chain (option A)) (x : A) (H : c 0 = Some x) : chain A := +Program Definition option_chain (c : chain (option A)) (x : A) : chain A := {| chain_car n := from_option x (c n) |}. -Next Obligation. - intros c x ? n i ?; simpl. - destruct (c 0) eqn:?; simplify_eq/=. - by feed inversion (chain_cauchy c n i). -Qed. +Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed. Instance option_compl : Compl (option A) := λ c, - match Some_dec (c 0) with - | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None - end. + match c 0 with Some x => Some (compl (option_chain c x)) | None => None end. Definition option_cofe_mixin : CofeMixin (option A). Proof. split. @@ -31,14 +24,9 @@ Proof. + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etrans; eauto. - by inversion_clear 1; constructor; apply dist_S. - - intros n c; unfold compl, option_compl. - destruct (Some_dec (c 0)) as [[x Hx]|]. - { assert (is_Some (c n)) as [y Hy]. - { feed inversion (chain_cauchy c 0 n); eauto with lia congruence. } - rewrite Hy; constructor. - by rewrite (conv_compl n (option_chain c x Hx)) /= Hy. } - feed inversion (chain_cauchy c 0 n); eauto with lia congruence. - constructor. + - intros n c; rewrite /compl /option_compl. + feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. + rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver. Qed. Canonical Structure optionC := CofeT option_cofe_mixin. Global Instance option_discrete : Discrete A → Discrete optionC.