Commit 5226baf6 authored by Robbert Krebbers's avatar Robbert Krebbers

FAIL : Less canonical projections.

parent c305d664
......@@ -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.
......
......@@ -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 *)
......
......@@ -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.
......
......@@ -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.
......
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