Update and start testing rewrite-in-type code.

4 files changed, 25 insertions, 70 deletions

diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
index 68a6dcd63..b540feabf 100644
--- a/theories/Classes/CEquivalence.v
+++ b/theories/Classes/CEquivalence.v
@@ -17,8 +17,8 @@ Require Import Coq.Program.Tactics.
 
 Require Import Coq.Classes.Init.
 Require Import Relation_Definitions.
-Require Export Coq.Classes.RelationClasses.
-Require Import Coq.Classes.Morphisms.
+Require Export Coq.Classes.CRelationClasses.
+Require Import Coq.Classes.CMorphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 5737c88b5..4b031f949 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -15,7 +15,8 @@
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
-Require Export Coq.Classes.RelationClasses.
+Require Import Setoid.
+Require Export Coq.Classes.CRelationClasses.
 
 Generalizable Variables A eqA B C D R RA RB RC m f x y.
 Local Obligation Tactic := simpl_crelation.
@@ -31,8 +32,7 @@ Set Universe Polymorphism.
    The relation [R] will be instantiated by [respectful] and [A] by an arrow
    type for usual morphisms. *)
 Section Proper.
-  Let U := Type.
-  Context {A B : U}.
+  Context {A B : Type}.
 
   Class Proper (R : crelation A) (m : A) :=
     proper_prf : R m m.
@@ -145,16 +145,15 @@ Ltac f_equiv :=
  end.
 
 Section Relations.
-  Let U := Type.
-  Context {A B : U}. 
+  Context {A B : Type}. 
 
   (** [forall_def] reifies the dependent product as a definition. *)
   
-  Definition forall_def (P : A -> U) : Type := forall x : A, P x.
+  Definition forall_def (P : A -> Type) : Type := forall x : A, P x.
   
   (** Dependent pointwise lifting of a crelation on the range. *)
   
-  Definition forall_relation (P : A -> U)
+  Definition forall_relation (P : A -> Type)
              (sig : forall a, crelation (P a)) : crelation (forall x, P x) :=
     fun f g => forall a, sig a (f a) (g a).
 
@@ -206,12 +205,11 @@ Section Relations.
   Proof. reduce. unfold pointwise_relation in *. apply sub. auto. Qed.
   
   (** For dependent function types. *)
-  Lemma forall_subrelation (P : A -> U) (R S : forall x : A, crelation (P x)) :
+  Lemma forall_subrelation (P : A -> Type) (R S : forall x : A, crelation (P x)) :
     (forall a, subrelation (R a) (S a)) -> 
     subrelation (forall_relation P R) (forall_relation P S).
   Proof. reduce. firstorder. Qed.
 End Relations.
-
 Typeclasses Opaque respectful pointwise_relation forall_relation.
 Arguments forall_relation {A P}%type sig%signature _ _.
 Arguments pointwise_relation A%type {B}%type R%signature _ _.
@@ -260,8 +258,7 @@ Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)
 
 Section GenericInstances.
   (* Share universes *)
-  Let U := Type.
-  Context {A B C : U}.
+  Context {A B C : Type}.
 
   (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
@@ -344,15 +341,6 @@ Section GenericInstances.
   Qed.
 
   Global Program 
-  Instance trans_co_impl_morphism
-    `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
-
-  Next Obligation.
-  Proof with auto.
-    transitivity x0...
-  Qed.
-
-  Global Program 
   Instance trans_co_impl_type_morphism
     `(Transitive A R) : Proper (R ++> arrow) (R x) | 3.
 
@@ -362,15 +350,6 @@ Section GenericInstances.
   Qed.
 
   Global Program 
-  Instance trans_sym_co_inv_impl_morphism
-    `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
-
-  Next Obligation.
-  Proof with auto.
-    transitivity y... symmetry...
-  Qed.
-
-  Global Program 
   Instance trans_sym_co_inv_impl_type_morphism
     `(PER A R) : Proper (R ++> flip arrow) (R x) | 3.
 
@@ -379,14 +358,6 @@ Section GenericInstances.
     transitivity y... symmetry...
   Qed.
 
-  Global Program Instance trans_sym_contra_impl_morphism
-    `(PER A R) : Proper (R --> impl) (R x) | 3.
-
-  Next Obligation.
-  Proof with auto.
-    transitivity x0... symmetry...
-  Qed.
-
   Global Program Instance trans_sym_contra_arrow_morphism
     `(PER A R) : Proper (R --> arrow) (R x) | 3.
 
@@ -395,17 +366,6 @@ Section GenericInstances.
     transitivity x0... symmetry...
   Qed.
 
-  Global Program Instance per_partial_app_morphism
-  `(PER A R) : Proper (R ==> iff) (R x) | 2.
-
-  Next Obligation.
-  Proof with auto.
-    split. intros ; transitivity x0...
-    intros.
-    transitivity y...
-    symmetry...
-  Qed.
-
   Global Program Instance per_partial_app_type_morphism
   `(PER A R) : Proper (R ==> iffT) (R x) | 2.
 
@@ -440,19 +400,6 @@ Section GenericInstances.
   (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)
 
   Global Program 
-  Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
-
-  Next Obligation.
-  Proof with auto.
-    split ; intros.
-    transitivity x0... transitivity x... symmetry...
-
-    transitivity y... transitivity y0... symmetry...
-  Qed.
-
-  (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)
-
-  Global Program 
   Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1.
 
   Next Obligation.
@@ -491,8 +438,8 @@ Section GenericInstances.
     intros R R' HRR' S S' HSS' f g.
     unfold respectful, relation_equivalence in * ; simpl in *.
     split ; intros H x y Hxy.
-    setoid_rewrite <- HSS'. apply H. now rewrite HRR'.
-    rewrite HSS'. apply H. now rewrite <- HRR'.
+    apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). 
+    apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). 
   Qed.
 
   (** [R] is Reflexive, hence we can build the needed proof. *)
@@ -594,8 +541,8 @@ Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper
 Proof.
   intros A R R' HRR' x y <-. red in HRR'.
   split ; red ; intros. 
-  now setoid_rewrite <- HRR'.
-  now setoid_rewrite HRR'.
+  now apply (fst (HRR' _ _)). 
+  now apply (snd (HRR' _ _)).
 Qed.
 
 Ltac proper_reflexive :=
@@ -633,7 +580,7 @@ Section Normalize.
   Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
   Proof.
     red in H, H0. red in H.
-    setoid_rewrite H.
+    apply (snd (H _ _)). 
     assumption.
   Qed.
 
@@ -722,7 +669,7 @@ Qed.
 
 (** A [PartialOrder] is compatible with its underlying equivalence. *)
 Require Import Relation_Definitions.
-Instance PartialOrder_proper `(PartialOrder A eqA (R : relation A)) :
+Instance PartialOrder_proper `(PartialOrder A eqA (R : crelation A)) :
   Proper (eqA==>eqA==>iff) R.
 Proof.
 intros.
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.
diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget
index 75024b947..18147f2a4 100644
--- a/theories/Classes/vo.itarget
+++ b/theories/Classes/vo.itarget
@@ -10,3 +10,6 @@ SetoidClass.vo
 SetoidDec.vo
 SetoidTactics.vo
 RelationPairs.vo
+CRelationClasses.vo
+CMorphisms.vo
+CEquivalence.vo