Commit a9e2d8f3 authored by Robbert Krebbers's avatar Robbert Krebbers

Another failed approach to avoid declaring other projections than the carrier as canonical.

parent bf069d12
This diff is collapsed.
......@@ -52,7 +52,7 @@ Record tower := {
}.
Instance tower_equiv : Equiv tower := λ X Y, k, X k Y k.
Instance tower_dist : Dist tower := λ n X Y, k, X k {n} Y k.
Definition tower_ofe_mixin : OfeMixin tower.
Lemma tower_ofe_laws : ofe_laws tower.
Proof.
split.
- intros X Y; split; [by intros HXY n k; apply equiv_dist|].
......@@ -64,6 +64,7 @@ Proof.
- intros k X Y HXY n; apply dist_S.
by rewrite -(g_tower X) (HXY (S n)) g_tower.
Qed.
Definition tower_ofe_mixin := OfeMixin tower_ofe_laws.
Definition T : ofeT := OfeT tower tower_ofe_mixin.
Program Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
......
From iris.algebra Require Export cmra.
From iris.prelude Require Export gmap.
(*
From iris.algebra Require Import updates local_updates.
From iris.base_logic Require Import base_logic.
*)
Set Default Proof Using "Type".
Section cofe.
......@@ -10,12 +12,33 @@ Implicit Types m : gmap K A.
Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
i, m1 !! i {n} m2 !! i.
Definition gmap_ofe_mixin : OfeMixin (gmap K A).
Definition gmap_ofe_mixin : ofe_laws (gmap K A).
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.
Check @equiv_dist.
apply equiv_dist.
(** FOOBAR -- This gives:
Error:
In environment
K : Type
EqDecision0 : EqDecision K
H : Countable K
A : ofeT
m1, m2 : gmap K A
Hm : ∀ n : nat, m1 ≡{n}≡ m2
k : K
Unable to unify
"(?M4301 ≡ ?M4302 → ∀ n : nat, ?M4301 ≡{n}≡ ?M4302)
∧ ((∀ n : nat, ?M4301 ≡{n}≡ ?M4302) → ?M4301 ≡ ?M4302)" with
"option_Forall2 equiv (m1 !! k) (m2 !! k)".
*)
(A:=optionC A).
apply H0.
apply equiv_dist. intros n; apply Hm.
- intros n; split.
+ by intros m k.
+ by intros m1 m2 ? k.
......
......@@ -33,40 +33,45 @@ Tactic Notation "cofe_subst" :=
| H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
end.
Record OfeMixin A `{Equiv A, Dist A} := {
mixin_equiv_dist x y : x y n, x {n} y;
mixin_dist_equivalence n : Equivalence (dist n);
mixin_dist_S n x y : x {S n} y x {n} y
Record ofe_laws A `{Equiv A, Dist A} := {
law_equiv_dist x y : x y n, x {n} y;
law_dist_equivalence n : Equivalence (dist n);
law_dist_S n x y : x {S n} y x {n} y
}.
Record ofe_mixin A := OfeMixin {
ofe_mixin_equiv : Equiv A;
ofe_mixin_dist : Dist A;
ofe_mixin_laws_of : ofe_laws A;
}.
Arguments OfeMixin {_ _ _} _.
(** Bundeled version *)
Structure ofeT := OfeT' {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car;
_ : Type
}.
Arguments OfeT' _ {_ _} _ _.
Structure ofeT := OfeT' { ofe_car :> Type; _ : ofe_mixin ofe_car; _ : Type }.
Notation OfeT A m := (OfeT' A m A).
Add Printing Constructor ofeT.
Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
Arguments ofe_car : simpl never.
Definition ofe_mixin_of (A : ofeT) : ofe_mixin A := let 'OfeT' _ m _ := A in m.
Arguments ofe_mixin_of : simpl never.
Definition ofe_equiv {A : ofeT} : Equiv A := ofe_mixin_equiv _ (ofe_mixin_of A).
Arguments ofe_equiv : simpl never.
Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
Definition ofe_dist {A : ofeT} : Dist A := ofe_mixin_dist _ (ofe_mixin_of A).
Arguments ofe_dist : simpl never.
Arguments ofe_mixin : simpl never.
Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
(** Lifting properties from the mixin *)
Section ofe_mixin.
Context {A : ofeT}.
Implicit Types x y : A.
Local Coercion ofe_mixin_of : ofeT >-> ofe_mixin.
Lemma equiv_dist x y : x y n, x {n} y.
Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
Proof. apply (law_equiv_dist _ (ofe_mixin_laws_of _ A)). Qed.
Global Instance dist_equivalence n : Equivalence (@dist A _ n).
Proof. apply (mixin_dist_equivalence _ (ofe_mixin A)). Qed.
Proof. apply (law_dist_equivalence _ (ofe_mixin_laws_of _ A)). Qed.
Lemma dist_S n x y : x {S n} y x {n} y.
Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
Proof. apply (law_dist_S _ (ofe_mixin_laws_of _ A)). Qed.
End ofe_mixin.
Hint Extern 1 (_ {_} _) => apply equiv_dist; assumption.
......@@ -100,8 +105,7 @@ Class Cofe (A : ofeT) := {
}.
Arguments compl : simpl never.
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A B) c
`(NonExpansive f) :
Lemma compl_chain_map `{Cofe A, Cofe B} (f : A B) c `(NonExpansive f) :
compl (chain_map f c) f (compl c).
Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
......@@ -395,7 +399,7 @@ Section ofe_fun.
Context {A : Type} {B : ofeT}.
Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, x, f x g x.
Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, x, f x {n} g x.
Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B).
Definition ofe_fun_ofe_laws : ofe_laws (ofe_fun A B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
......@@ -406,6 +410,7 @@ Section ofe_fun.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
Qed.
Definition ofe_fun_ofe_mixin := OfeMixin ofe_fun_ofe_laws.
Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
Program Definition ofe_fun_chain `(c : chain ofe_funC)
......@@ -441,7 +446,7 @@ Section ofe_mor.
Proof. apply ne_proper, ofe_mor_ne. Qed.
Instance ofe_mor_equiv : Equiv (ofe_mor A B) := λ f g, x, f x g x.
Instance ofe_mor_dist : Dist (ofe_mor A B) := λ n f g, x, f x {n} g x.
Definition ofe_mor_ofe_mixin : OfeMixin (ofe_mor A B).
Definition ofe_mor_ofe_laws : ofe_laws (ofe_mor A B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
......@@ -452,6 +457,7 @@ Section ofe_mor.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
Qed.
Definition ofe_mor_ofe_mixin := OfeMixin ofe_mor_ofe_laws.
Canonical Structure ofe_morC := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
Program Definition ofe_mor_chain (c : chain ofe_morC)
......@@ -518,8 +524,9 @@ Qed.
(** unit *)
Section unit.
Instance unit_dist : Dist unit := λ _ _ _, True.
Definition unit_ofe_mixin : OfeMixin unit.
Definition unit_ofe_laws : ofe_laws unit.
Proof. by repeat split; try exists 0. Qed.
Definition unit_ofe_mixin := OfeMixin unit_ofe_laws.
Canonical Structure unitC : ofeT := OfeT unit unit_ofe_mixin.
Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
......@@ -538,7 +545,7 @@ Section product.
NonExpansive2 (@pair A B) := _.
Global Instance fst_ne : NonExpansive (@fst A B) := _.
Global Instance snd_ne : NonExpansive (@snd A B) := _.
Definition prod_ofe_mixin : OfeMixin (A * B).
Definition prod_ofe_laws : ofe_laws (A * B).
Proof.
split.
- intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
......@@ -546,6 +553,7 @@ Section product.
- apply _.
- by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
Qed.
Definition prod_ofe_mixin := OfeMixin prod_ofe_laws.
Canonical Structure prodC : ofeT := OfeT (A * B) prod_ofe_mixin.
Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodC :=
......@@ -704,7 +712,7 @@ Section sum.
Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _.
Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _.
Definition sum_ofe_mixin : OfeMixin (A + B).
Definition sum_ofe_laws : ofe_laws (A + B).
Proof.
split.
- intros x y; split=> Hx.
......@@ -713,6 +721,7 @@ Section sum.
- apply _.
- destruct 1; constructor; by apply dist_S.
Qed.
Definition sum_ofe_mixin := OfeMixin sum_ofe_laws.
Canonical Structure sumC : ofeT := OfeT (A + B) sum_ofe_mixin.
Program Definition inl_chain (c : chain sumC) (a : A) : chain A :=
......@@ -787,20 +796,22 @@ Section discrete_cofe.
Context `{Equiv A, @Equivalence A ()}.
Instance discrete_dist : Dist A := λ n x y, x y.
Definition discrete_ofe_mixin : OfeMixin A.
Definition discrete_ofe_laws : ofe_laws A.
Proof using Type*.
split.
- intros x y; split; [done|intros Hn; apply (Hn 0)].
- done.
- done.
Qed.
Definition discrete_ofe_mixin := OfeMixin discrete_ofe_laws.
Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
{ compl c := c 0 }.
Next Obligation.
intros n c. rewrite /compl /=;
symmetry; apply (chain_cauchy c 0 n). omega.
intros n c. by rewrite /compl /= -(chain_cauchy c 0 n); last omega.
Qed.
Global Instance discrete_discrete : Discrete (OfeT A discrete_ofe_mixin).
Proof. by intros x y. Qed.
End discrete_cofe.
Notation discreteC A := (OfeT A discrete_ofe_mixin).
......@@ -826,7 +837,7 @@ Section option.
Lemma dist_option_Forall2 n mx my : mx {n} my option_Forall2 (dist n) mx my.
Proof. done. Qed.
Definition option_ofe_mixin : OfeMixin (option A).
Definition option_ofe_laws : ofe_laws (option A).
Proof.
split.
- intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
......@@ -835,6 +846,7 @@ Section option.
- apply _.
- destruct 1; constructor; by apply dist_S.
Qed.
Definition option_ofe_mixin := OfeMixin option_ofe_laws.
Canonical Structure optionC := OfeT (option A) option_ofe_mixin.
Program Definition option_chain (c : chain optionC) (x : A) : chain A :=
......@@ -927,7 +939,7 @@ Section later.
Instance later_equiv : Equiv (later A) := λ x y, later_car x later_car y.
Instance later_dist : Dist (later A) := λ n x y,
dist_later n (later_car x) (later_car y).
Definition later_ofe_mixin : OfeMixin (later A).
Definition later_ofe_laws : ofe_laws (later A).
Proof.
split.
- intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
......@@ -938,6 +950,7 @@ Section later.
+ by intros [x] [y] [z] ??; trans y.
- intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S.
Qed.
Definition later_ofe_mixin := OfeMixin later_ofe_laws.
Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin.
Program Definition later_chain (c : chain laterC) : chain A :=
......@@ -1046,7 +1059,7 @@ Section sigma.
Proof. done. Qed.
Global Instance proj1_sig_ne : NonExpansive (@proj1_sig _ P).
Proof. by intros n [a Ha] [b Hb] ?. Qed.
Definition sig_ofe_mixin : OfeMixin (sig P).
Definition sig_ofe_laws : ofe_laws (sig P).
Proof.
split.
- intros [a ?] [b ?]. rewrite /dist /sig_dist /equiv /sig_equiv /=.
......@@ -1055,6 +1068,7 @@ Section sigma.
split; [intros []| intros [] []| intros [] [] []]=> //= -> //.
- intros n [a ?] [b ?]. rewrite /dist /sig_dist /=. apply dist_S.
Qed.
Definition sig_ofe_mixin := OfeMixin sig_ofe_laws.
Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
(* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving
......
......@@ -28,7 +28,8 @@ Section cofe.
Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
{ uPred_in_dist : n' x, n' n {n'} x P n' x Q n' x }.
Instance uPred_dist : Dist (uPred M) := uPred_dist'.
Definition uPred_ofe_mixin : OfeMixin (uPred M).
Lemma uPred_ofe_laws : ofe_laws (uPred M).
Proof.
split.
- intros P Q; split.
......@@ -41,6 +42,7 @@ Section cofe.
by trans (Q i x);[apply HP|apply HQ].
- intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
Qed.
Definition uPred_ofe_mixin := OfeMixin uPred_ofe_laws.
Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.
Program Definition uPred_compl : Compl uPredC := λ c,
......@@ -73,9 +75,27 @@ Qed.
(** functor *)
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CMRAMonotone f} (P : uPred M1) :
`{!CMRAMonotone f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
Next Obligation. (* naive_solver eauto using uPred_mono, cmra_monotoneN. *)
intros; simpl in *.
eapply uPred_mono. eauto.
eapply cmra_monotoneN.
(** FOOBAR -- This yields:
Error:
In environment
M1, M2 : ucmraT
f : M2 -n> M1
CMRAMonotone0 : CMRAMonotone f
P : uPred M1
n : nat
x1, x2 : M2
H : P n (f x1)
H0 : x1 ≼{n} x2
Unable to unify "∃ z : ?B, ?M3650 ?M3654 ≡{?M3652}≡ ?M3650 ?M3653 ⋅ z" with
"∃ z : M1, f x2 ≡{n}≡ f x1 ⋅ z".
*)
Qed.
Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
......
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