Use manual implicts in Classes and rationalize class parameter names.

Now it's [A] and [R] for carriers and relations and [eqA] when the
relation is supposed to be an equivalence. The types are always implicit
except for [pointwise_relation] which now takes the domain type as an
explicit argument.


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

6 files changed, 48 insertions, 105 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 197786c8b..9909f18ad 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -111,8 +111,7 @@ Section Respecting.
     { morph : A -> B | respectful R R' morph morph }.
   
   Program Instance respecting_equiv [ eqa : Equivalence A R, eqb : Equivalence B R' ] :
-    Equivalence respecting
-    (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+    Equivalence (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
   Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
 
@@ -125,8 +124,8 @@ End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] :
-  Equivalence (A -> B) (pointwise_relation eqB) | 9.
+Program Instance pointwise_equivalence A ((eqb : Equivalence B eqB)) :
+  Equivalence (pointwise_relation A eqB) | 9.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 270b9d8ac..574b0ceb3 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -15,14 +15,13 @@
 
 (* $Id$ *)
 
+Set Manual Implicit Arguments.
+
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
-Set Implicit Arguments.
-Unset Strict Implicit.
-
 (** * Morphisms.
 
    We now turn to the definition of [Morphism] and declare standard instances. 
@@ -32,13 +31,9 @@ Unset Strict Implicit.
    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 :=
+Class Morphism {A} (R : relation A) (m : A) : Prop :=
   respect : R m m.
 
-(** We make the type implicit, it can be infered from the relations. *)
-
-Implicit Arguments Morphism [A].
-
 (** Respectful morphisms. *)
 
 (** The fully dependent version, not used yet. *)
@@ -53,7 +48,7 @@ Definition respectful_hetero
 
 (** The non-dependent version is an instance where we forget dependencies. *)
 
-Definition respectful (A B : Type) 
+Definition respectful {A B : Type}
   (R : relation A) (R' : relation B) : relation (A -> B) :=
   Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
 
@@ -84,11 +79,11 @@ Arguments Scope forall_relation [type_scope type_scope signature_scope].
 
 (** Non-dependent pointwise lifting *)
 
-Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
+Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := 
   Eval compute in forall_relation (B:=λ _, B) (λ _, R).
 
 Lemma pointwise_pointwise A B (R : relation B) : 
-  relation_equivalence (pointwise_relation R) (@eq A ==> R).
+  relation_equivalence (pointwise_relation A R) (@eq A ==> R).
 Proof. intros. split. simpl_relation. firstorder. Qed.
 
 (** We can build a PER on the Coq function space if we have PERs on the domain and
@@ -101,7 +96,7 @@ Hint Unfold Transitive : core.
 Typeclasses Opaque respectful pointwise_relation forall_relation.
 
 Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
-  PER (A -> B) (R ==> R').
+  PER (R ==> R').
 
   Next Obligation.
   Proof with auto.
@@ -162,8 +157,8 @@ Proof. firstorder. Qed.
 Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
 Proof. firstorder. Qed.
 
-Instance pointwise_subrelation [ sub : subrelation A R R' ] :
-  subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
+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. *)
@@ -316,7 +311,7 @@ Qed.
    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 :=
+Class MorphismProxy {A} (R : relation A) (m : A) : Prop :=
   respect_proxy : R m m.
 
 Instance reflexive_morphism_proxy
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index ec62e12ec..3bbd56cfd 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -1,4 +1,3 @@
-(* -*- 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 *)
@@ -32,18 +31,6 @@ Program Instance not_iff_morphism :
 Program Instance and_impl_morphism :
   Morphism (impl ==> impl ==> 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_inverse_impl_iff_morphism :  *)
-(*   Morphism (inverse impl ==> iff ==> inverse impl) and. *)
-
-(* Program Instance and_iff_inverse_impl_morphism :  *)
-(*   Morphism (iff ==> inverse impl ==> inverse impl) and. *)
-
 Program Instance and_iff_morphism : 
   Morphism (iff ==> iff ==> iff) and.
 
@@ -52,18 +39,6 @@ Program Instance and_iff_morphism :
 Program Instance or_impl_morphism : 
   Morphism (impl ==> impl ==> 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_inverse_impl_iff_morphism : *)
-(*   Morphism (inverse impl ==> iff ==> inverse impl) or. *)
-
-(* Program Instance or_iff_inverse_impl_morphism :  *)
-(*   Morphism (iff ==> inverse impl ==> inverse impl) or. *)
-
 Program Instance or_iff_morphism : 
   Morphism (iff ==> iff ==> iff) or.
 
@@ -73,7 +48,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (** Morphisms for quantifiers *)
 
-Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@ex A).
+Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation A iff ==> iff) (@ex A).
 
   Next Obligation.
   Proof.
@@ -87,7 +62,7 @@ Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff =
   Qed.
 
 Program Instance ex_impl_morphism {A : Type} :
-  Morphism (pointwise_relation impl ==> impl) (@ex A).
+  Morphism (pointwise_relation A impl ==> impl) (@ex A).
 
   Next Obligation.
   Proof.
@@ -96,7 +71,7 @@ Program Instance ex_impl_morphism {A : Type} :
   Qed.
 
 Program Instance ex_inverse_impl_morphism {A : Type} : 
-  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
+  Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A).
 
   Next Obligation.
   Proof.
@@ -105,7 +80,7 @@ Program Instance ex_inverse_impl_morphism {A : Type} :
   Qed.
 
 Program Instance all_iff_morphism {A : Type} : 
-  Morphism (pointwise_relation iff ==> iff) (@all A).
+  Morphism (pointwise_relation A iff ==> iff) (@all A).
 
   Next Obligation.
   Proof.
@@ -114,7 +89,7 @@ Program Instance all_iff_morphism {A : Type} :
   Qed.
 
 Program Instance all_impl_morphism {A : Type} : 
-  Morphism (pointwise_relation impl ==> impl) (@all A).
+  Morphism (pointwise_relation A impl ==> impl) (@all A).
   
   Next Obligation.
   Proof.
@@ -123,7 +98,7 @@ Program Instance all_impl_morphism {A : Type} :
   Qed.
 
 Program Instance all_inverse_impl_morphism {A : Type} : 
-  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
+  Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@all A).
   
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 1b3896678..24b8d6364 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -1,4 +1,3 @@
-(* -*- 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 *)
@@ -42,17 +41,14 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed.
 (*    when [R] and [R'] are in [relation_equivalence]. *)
 
 Instance relation_equivalence_pointwise :
-  Morphism (relation_equivalence ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) iff)) id.
+  Morphism (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
 Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed.
 
 Instance subrelation_pointwise :
-  Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
+  Morphism (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
 Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
 
 
 Lemma inverse_pointwise_relation A (R : relation A) : 
-  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
+  relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)).
 Proof. intros. split; firstorder. Qed.
-
-
-
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 7c7362cad..b58998d1f 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -40,19 +40,19 @@ Proof. reflexivity. Qed.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class Reflexive A (R : relation A) :=
+Class Reflexive {A} (R : relation A) :=
   reflexivity : forall x, R x x.
 
-Class Irreflexive A (R : relation A) := 
+Class Irreflexive {A} (R : relation A) := 
   irreflexivity :> Reflexive (complement R).
 
-Class Symmetric A (R : relation A) := 
+Class Symmetric {A} (R : relation A) := 
   symmetry : forall x y, R x y -> R y x.
 
-Class Asymmetric A (R : relation A) := 
+Class Asymmetric {A} (R : relation A) := 
   asymmetry : forall x y, R x y -> R y x -> False.
 
-Class Transitive A (R : relation A) := 
+Class Transitive {A} (R : relation A) := 
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
 Hint Resolve @irreflexivity : ord.
@@ -158,26 +158,26 @@ Program Instance eq_Transitive : Transitive (@eq A).
 
 (** A [PreOrder] is both Reflexive and Transitive. *)
 
-Class PreOrder A (R : relation A) : Prop :=
+Class PreOrder {A} (R : relation A) : Prop :=
   PreOrder_Reflexive :> Reflexive R ;
   PreOrder_Transitive :> Transitive R.
 
 (** A partial equivalence relation is Symmetric and Transitive. *)
 
-Class PER (carrier : Type) (pequiv : relation carrier) : Prop :=
-  PER_Symmetric :> Symmetric pequiv ;
-  PER_Transitive :> Transitive pequiv.
+Class PER {A} (R : relation A) : Prop :=
+  PER_Symmetric :> Symmetric R ;
+  PER_Transitive :> Transitive R.
 
 (** Equivalence relations. *)
 
-Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
-  Equivalence_Reflexive :> Reflexive equiv ;
-  Equivalence_Symmetric :> Symmetric equiv ;
-  Equivalence_Transitive :> Transitive equiv.
+Class Equivalence {A} (R : relation A) : Prop :=
+  Equivalence_Reflexive :> Reflexive R ;
+  Equivalence_Symmetric :> Symmetric R ;
+  Equivalence_Transitive :> Transitive R.
 
 (** An Equivalence is a PER plus reflexivity. *)
 
-Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 :=
+Instance Equivalence_PER [ Equivalence A R ] : PER R | 10 :=
   PER_Symmetric := Equivalence_Symmetric ;
   PER_Transitive := Equivalence_Transitive.
 
@@ -193,17 +193,17 @@ Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} :
    The instance has low priority as it is always applicable 
    if only the type is constrained. *)
 
-Program Instance eq_equivalence : Equivalence A (@eq A) | 10.
+Program Instance eq_equivalence : Equivalence (@eq A) | 10.
 
 (** Logical equivalence [iff] is an equivalence relation. *)
 
-Program Instance iff_equivalence : Equivalence Prop iff.
+Program Instance iff_equivalence : Equivalence iff.
 
 (** We now develop a generalization of results on relations for arbitrary predicates.
    The resulting theory can be applied to homogeneous binary relations but also to
    arbitrary n-ary predicates. *)
 
-Require Import List.
+Require Import Coq.Lists.List.
 
 (* Notation " [ ] " := nil : list_scope. *)
 (* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
@@ -317,7 +317,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
 Program Instance predicate_equivalence_equivalence :
-  Equivalence (predicate l) predicate_equivalence.
+  Equivalence (@predicate_equivalence l).
 
   Next Obligation.
     induction l ; firstorder.
@@ -335,7 +335,7 @@ Program Instance predicate_equivalence_equivalence :
   Qed.
 
 Program Instance predicate_implication_preorder :
-  PreOrder (predicate l) predicate_implication.
+  PreOrder (@predicate_implication l).
 
   Next Obligation.
     induction l ; firstorder.
@@ -367,10 +367,10 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
 Instance relation_equivalence_equivalence (A : Type) :
-  Equivalence (relation A) relation_equivalence.
+  Equivalence (@relation_equivalence A).
 Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
 
-Instance relation_implication_preorder : PreOrder (relation A) subrelation.
+Instance relation_implication_preorder : PreOrder (@subrelation A).
 Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
 
 (** *** Partial Order.
@@ -378,7 +378,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
    We give an equivalent definition, up-to an equivalence relation 
    on the carrier. *)
 
-Class [ equ : Equivalence A eqA, preo : PreOrder A R ] => PartialOrder :=
+Class PartialOrder ((equ : Equivalence A eqA)) ((preo : PreOrder A R)) :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index f2ce4fe12..46d26553e 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -29,7 +28,7 @@ Require Import Coq.Classes.Functions.
 
 Class Setoid A :=
   equiv : relation A ;
-  setoid_equiv :> Equivalence A equiv.
+  setoid_equiv :> Equivalence equiv.
 
 Typeclasses unfold equiv.
 
@@ -135,11 +134,6 @@ Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morph
 
 Existing Instance setoid_partial_app_morphism.
 
-Definition type_eq : relation Type :=
-  fun x y => x = y.
-
-Program Instance type_equivalence : Equivalence Type type_eq.
-
 Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
 Ltac obligation_tactic ::= morphism_tac.
@@ -150,27 +144,11 @@ Ltac obligation_tactic ::= morphism_tac.
 
 Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) 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 ] =>  *)
-(*   compose_morphism : ? Morphism (compose_respect R R') (g o f). *)
-
-(* Next Obligation. *)
-(* Proof. *)
-(*   apply (respect (m0:=mg)). *)
-(*   apply (respect (m0:=mf)). *)
-(*   assumption. *)
-(* Qed. *)
-
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
-Class PartialSetoid (carrier : Type) :=
-  pequiv : relation carrier ;
-  pequiv_prf :> PER carrier pequiv.
+Class PartialSetoid (A : Type) :=
+  pequiv : relation A ;
+  pequiv_prf :> PER pequiv.
 
 (** Overloaded notation for partial setoid equivalence. *)