modif generales claude

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

1 files changed, 550 insertions, 124 deletions

diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index a252a1fd9..3e3a93e7f 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -45,6 +45,7 @@ side, they are used without the question mark.
 The main entry of the grammar is {\tacexpr}. This language is used in
 proof mode but it can also be used in toplevel definitions as shown in
 table~\ref{ltactop}.
+
 \begin{Remarks}
 \item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt
     ;} \dots'' are associative. 
@@ -68,41 +69,40 @@ is understood as
 \end{Remarks}
 
 
-\begin{table}[htbp]
-\noindent{}\framebox[6in][l]
-{\parbox{6in}
-{\begin{center}
+\begin{figure}[htbp]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
 \begin{tabular}{lcl}
-{\tacexpr} & \cn{}::= &
+{\tacexpr} & ::= &
            {\tacexpr} {\tt ;} {\tacexpr}\\
-& \cn{}| & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
-& \cn{}| & {\tacexprpref}\\
+& | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
+& | & {\tacexprpref}\\
 \\
-{\tacexprpref} & \cn{}::= &
+{\tacexprpref} & ::= &
            {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
-& \cn{}| & {\tt info} {\tacexprpref}\\
-& \cn{}| & {\tt progress} {\tacexprpref}\\
-& \cn{}| & {\tt repeat} {\tacexprpref}\\
-& \cn{}| & {\tt try} {\tacexprpref}\\
-& \cn{}| & {\tacexprinf} \\
+& | & {\tt info} {\tacexprpref}\\
+& | & {\tt progress} {\tacexprpref}\\
+& | & {\tt repeat} {\tacexprpref}\\
+& | & {\tt try} {\tacexprpref}\\
+& | & {\tacexprinf} \\
 \\
-{\tacexprinf} & \cn{}::= &
+{\tacexprinf} & ::= &
            {\tacexprlow} {\tt ||} {\tacexprpref}\\
-& \cn{}| & {\tacexprlow}\\
+& | & {\tacexprlow}\\
 \\
-{\tacexprlow} & \cn{}::= &
+{\tacexprlow} & ::= &
 {\tt fun} \nelist{\name}{} {\tt =>} {\atom}\\
-& \cn{}| &
+& | &
 {\tt let} \nelist{\letclause}{\tt with} {\tt in}
 {\atom}\\
-& \cn{}| &
+& | &
 {\tt let rec} \nelist{\recclause}{\tt with} {\tt in}
 {\tacexpr}\\
-& \cn{}| &
+& | &
 {\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
-& \cn{}| &
+& | &
 {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
-& \cn{}| &
+& | &
 {\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
 & \cn{}| & {\tt abstract} {\atom}\\
 & \cn{}| & {\tt abstract} {\atom} {\tt using} {\ident} \\
@@ -119,22 +119,22 @@ is understood as
 & \cn{}| & {\qualid} \nelist{\tacarg}{}\\
 & \cn{}| & {\atom}\\
 \\
-{\atom} & \cn{}::= &
+{\atom} & ::= &
            {\qualid} \\
-& \cn{}| & ()\\
-& \cn{}| & {\tt (} {\tacexpr} {\tt )}\\
+& | & ()\\
+& | & {\tt (} {\tacexpr} {\tt )}\\
 \end{tabular}
-\end{center}}}
+\end{minipage}}
+\end{center}
 \caption{Syntax of the tactic language}
 \label{ltac}
-\end{table}
+\end{figure}
 
 
 
-\begin{table}[htbp]
-\noindent{}\framebox[6in][l]
-{\parbox{6in}
-{\begin{center}
+\begin{figure}[htbp]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
 \begin{tabular}{lcl}
 \tacarg & ::= & 
         {\qualid}\\
@@ -158,24 +158,25 @@ is understood as
 & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt \_ =>} {\tacexpr}\\
 \end{tabular}
-\end{center}}}
+\end{minipage}}
+\end{center}
 \caption{Syntax of the tactic language (continued)}
 \label{ltac_aux}
-\end{table}
+\end{figure}
 
-\begin{table}[ht]
-\noindent{}\framebox[6in][l]
-{\parbox{6in}
-{\begin{center}
+\begin{figure}[ht]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
 \begin{tabular}{lcl}
 \nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
 \nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
 \end{tabular}
-\end{center}}}
+\end{minipage}}
+\end{center}
 \caption{Tactic toplevel definitions}
 \label{ltactop}
