A pass on documentation:

- Don't use [Eq] and [eq] in the typeclasses documentation, as advised by Assia.
- Explain the importance of [Transparent/Opaque] for typeclasses and
[setoid_rewrite].
- Fix and rework doc on [dependent induction].
- A word on [Global] instance.


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

4 files changed, 151 insertions, 103 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 444796647..2db0ab286 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -56,18 +56,18 @@ is given by $\ident$ and type is an instantiation of the record type.
 We'll use the following example class in the rest of the chapter:
 
 \begin{coq_example*}
-Class Eq (A : Type) :=
-  eq : A -> A -> bool ;
-  eq_leibniz : forall x y, eq x y = true -> x = y.
+Class EqDec (A : Type) :=
+  eqb : A -> A -> bool ;
+  eqb_leibniz : forall x y, eqb x y = true -> x = y.
 \end{coq_example*}
 
 This class implements a boolean equality test which is compatible with
 leibniz equality on some type. An example implementation is:
 
 \begin{coq_example*}
-Instance unit_Eq : Eq unit :=
-  eq x y := true ;
-  eq_leibniz x y H := 
+Instance unit_EqDec : EqDec unit :=
+  eqb x y := true ;
+  eqb_leibniz x y H := 
     match x, y return x = y with tt, tt => refl_equal tt end.
 \end{coq_example*}
 
@@ -76,14 +76,14 @@ declaration, Coq enters the proof-mode and the user is asked to build
 inhabitants of the remaining fields, e.g.:
 
 \begin{coq_example*}
-Instance eq_bool : Eq bool :=
-  eq x y := if x then y else negb y.
+Instance eq_bool : EqDec bool :=
+  eqb x y := if x then y else negb y.
 \end{coq_example*}
 
 \begin{coq_example}
-  Proof. intros x y H.
-  destruct x ; destruct y ; try discriminate ; reflexivity. 
-  Defined.
+Proof. intros x y H.
+  destruct x ; destruct y ; (discriminate || reflexivity). 
+Defined.
 \end{coq_example}
 
 One has to take care that the transparency of every field is determined
@@ -95,17 +95,17 @@ richer facilities for dealing with obligations.
 
 Once a type class is declared, one can use it in class binders:
 \begin{coq_example}
