From 6f0a48a3a04b9c31a7d34bcd43d403ed80d0f879 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 19 Mar 2016 22:39:22 +0100
Subject: [PATCH] Simplify compl on excl, one_shot and option.

---
 algebra/cofe.v     |  1 -
 algebra/excl.v     | 25 ++++++-------------------
 algebra/one_shot.v | 27 ++++++---------------------
 algebra/option.v   | 24 ++++++------------------
 4 files changed, 18 insertions(+), 59 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index dfd10fcbd..99586fb52 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 89b4f4087..bca3134c9 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 6be12c477..18db970bb 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 d9241aba5..1a34c4827 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.
-- 
GitLab