Commit 6f0a48a3 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify compl on excl, one_shot and option.

parent 91a2d149
Pipeline #372 passed with stage
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment