From 5226baf68e13e3774d06c4ccd6466dda678c041d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Feb 2016 17:19:59 +0100
Subject: [PATCH] FAIL : Less canonical projections.

---
 algebra/cmra.v     |  4 +++-
 algebra/cofe.v     | 21 +++++++++++----------
 algebra/fin_maps.v | 44 +++++++++++++++++++++++++++++++++++++++++++-
 algebra/upred.v    |  2 ++
 4 files changed, 59 insertions(+), 12 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 5d61df86a..ce5bc5833 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -464,6 +464,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
   ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
 }.
 
+(*
 Section discrete.
   Context {A : cofeT} `{∀ x : A, Timeless x}.
   Context {v : Valid A} `{Unit A, Op A, Minus A} (ra : RA A).
@@ -480,7 +481,7 @@ Section discrete.
     apply (timeless _), dist_le with n; auto with lia.
   Qed.
   Definition discreteRA : cmraT :=
-    CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
+    CMRAT (let 'CofeT _ _ _ _ m := A in m) discrete_cmra_mixin discrete_extend_mixin.
   Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
     (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
   Proof. intros Hvalid n z; apply Hvalid. Qed.
@@ -505,6 +506,7 @@ Section unit.
   Global Instance unit_cmra_identity : CMRAIdentity unitRA.
   Proof. by split; intros []. Qed.
 End unit.
+*)
 
 (** ** Product *)
 Section prod.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 048ce9153..6866d4e66 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -62,32 +62,33 @@ Class Contractive `{Dist A, Dist B} (f : A -> B) :=
 (** Bundeled version *)
 Structure cofeT := CofeT {
   cofe_car :> Type;
-  cofe_equiv : Equiv cofe_car;
-  cofe_dist : Dist cofe_car;
-  cofe_compl : Compl cofe_car;
-  cofe_mixin : CofeMixin cofe_car
+  _ : Equiv cofe_car;
+  _ : Dist cofe_car;
+  _ : Compl cofe_car;
+  _ : CofeMixin cofe_car
 }.
 Arguments CofeT {_ _ _ _} _.
 Add Printing Constructor cofeT.
-Existing Instances cofe_equiv cofe_dist cofe_compl.
+Instance cofe_equiv (A : cofeT) : Equiv A := let 'CofeT _ e _ _ _ := A in e.
+Instance cofe_dist (A : cofeT) : Dist A := let 'CofeT _ _ d _ _ := A in d.
+Instance cofe_compl (A : cofeT) : Compl A := let 'CofeT _ _ _ c _ := A in c.
 Arguments cofe_car : simpl never.
 Arguments cofe_equiv : simpl never.
 Arguments cofe_dist : simpl never.
 Arguments cofe_compl : simpl never.
-Arguments cofe_mixin : simpl never.
 
 (** Lifting properties from the mixin *)
 Section cofe_mixin.
   Context {A : cofeT}.
   Implicit Types x y : A.
   Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y.
-  Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed.
+  Proof. by destruct A as [???? []]. Qed.
   Global Instance dist_equivalence n : Equivalence (@dist A _ n).
-  Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
+  Proof. by destruct A as [???? []]. Qed.
   Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
-  Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
+  Proof. destruct A as [???? []]; auto. Qed.
   Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c (S n).
-  Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
+  Proof. destruct A as [???? []]; auto. Qed.
 End cofe_mixin.
 
 (** General properties *)
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 92714de8d..8c8d46416 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -18,7 +18,49 @@ Proof.
   split.
   - intros m1 m2; split.
     + by intros Hm n k; apply equiv_dist.
-    + intros Hm k; apply equiv_dist; intros n; apply Hm.
+    + intros Hm k.
+
+(**
+Goal is
+
+  @equiv (option (cofe_car A)) (@option_equiv (cofe_car A) (cofe_equiv A))
+    (@lookup K (cofe_car A) (@gmap K H H0 (cofe_car A)) (@gmap_lookup K H H0 (cofe_car A)) k m1)
+    (@lookup K (cofe_car A) (@gmap K H H0 (cofe_car A)) (@gmap_lookup K H H0 (cofe_car A)) k m2)
+*)
+
+(** LHS of equiv_dist is:
+
+  @equiv (cofe_car B) (cofe_equiv B) x y
+
+for some [B : cofeT].
+*)
+
+Fail apply equiv_dist.
+
+(* Works: apply @equiv_dist.  *)
+
+
+(* Note that equiv_dist is an iff, so [apply:] needs some help. But it works.
+
+apply: (fun {A} x y => proj2 (@equiv_dist A x y)).
+*)
+
+(* I do not think it is just about the type of the projection of the [equiv]
+operational typeclass being in the way. The following also fails. *)
+
+change (option (cofe_car A)) with (cofe_car (optionC A)).
+
+Fail apply equiv_dist.
+
+change (@option_equiv (cofe_car A) (cofe_equiv A)) with
+  (@cofe_equiv (optionC A)).
+
+(* Only now it works *)
+apply equiv_dist.
+
+
+
+intros n; apply Hm.
   - intros n; split.
     + by intros m k.
     + by intros m1 m2 ? k.
diff --git a/algebra/upred.v b/algebra/upred.v
index 0e1f6ea1d..88d042617 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -876,12 +876,14 @@ Lemma later_equivI {A : cofeT} (x y : later A) :
   (x ≡ y)%I ≡ (▷ (later_car x ≡ later_car y) : uPred M)%I.
 Proof. done. Qed.
 
+(*
 (* Discrete *)
 (* For equality, there already is timeless_eq *)
 Lemma discrete_validI {A : cofeT} `{∀ x : A, Timeless x}
   `{Op A, Valid A, Unit A, Minus A} (ra : RA A) (x : discreteRA ra) :
   (✓ x)%I ≡ (■ ✓ x : uPred M)%I.
 Proof. done. Qed.
+*)
 
 (* Timeless *)
 Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
-- 
GitLab