Rename [Morphism] into [Proper] and [respect] into [proper] to comply

with standard math nomenclature. Also clean up in rewrite.ml4.


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

1 files changed, 63 insertions, 63 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index e2ab8b118..65d6687ea 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -24,15 +24,15 @@ Require Export Coq.Classes.RelationClasses.
 
 (** * Morphisms.
 
-   We now turn to the definition of [Morphism] and declare standard instances. 
+   We now turn to the definition of [Proper] and declare standard instances. 
    These will be used by the [setoid_rewrite] tactic later. *)
 
-(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
+(** A morphism for a relation [R] is a proper element of the relation.
    The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
    for usual morphisms. *)
 
-Class Morphism {A} (R : relation A) (m : A) : Prop :=
-  respect : R m m.
+Class Proper {A} (R : relation A) (m : A) : Prop :=
+  proper : R m m.
 
 (** Respectful morphisms. *)
 
@@ -56,10 +56,10 @@ Definition respectful {A B : Type}
 
 Delimit Scope signature_scope with signature.
 
-Arguments Scope Morphism [type_scope signature_scope].
+Arguments Scope Proper [type_scope signature_scope].
 Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
 
-Module MorphismNotations.
+Module ProperNotations.
 
   Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
     (right associativity, at level 55) : signature_scope.
@@ -70,9 +70,9 @@ Module MorphismNotations.
   Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
     (right associativity, at level 55) : signature_scope.
 
-End MorphismNotations.
+End ProperNotations.
 
-Export MorphismNotations.
+Export ProperNotations.
 
 Open Local Scope signature_scope.
 
@@ -113,30 +113,30 @@ Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B
 
 (** Subrelations induce a morphism on the identity. *)
 
-Instance subrelation_id_morphism `(subrelation A R₁ R₂) : Morphism (R₁ ==> R₂) id.
+Instance subrelation_id_proper `(subrelation A R₁ R₂) : Proper (R₁ ==> R₂) id.
 Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance morphisms_subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
+Instance subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
   subrelation (R₁ ==> S₁) (R₂ ==> S₂).
 Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
 (** And of course it is reflexive. *)
 
-Instance morphisms_subrelation_refl : ! subrelation A R R.
+Instance subrelation_refl : ! subrelation A R R.
 Proof. simpl_relation. Qed.
 
-(** [Morphism] is itself a covariant morphism for [subrelation]. *)
+(** [Proper] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism `(mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
-  sub : subrelation A R₁ R₂) : Morphism R₂ m.
+Lemma subrelation_proper `(mor : Proper A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
+  sub : subrelation A R₁ R₂) : Proper R₂ m.
 Proof.
   intros. apply sub. apply mor.
 Qed.
 
-Instance morphism_subrelation_morphism : 
-  Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).
+Instance proper_subrelation_proper : 
+  Proper (subrelation ++> @eq _ ==> impl) (@Proper A).
 Proof. reduce. subst. firstorder. Qed.
 
 (** We use an external tactic to manage the application of subrelation, which is otherwise
@@ -149,11 +149,11 @@ Inductive normalization_done : Prop := did_normalization.
 Ltac subrelation_tac := 
   match goal with
     | [ _ : subrelation_done |- _ ] => fail 1
-    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
-      set(H:=did_subrelation) ; eapply @subrelation_morphism
+    | [ |- @Proper _ _ _ ] => let H := fresh "H" in
+      set(H:=did_subrelation) ; eapply @subrelation_proper
   end.
 
-Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
+Hint Extern 5 (@Proper _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
@@ -167,11 +167,11 @@ Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
   subrelation (pointwise_relation A R) (pointwise_relation A R') | 4.
 Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
 
-(** The complement of a relation conserves its morphisms. *)
+(** The complement of a relation conserves its proper elements. *)
 
-Program Instance complement_morphism
-  `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-  Morphism (RA ==> RA ==> iff) (complement R).
+Program Instance complement_proper
+  `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
+  Proper (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
   Proof.
@@ -182,9 +182,9 @@ Program Instance complement_morphism
 
 (** The [inverse] too, actually the [flip] instance is a bit more general. *) 
 
-Program Instance flip_morphism
-  `(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) :
-  Morphism (RB ==> RA ==> RC) (flip f).
+Program Instance flip_proper
+  `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
+  Proper (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
   Proof.
@@ -195,7 +195,7 @@ Program Instance flip_morphism
    contravariant in the first argument, covariant in the second. *)
 
 Program Instance trans_contra_co_morphism
-  `(Transitive A R) : Morphism (R --> R ++> impl) R.
+  `(Transitive A R) : Proper (R --> R ++> impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -203,10 +203,10 @@ Program Instance trans_contra_co_morphism
     transitivity x0...
   Qed.
 
-(** Morphism declarations for partial applications. *)
+(** Proper declarations for partial applications. *)
 
 Program Instance trans_contra_inv_impl_morphism
-  `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3.
+  `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -214,7 +214,7 @@ Program Instance trans_contra_inv_impl_morphism
   Qed.
 
 Program Instance trans_co_impl_morphism
-  `(Transitive A R) : Morphism (R ==> impl) (R x) | 3.
+  `(Transitive A R) : Proper (R ==> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -222,7 +222,7 @@ Program Instance trans_co_impl_morphism
   Qed.
 
 Program Instance trans_sym_co_inv_impl_morphism
-  `(PER A R) : Morphism (R ==> inverse impl) (R x) | 2.
+  `(PER A R) : Proper (R ==> inverse impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -230,7 +230,7 @@ Program Instance trans_sym_co_inv_impl_morphism
   Qed.
 
 Program Instance trans_sym_contra_impl_morphism
-  `(PER A R) : Morphism (R --> impl) (R x) | 2.
+  `(PER A R) : Proper (R --> impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -238,7 +238,7 @@ Program Instance trans_sym_contra_impl_morphism
   Qed.
 
 Program Instance per_partial_app_morphism
-  `(PER A R) : Morphism (R ==> iff) (R x) | 1.
+  `(PER A R) : Proper (R ==> iff) (R x) | 1.
 
   Next Obligation.
   Proof with auto.
@@ -252,7 +252,7 @@ Program Instance per_partial_app_morphism
    to get an [R y z] goal. *)
 
 Program Instance trans_co_eq_inv_impl_morphism
-  `(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
+  `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2.
 
   Next Obligation.
   Proof with auto.
@@ -261,7 +261,7 @@ Program Instance trans_co_eq_inv_impl_morphism
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1.
+Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
@@ -274,8 +274,8 @@ Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1.
 Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
 Proof. firstorder. Qed.
   
-Program Instance compose_morphism A B C R₀ R₁ R₂ :
-  Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
+Program Instance compose_proper A B C R₀ R₁ R₂ :
+  Proper ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
 
   Next Obligation.
   Proof.
@@ -293,7 +293,7 @@ Proof. simpl_relation. Qed.
 (** [respectful] is a morphism for relation equivalence. *)
 
 Instance respectful_morphism : 
-  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
+  Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
 Proof.
   reduce.
   unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
@@ -313,25 +313,25 @@ Qed.
 (** Every element in the carrier of a reflexive relation is a morphism for this relation.
    We use a proxy class for this case which is used internally to discharge reflexivity constraints.
    The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of 
-   [Morphism (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
+   [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
    to set different priorities in different hint bases and select a particular hint database for
    resolution of a type class constraint.*) 
 
-Class MorphismProxy {A} (R : relation A) (m : A) : Prop :=
-  respect_proxy : R m m.
+Class ProperProxy {A} (R : relation A) (m : A) : Prop :=
+  proper_proxy : R m m.
 
-Instance reflexive_morphism_proxy
-  `(Reflexive A R) (x : A) : MorphismProxy R x | 1.
+Instance reflexive_proper_proxy
+  `(Reflexive A R) (x : A) : ProperProxy R x | 1.
 Proof. firstorder. Qed.
 
-Instance morphism_morphism_proxy
-  `(Morphism A R x) : MorphismProxy R x | 2.
+Instance proper_proper_proxy
+  `(Proper A R x) : ProperProxy R x | 2.
 Proof. firstorder. Qed.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) :
-   Morphism R' (m x).
+Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
+   Proper R' (m x).
 Proof. simpl_relation. Qed.
 
 Class Params {A : Type} (of : A) (arity : nat).
@@ -367,7 +367,7 @@ Ltac partial_application_tactic :=
     | [ _ : subrelation_done |- _ ] => fail 1
     | [ _ : normalization_done |- _ ] => fail 1
     | [ _ : @Params _ _ _ |- _ ] => fail 1
-    | [ |- @Morphism ?T _ (?m ?x) ] => 
+    | [ |- @Proper ?T _ (?m ?x) ] => 
       match goal with 
         | [ _ : PartialApplication |- _ ] => 
           eapply @Reflexive_partial_app_morphism
@@ -378,7 +378,7 @@ Ltac partial_application_tactic :=
       end
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
+Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
   relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
@@ -429,13 +429,13 @@ Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor.
+Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor.
 
-Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances.
+Hint Extern 2 (@Proper _ (flip _) _) => eapply @proper_inverse_proper : typeclass_instances.
 
 (** Bootstrap !!! *)
 
-Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
+Instance proper_proper : Proper (relation_equivalence ==> @eq _ ==> iff) (@Proper A).
 Proof.
   simpl_relation.
   reduce in H.
@@ -446,37 +446,37 @@ Proof.
   apply H0.
 Qed.
 
-Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m.
+Lemma proper_releq_proper `(Normalizes A R R', Proper _ R' m) : Proper R m.
 Proof.
   intros.
 
-  pose respect as r.
+  pose proper as r.
   pose normalizes as norm.
   setoid_rewrite norm.
   assumption.
 Qed.
 
-Ltac morphism_normalization := 
+Ltac proper_normalization := 
   match goal with
     | [ _ : subrelation_done |- _ ] => fail 1
     | [ _ : normalization_done |- _ ] => fail 1
-    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
-      set(H:=did_normalization) ; eapply @morphism_releq_morphism
+    | [ |- @Proper _ _ _ ] => let H := fresh "H" in
+      set(H:=did_normalization) ; eapply @proper_releq_proper
   end.
 
-Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
+Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances.
 
 (** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
 
-Lemma reflexive_morphism `{Reflexive A R} (x : A)
-   : Morphism R x.
+Lemma reflexive_proper `{Reflexive A R} (x : A)
+   : Proper R x.
 Proof. firstorder. Qed.
 
-Ltac morphism_reflexive :=
+Ltac proper_reflexive :=
   match goal with
     | [ _ : normalization_done |- _ ] => fail 1
     | [ _ : subrelation_done |- _ ] => fail 1
-    | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
+    | [ |- @Proper _ _ _ ] => eapply @reflexive_proper
   end.
 
-Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
+Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.