Correct implementation of normalization of signatures using setoid

rewriting, in some sense bootstrapping the system. Remove redundant
morphisms for now to test for completeness (small performance penalty).


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

4 files changed, 127 insertions, 53 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 998e767f5..b2684a392 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -824,8 +824,8 @@ let cl_rewrite_clause_aux hypinfo goal_meta occs clause gl =
 		  if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd)
 		  else tclIDTAC
 	      in tclTHENLIST [evartac; rewtac] gl
-	    with UserError (env, e) -> 
-	      tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints") gl)
+	    with UserError (s, pp) -> 
+	      tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints:" ++ fnl () ++ pp) gl)
       | None -> 
 	  let {l2r=l2r; c1=x; c2=y} = !hypinfo in
 	    raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y)))
@@ -1134,8 +1134,6 @@ let default_morphism sign m =
   let mor = resolve_one_typeclass env morph in
     mor, respect_projection mor morph
     	  
-let unfold_respectful = lazy (Tactics.unfold_in_concl [[], EvalConstRef (destConst (Lazy.force respectful))])
-
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      [	init_setoid ();
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index b90fdc97e..5543f615d 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -26,6 +26,11 @@ Require Export Coq.Classes.SetoidTactics.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
+
+Instance [ ! Equivalence A R ] => 
+  equivalence_default : DefaultRelation A R | 4.
+
 Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
@@ -152,8 +157,3 @@ Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scop
 (** Reset the default Program tactic. *)
 
 Ltac obligations_tactic ::= program_simpl.
-
-(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
-
-Instance [ ! Equivalence A R ] => 
-  equivalence_default : DefaultRelation A R | 4.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index fbe90a9a9..a6ca6a031 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -220,52 +220,9 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C)
 
   Next Obligation.
   Proof.
-    unfold flip. 
     apply respect ; auto.
   Qed.
 
-(** Partial applications are ok when a proof of refl is available. *)
-
-(** A proof of [R x x] is available. *)
-
-(* Program Instance (A : Type) R B (R' : relation B) *)
-(*   [ Morphism (R ==> R') m ] [ Morphism R x ] => *)
-(*   morphism_partial_app_morphism : Morphism R' (m x). *)
-
-(*   Next Obligation. *)
-(*   Proof with auto. *)
-(*     apply (respect (m:=m))... *)
-(*     apply respect. *)
-(*   Qed. *)
-
-(** Every morphism gives rise to a morphism on the inverse relation. *)
-
-Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B)
-  [ Morphism (R ==> R') m ] => morphism_inverse_morphism :
-  Morphism (R --> inverse R') m.
-
-  Next Obligation.
-  Proof.
-    unfold inverse in *.
-    pose respect.
-    unfold respectful in r.
-    apply r ; auto.
-  Qed.
-
-(* Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) (C : Type) (R'' : relation C) *)
-(*   [ Morphism (R ++> R' ++> R'') m ] => *)
-(*   morphism_inverse_inverse_morphism : *)
-(*   Morphism (R --> R' --> inverse R'') m. *)
-
-(*   Next Obligation. *)
-(*   Proof. *)
-(*     unfold inverse in *. *)
-(*     pose respect. *)
-(*     unfold respectful in r. *)
-(*     apply r ; auto. *)
-(*   Qed. *)
-
-
 (** Every transitive relation gives rise to a binary morphism on [impl], 
    contravariant in the first argument, covariant in the second. *)
 
@@ -493,3 +450,97 @@ Proof. simpl_relation. Qed.
 Instance (A B : Type) [ ! Reflexive B R' ] => 
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
+
+(** [respectful] is a morphism for relation equivalence. *)
+
+Instance respectful_morphism : 
+  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). 
+Proof.
+  do 2 red ; intros.
+  unfold respectful, relation_equivalence in *.
+  red ; intros.
+  split ; intros.
+  
+    rewrite <- H0.
+    apply H1.
+    rewrite H.
+    assumption.
+
+    rewrite H0.
+    apply H1.
+    rewrite <- H.
+    assumption.
+Qed.
+
+Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
+  inverse (R ==> R') ==rel (inverse R ==> inverse R').
+Proof.
+  intros.
+  unfold inverse, flip.
+  unfold respectful.
+  split ; intros ; intuition.
+Qed.
+
+Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) :=
+  normalizes : R m m'.
+
+Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
+  Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) .
+Proof.
+  symmetry ; apply inverse_respectful.
+Qed.
+
+Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B) 
+  [ Normalizes relation_equivalence R' (inverse R'') ] =>
+  Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
+Proof.
+  pose normalizes.
+  setoid_rewrite r.
+  setoid_rewrite inverse_respectful.
+  reflexivity.
+Qed.
+
+Program Instance (A : Type) (R : relation A)
+  [ Morphism R m ] => morphism_inverse_morphism :
+  Morphism (inverse R) m | 2.
+
+  Next Obligation.
+  Proof.
+    apply respect.
+  Qed.
+
+(** Bootstrap !!! *)
+
+Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
+Proof.
+  simpl_relation.
+  subst.
+  unfold relation_equivalence in H.
+  split ; constructor ; intros.
+  setoid_rewrite <- H.
+  apply respect.
+  setoid_rewrite H.
+  apply respect.
+Qed.
+  
+Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A)
+  [ Normalizes relation_equivalence R R' ]
+  [ Morphism R' m ] : Morphism R m.
+Proof.
+  intros. 
+  pose respect.
+  assert(n:=normalizes).
+  setoid_rewrite n.
+  assumption.
+Qed.
+
+Inductive normalization_done : Prop := did_normalization.
+
+Ltac morphism_normalization := 
+  match goal with
+    | [ _ : normalization_done |- @Morphism _ _ _ ] => fail
+    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
+      set(H:=did_normalization) ; eapply @morphism_releq_morphism
+  end.
+
+Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 20ac475b9..68352abd0 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -227,3 +227,28 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid
   (fun f g => forall (x y : a), R x y -> R' (f x) (g y)).
 *)
 
+Definition relation_equivalence {A : Type} : relation (relation A) :=
+  fun (R R' : relation A) => forall x y, R x y <-> R' x y.
+
+Infix "==rel" := relation_equivalence (at level 70).
+
+Program Instance relation_equivalence_equivalence :
+  Equivalence (relation A) relation_equivalence.
+
+  Next Obligation.
+  Proof.
+    constructor ; red ; intros.
+    apply reflexive.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    constructor ; red ; intros.
+    apply symmetric ; apply H.
+  Qed.
+  
+  Next Obligation.
+  Proof.
+    constructor ; red ; intros.
+    apply transitive with (y x0 y0) ; [ apply H | apply H0 ].
+  Qed.