-  Definition neq {A : Type} [ Eq A ] (x y : A) := negb (eq x y).
+  Definition neqb {A : Type} [ EqDec A ] (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 When one calls a class method, a constraint is generated that is
 satisfied only in contexts where the appropriate instances can be
-found. In the example above, a constraint \texttt{Eq A} is generated and
-satisfied by \texttt{[ Eq A ]}. In case no satisfying constraint can be
+found. In the example above, a constraint \texttt{EqDec A} is generated and
+satisfied by \texttt{[ EqDec A ]}. In case no satisfying constraint can be
 found, an error is raised:
 
 \begin{coq_example}
-  Definition neq' (A : Type) (x y : A) := negb (eq x y).
+  Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 The algorithm used to solve constraints is a variant of the eauto tactic
@@ -115,7 +115,7 @@ local hypotheses as well as declared lemmas in the
 written:
 
 \begin{coq_example}
-  Definition neq' (A : Type) (eqa : Eq A) (x y : A) := negb (eq x y).
+  Definition neqb' (A : Type) (eqa : EqDec A) (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 However, the bracketed binders should be used instead as they have
@@ -136,17 +136,18 @@ particular support for type classes:
 Implicit quantification is an automatic elaboration of a statement with
 free variables into a closed statement where these variables are
 quantified explicitely. Implicit generalization is done only inside
-bracketed binders.
+bracketed binders and the codomain of \texttt{Instance} declarations.
 
 Following the previous example, one can write:
 \begin{coq_example}
-  Definition neq_impl [ eqa : Eq A ] (x y : A) := negb (eq x y).
+  Definition neqb_impl [ eqa : EqDec A ] (x y : A) := negb (eqb x y).
 \end{coq_example}
 
 Here \texttt{A} is implicitely generalized, and the resulting function
 is equivalent to the one above. One must be careful that \emph{all} the
 free variables are generalized, which may result in confusing errors in
-case of typos. 
+case of typos. In such cases, the context will probably contain some
+unexpected generalized variable.
 
 The bracket binders [ ] are a shorthand for double-braces \{\{ \}\} binders
 which declare the variables directly bound inside them as implicit
@@ -159,12 +160,12 @@ are always set as maximally-inserted implicit arguments.
 One can declare parameterized instances as in \Haskell simply by giving
 the constraints as a binding context before the instance, e.g.:
 
-\begin{coq_example*}
-Instance prod_eq [ eqa : Eq A, eqb : Eq B ] : Eq (A * B) :=
-  eq x y := match x, y with
-  | (la, ra), (lb, rb) => andb (eq la lb) (eq ra rb)
+\begin{coq_example}
+Instance prod_eqb [ EA : EqDec A, EB : EqDec B ] : EqDec (A * B) :=
+  eqb x y := match x, y with
+  | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
   end.
-\end{coq_example*}
+\end{coq_example}
 \begin{coq_eval}
 Admitted.
 \end{coq_eval}
@@ -180,21 +181,23 @@ hierarchy of classes and superclasses. In the same way, we give the
 superclasses as a binding context:
 
 \begin{coq_example}
-Class (( Eq A )) => Ord :=
+Class (( E : EqDec A )) => Ord :=
   le : A -> A -> bool.
 \end{coq_example}
 
 This declaration means that any instance of the \texttt{Ord} class must
-have an instance of \texttt{Eq}. The parameters of the subclass contain
+have an instance of \texttt{EqDec}. The parameters of the subclass contain
 at least all the parameters of its superclasses in their order of
-appearance (here \texttt{A} is the only one). 
+appearance (here \texttt{A} is the only one). One should always give a
+name to each superclass, but one will be generated automatically if it
+is missing.
 
 Internally, \texttt{Ord} will become a record type with two parameters:
-a type \texttt{A} and an object of type \texttt{Eq A}. However, one can
+a type \texttt{A} and an \texttt{E} of type \texttt{EqDec A}. However, one can
 still use it as if it had a single parameter inside class binders: the
 generalization of superclasses will be done automatically. 
 \begin{coq_example}
-Definition le_eq [ Ord A ] (x y : A) :=
+Definition le_eqb [ Ord A ] (x y : A) :=
   andb (le x y) (le y x).
 \end{coq_example}
 
@@ -203,10 +206,10 @@ explicitely the superclasses. It is is possible to do it directly in regular
 binders, and using the \texttt{!} modifier in class binders. For
 example:
 
-\begin{coq_example*}
-Definition lt [ eqa : Eq A, ! Ord eqa ] (x y : A) :=
-  andb (le x y) (neq x y).
-\end{coq_example*}
+\begin{coq_example}
+Definition lt [ eqa : EqDec A, ! Ord eqa ] (x y : A) :=
+  andb (le x y) (neqb x y).
+\end{coq_example}
 
 The \texttt{!} modifier switches the way a binder is parsed back to the
 regular interpretation of Coq. In particular, it uses the implicit
@@ -215,7 +218,7 @@ arguments mechanism if available, as shown in the example.
 One can notice that superclasses are in fact equivalent to parameters of
 the class, hence the above declaration is the same as:
 \begin{coq_example*}
-Class Ord ((Eq A)) := le : A -> A -> bool.
+Class Ord ((EqDec A)) := le : A -> A -> bool.
 \end{coq_example*}
 
 \subsection{Substructures}
@@ -280,6 +283,16 @@ field of the class. Missing fields must be filled in interactive proof mode.
 An arbitrary context of the form {\tt \binder$_1$ \ldots \binder$_n$}
 can be put after the name of the instance and before the colon to declare a parameterized instance.
 
+\begin{Variants}
+\item {\tt Global Instance} One can use the \texttt{Global} modifier on
+  instances declared in a section so that their generalization is automatically
+  redeclared after the section is closed.
+
+\item {\tt Program Instance} \comindex{Program Instance}
+  Switches the type-checking to \Program~(chapter \ref{Program})
+  and uses the obligation mechanism to manage missing fields.
+\end{Variants}
+
 Besides the {\tt Class} and {\tt Instance} vernacular commands, there
 are a few other commands related to type classes.
 
@@ -293,15 +306,23 @@ instances at the end of sections, or declaring structure projections as
 instances. This is almost equivalent to {\tt Hint Resolve {\ident} :
   typeclass\_instances}.
 
-\subsection{\tt Typeclasses unfold {\ident$_1$ \ldots \ident$_n$}}
-\comindex{Typeclasses unfold}
-\label{TypeclassesUnfold}
+\subsection{\tt Typeclasses Transparent, Opaque {\ident$_1$ \ldots \ident$_n$}}
+\comindex{Typeclasses Transparent}
+\comindex{Typeclasses Opaque}
+\label{TypeclassesTransparency}
+
+This commands defines the transparency of {\ident$_1$ \ldots \ident$_n$} 
+during type class resolution. It is useful when some constants prevent some
+unifications and make resolution fail. It is also useful to declare
+constants which should never be unfolded during proof-search, like
+fixpoints or anything which does not look like an abbreviation. This can
+additionally speed up proof search as the typeclass map can be indexed
+by such rigid constants (see \ref{HintTransparency}).
+By default, all constants and local variables are considered transparent.
+One should take care not to make opaque any constant that is used to
+abbreviate a type, like {\tt relation A := A -> A -> Prop}.
 
-This commands declares {\ident} as an unfoldable constant during type
-class resolution. It is useful when some constants prevent some
-unifications and make resolution fail. It happens in particular when constants are
-used to abbreviate types, like {\tt relation A := A -> A -> Prop}.
-This is equivalent to {\tt Hint Unfold {\ident} : typeclass\_instances}.
+This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.
 
 \subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]}
 \comindex{Typeclasses eauto}
