diff --git a/theories/base.v b/theories/base.v index d2147c54779fbb50d7db21d234d59b0bef5b112a..cbadbb04f6f714c20a0e946e92d66dac59830bc3 100644 --- a/theories/base.v +++ b/theories/base.v @@ -191,7 +191,11 @@ Proof. split; repeat intro; congruence. Qed. "canonical" equivalence for a type. The typeclass is tied to the \equiv symbol. This is based on (Spitters/van der Weegen, 2011). *) Class Equiv A := equiv: relation A. -Typeclasses Opaque equiv. + +(* No Typeclasses Opaque because we often rely on [≡] being unified with [=] in +case of types with Leibniz equality as [≡]. +Typeclasses Opaque equiv. *) + (* No Hint Mode set because of Coq bug #5735 Hint Mode Equiv ! : typeclass_instances. *) @@ -239,8 +243,6 @@ Ltac unfold_leibniz := repeat end. Definition equivL {A} : Equiv A := (=). -Instance equivL_equivalence {A} : Equivalence (@equiv A equivL). -Proof. unfold equiv; apply _. Qed. (** A [Params f n] instance forces the setoid rewriting mechanism not to rewrite in the first [n] arguments of the function [f]. We will declare such @@ -663,14 +665,12 @@ Section prod_relation. End prod_relation. Instance prod_equiv {Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡). -Instance pair_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡) ==> (≡)) (@pair A B). -Proof. apply pair_proper'. Qed. -Instance pair_equiv_inj {Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B). -Proof. apply pair_inj'. Qed. -Instance fst_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B). -Proof. apply fst_proper'. Qed. -Instance snd_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B). -Proof. apply snd_proper'. Qed. +Instance pair_proper {Equiv A, Equiv B} : + Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) := _. +Instance pair_equiv_inj {Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _. +Instance fst_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _. +Instance snd_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _. +Typeclasses Opaque prod_equiv. Instance prod_leibniz {LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B). Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed. @@ -724,14 +724,11 @@ Section sum_relation. End sum_relation. Instance sum_equiv {Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡). -Instance inl_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B). -Proof. apply inl_proper'. Qed. -Instance inr_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B). -Proof. apply inr_proper'. Qed. -Instance inl_equiv_inj {Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B). -Proof. apply inl_inj'. Qed. +Instance inl_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _. +Instance inr_proper {Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _. +Instance inl_equiv_inj {Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _. Instance inr_equiv_inj {Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _. -Proof. apply inr_inj'. Qed. +Typeclasses Opaque sum_equiv. (** ** Option *) Instance option_inhabited {A} : Inhabited (option A) := populate None. diff --git a/theories/option.v b/theories/option.v index 4c8e683051f69cdffccc3e931eb8270096cca873..7900d9db784d7e258c386680126bd6151d817ca0 100644 --- a/theories/option.v +++ b/theories/option.v @@ -122,7 +122,7 @@ Section setoids. Global Instance option_equivalence : Equivalence (≡@{A}) → Equivalence (≡@{option A}). - Proof. apply option_Forall2_equiv. Qed. + Proof. apply _. Qed. Global Instance Some_proper : Proper ((≡) ==> (≡@{option A})) Some. Proof. by constructor. Qed. Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some. diff --git a/theories/streams.v b/theories/streams.v index c0645c8d3d0ea88710dce5464a78c4de12fc1bef..2880a9a9c185c9ab2efcdfd672d19816938766cb 100644 --- a/theories/streams.v +++ b/theories/streams.v @@ -40,9 +40,9 @@ Lemma scons_equiv s1 s2 : shead s1 = shead s2 → stail s1 ≡ stail s2 → s1 Proof. by constructor. Qed. Global Instance equal_equivalence : Equivalence (≡@{stream A}). Proof. - unfold equiv, stream_equiv. split. - - cofix FIX; intros [??]; by constructor. - - cofix FIX; intros ?? [??]; by constructor. + split. + - now cofix FIX; intros [??]; constructor. + - now cofix FIX; intros ?? [??]; constructor. - cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto. Qed. Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).