Using the "relation" constant made some unifications fail in the new

setoid rewrite. Refine and use the new unification flags setup by Hugo
to do a little bit of delta in clenv_unify/w_unify. Moved from a boolean
indicating conversion is wanted to a Cpred representing the
constants one wants to get unfolded to have more precise control. Add
corresponding test-suite file.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10684 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 0 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index eaf300fd27..dd964433c0 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -305,6 +305,45 @@ Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) (C : T
     apply r ; auto.
   Qed.
 
+
+(** Every transitive relation gives rise to a binary morphism on [impl], 
+   contravariant in the first argument, covariant in the second. *)
+
+Program Instance [ ! Transitive A (R : relation A) ] => 
+  trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans x...
+    trans x0...
+  Qed.
+
+(** Dually... *)
+
+Program Instance [ ! Transitive A (R : relation A) ] =>
+  trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
+  
+  Next Obligation.
+  Proof with auto.
+    intros.
+    destruct (trans_contra_co_morphism (R:=inverse R)).
+    revert respect0.
+    unfold respectful, inverse, flip, impl in * ; intros.
+    eapply respect0 ; eauto.
+  Qed.
+
+(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *)
+(*   trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R. *)
+
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     trans y... *)
+(*     sym... *)
+(*     trans y0... *)
+(*     sym... *)
+(*   Qed. *)
+
+
 (** Morphism declarations for partial applications. *)
 
 Program Instance [ ! Transitive A R ] (x : A) =>