*** empty log message ***

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

1 files changed, 111 insertions, 479 deletions

diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 84ec732fbf..b7be362578 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -5,10 +5,12 @@
 
 This chapter gives a compact documentation of Ltac, the tactic
 language available in {\Coq}. We start by giving the syntax, and next,
-we present the informal semantics. Finally, we show some examples which
-deal with small but also with non-trivial problems. If you want to
-know more regarding this language and especially about its fundations,
-you can refer to~\cite{Del00}.
+we present the informal semantics. If you want to know more regarding
+this language and especially about its fundations, you can refer
+to~\cite{Del00}. Chapter~\ref{Tactics-examples} is devoted to giving
+examples of use of this language on small but also with non-trivial
+problems.
+
 
 \section{Syntax}
 
@@ -22,29 +24,49 @@ you can refer to~\cite{Del00}.
 \def\matchrule{\textrm{\textsl{match\_rule}}}
 \def\contextrule{\textrm{\textsl{context\_rule}}}
 \def\contexthyps{\textrm{\textsl{context\_hyps}}}
-\def\primitivetactic{\textrm{\textsl{primitive\_tactic}}}
-\def\tacarg{\textrm{\textsl{arg}}}
-\def\qstring{\textrm{\textsl{string}}}
+\def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
 
 The syntax of the tactic language is given in tables~\ref{ltac}
 and~\ref{ltac_aux}. See section~\ref{BNF-syntax} for a description of
 the BNF metasyntax used in these tables. Various already defined
 entries will be used in this chapter: entries {\naturalnumber},