@@ -320,5 +341,5 @@ based on a variant of eauto. The flags semantics are:
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% compile-command: "make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
+%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
 %%% End: 
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 3580684a7..dfcebf186 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -1,7 +1,3 @@
-\def\Program{\textsc{Program}}
-\def\Russell{\textsc{Russell}}
-\def\PVS{\textsc{PVS}}
-
 \achapter{\Program{}}
 \label{Program}
 \aauthor{Matthieu Sozeau}
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index c5b914f97..5da43ec0b 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -593,8 +593,8 @@ Reset Initial.
 
 The tactics \depind and \depdestr are another solution for inverting
 inductive predicate instances and potentially doing induction at the
-same time. It is based on the Basic Elim tactic of Conor McBride which
-work by abstracting each argument of an inductive instance by a variable
+same time. It is based on the \texttt{BasicElim} tactic of Conor McBride which
+works by abstracting each argument of an inductive instance by a variable
 and constraining it by equalities afterwards. This way, the usual 
 {\tt induction} and {\tt destruct} tactics can be applied to the
 abstracted instance and after simplification of the equalities we get
@@ -608,6 +608,9 @@ For example, revisiting the first example of the inversion documentation above:
 \begin{coq_example*}
 Require Import Coq.Logic.JMeq.
 \end{coq_example*}
+\begin{coq_eval}
+Require Import Coq.Program.Equality.
+\end{coq_eval}
 
 \begin{coq_eval}
 Inductive Le : nat -> nat -> Set :=
@@ -618,7 +621,7 @@ Variable Q : forall n m:nat, Le n m -> Prop.
 \end{coq_eval}
 
 \begin{coq_example*}
-Lemma ex : forall n m:nat, Le (S n) m -> P n m.
+Goal forall n m:nat, Le (S n) m -> P n m.
 intros n m H.
 \end{coq_example*}
 \begin{coq_example}
@@ -627,45 +630,61 @@ generalize_eqs H.
 
 The index {\tt S n} gets abstracted by a variable here, but a
 corresponding equality is added under the abstract instance so that no
-information is actually lost. The goal is now ammenable to do induction
-or case analysis. Note that the abstract instance is also related to the
-original one using an heterogeneous equality that will become a regular
-one once the equalities are substituted. In the non-dependent case where
-the hypothesis does not appear in the goal, this equality is actually
-not needed and we can make it disappear, along with the original
-hypothesis:
+information is actually lost. The goal is now almost ammenable to do induction
+or case analysis. One should indeed first move {\tt n} into the goal to
+strengthen it before doing induction, or {\tt n} will be fixed in
+the inductive hypotheses (this does not matter for case analysis). 
+As a rule of thumb, all the variables that appear inside constructors in
+the indices of the hypothesis should be generalized. This is exactly
+what the \texttt{generalize\_eqs\_vars} variant does:
+
+\begin{coq_eval} 
+Undo 1.
+\end{coq_eval}
+\begin{coq_example}
+generalize_eqs_vars H.
+induction H.
+\end{coq_example}
+
+As the hypothesis itself did not appear in the goal, we did not need to
+use an heterogeneous equality to relate the new hypothesis to the old
+one (which just disappeared here). However, the tactic works just a well
+in this case, e.g.:
+
+\begin{coq_eval}
+Admitted.
+\end{coq_eval}
 
 \begin{coq_example}
-intros gen_x gen_H _ ; clear H.
+Goal forall n m (p : Le (S n) m), Q (S n) m p.
+intros n m p ; generalize_eqs_vars p.
 \end{coq_example}
 
-One drawback is that in the branches one will have to
+One drawback of this approach is that in the branches one will have to
 substitute the equalities back into the instance to get the right
 assumptions. Sometimes injection of constructors will also be needed to
 recover the needed equalities. Also, some subgoals should be directly
 solved because of inconsistent contexts arising from the constraints on 
  indices. The nice thing is that we can make a tactic based on
