Fixes in new Morphisms files.

- Use a notation for predicate instead of a
definition (better pretty-printing this way, and no delta
problem!).
- Correct inadvertent import of Coq.Program.Program which sets
implicit arguments for left,right and so on. Should fix the contribs
that used to compile. 
- Correct normalization_tac to do normalization of "inverse"
signatures. Add a missing instance, and name the existing ones.


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

4 files changed, 38 insertions, 38 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 7cabc836dc..975dcf1dd0 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -232,7 +232,7 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
 Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
-  Reflexive_partial_app_morphism : Morphism R' (m x) | 3.
+  Reflexive_partial_app_morphism : Morphism R' (m x) | 4.
 
 (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
@@ -330,23 +330,32 @@ Proof.
   split ; intros ; intuition.
 Qed.
 
+(** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
 
-Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) : Prop :=
-  normalizes : R m m'.
+Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
+  normalizes : relation_equivalence m m'.
 
 Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
-  Normalizes subrelation (inverse R ==> inverse R') (inverse (R ==> R')) .
-Proof. simpl_relation. Qed.
+  inverse_respectful_norm : Normalizes _ (inverse R ==> inverse R') (inverse (R ==> R')) .
+Proof. firstorder. Qed.
 
-Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] =>
-  ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
-Proof. red ; intros. 
+(* If not an inverse on the left, do a double inverse. *)
+
+Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
+  not_inverse_respectful_norm : Normalizes _ (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+Proof. firstorder. Qed.
+
+Instance [ Normalizes B R' (inverse R'') ] =>
+  inverse_respectful_rec_norm : Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
+Proof. red ; intros.  
   pose normalizes as r.
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
   reflexivity.
 Qed.
 
+(** Once we have normalized, we will apply this instance to simplify the problem. *)
+
 Program Instance [ Morphism A R m ] => 
   morphism_inverse_morphism : Morphism (inverse R) m | 2.
 
@@ -363,9 +372,7 @@ Proof.
   apply H0.
 Qed.
 
-Lemma morphism_releq_morphism 
-  [ Normalizes (relation A) relation_equivalence R R',
-    Morphism _ R' m ] : Morphism R m.
+Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
   pose respect as r.
@@ -378,7 +385,7 @@ Inductive normalization_done : Prop := did_normalization.
 
 Ltac morphism_normalization := 
   match goal with
-    | [ _ : normalization_done |- @Morphism _ _ _ ] => fail
+    | [ _ : normalization_done |- _ ] => fail
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
       set(H:=did_normalization) ; eapply @morphism_releq_morphism
   end.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index d22ab06cb7..301fba5346 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -14,7 +14,8 @@
    91405 Orsay, France *)
 
 Require Import Coq.Classes.Morphisms.
-Require Import Coq.Program.Program.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
 
 (** Standard instances for [not], [iff] and [impl]. *)
 
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 274389496b..5018fa01ec 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -31,11 +31,11 @@ Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) =
 Require Import List.
 
 Lemma predicate_equivalence_pointwise (l : list Type) :
-  Morphism (@predicate_equivalence l ==> lift_pointwise l iff) id.
+  Morphism (@predicate_equivalence l ==> pointwise_lifting iff l) id.
 Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
 
 Lemma predicate_implication_pointwise (l : list Type) :
-  Morphism (@predicate_implication l ==> lift_pointwise l impl) id.
+  Morphism (@predicate_implication l ==> pointwise_lifting impl l) id.
 Proof. do 2 red. unfold predicate_implication. auto. Qed.
 
 (** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 8dfb662b28..c1ee3566ec 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -240,13 +240,13 @@ Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
 
 (** We define n-ary [predicate]s as functions into [Prop]. *)
 
-Definition predicate (l : list Type) := arrows l Prop.
+Notation predicate l := (arrows l Prop).
 
 (** Unary predicates, or sets. *)
 
 Definition unary_predicate A := predicate (cons A nil).
 
-(** Homogenous binary relations, equivalent to [relation A]. *)
+(** Homogeneous binary relations, equivalent to [relation A]. *)
 
 Definition binary_relation A := predicate (cons A (cons A nil)).
 
@@ -265,39 +265,35 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
   end.
 
 (** Pointwise extension of a binary operation on [T] to a binary operation 
-   on functions whose codomain is [T]. *)
+   on functions whose codomain is [T].
+   For an operator on [Prop] this lifts the operator to a binary operation. *)
 
-Fixpoint pointwise_extension {l : list Type} {T : Type}
-  (op : binary_operation T) : binary_operation (arrows l T) :=
+Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
+  (l : list Type) : binary_operation (arrows l T) :=
   match l with
     | nil => fun R R' => op R R'
     | A :: tl => fun R R' => 
-      fun x => pointwise_extension op (R x) (R' x)
+      fun x => pointwise_extension op tl (R x) (R' x)
   end.
 
-(** For an operator on [Prop] this lifts the operator to a binary operation. *)
-
-Definition pointwise_relation_extension (l : list Type) (op : binary_relation Prop) : 
-  binary_operation (predicate l) := pointwise_extension op.
-
 (** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *)
 
-Fixpoint lift_pointwise (l : list Type) (op : binary_relation Prop) : binary_relation (predicate l) :=
+Fixpoint pointwise_lifting (op : binary_relation Prop)  (l : list Type) : binary_relation (predicate l) :=
   match l with
     | nil => fun R R' => op R R'
     | A :: tl => fun R R' => 
-      forall x, lift_pointwise tl op (R x) (R' x)
+      forall x, pointwise_lifting op tl (R x) (R' x)
   end.
 
 (** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *)
 
 Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) :=
-  lift_pointwise l iff.
+  pointwise_lifting iff l.
 
 (** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *)
 
 Definition predicate_implication {l : list Type} :=
-  lift_pointwise l impl.
+  pointwise_lifting impl l.
 
 (** Notations for pointwise equivalence and implication of predicates. *)
 
@@ -309,11 +305,8 @@ Open Local Scope predicate_scope.
 (** The pointwise liftings of conjunction and disjunctions.
    Note that these are [binary_operation]s, building new relations out of old ones. *)
 
-Definition predicate_intersection {l : list Type} : binary_operation (predicate l) :=
-  pointwise_relation_extension l and.
-
-Definition predicate_union {l : list Type} : binary_operation (predicate l) :=
-  pointwise_relation_extension l or.
+Definition predicate_intersection := pointwise_extension and.
+Definition predicate_union := pointwise_extension or.
 
 Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope.
 Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope.
@@ -349,9 +342,9 @@ Program Instance predicate_equivalence_equivalence :
   Qed.
   
   Next Obligation.
-    fold lift_pointwise.
+    fold pointwise_lifting.
     induction l. firstorder.
-    intros. simpl in *. intro. pose (IHl (x x0) (y x0) (z x0)).
+    intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
     firstorder.
   Qed.
 
@@ -363,7 +356,6 @@ Program Instance predicate_implication_preorder :
   Qed.
 
   Next Obligation.
-    fold lift_pointwise.
     induction l. firstorder.
     unfold predicate_implication in *. simpl in *. 
     intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.