Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve

des théorèmes prouvés par récursion ou corécursion mutuelle.

Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.



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

2 files changed, 94 insertions, 0 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 23c19d60b6..28cb402f35 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1568,6 +1568,30 @@ All these commands are synonymous of \texttt{Theorem}
 % %within the section will be replaced by the proof of  {\ident}.
 % Same as {\tt Remark} except
 % that the innermost section name is dropped from the full name.
+\item {\tt Theorem \nelist{{\ident} : {\type}}{with}.}
+
+This command is useful for theorems that are proved by simultaneous
+induction over a mutually inductive assumption, or that state mutually
+dependent statements in some mutual coinductive type. It is equivalent
+to {\tt Fixpoint} (see Section~\ref{Fixpoint}) or {\tt CoFixpoint}
+(see Section~\ref{CoFixpoint}) but using tactics to build the proof of
+the statements (or the body of the specification, depending on the
+point of view). The inductive or coinductive types on which the
+induction or coinduction has to be done is assumed to be non ambiguous
+and is guessed by the system. 
+
+Like in a {\tt Fixpoint} or {\tt CoFixpoint} definition, the induction
+hypotheses have to be used on {\em structurally smaller} arguments
+(for a {\tt Fixpoint}) or be {\em guarded by a constructor} (for a {\tt
+  CoFixpoint}).  The verification that recursive proof arguments are
+correct is done only at the time of registering the lemma in the
+environment. To know if the use of induction hypotheses is correct at
+some time of the interactive development of a proof, use the command
+{\tt Guarded} (see Section~\ref{Guarded}).
+
+The command can be used also with {\tt Lemma},
+{\tt Remark}, etc. instead of {\tt Theorem}.
+
 \item {\tt Definition {\ident} : {\type}.} \\
 Allow to define a term of type {\type} using the proof editing mode. It
 behaves as {\tt Theorem} but is intended for the interactive
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1ba08344cb..cd32fb35af 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -806,6 +806,76 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
+\subsection{\tt fix {\ident} {\num}
+\tacindex{fix}
+\label{tactic:fix}}
+
+This tactic is a primitive tactic to start a proof by induction. In
+general, it is easier to rely on higher-level induction tactics such
+as the ones described in Section~\ref{Tac-induction}.
+
+In the syntax of the tactic, the identifier {\ident} is the name given
+to the induction hypothesis. The natural number {\num} tells on which
+premise of the current goal the induction acts, starting
+from 1 and counting both dependent and non dependent
+products. Especially, the current lemma must be composed of at least
+{\num} products.
+
+Like in a {\tt fix} expression, the induction
+hypotheses have to be used on structurally smaller arguments.
+The verification that inductive proof arguments are correct is done
+only at the time of registering the lemma in the environment. To know
+if the use of induction hypotheses is correct at some
+time of the interactive development of a proof, use the command {\tt
+  Guarded} (see Section~\ref{Guarded}).
+
+\begin{Variants}
+  \item {\tt fix} {\ident}$_1$ {\num} {\tt with (} {\ident}$_2$
+    \nelist{{\binder}$_{2}$}{} \zeroone{{\tt \{ struct {\ident$'_2$}
+      \}}} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt (} {\ident}$_1$
+    \nelist{{\binder}$_n$}{} \zeroone{{\tt \{ struct {\ident$'_n$} \}}}
+           {\tt :} {\type}$_n$ {\tt )}
+
+This starts a proof by mutual induction. The statements to be
+simultaneously proved are respectively {\tt forall}
+  \nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$.  The identifiers
+{\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the induction
+hypotheses. The identifiers {\ident}$'_2$ {\ldots} {\ident}$'_n$ are the
+respective names of the premises on which the induction is performed
+in the statements to be simultaneously proved (if not given, the
+system tries to guess itself what they are).
+
+\end{Variants}
+
+\subsection{\tt cofix {\ident}
+\tacindex{cofix}
+\label{tactic:cofix}}
+
+This tactic starts a proof by coinduction. The identifier {\ident} is
+the name given to the coinduction hypothesis.  Like in a {\tt cofix}
+expression, the use of induction hypotheses have to guarded by a
+constructor.  The verification that the use of coinductive hypotheses
+is correct is done only at the time of registering the lemma in the
+environment. To know if the use of coinduction hypotheses is correct
+at some time of the interactive development of a proof, use the
+command {\tt Guarded} (see Section~\ref{Guarded}).
+
+
+\begin{Variants}
+  \item {\tt cofix} {\ident}$_1$ {\tt with (} {\ident}$_2$
+    \nelist{{\binder}$_2$}{} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt
+      (} {\ident}$_1$ \nelist{{\binder}$_1$}{} {\tt :} {\type}$_n$
+           {\tt )}
+
+This starts a proof by mutual coinduction. The statements to be
+simultaneously proved are respectively {\tt forall}
+\nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$. The identifiers
+    {\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the
+    coinduction hypotheses.
+
+\end{Variants}
 
 \section{Negation and contradiction}