diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 21:38:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 21:38:58 +0200 |
| commit | e681d5809844c2a1514e0fc6b2a334002466db7a (patch) | |
| tree | f41341a8947fdb6a13e415f85cbd4de3f5a83d7c /theories/Classes/CRelationClasses.v | |
| parent | 816353f8bee87a8ae1c70263cc3f2dc8ad5358cd (diff) | |
Update and start testing rewrite-in-type code.
Diffstat (limited to 'theories/Classes/CRelationClasses.v')
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index 5e04671ba..ed43a5e52 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -25,6 +25,10 @@ Set Universe Polymorphism. Definition crelation (A : Type) := A -> A -> Type. +Definition arrow (A B : Type) := A -> B. + +Definition flip {A B C : Type} (f : A -> B -> C) := fun x y => f y x. + Definition iffT (A B : Type) := ((A -> B) * (B -> A))%type. (** We allow to unfold the [crelation] definition while doing morphism search. *) @@ -334,7 +338,8 @@ Section Binary. Qed. Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). - Proof. firstorder. Qed. + Proof. unfold flip; constructor; unfold flip. intros. apply H. apply symmetry. apply X. + unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed. End Binary. Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. |