Fix the clrewrite tactic, change Relations.v to work on relations in Prop

only, and get rid of the "relation" definition which makes unification
fail blatantly. Replace it with a notation :) In its current state,
the new tactic seems ready for larger tests.


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

3 files changed, 42 insertions, 74 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 09a58fa01..72db276e4 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -29,23 +29,16 @@ Unset Strict Implicit.
 
 (** Respectful morphisms. *)
 
-Definition respectful_depT (A : Type) (R : relationT A) 
-  (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := 
+Definition respectful_dep (A : Type) (R : relation A) 
+  (B : A -> Type) (R' : forall x y, B x -> B y -> Prop) : relation (forall x : A, B x) := 
   fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
 
-Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
-  Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
-
 Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
   fun f g => forall x y : A, R x y -> R' (f x) (g y).
 
-(** Notations reminiscent of the old syntax for declaring morphisms.
-   We use three + or - for type morphisms, and two for [Prop] ones.
-   *)
-
-Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
-Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
 
+Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20).
 Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
 Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
 
@@ -53,7 +46,7 @@ Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity,
    The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
    for usual morphisms. *)
 
-Class Morphism A (R : relationT A) (m : A) :=
+Class Morphism A (R : relation A) (m : A) :=
   respect : R m m.
 
 (** Here we build an equivalence instance for functions which relates respectful ones only. *)
@@ -63,7 +56,7 @@ Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : rela
 
 Ltac obligations_tactic ::= program_simpl.
 
-Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => 
+Program Instance [ Equivalence A R, Equivalence B R' ] => 
   respecting_equiv : Equivalence respecting
   (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
 
@@ -93,12 +86,6 @@ Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation
 
 Ltac obligations_tactic ::= program_simpl ; simpl_relation.
 
-Program Instance notT_arrow_morphism : 
-  Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
-
-Program Instance not_iso_morphism : 
-  Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
-
 Program Instance not_impl_morphism :
   Morphism (Prop -> Prop) (impl --> impl) not.
 
@@ -134,7 +121,7 @@ Program Instance `A` (R : relation A) `B` (R' : relation B)
     destruct respect with x y x0 y0 ; auto.
   Qed.
 
-Program Instance `A` (R : relation A) `B` (R' : relation B)
+Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
   [ ? Morphism (R ++> R' ++> iff) m ] =>
   iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
 
@@ -171,7 +158,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 (* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
 (*   fun x y => R x y -> R' (f x) (f y). *)
 
-(* Definition morphism_respectful' A (R : relation A) B (R' : relation B) (f : A -> B) *)
+(* Definition morphism_respectful' A R B (R' : relation B) (f : A -> B) *)
 (*   [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *)
 (* intros. *)
 (* destruct H. *)
@@ -182,7 +169,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 
 (* Existing Instance morphism_respectful'. *)
 
-(* Goal forall A [ Equivalence A (eqA : relation A) ] (R : relation A) [ ? Morphism (eqA ++> iff) m ] (x y : A)  *)
+(* Goal forall A [ Equivalence A (eqA : relation A) ] R [ ? Morphism (eqA ++> iff) m ] (x y : A)  *)
 (*   [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *)
 (*   intros. *)
 (*   cut (relation A) ; intros R'. *)
@@ -210,7 +197,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 
 (** A proof of [R x x] is available. *)
 
-(* Program Instance (A : Type) (R : relation A) B (R' : relation B) *)
+(* Program Instance (A : Type) R B (R' : relation B) *)
 (*   [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *)
 (*   morphism_partial_app_morphism : ? Morphism R' (m x). *)
 
@@ -223,7 +210,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 
 (** Morpshism declarations for partial applications. *)
 
-Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -231,7 +218,7 @@ Program Instance [ Transitive A (R : relation A) ] (x : A) =>
     trans y...
   Qed.
 
-Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_co_impl_morphism : ? Morphism (R ++> impl) (R x).
 
   Next Obligation.
@@ -239,7 +226,7 @@ Program Instance [ Transitive A (R : relation A) ] (x : A) =>
     trans x0...
   Qed.
 
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
   trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x).
 
   Next Obligation.
@@ -248,7 +235,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
     sym...
   Qed.
 
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
   trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x).
 
   Next Obligation.
@@ -257,7 +244,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
     sym...
   Qed.
 
-Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
+Program Instance [ Equivalence A R ] (x : A) =>
   equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x).
 
   Next Obligation.
@@ -270,7 +257,7 @@ Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
 
 (** With symmetric relations, variance is no issue ! *)
 
-Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) 
+Program Instance [ Symmetric A R ] B (R' : relation B) 
   [ Morphism _ (R ++> R') m ] => 
   sym_contra_morphism : ? Morphism (R --> R') m.
 
@@ -282,7 +269,7 @@ Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B)
 
 (** [R] is reflexive, hence we can build the needed proof. *)
 
-Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
+Program Instance [ Reflexive A R ] B (R' : relation B)
   [ ? Morphism (R ++> R') m ] (x : A) =>
   reflexive_partial_app_morphism : ? Morphism R' (m x).
 
@@ -295,7 +282,7 @@ Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
 
 (** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] => 
+Program Instance [ Transitive A R, Symmetric A R ] => 
   trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
 
   Next Obligation.
@@ -306,7 +293,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] =>
     trans y... trans y0... sym...
   Qed.
 
-Program Instance [ Equivalence A (R : relation A) ] => 
+Program Instance [ Equivalence A R ] => 
   equiv_morphism : ? Morphism (R ++> R ++> iff) R.
 
   Next Obligation.
@@ -335,16 +322,16 @@ Program Instance inverse_iff_impl_id :
 
 (** Logical conjunction. *)
 
-(* Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. *)
+Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
 
-(* Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. *)
+Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
 
 Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
 
 (** Logical disjunction. *)
 
-(* Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. *)
+Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
 
-(* Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. *)
+Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
 
 Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index aaeb18654..9cc78a970 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -22,41 +22,35 @@ Require Import Coq.Classes.Init.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Definition relationT A := A -> A -> Type.
-Definition relation A := A -> A -> Prop.
+Notation "'relation' A " := (A -> A -> Prop) (at level 0).
 
 Definition inverse A (R : relation A) : relation A := fun x y => R y x.
 
 Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
 Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
 
-Definition complementT A (R : relationT A) := fun x y => notT (R x y).
-
 Definition complement A (R : relation A) := fun x y => R x y -> False.
 
 (** These are convertible. *)
 
-Lemma complementT_flip : forall A (R : relationT A), complementT (flip R) = flip (complementT R).
-Proof. reflexivity. Qed.
-
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
 Proof. reflexivity. Qed.
 
 (** We rebind relations in separate classes to be able to overload each proof. *)
 
-Class Reflexive A (R : relationT A) :=
+Class Reflexive A (R : relation A) :=
   reflexive : forall x, R x x.
 
-Class Irreflexive A (R : relationT A) := 
+Class Irreflexive A (R : relation A) := 
   irreflexive : forall x, R x x -> False.
 
-Class Symmetric A (R : relationT A) := 
+Class Symmetric A (R : relation A) := 
   symmetric : forall x y, R x y -> R y x.
 
-Class Asymmetric A (R : relationT A) := 
+Class Asymmetric A (R : relation A) := 
   asymmetric : forall x y, R x y -> R y x -> False.
 
-Class Transitive A (R : relationT A) := 
+Class Transitive A (R : relation A) := 
   transitive : forall x y z, R x y -> R y z -> R x z.
 
 Implicit Arguments Reflexive [A].
@@ -141,23 +135,6 @@ Ltac simpl_relation :=
 
 Ltac obligations_tactic ::= simpl_relation.
 
-(** The arrow is a reflexive and transitive relation on types. *)
-
-Program Instance arrow_refl : ? Reflexive arrow := 
-  reflexive X := id.
-
-Program Instance arrow_trans : ? Transitive arrow := 
-  transitive X Y Z f g := g o f.
-
-(** Isomorphism. *)
-
-Definition iso (A B : Type) := 
-  A -> B * B -> A.
-
-Program Instance iso_refl : ? Reflexive iso.
-Program Instance iso_sym : ? Symmetric iso.
-Program Instance iso_trans : ? Transitive iso.
-
 (** Logical implication. *)
 
 Program Instance impl_refl : ? Reflexive impl.
@@ -180,7 +157,7 @@ Program Instance eq_trans : ? Transitive (@eq A).
    - a tactic to immediately solve a goal without user intervention
    - a tactic taking input from the user to make progress on a goal *)
 
-Definition relate A (R : relationT A) : relationT A := R.
+Definition relate A (R : relation A) : relation A := R.
 
 Ltac relationify_relation R R' :=
   match goal with
@@ -287,7 +264,7 @@ Ltac relation_tac := relation_refl || relation_sym || relation_trans.
 
 (** The [PER] typeclass. *)
 
-Class PER (carrier : Type) (pequiv : relationT carrier) :=
+Class PER (carrier : Type) (pequiv : relation carrier) :=
   per_sym :> Symmetric pequiv ;
   per_trans :> Transitive pequiv.
 
@@ -307,14 +284,14 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
 
 (** The [Equivalence] typeclass. *)
 
-Class Equivalence (carrier : Type) (equiv : relationT carrier) :=
+Class Equivalence (carrier : Type) (equiv : relation carrier) :=
   equiv_refl :> Reflexive equiv ;
   equiv_sym :> Symmetric equiv ;
   equiv_trans :> Transitive equiv.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class [ Equivalence A eqA ] => Antisymmetric (R : relationT A) := 
+Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetric : forall x y, R x y -> R y x -> eqA x y.
 
 Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 5e18ef2af..8c8c8c67c 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -31,9 +31,10 @@ Class Setoid A :=
   equiv : relation A ;
   setoid_equiv :> Equivalence A equiv.
 
-Program Instance [ eqa : Equivalence A (eqA : relation A) ] => 
-  equivalence_setoid : Setoid A :=
-  equiv := eqA ; setoid_equiv := eqa.
+(* Too dangerous instance *)
+(* Program Instance [ eqa : Equivalence A eqA ] =>  *)
+(*   equivalence_setoid : Setoid A := *)
+(*   equiv := eqA ; setoid_equiv := eqa. *)
 
 (** Shortcuts to make proof search easier. *)
 
@@ -46,6 +47,10 @@ Proof. eauto with typeclass_instances. Qed.
 Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
+Existing Instance setoid_refl.
+Existing Instance setoid_sym.
+Existing Instance setoid_trans.
+
 (** Standard setoids. *)
 
 (* Program Instance eq_setoid : Setoid A := *)
@@ -142,11 +147,10 @@ Ltac obligations_tactic ::= morphism_tac.
 
 Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
 
-Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id.
+(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
 
 (* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
 (*   (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
-    
 
 (* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
 (*   [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] =>  *)