New algorithm to resolve morphisms, after discussion with Nicolas

Tabareau: 
- first pass: generation of the Morphism constraints with metavariables
  for unspecified relations by one fold over the term. 
  This builds a "respect" proof term for the whole term with holes.
- second pass: constraint solving of the evars, taking care of finding a
  solution for all the evars at once. 
- third step: normalize proof term by found evars, apply it, done!
Works with any relation, currently not as efficient as it could be due
to bad handling of evars. Also needs some fine tuning of the instances
declared in Morphisms.v that are used during proof search, e.g. using
priorities.

Reorganize Classes.* accordingly, separating the setoids in
Classes.SetoidClass from the general morphisms in Classes.Morphisms
and the generally applicable relation theory in Classes.Relations.


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

1 files changed, 12 insertions, 14 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 78e53aa01..5e18ef2af 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -23,6 +23,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
 
 (** A setoid wraps an equivalence. *)
 
@@ -30,6 +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.
+
 (** Shortcuts to make proof search easier. *)
 
 Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
@@ -43,8 +48,8 @@ Proof. eauto with typeclass_instances. Qed.
 
 (** Standard setoids. *)
 
-Program Instance eq_setoid : Setoid A :=
-  equiv := eq ; setoid_equiv := eq_equivalence.
+(* Program Instance eq_setoid : Setoid A := *)
+(*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
 Program Instance iff_setoid : Setoid Prop :=
   equiv := iff ; setoid_equiv := iff_equivalence.
@@ -56,14 +61,7 @@ Program Instance iff_setoid : Setoid Prop :=
 
 Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
 
-Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
-
-Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x.
-Proof with auto.
-  intros ; red ; intros.
-  apply H.
-  sym...
-Qed.
+Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
@@ -82,15 +80,15 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
-Proof.
-  intros; intro. 
+Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
+Proof with auto.
+  intros; intro.
   assert(z == y) by relation_sym.
   assert(x == y) by relation_trans.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
   assert(y == x) by relation_sym.