-discriminate and injection to automatically do such simplifications in
-any context. This is what the {\tt simpl\_depind} tactic from
-{\tt Coq.Program.Equality} does. For example, compare:
-\begin{coq_example*}
-Require Import Coq.Program.Equality.
-\end{coq_example*}
-\begin{coq_example}
-destruct gen_H.
-\end{coq_example}
-and
-\begin{coq_eval}
-Undo.
-\end{coq_eval}
+discriminate, injection and variants of substitution to automatically 
+do such simplifications (which may involve the K axiom). 
+This is what the {\tt simplify\_dep\_elim} tactic from
+{\tt Coq.Program.Equality} does. For example, we might simplify the
+previous goals considerably:
+% \begin{coq_eval} 
+% Abort.
+% Goal forall n m:nat, Le (S n) m -> P n m.
+% intros n m H ; generalize_eqs_vars H.
+% \end{coq_eval}
+
 \begin{coq_example}
-destruct gen_H ; intros ; simpl_depind.
+induction p ; simplify_dep_elim.
 \end{coq_example}
 
 The higher-order tactic {\tt do\_depind} defined in {\tt
   Coq.Program.Equality} takes a tactic and combines the
-building blocks we've seen with it: generalizing by equalities, cleaning
-the goal if it's not dependent, calling the given tactic with the
+building blocks we've seen with it: generalizing by equalities 
+calling the given tactic with the
 generalized induction hypothesis as argument and cleaning the subgoals
 with respect to equalities. Its most important instantiations are
 \depind and \depdestr that do induction or simply case analysis on the
@@ -715,9 +734,11 @@ generalized hypothesis only when it has a type of the form {\tt vector
  (S n)}, that is only in the second case of the {\tt destruct}. The
 first one is dismissed because {\tt S n <> 0}.
 
-This technique also works with {\tt induction} on inductive
-predicates. We will now develop an example application to the
-theory of simply-typed lambda-calculus in a dependently-typed style:
+\subsection{A larger example}
+
+Let's see how the technique works with {\tt induction} on inductive
+predicates on a real example. We will develop an example application to the
+theory of simply-typed lambda-calculus formalized in a dependently-typed style:
 
 \begin{coq_example*}
 Inductive type : Type :=
@@ -797,9 +818,10 @@ Proof with simpl in * ; simpl_depind ; auto.
 
 This call to \depind has an additional arguments which is a list of
 variables appearing in the instance that should be generalized in the
-goal, so that they can vary in the induction hypotheses. Generally, all
-variables appearing inside constructors of the instantiated hypothesis
-should be generalized. 
+goal, so that they can vary in the induction hypotheses. By default, all
+variables appearing inside constructors (except in a parameter position)
+of the instantiated hypothesis will be generalized automatically but
+one can always give the list explicitely.
 
 \begin{coq_example}
   Show.
@@ -808,9 +830,9 @@ should be generalized.
 The {\tt simpl\_depind} tactic includes an automatic tactic that tries
 to simplify equalities appearing at the beginning of induction
 hypotheses, generally using trivial applications of
-reflexiviy. In some cases though, one must help the automation by giving
-some arguments first, using the {\tt narrow} tactic from  
-{\tt Coq.Init.Tactics}.
+reflexiviy. In cases where the equality is not between constructor
+forms though, one must help the automation by giving
+some arguments, using the {\tt specialize} tactic.
 
 \begin{coq_example*}
 destruct D... apply weak ; apply ax. apply ax.
@@ -820,12 +842,16 @@ destruct D...
 Show.
 \end{coq_example}
 \begin{coq_example}
-  narrow IHterm with G empty.
+  specialize (IHterm G empty).
 \end{coq_example}
 
 Then the automation can find that the needed equality {\tt G = G} to
 narrow the induction hypothesis further. This concludes our example.
 
+\begin{coq_example}
+  simpl_depind.
+\end{coq_example}
+
 \SeeAlso The induction \ref{elim}, case \ref{case} and inversion \ref{inversion} tactics.
 
 \section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 76ce6ca4b..74a38d4aa 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -324,8 +324,10 @@ instance mechanism. The behavior on section close is to generalize
 the instances by the variables of the section (and possibly hypotheses
 used in the proofs of instance declarations) but not to export them in
 the rest of the development for proof search. One can use the
-\texttt{Existing Instance} command to do so, using the name of the
-declared morphism suffixed by \texttt{\_Morphism}.
+\texttt{Existing Instance} command to do so outside the section,
+using the name of the declared morphism suffixed by \texttt{\_Morphism}, 
+or use the \texttt{Global} modifier for the corresponding class instance
+declaration (see \S\ref{setoid:first-class}) at definition time.
 When loading a compiled file or importing a module,
 all the declarations of this module will be loaded.
 
