diff options
| -rw-r--r-- | theories/Classes/Morphisms.v | 18 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 21 |
2 files changed, 24 insertions, 15 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index a0ce827a9..76da120e0 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -483,8 +483,7 @@ Proof. intros. apply reflexive_proper. Qed. Ltac proper_reflexive := match goal with | [ _ : normalization_done |- _ ] => fail 1 - | [ _ : apply_subrelation |- _ ] => class_apply proper_eq || class_apply @reflexive_proper - | _ => class_apply proper_eq + | _ => class_apply proper_eq || class_apply @reflexive_proper end. Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. @@ -545,7 +544,7 @@ Qed. [lt = le /\ ~eq]. If the order is total, we could also say [gt = ~le]. *) -Instance PartialOrder_StrictOrder `(PartialOrder A eqA R) : +Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) : StrictOrder (relation_conjunction R (complement eqA)). Proof. split; compute. @@ -558,11 +557,14 @@ apply partial_order_antisym; auto. rewrite Hxz; auto. Qed. +Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => + class_apply PartialOrder_StrictOrder : typeclass_instances. + (** From a [StrictOrder] to the corresponding [PartialOrder]: [le = lt \/ eq]. If the order is total, we could also say [ge = ~lt]. *) -Instance StrictOrder_PreOrder +Lemma StrictOrder_PreOrder `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) : PreOrder (relation_disjunction R eqA). Proof. @@ -575,7 +577,10 @@ left. rewrite Hxy; auto. right. transitivity y; auto. Qed. -Instance StrictOrder_PartialOrder +Hint Extern 4 (PreOrder (relation_disjunction _ _)) => + class_apply StrictOrder_PreOrder : typeclass_instances. + +Lemma StrictOrder_PartialOrder `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) : PartialOrder eqA (relation_disjunction R eqA). Proof. @@ -583,3 +588,6 @@ intros. intros x y. compute. intuition. elim (StrictOrder_Irreflexive x). transitivity y; auto. Qed. + +Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => + class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 83095720a..0d6130263 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -426,21 +426,22 @@ Class StrictOrder {A : Type} (R : relation A) := { }. Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R. -Proof. - firstorder. -Qed. +Proof. firstorder. Qed. (** Inversing a [StrictOrder] gives another [StrictOrder] *) -Instance StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R). +Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R). +Proof. firstorder. Qed. (** Same for [PartialOrder]. *) -Instance PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R). +Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R). +Proof. firstorder. Qed. -Instance PartialOrder_inverse `(PartialOrder A eqA R) : - PartialOrder eqA (inverse R). -Proof. -firstorder. -Qed. +Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances. +Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances. + +Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R). +Proof. firstorder. Qed. +Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances. |