-{\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and
-{\primitivetactic} represent respectively the natural and integer
-numbers, the authorized identificators and qualified names, {\Coq}'s
-terms and patterns and all the basic tactics. The syntax of
-{\cpattern} is the same as that of terms, but there can
-be specific variables like {\tt ?id} where {\tt id} is a {\ident} or
-{\tt \_}, which are metavariables for pattern matching. {\tt ?id} allows
-us to keep instantiations and to make constraints whereas {\tt \_}
-shows that we are not interested in what will be matched. On the right
-hand side, they are used without the question mark.
+{\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and {\atomictac}
+represent respectively the natural and integer numbers, the authorized
+identificators and qualified names, {\Coq}'s terms and patterns and
+all the atomic tactics described in chapter~\ref{Tactics}. The syntax
+of {\cpattern} is the same as that of terms, but there can be specific
+variables like {\tt ?id} where {\tt id} is a {\ident} or {\tt \_},
+which are metavariables for pattern matching. {\tt ?id} allows us to
+keep instantiations and to make constraints whereas {\tt \_} shows
+that we are not interested in what will be matched. On the right hand
+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. 
+
+\item As shown by the figure, tactical {\tt ||} binds more than the
+prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and
+{\tt abstract} which themselves bind more than the postfix tactical
+``{\tt \dots\ ;[ \dots\ ]}'' which binds more than ``\dots\ {\tt ;}
+\dots''.
+
+For instance
+\begin{tabbing}
+{\tt try repeat \tac$_1$ ||
+  \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
+\end{tabbing}
+is understood as 
+\begin{tabbing}
+{\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
+{\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
+\end{tabbing}
+\end{Remarks}
+
 
 \begin{table}[htbp]
 \noindent{}\framebox[6in][l]
@@ -93,7 +115,7 @@ table~\ref{ltactop}.
 & \cn{}| & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
 & \cn{}| & {\tt type of} {\term}\\
 & \cn{}| & {\tt constr :} {\term}\\
-& \cn{}| & \primitivetactic\\
+& \cn{}| & \atomictac\\
 & \cn{}| & {\qualid} \nelist{\tacarg}{}\\
 & \cn{}| & {\atom}\\
 \\
@@ -157,7 +179,12 @@ table~\ref{ltactop}.
 \label{ltactop}
 \end{table}
 
+
+%%
+%% Semantics
+%%
 \section{Semantics}
+\index[tactic]{Tacticals}\index{Tacticals}\label{Tacticals}
 
 Tactic expressions can only be applied in the context of a goal.  The
 evaluation yields either a term, an integer or a tactic. Intermediary
@@ -217,6 +244,8 @@ of Ltac.
 
 \subsubsection{Sequence}
 \tacindex{;}
+\index{;@{\tt ;}}
+\index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
 
 A sequence is an expression of the following form:\\
 
@@ -224,11 +253,13 @@ A sequence is an expression of the following form:\\
 
 {\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 the subgoals generated by the application of
+and $v_2$ is applied to every subgoal generated by the application of
 $v_1$. Sequence is left associating.
 
 \subsubsection{General sequence}
 \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:\\
 
@@ -242,18 +273,21 @@ $v_0$ does not generate exactly $n$ subgoals.
 
 \subsubsection{For loop}
 \tacindex{do}
+\index{Tacticals!do@{\tt do}}
 
-We have a for loop with:\\
+There is a for loop that repeats a tactic {\num} times:\\
 
-{\tt do} $n$ {\tacexpr}\\
+{\tt do} {\num} {\tacexpr}\\
 
-{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied $n$
-times. Supposing $n>1$, after the first application of $v$, $v$ is applied, at
-least once, to the generated subgoals and so on. It fails if the application of
-$v$ fails before the $n$ applications have been completed.
+{\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
+subgoals and so on. It fails if the application of $v$ fails before
+the {\num} applications have been completed.
 
 \subsubsection{Repeat loop}
 \tacindex{repeat}
+\index{Tacticals!repeat@{\tt repeat}}
 
 We have a repeat loop with:\\
 
@@ -267,6 +301,7 @@ fails.
 
 \subsubsection{Error catching}
 \tacindex{try}
+\index{Tacticals!try@{\tt try}}
 
 We can catch the tactic errors with:\\
 
@@ -289,12 +324,12 @@ 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
 raised. 
 
-{\tt Error message:}\\
+\ErrMsg \errindex{Failed to progress}
 
-\errindex{Failed to progress}
 
 \subsubsection{Branching}
 \tacindex{||}
+\index{Tacticals!orelse@{\tt ||}}
 
 We can easily branch with the following structure:\\
 
@@ -305,6 +340,8 @@ $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.
 
 \subsubsection{First tactic to work}
+\tacindex{first}
+\index{Tacticals!first@{\tt first}}
 
 We may consider the first tactic to work (i.e. which does not fail) among a
 panel of tactics:\\
@@ -315,11 +352,11 @@ panel of tactics:\\
 $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.\\
 
-{\tt Error message:}\\
-
-{\tt No applicable tactic}
+\ErrMsg \errindex{No applicable tactic}
 
 \subsubsection{Solving}
+\tacindex{solve}
+\index{Tacticals!solve@{\tt solve}}
 
 We may consider the first to solve (i.e. which generates no subgoal) among a
 panel of tactics:\\
@@ -330,37 +367,36 @@ panel of tactics:\\
 $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.\\
 
-{\tt Error message:}\\
-
-{\tt Cannot solve the goal}
+\ErrMsg \errindex{Cannot solve the goal}
 
 \subsubsection{Identity}
+\tacindex{idtac}
+\index{Tacticals!idtac@{\tt idtac}}
 
-We have the identity tactic:\\
+The constant {\tt idtac} is the identity tactic: it leaves any goal
+unchanged but it appears in the proof script.\\
 
 {\tt idtac} and {\tt idtac "message"}\\
 
-It leaves the goal unchanged but it appears in the proof script.
-If there is a string as argument then it prints this string on the
-standard output. 
+The latter variant prints the string on the standard output.
 
 \subsubsection{Failing}
+\tacindex{fail}
+\index{Tacticals!fail@{\tt fail}}
 
-We have the failing tactic:\\
+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:\\
 
-{\tt fail}, {\tt fail $n$}, {\tt fail "message"}
- and {\tt fail $n$ "message"}  \\
+{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}  \\
 
-It always fails and leaves the goal unchanged. It does not appear in
-the proof script and can be catched by {\tt try}. The number $n$ is
-the failure level. If no level is specified, it defaults to $0$.  The
-level is used in {\tt match goal}.  If $0$, it makes {\tt match
-goal} considering the next clause. If non zero, the current {\tt
-match goal} block is aborted and the level is decremented.
+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
+(backtracking). If non zero, the current {\tt match goal} block or
+{\tt try} command is aborted and the level is decremented.
 
-{\tt Error message:}\\
-
-\errindex{Tactic Failure "message" (level $n$)}.
+\ErrMsg \errindex{Tactic Failure "message" (level $n$)}.
 
 \subsubsection{Local definitions}
 \tacindex{let}
@@ -443,15 +479,12 @@ immediately applied to the current goal (in contrast with {\tt match
 goal}). If all clauses fail (in particular, there is no pattern {\_})
 then a no-matching error is raised. \\
 
-{\tt Error messages:}\\
-
-\errindex{No matching clauses for match}
-
+\begin{ErrMsgs}
+\item \errindex{No matching clauses for match}\\
 \hx{4}No pattern can be used and, in particular, there is no {\tt \_} pattern.
-
-\errindex{Argument of match does not evaluate to a term}
-
+\item \errindex{Argument of match does not evaluate to a term}\\
 \hx{4}This happens when {\tacexpr} does not denote a term.
+\end{ErrMsgs}
 
 \tacindex{context (in pattern)}
 There is a special form of patterns to match a subterm against the
@@ -506,10 +539,7 @@ pattern is tried and so on. If the next to last proof context pattern
 fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$
 is applied.\\
 
-{\tt Error message:}\\
-
-\errindex{No matching clauses for match goal}
-
+\ErrMsg \errindex{No matching clauses for match goal}\\
 \hx{4}No goal pattern can be used and, in particular, there is no {\tt
 \_} goal pattern.
 
@@ -535,10 +565,7 @@ pattern of a {\tt match} expression. This expression evaluates
 replaces the hole of the value of {\ident} by the value of
 {\tacexpr}.
 
-{\tt Error message:}\\
-
-\errindex{not a context variable}
-
+\ErrMsg \errindex{not a context variable}
 
 \subsubsection{Generating fresh hypothesis names}
 \tacindex{fresh}
@@ -577,32 +604,33 @@ hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
 
 \subsubsection{Accessing tactic decomposition}
 \tacindex{info}
+\index{Tacticals!info@{\tt info}}
 
-It is possible to print on standard output how a tactic was
-decomposed with:\\
+Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For
+elementary tactics, this is equivalent to \tacexpr. For complex tactic
+like \texttt{auto}, it displays the operations performed by the
+tactic.
 
-{\tt info} {\tacexpr}\\
 
-This may be useful to know what steps an automatic tactic made.
-
-
-\subsubsection{Making a subproof as a separate lemma}
+\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
+current goal and \textit{n} is chosen so that this is a fresh name.
 
-This tactical was made to avoid efficiency problems with huge proof
-terms. It allows to prove the current goal as a separate lemma by
-applying a tactic. This tactic is supposed to solve the goal.
-
-{\tt abstract} {\tacexpr} {\tt using} {\ident}
-
-Creates a constant {\ident} (if not provided, a fresh name is
-generated by the tactical), which type is the current goal and applies
-{\tacexpr} on it.
+This tactical is useful with tactics such as \texttt{omega} or
+\texttt{discriminate} that generate huge proof terms. With that tool
+the user can avoid the explosion at time of the \texttt{Save} command
+without having to cut manually the proof in smaller lemmas.
 
-{\tt Error messages:}
-
-\errindex{Proof is not complete}
+\begin{Variants}
+\item \texttt{abstract {\tacexpr} using {\ident}}.\\
+  Give explicitly the name of the auxiliary lemma.
+\end{Variants}
 
+\ErrMsg \errindex{Proof is not complete}
 
 \subsection{Tactic toplevel definitions}
 \comindex{Ltac}
@@ -646,400 +674,4 @@ possible with the syntax:
 %usual except that the substitutions are lazily carried out (when an identifier
 %to be evaluated is the name of a recursive definition).
 
-\section{Examples}
-
-\subsection{About the cardinality of the natural number set}
-
-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}.
-
-\begin{coq_eval}
-Reset Initial.
-Require Import Arith.
-Require Import List.
-\end{coq_eval}
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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*}
-}}
-\caption{A proof on cardinality of natural numbers}
-\label{cnatltac}
-\end{table}
-
-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}
-
-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{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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*}
-}}
-\caption{Definition of the permutation predicate}
-\label{permutpred}
-\end{table}
-
-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}.
- 
-\begin{table}[p]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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}
-}}
-\caption{Permutation tactic}
-\label{permutltac}
-\end{table}
-
-With {\tt PermutProve}, we can now prove lemmas such those shown in
-table~\ref{permutlem}.
-
-\begin{table}[p]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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*}
-}}
-\caption{Examples of {\tt PermutProve} use}
-\label{permutlem}
-\end{table}
-
-\subsection{Deciding intuitionistic propositional logic}
-
-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 as shown in table~\ref{tautoltac}. The
-tactic {\tt Axioms} tries to conclude using usual axioms. The tactic
-{\tt DSimplif} applies all the reversible rules of Dyckhoff's
-system. Finally, the tactic {\tt TautoProp} (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{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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).
-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}
-}}
-\caption{Deciding intuitionistic propositions}
-\label{tautoltac}
-\end{table}
-
-For example, with {\tt TautoProp}, we can prove tautologies like those in
-table~\ref{tautolem}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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*}
-}}
-\caption{Proofs of tautologies with {\tt TautoProp}}
-\label{tautolem}
-\end{table}
-
-\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{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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*}
-}}
-\caption{Type isomorphism axioms}
-\label{isosax}
-\end{table}
-
-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{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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}
-}}
-\caption{Type isomorphism tactic (1)}
-\label{isosltac1}
-\end{table}
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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}
-}}
-\caption{Type isomorphism tactic (2)}
-\label{isosltac2}
-\end{table}
-
-Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
-
-\begin{table}[ht]
-\noindent{}\framebox[6.4in][l]
-{\parbox{6.4in}
-{
-\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*}
-}}
-\caption{Type equalities solved by {\tt IsoProve}}
-\label{isoslem}
-\end{table}