Commit 6df6c641 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove `contractive_ne` and `contractive_proper` as instances.

Instead, make them `Hint Immediate` so they are only used at leaves.
parent 329b8c2c
......@@ -197,6 +197,9 @@ Section ofe.
Proof. by rewrite -!discrete_iff. Qed.
End ofe.
Hint Immediate ne_proper : typeclass_instances.
Hint Immediate ne_proper_2 : typeclass_instances.
(** Contractive functions *)
Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
match n with 0 => True | S n => x {n} y end.
......@@ -234,12 +237,15 @@ Section contractive.
Lemma contractive_S n x y : x {n} y f x {S n} f y.
Proof. intros. by apply (_ : Contractive f). Qed.
Global Instance contractive_ne : NonExpansive f | 100.
Lemma contractive_ne : NonExpansive f.
Proof. by intros n x y ?; apply dist_S, contractive_S. Qed.
Global Instance contractive_proper : Proper (() ==> ()) f | 100.
Proof. apply (ne_proper _). Qed.
Lemma contractive_proper : Proper (() ==> ()) f.
Proof. apply ne_proper, contractive_ne. Qed.
End contractive.
Hint Immediate contractive_ne : typeclass_instances.
Hint Immediate contractive_proper : typeclass_instances.
Ltac f_contractive :=
match goal with
| |- ?f _ {_} ?f _ => simple apply (_ : Proper (dist_later _ ==> _) f)
......@@ -798,12 +804,11 @@ Next Obligation.
apply ofe_morO_map_ne; apply oFunctor_map_ne; split; by apply Hfg.
Qed.
Next Obligation.
intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_map_id.
apply (ne_proper f). apply oFunctor_map_id.
intros F1 F2 A ? B ? [f ?] ?; simpl. by rewrite /= !oFunctor_map_id.
Qed.
Next Obligation.
intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
rewrite -!oFunctor_map_compose. do 2 apply (ne_proper _). apply oFunctor_map_compose.
by rewrite -!oFunctor_map_compose.
Qed.
Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
......
Supports Markdown
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