-\end{table}
+\end{figure}
 
 
 %%
@@ -203,7 +204,7 @@ of Ltac.
 %% Values are given by table~\ref{ltacval}. All these values are tactic values,
 %% i.e. to be applied to a goal, except {\tt Fun}, {\tt Rec} and $arg$ values.
 
-%% \begin{table}[ht]
+%% \begin{figure}[ht]
 %% \noindent{}\framebox[6in][l]
 %% {\parbox{6in}
 %% {\begin{center}
@@ -236,7 +237,7 @@ of Ltac.
 %% \end{center}}}
 %% \caption{Values of ${\cal L}_{tac}$}
 %% \label{ltacval}
-%% \end{table}
+%% \end{figure}
 
 %% \subsection{Evaluation}
 
@@ -245,25 +246,27 @@ of Ltac.
 \index{;@{\tt ;}}
 \index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
 
-A sequence is an expression of the following form:
-\begin{center}
+\begin{tabbing}
 {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
-\end{center}
+\end{tabbing}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied
 and $v_2$ is applied to every subgoal generated by the application of
 $v_1$. Sequence is left associating.
 
 \subsubsection{General sequence}
+
+\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}
 \tacindex{; [ | ]}
 \index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
 \index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
-We can generalize the previous sequence operator by:
-\begin{center}
+
+We can generalize the previous sequence operator as
+\begin{tabbing}
 {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
 {\tacexpr}$_n$ {\tt ]}
