Commit d6456080 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove type class instances non-expansive -> proper.

parent 411de288
......@@ -91,6 +91,8 @@ Proof.
Qed.
Instance: Proper (dist n ==> dist n ==> dist n) op.
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy,!(commutative _ _ y2), Hx. Qed.
Instance: Proper (() ==> () ==> ()) op := ne_proper_2 _.
Global Instance agree_cmra : CMRA (agree A).
Proof.
split; try (apply _ || done).
......@@ -133,6 +135,7 @@ Section agree_map.
Next Obligation. by intros x n i ??; simpl; rewrite (agree_cauchy x n i). Qed.
Global Instance agree_map_ne n : Proper (dist n ==> dist n) agree_map.
Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
Global Instance agree_map_proper: Proper (()==>()) agree_map := ne_proper _.
Global Instance agree_map_preserving : CMRAPreserving agree_map.
Proof.
split; [|by intros n ?].
......
......@@ -68,7 +68,8 @@ Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (validN n).
Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
Global Instance cmra_ra : RA A.
Proof.
split; try by (destruct cmra; eauto with typeclass_instances).
split; try by (destruct cmra;
eauto using ne_proper, ne_proper_2 with typeclass_instances).
* by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite <-Hx.
* intros x y; rewrite !cmra_valid_validN; intros ? n.
by apply cmra_valid_op_l with y.
......@@ -87,14 +88,14 @@ Proof.
intros x1 x2 Hx y1 y2 Hy.
by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2).
Qed.
Lemma cmra_unit_valid x n : validN n x validN n (unit x).
Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
Lemma cmra_included_dist_l x1 x2 x1' n :
x1 x2 x1' ={n}= x1 x2', x1' x2' x2' ={n}= x2.
Proof.
rewrite ra_included_spec; intros [z Hx2] Hx1; exists (x1' z); split.
apply ra_included_l. by rewrite Hx1, Hx2.
Qed.
Lemma cmra_unit_valid x n : validN n x validN n (unit x).
Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
End cmra.
(* Also via [cmra_cofe; cofe_equivalence] *)
......
......@@ -3,7 +3,7 @@ Obligation Tactic := idtac.
(** Unbundeled version *)
Class Dist A := dist : nat relation A.
Instance: Params (@dist) 2.
Instance: Params (@dist) 3.
Notation "x ={ n }= y" := (dist n x y)
(at level 70, n at next level, format "x ={ n }= y").
Hint Extern 0 (?x ={_}= ?x) => reflexivity.
......@@ -65,13 +65,10 @@ Section cofe.
Proof. by apply dist_proper. Qed.
Lemma dist_le x y n n' : x ={n}= y n' n x ={n'}= y.
Proof. induction 2; eauto using dist_S. Qed.
Global Instance contractive_ne `{Cofe B} (f : A B) `{!Contractive f} n :
Proper (dist n ==> dist n) f | 100.
Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
Global Instance ne_proper `{Cofe B} (f : A B)
Instance ne_proper `{Cofe B} (f : A B)
`{! n, Proper (dist n ==> dist n) f} : Proper (() ==> ()) f | 100.
Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
Global Instance ne_proper_2 `{Cofe B, Cofe C} (f : A B C)
Instance ne_proper_2 `{Cofe B, Cofe C} (f : A B C)
`{! n, Proper (dist n ==> dist n ==> dist n) f} :
Proper (() ==> () ==> ()) f | 100.
Proof.
......@@ -82,6 +79,11 @@ Section cofe.
Proof. intros. by rewrite (conv_compl c1 n), (conv_compl c2 n). Qed.
Lemma compl_ext (c1 c2 : chain A) : ( i, c1 i c2 i) compl c1 compl c2.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
Global Instance contractive_ne `{Cofe B} (f : A B) `{!Contractive f} n :
Proper (dist n ==> dist n) f | 100.
Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
Global Instance contractive_proper `{Cofe B} (f : A B) `{!Contractive f} :
Proper (() ==> ()) f | 100 := _.
End cofe.
(** Fixpoint *)
......@@ -153,9 +155,11 @@ Proof.
* intros c n x; simpl.
rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
Qed.
Instance cofe_mor_car_proper :
Proper (() ==> () ==> ()) (@cofe_mor_car A B).
Proof. intros A B f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
Instance cofe_mor_car_ne A B n :
Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
Instance cofe_mor_car_proper A B :
Proper (() ==> () ==> ()) (@cofe_mor_car A B) := ne_proper_2 _.
Lemma cofe_mor_ext {A B} (f g : cofeMor A B) : f g x, f x g x.
Proof. done. Qed.
Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B).
......
......@@ -179,17 +179,23 @@ Global Instance iprop_and_ne n :
Proof.
intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
Qed.
Global Instance iprop_and_proper :
Proper (() ==> () ==> ()) (@iprop_and A) := ne_proper_2 _.
Global Instance iprop_or_ne n :
Proper (dist n ==> dist n ==> dist n) (@iprop_or A).
Proof.
intros P P' HP Q Q' HQ; split; intros [?|?];
first [by left; apply HP | by right; apply HQ].
Qed.
Global Instance iprop_or_proper :
Proper (() ==> () ==> ()) (@iprop_or A) := ne_proper_2 _.
Global Instance iprop_impl_ne n :
Proper (dist n ==> dist n ==> dist n) (@iprop_impl A).
Proof.
intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
Qed.
Global Instance iprop_impl_proper :
Proper (() ==> () ==> ()) (@iprop_impl A) := ne_proper_2 _.
Global Instance iprop_sep_ne n :
Proper (dist n ==> dist n ==> dist n) (@iprop_sep A).
Proof.
......@@ -197,12 +203,16 @@ Proof.
exists x1, x2; rewrite Hx in Hx'; split_ands; try apply HP; try apply HQ;
eauto using cmra_valid_op_l, cmra_valid_op_r.
Qed.
Global Instance iprop_sep_proper :
Proper (() ==> () ==> ()) (@iprop_sep A) := ne_proper_2 _.
Global Instance iprop_wand_ne n :
Proper (dist n ==> dist n ==> dist n) (@iprop_wand A).
Proof.
intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
apply HQ, HPQ, HP; eauto using cmra_valid_op_r.
Qed.
Global Instance iprop_wand_proper :
Proper (() ==> () ==> ()) (@iprop_wand A) := ne_proper_2 _.
Global Instance iprop_eq_ne {B : cofeT} n :
Proper (dist n ==> dist n ==> dist n) (@iprop_eq A B).
Proof.
......@@ -210,14 +220,24 @@ Proof.
* by rewrite <-(dist_le _ _ _ _ Hx), <-(dist_le _ _ _ _ Hy) by auto.
* by rewrite (dist_le _ _ _ _ Hx), (dist_le _ _ _ _ Hy) by auto.
Qed.
Global Instance iprop_eq_proper {B : cofeT} :
Proper (() ==> () ==> ()) (@iprop_eq A B) := ne_proper_2 _.
Global Instance iprop_forall_ne {B : cofeT} :
Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_forall B A).
Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Global Instance iprop_forall_proper {B : cofeT} :
Proper (pointwise_relation _ () ==> ()) (@iprop_forall B A).
Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Global Instance iprop_exists_ne {B : cofeT} :
Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_exist B A).
Proof.
by intros n P1 P2 HP12 x n'; split; intros [a HP]; exists a; apply HP12.
Qed.
Global Instance iprop_exist_proper {B : cofeT} :
Proper (pointwise_relation _ () ==> ()) (@iprop_exist B A).
Proof.
by intros P1 P2 HP12 x n'; split; intros [a HP]; exists a; apply HP12.
Qed.
(** Introduction and elimination rules *)
Lemma iprop_True_intro P : P True%I.
......
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