@@ -432,6 +434,7 @@ constraints generated by a rewrite and will not try to find \emph{all}
 possible solutions to warn the user about.
 
 \asection{First class setoids and morphisms}
+\label{setoid:first-class}
 
 The implementation is based on a first-class representation of
 properties of relations and morphisms as type classes. That is, 
@@ -453,21 +456,22 @@ is equivalent to an instance declaration:
 
 \begin{quote}
   \texttt{Instance} ($x_1 : T_1$) \ldots ($x_n : T_k$) \texttt{=>}
-  \textit{id} : \texttt{Equivalence} \textit{(A $t_1$ \ldots $t_n$) (Aeq
+  \textit{id} : \texttt{@Equivalence} \textit{(A $t_1$ \ldots $t_n$) (Aeq
     $t'_1$ \ldots $t'_m$)} :=\\
-  ~\zeroone{\texttt{equivalence\_reflexive :=} \textit{refl}}\\
-  ~\zeroone{\texttt{equivalence\_symmetric :=} \textit{sym}}\\
-  ~\zeroone{\texttt{equivalence\_transitive :=} \textit{trans}}.
+  ~\zeroone{\texttt{Equivalence\_Reflexive :=} \textit{refl}}\\
+  ~\zeroone{\texttt{Equivalence\_Symmetric :=} \textit{sym}}\\
+  ~\zeroone{\texttt{Equivalence\_Transitive :=} \textit{trans}}.
 \end{quote}
 
 The declaration itself amounts to the definition of an object of the
-record type \texttt{Equivalence} and a hint added to the
-\texttt{typeclass\_instances} hint database. 
+record type \texttt{Coq.Classes.RelationClasses.Equivalence} and a
+hint added to the \texttt{typeclass\_instances} hint database. 
 Morphism declarations are also instances of a type class defined in
 \texttt{Classes.Morphisms}.
-See the theories files in \texttt{Classes} for further explanations. 
+See the documentation on type classes \ref{typeclasses} and 
+the theories files in \texttt{Classes} for further explanations. 
 
-One can then inform the rewrite tactic about morphisms and relations just by
+One can inform the rewrite tactic about morphisms and relations just by
 using the typeclass metchanism to declare them using \texttt{Instance}
 and \texttt{Context} vernacular commands.
 Any object of type \texttt{Morphism} in the local context will also be
@@ -624,7 +628,7 @@ Require Import Setoid.
 \end{coq_eval}
 \begin{coq_example}
 Instance all_iff_morphism (A : Type) :
-  Morphism (pointwise_relation iff ==> iff) (@all A).
+  Morphism (pointwise_relation A iff ==> iff) (@all A).
 Proof. simpl_relation. 
 \end{coq_example}
 \begin{coq_eval}
@@ -637,9 +641,9 @@ declared such a morphism, it will be used by the setoid rewriting tactic
 each time we try to rewrite under a binder. Indeed, when rewriting under
 a lambda, binding variable $x$, say from $P~x$ to $Q~x$ using the
 relation \texttt{iff}, the tactic will generate a proof of
-\verb|pointwise_relation iff (fun x => P x) (fun x => Q x)| 
+\verb|pointwise_relation A iff (fun x => P x) (fun x => Q x)| 
 from the proof of \verb|iff (P x) (Q x)| and a
-constraint of the form \verb|Morphism (pointwise_relation iff ==> ?) m|
+constraint of the form \verb|Morphism (pointwise_relation A iff ==> ?) m|
 will be generated for the surrounding morphism \texttt{m}. 
 
 Hence, one can add higher-order combinators as morphisms by providing
@@ -696,11 +700,12 @@ prime example of a completely user-space extension of the algorithm.
 
 \asection{Constant unfolding}
 
-The resolution tactic is based on type classes and regards user-defined 
-constants as opaque by default to avoid unwanted unfoldings. This may also
-prevent some desirable unifications, so the command \texttt{Typeclasses
-  unfold} (see \S \ref{TypeclassesUnfold}) can be used to declare a constant as unfoldable
-during resolution.
+The resolution tactic is based on type classes and hence regards user-defined 
+constants as transparent by default. This may slow down the resolution
+due to a lot of unifications (all the declared \texttt{Morphism}
+instances are tried at each node of the search tree).
+To speed it up, declare your constant as rigid for proof search
+using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparency}).
 
 %%% Local Variables: 
 %%% mode: latex