-\end{center}
+\end{tabbing}
 {\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is
 applied and $v_i$ is applied to the $i$-th generated subgoal by the
 application of $v_0$, for $=1,...,n$. It fails if the application of
@@ -274,9 +277,9 @@ $v_0$ does not generate exactly $n$ subgoals.
 \index{Tacticals!do@{\tt do}}
 
 There is a for loop that repeats a tactic {\num} times:
-\begin{center}
+\begin{tabbing}
 {\tt do} {\num} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied {\num} times. Supposing ${\num}>1$, after the first
 application of $v$, $v$ is applied, at least once, to the generated
@@ -288,9 +291,9 @@ the {\num} applications have been completed.
 \index{Tacticals!repeat@{\tt repeat}}
 
 We have a repeat loop with:
-\begin{center}
+\begin{tabbing}
 {\tt repeat} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied until it fails. Supposing $n>1$, after the first application
 of $v$, $v$ is applied, at least once, to the generated subgoals and
@@ -302,9 +305,9 @@ fails.
 \index{Tacticals!try@{\tt try}}
 
 We can catch the tactic errors with:
-\begin{center}
+\begin{tabbing}
 {\tt try} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ fails, it catches the error and
 leaves the goal unchanged. If the level of the exception is positive,
@@ -314,9 +317,9 @@ then the exception is re-raised with its level decremented.
 \tacindex{progress}
 
 We can check if a tactic made progress with:
-\begin{center}
+\begin{tabbing}
 {\tt progress} {\tacexpr}
-\end{center}
+\end{tabbing}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ produced one subgoal equal to the
 initial goal (up to syntactical equality), then an error of level 0 is
@@ -324,15 +327,14 @@ raised.
 
 \ErrMsg \errindex{Failed to progress}
 
-
 \subsubsection{Branching}
 \tacindex{||}
 \index{Tacticals!orelse@{\tt ||}}
 
 We can easily branch with the following structure:
-\begin{center}
+\begin{tabbing}
 {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
-\end{center}
+\end{tabbing}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if
 it fails then $v_2$ is applied. Branching is left associating.
@@ -343,9 +345,9 @@ it fails then $v_2$ is applied. Branching is left associating.
 
 We may consider the first tactic to work (i.e. which does not fail) among a
 panel of tactics:
-\begin{center}
+\begin{tabbing}
 {\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
-\end{center}
+\end{tabbing}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it
 tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
@@ -358,9 +360,9 @@ tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
 
 We may consider the first to solve (i.e. which generates no subgoal) among a
 panel of tactics:
-\begin{center}
+\begin{tabbing}
 {\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
-\end{center}
+\end{tabbing}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it
 tries to apply $v_2$ and so on. It fails if there is no solving tactic.
@@ -373,11 +375,12 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.
 
 The constant {\tt idtac} is the identity tactic: it leaves any goal
 unchanged but it appears in the proof script.
-\begin{center}
+\begin{tabbing}
 {\tt idtac} and {\tt idtac "message"}
-\end{center}
+\end{tabbing}
 The latter variant prints the string on the standard output.
 
+
 \subsubsection{Failing}
 \tacindex{fail}
 \index{Tacticals!fail@{\tt fail}}
@@ -385,9 +388,9 @@ The latter variant prints the string on the standard output.
 The tactic {\tt fail} is the always-failing tactic: it does not solve
 any goal. It is useful for defining other tacticals since it can be
 catched by {\tt try} or {\tt match goal}. There are three variants:
-\begin{center}
+\begin{tabbing}
 {\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}
-\end{center}
+\end{tabbing}
 The number $n$ is the failure level. If no level is specified, it
 defaults to $0$.  The level is used by {\tt try} and {\tt match goal}.
 If $0$, it makes {\tt match goal} considering the next clause
@@ -397,24 +400,19 @@ If $0$, it makes {\tt match goal} considering the next clause
 \ErrMsg \errindex{Tactic Failure "message" (level $n$)}.
 
 \subsubsection{Local definitions}
-\tacindex{let}
-\tacindex{let rec}
+\index{Ltac!let}
+\index{Ltac!let rec}
+\index{let!in Ltac}
+\index{let rec!in Ltac}
 
 Local definitions can be done as follows:
-
-%\newpage{}
-
-%\phantom{}
-%\vfill{}
-
-\begin{tabular}{l}
+\begin{tabbing}
 {\tt let} {\ident}$_1$ {\tt :=} {\tacexpr}$_1$\\
 {\tt with} {\ident}$_2$ {\tt :=} {\tacexpr}$_2$\\
 ...\\
 {\tt with} {\ident}$_n$ {\tt :=} {\tacexpr}$_n$ {\tt in}\\
 {\tacexpr}
-\end{tabular}
-
+\end{tabbing}
 each {\tacexpr}$_i$ is evaluated to $v_i$, then, {\tacexpr} is
 evaluated by substituting $v_i$ to each occurrence of {\ident}$_i$,
 for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$
@@ -427,9 +425,9 @@ argument is required.
 \subsubsection{Application}
 
 An application is an expression of the following form:
-\begin{center}
+\begin{tabbing}
 {\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$
-\end{center}
+\end{tabbing}
 The reference {\qualid} must be bound to some defined tactic
 definition expecting at least $n$ arguments.  The expressions
 {\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$.
@@ -441,22 +439,23 @@ definition expecting at least $n$ arguments.  The expressions
 %\subsection{Application of tactic values}
 
 \subsubsection{Function construction}
-\tacindex{fun}
+\index{fun!in Ltac}
+\index{Ltac!fun}
 
 A parameterized tactic can be built anonymously (without resorting to
 local definitions) with:
-\begin{center}
+\begin{tabbing}
 {\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}
-\end{center}
+\end{tabbing}
 Indeed, local definitions of functions are a syntactic sugar for
 binding a {\tt fun} tactic to an identifier.
 
 \subsubsection{Pattern matching on terms}
-\tacindex{match}
+\index{Ltac!match}
+\index{match!in Ltac}
 
 We can carry out pattern matching on terms with:
-
-\begin{tabular}{l}
+\begin{tabbing}
 {\tt match} {\tacexpr} {\tt with}\\
 ~~~{\cpattern}$_1$ {\tt =>} {\tacexpr}$_1$\\
 ~{\tt |} {\cpattern}$_2$ {\tt =>} {\tacexpr}$_2$\\
@@ -464,8 +463,7 @@ We can carry out pattern matching on terms with:
 ~{\tt |} {\cpattern}$_n$ {\tt =>} {\tacexpr}$_n$\\
 ~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\
 {\tt end}
-\end{tabular}
-
+\end{tabbing}
 The {\tacexpr} is evaluated and should yield a term which is matched
 (non-linear first order unification) against {\cpattern}$_1$ then
 {\tacexpr}$_1$ is evaluated into some value by substituting the
@@ -478,18 +476,23 @@ goal}). If all clauses fail (in particular, there is no pattern {\_})
 then a no-matching error is raised.
 
 \begin{ErrMsgs}
-\item \errindex{No matching clauses for match}\\
-No pattern can be used and, in particular, there is no {\tt \_} pattern.
-\item \errindex{Argument of match does not evaluate to a term}\\
-This happens when {\tacexpr} does not denote a term.
+
+\item \errindex{No matching clauses for match}
+
+  No pattern can be used and, in particular, there is no {\tt \_} pattern.
+
+\item \errindex{Argument of match does not evaluate to a term}
+
+  This happens when {\tacexpr} does not denote a term.
+
 \end{ErrMsgs}
 
-\tacindex{context (in pattern)}
+\index{context!in pattern}
 There is a special form of patterns to match a subterm against the
 pattern:
-\begin{center}
+\begin{tabbing}
 {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
-\end{center}
+\end{tabbing}
 It matches any term which one subterm matches {\cpattern}. If there is
 a match, the optional {\ident} is assign the ``matched context'', that
 is the initial term where the matched subterm is replaced by a
@@ -503,23 +506,25 @@ the order of matching is left unspecified.
 
 
 \subsubsection{Pattern matching on goals}
-\tacindex{match goal}
-\tacindex{match reverse goal}
+\index{Ltac!match goal}
+\index{Ltac!match reverse goal}
+\index{match goal!in Ltac}
+\index{match reverse goal!in Ltac}
 
 We can make pattern matching on goals using the following expression:
-
-\begin{tabular}{l}
+\begin{tabbing}
 {\tt match goal with}\\
-~~~$hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$
+~~\={\tt |} $hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$
    ~~{\tt |-}{\cpattern}$_1${\tt =>} {\tacexpr}$_1$\\
-~~{\tt |}$hyps_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$
+  \>{\tt |} $hyp_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$
    ~~{\tt |-}{\cpattern}$_2${\tt =>} {\tacexpr}$_2$\\
 ~~...\\
-~~{\tt |}$hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$
+  \>{\tt |} $hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$
    ~~{\tt |-}{\cpattern}$_n${\tt =>} {\tacexpr}$_n$\\
-~~{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\
+  \>{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\
 {\tt end}
-\end{tabular}
+\end{tabbing}
+
 
 % TODO: specify order of hypothesis and explain reverse...
 
@@ -539,8 +544,9 @@ is applied.
 
 \ErrMsg \errindex{No matching clauses for match goal}
 
-No goal pattern can be used and, in particular, there is no {\tt
-\_} goal pattern.
+  No goal pattern can be used and, in particular, there is no {\tt
+    \_} goal pattern.
+
 \medskip
 
 It is important to know that each hypothesis of the goal can be
@@ -552,14 +558,14 @@ first), but it possible to reverse this order (older first) with
 the {\tt match reverse goal with} variant.
 
 \subsubsection{Filling a term context}
-\tacindex{context (in expressions)}
+\index{context!in expression}
 
 The following expression is not a tactic in the sense that it does not
 produce subgoals but generates a term to be used in tactic
 expressions:
-\begin{center}
+\begin{tabbing}
 {\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]}
-\end{center}
+\end{tabbing}
 {\ident} must denote a context variable bound by a {\tt context}
 pattern of a {\tt match} expression. This expression evaluates
 replaces the hole of the value of {\ident} by the value of
@@ -567,34 +573,38 @@ replaces the hole of the value of {\ident} by the value of
 
 \ErrMsg \errindex{not a context variable}
 
+
 \subsubsection{Generating fresh hypothesis names}
-\tacindex{fresh}
+\index{Ltac!fresh}
+\index{fresh!in Ltac}
 
 Tactics sometimes have to generate new names for hypothesis. Letting
 the system decide a name with the {\tt intro} tactic is not so good
 since it is very awkward to retrieve the name the system gave.
 
 As before, the following expression returns a term:
-\begin{center}
+\begin{tabbing}
 {\tt fresh} {\qstring}
-\end{center}
+\end{tabbing}
 It evaluates to an identifier unbound in the goal, which is obtained
 by padding {\qstring} with a number if necessary. If no name is given,
 the prefix is {\tt H}.
 
 \subsubsection{{\tt type of} {\term}}
-\tacindex{type of}
+%\tacindex{type of}
+\index{Ltac!type of}
+\index{type of!in Ltac}
 
 This tactic computes the type of {\term}.
 
-
 \subsubsection{Computing in a constr}
-\tacindex{eval}
+\index{Ltac!eval}
+\index{eval!in Ltac}
 
 Evaluation of a term can be performed with:
-\begin{center}
+\begin{tabbing}
 {\tt eval} {\nterm{redexpr}} {\tt in} {\term}
-\end{center}
+\end{tabbing}
 where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt
 hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
 {\tt fold}, {\tt pattern}.
@@ -609,10 +619,10 @@ elementary tactics, this is equivalent to \tacexpr. For complex tactic
 like \texttt{auto}, it displays the operations performed by the
 tactic.
 
-
 \subsubsection{Proving a subgoal as a separate lemma}
 \tacindex{abstract}
 \index{Tacticals!abstract@{\tt abstract}}
+
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
@@ -640,22 +650,21 @@ Basically, tactics toplevel definitions are made as follows:
 %script is evaluated by substituting $v$ to {\ident}.
 %
 %We can define functional definitions by:\\
-\begin{center}
+\begin{tabbing}
 {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
 {\tacexpr}
-\end{center}
+\end{tabbing}
 This defines a new tactic that can be used in any tactic script or new
 tactic toplevel definition.
 
 \Rem The preceding definition can equivalently be written:
-\begin{center}
+\begin{tabbing}
 {\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$
 {\tt =>} {\tacexpr}
-\end{center}
+\end{tabbing}
 Recursive and mutual recursive function definitions are also
 possible with the syntax:
-\begin{center}
-\begin{tabular}{l}
+\begin{tabbing}
 {\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ...
 {\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\
 {\tt with} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=}
@@ -663,12 +672,429 @@ possible with the syntax:
 ...\\
 {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
 {\tacexpr}$_n$
-\end{tabular}
-\end{center}
+\end{tabbing}
 
 %This definition bloc is a set of definitions (use of
 %the same previous syntactical sugar) and the other scripts are evaluated as
 %usual except that the substitutions are lazily carried out (when an identifier
 %to be evaluated is the name of a recursive definition).
 
+\endinput
+
+\section{Examples}
 
+\subsection{About the cardinality of the natural number set}
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_eval}
+Reset Initial.
+Require Import Arith.
+Require Import List.
+\end{coq_eval}
+\begin{coq_example*}
+Lemma card_nat :
+ ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
+Proof.
+red; intros (x, (y, Hy)).
+elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
+ match goal with
+ | [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
+     cut (b = c); [ discriminate | apply trans_equal with a; auto ]
+ end.
+Qed.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{A proof on cardinality of natural numbers}
+\label{cnatltac}
+\end{figure}
+
+A first example which shows how to use the pattern matching over the proof
+contexts is the proof that natural numbers have more than two elements. The
+proof of such a lemma can be done as shown in table~\ref{cnatltac}.
+
+We can notice that all the (very similar) cases coming from the three
+eliminations (with three distinct natural numbers) are successfully solved by
+a {\tt match goal} structure and, in particular, with only one pattern (use
+of non-linear matching).
+
+\subsection{Permutation on closed lists}
+
+\begin{figure}[b]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Section Sort.
+Variable A : Set.
+Inductive permut : list A -> list A -> Prop :=
+  | permut_refl   : forall l, permut l l
+  | permut_cons   :
+      forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
+  | permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
+  | permut_trans  :
+      forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
+End Sort.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Definition of the permutation predicate}
+\label{permutpred}
+\end{figure}
+
+
+Another more complex example is the problem of permutation on closed
+lists. The aim is to show that a closed list is a permutation of
+another one.  First, we define the permutation predicate as shown in
+table~\ref{permutpred}.
+ 
+\begin{figure}[p]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac Permut n :=
+  match goal with
+  | |- (permut _ ?l ?l) => apply permut_refl
+  | |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
+      let newn := eval compute in (length l1) in
+      (apply permut_cons; Permut newn)
+  | |- (permut ?A (?a :: ?l1) ?l2) =>
+      match eval compute in n with
+      | 1 => fail
+      | _ =>
+          let l1' := constr:(l1 ++ a :: nil) in
+          (apply (permut_trans A (a :: l1) l1' l2);
+            [ apply permut_append | compute; Permut (pred n) ])
+      end
+  end.
+Ltac PermutProve :=
+  match goal with
+  | |- (permut _ ?l1 ?l2) =>
+      match eval compute in (length l1 = length l2) with
+      | (?n = ?n) => Permut n
+      end
+  end.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Permutation tactic}
+\label{permutltac}
+\end{figure}
+
+\begin{figure}[p]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Lemma permut_ex1 :
+  permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+Proof.
+PermutProve.
+Qed.
+
+Lemma permut_ex2 :
+  permut nat
+    (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
+    (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
+Proof.
+PermutProve.
+Qed.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Examples of {\tt PermutProve} use}
+\label{permutlem}
+\end{figure}
+
+Next, we can write naturally the tactic and the result can be seen in
+table~\ref{permutltac}. We can notice that we use two toplevel
+definitions {\tt PermutProve} and {\tt Permut}. The function to be
+called is {\tt PermutProve} which computes the lengths of the two
+lists and calls {\tt Permut} with the length if the two lists have the
+same length. {\tt Permut} works as expected.  If the two lists are
+equal, it concludes. Otherwise, if the lists have identical first
+elements, it applies {\tt Permut} on the tail of the lists.  Finally,
+if the lists have different first elements, it puts the first element
+of one of the lists (here the second one which appears in the {\tt
+  permut} predicate) at the end if that is possible, i.e., if the new
+first element has been at this place previously. To verify that all
+rotations have been done for a list, we use the length of the list as
+an argument for {\tt Permut} and this length is decremented for each
+rotation down to, but not including, 1 because for a list of length
+$n$, we can make exactly $n-1$ rotations to generate at most $n$
+distinct lists. Here, it must be noticed that we use the natural
+numbers of {\Coq} for the rotation counter. In table~\ref{ltac}, we
+can see that it is possible to use usual natural numbers but they are
+only used as arguments for primitive tactics and they cannot be
+handled, in particular, we cannot make computations with them. So, a
+natural choice is to use {\Coq} data structures so that {\Coq} makes
+the computations (reductions) by {\tt eval compute in} and we can get
+the terms back by {\tt match}.
+
+With {\tt PermutProve}, we can now prove lemmas such those shown in
+table~\ref{permutlem}.
+
+
+\subsection{Deciding intuitionistic propositional logic}
+
+\begin{figure}[b]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac Axioms :=
+  match goal with
+  | |- True => trivial
+  | _:False |- _  => elimtype False; assumption
+  | _:?A |- ?A  => auto
+  end.
+Ltac DSimplif :=
+  repeat
+   (intros;
+    match goal with
+     | id:(~ _) |- _ => red in id
+     | id:(_ /\ _) |- _ =>
+         elim id; do 2 intro; clear id
+     | id:(_ \/ _) |- _ =>
+         elim id; intro; clear id
+     | id:(?A /\ ?B -> ?C) |- _ =>
+         cut (A -> B -> C);
+          [ intro | intros; apply id; split; assumption ]
+     | id:(?A \/ ?B -> ?C) |- _ =>
+         cut (B -> C);
+          [ cut (A -> C);
+             [ intros; clear id
+             | intro; apply id; left; assumption ]
+          | intro; apply id; right; assumption ]
+     | id0:(?A -> ?B),id1:?A |- _ =>
+         cut B; [ intro; clear id0 | apply id0; assumption ]
+     | |- (_ /\ _) => split
+     | |- (~ _) => red
+     end).
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Deciding intuitionistic propositions (1)}
+\label{tautoltaca}
+\end{figure}
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac TautoProp :=
+  DSimplif;
+   Axioms ||
+     match goal with
+     | id:((?A -> ?B) -> ?C) |- _ =>
+          cut (B -> C);
+          [ intro; cut (A -> B);
+             [ intro; cut C;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; intro; assumption ]; TautoProp
+     | id:(~ ?A -> ?B) |- _ =>
+         cut (False -> B);
+          [ intro; cut (A -> False);
+             [ intro; cut B;
+                [ intro; clear id | apply id; assumption ]
+             | clear id ]
+          | intro; apply id; red; intro; assumption ]; TautoProp
+     | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
+     end.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Deciding intuitionistic propositions (2)}
+\label{tautoltacb}
+\end{figure}
+
+The pattern matching on goals allows a complete and so a powerful
+backtracking when returning tactic values. An interesting application
+is the problem of deciding intuitionistic propositional logic.
+Considering the contraction-free sequent calculi {\tt LJT*} of
+Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic
+using the tactic language. In Table~\ref{tautoltaca}, the tactic {\tt
+  Axioms} tries to conclude using usual axioms. The {\tt DSimplif}
+tactic applies all the reversible rules of Dyckhoff's system.
+Finally, in Table~\ref{tautoltacb}, the {\tt TautoProp} tactic (the
+main tactic to be called) simplifies with {\tt DSimplif}, tries to
+conclude with {\tt Axioms} and tries several paths using the
+backtracking rules (one of the four Dyckhoff's rules for the left
+implication to get rid of the contraction and the right or).
+
+\begin{figure}[tb]
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
+Proof.
+TautoProp.
+Qed.
+
+Lemma tauto_ex2 :
+   forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+Proof.
+TautoProp.
+Qed.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Proofs of tautologies with {\tt TautoProp}}
+\label{tautolem}
+\end{figure}
+
+For example, with {\tt TautoProp}, we can prove tautologies like those in
+table~\ref{tautolem}.
+
+
+\subsection{Deciding type isomorphisms}
+
+A more tricky problem is to decide equalities between types and modulo
+isomorphisms. Here, we choose to use the isomorphisms of the simply typed
+$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
+\cite{RC95}). The axioms of this $\lb{}$-calculus are given by
+table~\ref{isosax}.
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Open Scope type_scope.
+Section Iso_axioms.
+Variables A B C : Set.
+Axiom Com : A * B = B * A.
+Axiom Ass : A * (B * C) = A * B * C.
+Axiom Cur : (A * B -> C) = (A -> B -> C).
+Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
+Axiom P_unit : A * unit = A.
+Axiom AR_unit : (A -> unit) = unit.
+Axiom AL_unit : (unit -> A) = A.
+Lemma Cons : B = C -> A * B = A * C.
+Proof.
+intro Heq; rewrite Heq; apply refl_equal.
+Qed.
+End Iso_axioms.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Type isomorphism axioms}
+\label{isosax}
+\end{figure}
+
+The tactic to judge equalities modulo this axiomatization can be written as
+shown in tables~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
+simple. Types are reduced using axioms that can be oriented (this done by {\tt
+MainSimplif}). The normal forms are sequences of Cartesian
+products without Cartesian product in the left component. These normal forms
+are then compared modulo permutation of the components (this is done by {\tt
+CompareStruct}). The main tactic to be called and realizing this algorithm is
+{\tt IsoProve}.
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac DSimplif trm :=
+  match trm with
+  | (?A * ?B * ?C) =>
+      rewrite <- (Ass A B C); try MainSimplif
+  | (?A * ?B -> ?C) =>
+      rewrite (Cur A B C); try MainSimplif
+  | (?A -> ?B * ?C) =>
+      rewrite (Dis A B C); try MainSimplif
+  | (?A * unit) =>
+      rewrite (P_unit A); try MainSimplif
+  | (unit * ?B) =>
+      rewrite (Com unit B); try MainSimplif
+  | (?A -> unit) =>
+      rewrite (AR_unit A); try MainSimplif
+  | (unit -> ?B) =>
+      rewrite (AL_unit B); try MainSimplif
+  | (?A * ?B) =>
+      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
+  | (?A -> ?B) =>
+      (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
+  end
+ with MainSimplif :=
+  match goal with
+  | |- (?A = ?B) => try DSimplif A; try DSimplif B
+  end.
+Ltac Length trm :=
+  match trm with
+  | (_ * ?B) => let succ := Length B in constr:(S succ)
+  | _ => constr:1
+  end.
+Ltac assoc := repeat rewrite <- Ass.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Type isomorphism tactic (1)}
+\label{isosltac1}
+\end{figure}
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example}
+Ltac DoCompare n :=
+  match goal with
+  | [ |- (?A = ?A) ] => apply refl_equal
+  | [ |- (?A * ?B = ?A * ?C) ] =>
+    apply Cons; let newn := Length B in DoCompare newn
+  | [ |- (?A * ?B = ?C) ] =>
+    match eval compute in n with
+    | 1 => fail
+    | _ =>
+      pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
+    end
+  end.
+Ltac CompareStruct :=
+  match goal with
+  | [ |- (?A = ?B) ] =>
+      let l1 := Length A
+      with l2 := Length B in
+      match eval compute in (l1 = l2) with
+      | (?n = ?n) => DoCompare n
+      end
+  end.
+Ltac IsoProve := MainSimplif; CompareStruct.
+\end{coq_example}
+\end{minipage}}
+\end{center}
+\caption{Type isomorphism tactic (2)}
+\label{isosltac2}
+\end{figure}
+
+Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
+
+\begin{figure}
+\begin{center}
+\fbox{\begin{minipage}{0.95\textwidth}
+\begin{coq_example*}
+Lemma isos_ex1 : 
+  forall A B:Set, A * unit * B = B * (unit * A).
+Proof.
+intros; IsoProve.
+Qed.
+
+Lemma isos_ex2 :
+  forall A B C:Set,
+    (A * unit -> B * (C * unit)) =
+    (A * unit -> (C -> unit) * C) * (unit -> A -> B).
+Proof.
+intros; IsoProve.
+Qed.
+\end{coq_example*}
+\end{minipage}}
+\end{center}
+\caption{Type equalities solved by {\tt IsoProve}}
+\label{isoslem}
+\end{figure}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: