Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' of the Reference Manual.

1 files changed, 313 insertions, 330 deletions

diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 84810ddba..78719c1ef 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -25,7 +25,7 @@ argument an hypothesis to generalize. It uses the JMeq datatype
 defined in Coq.Logic.JMeq, hence we need to require it before. For
 example, revisiting the first example of the inversion documentation:
 
-.. coqtop:: in
+.. coqtop:: in reset
 
    Require Import Coq.Logic.JMeq.
 
@@ -63,6 +63,10 @@ to use an heterogeneous equality to relate the new hypothesis to the
 old one (which just disappeared here). However, the tactic works just
 as well in this case, e.g.:
 
+.. coqtop:: none
+
+   Abort.
+
 .. coqtop:: in
 
    Variable Q : forall (n m : nat), Le n m -> Prop.
@@ -80,7 +84,7 @@ to recover the needed equalities. Also, some subgoals should be
 directly solved because of inconsistent contexts arising from the
 constraints on indexes. The nice thing is that we can make a tactic
 based on discriminate, injection and variants of substitution to
-automatically do such simplifications (which may involve the K axiom).
+automatically do such simplifications (which may involve the axiom K).
 This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality``
 does. For example, we might simplify the previous goals considerably:
 
@@ -101,9 +105,9 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or
 simply case analysis on the generalized hypothesis. For example we can
 redo what we’ve done manually with dependent destruction:
 
-.. coqtop:: in
+.. coqtop:: none
 
-   Require Import Coq.Program.Equality.
+   Abort.
 
 .. coqtop:: in
 
@@ -122,9 +126,9 @@ destructed hypothesis actually appeared in the goal, the tactic would
 still be able to invert it, contrary to dependent inversion. Consider
 the following example on vectors:
 
-.. coqtop:: in
+.. coqtop:: none
 
-   Require Import Coq.Program.Equality.
+   Abort.
 
 .. coqtop:: in
 
@@ -167,7 +171,7 @@ 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:
 
-.. coqtop:: in
+.. coqtop:: in reset
 
    Inductive type : Type :=
             | base : type
@@ -226,11 +230,15 @@ name. A term is either an application of:
 
 Once we have this datatype we want to do proofs on it, like weakening:
 
-.. coqtop:: in undo
+.. coqtop:: in
 
    Lemma weakening : forall G D tau, term (G ; D) tau -> 
                      forall tau', term (G , tau' ; D) tau.
 
+.. coqtop:: none
+
+   Abort.
+
 The problem here is that we can’t just use induction on the typing
 derivation because it will forget about the ``G ; D`` constraint appearing
 in the instance. A solution would be to rewrite the goal as:
@@ -241,6 +249,10 @@ in the instance. A solution would be to rewrite the goal as:
                       forall G D, (G ; D) = G' ->
                       forall tau', term (G, tau' ; D) tau.
 
+.. coqtop:: none
+
+   Abort.
+
 With this proper separation of the index from the instance and the
 right induction loading (putting ``G`` and ``D`` after the inducted-on
 hypothesis), the proof will go through, but it is a very tedious
@@ -252,6 +264,7 @@ back automatically. Indeed we can simply write:
 .. coqtop:: in
 
    Require Import Coq.Program.Tactics.
+   Require Import Coq.Program.Equality.
 
 .. coqtop:: in
 
@@ -308,17 +321,14 @@ it can be used directly.
 
    apply weak, IHterm.
 
-If there is an easy first-order solution to these equations as in this
-subgoal, the ``specialize_eqs`` tactic can be used instead of giving
-explicit proof terms:
-
-.. coqtop:: all
+Now concluding this subgoal is easy.
 
-   specialize_eqs IHterm.
+.. coqtop:: in
 
-This concludes our example.
+   constructor; apply IHterm; reflexivity.
 
-See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics.
+.. seealso::
+   The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics.
 
 
 autorewrite
@@ -331,79 +341,83 @@ involves conditional rewritings and shows how to deal with them using
 the optional tactic of the ``Hint Rewrite`` command.
 
 
-Example 1: Ackermann function
+.. example::
+   Ackermann function
 
-.. coqtop:: in
+   .. coqtop:: in reset
 
-   Reset Initial.
+      Require Import Arith.
 
-.. coqtop:: in
+   .. coqtop:: in
 
-   Require Import Arith.
+      Variable Ack : nat -> nat -> nat.
 
-.. coqtop:: in
+   .. coqtop:: in
 
-   Variable Ack : nat -> nat -> nat.
+      Axiom Ack0 : forall m:nat, Ack 0 m = S m.
+      Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
+      Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
 
-.. coqtop:: in
+   .. coqtop:: in
 
-   Axiom Ack0 : forall m:nat, Ack 0 m = S m.
-   Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
-   Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
+      Hint Rewrite Ack0 Ack1 Ack2 : base0.
 
-.. coqtop:: in
+   .. coqtop:: all
 
-   Hint Rewrite Ack0 Ack1 Ack2 : base0.
+      Lemma ResAck0 : Ack 3 2 = 29.
 
-.. coqtop:: all
+   .. coqtop:: all
 
-   Lemma ResAck0 : Ack 3 2 = 29.
+      autorewrite with base0 using try reflexivity.
 
-.. coqtop:: all
+.. example::
+   MacCarthy function
 
-   autorewrite with base0 using try reflexivity.
+   .. coqtop:: in reset
 
-Example 2: Mac Carthy function
+      Require Import Omega.
 
-.. coqtop:: in
+   .. coqtop:: in
 
-   Require Import Omega.
+      Variable g : nat -> nat -> nat.
 
-.. coqtop:: in
+   .. coqtop:: in
 
-   Variable g : nat -> nat -> nat.
+      Axiom g0 : forall m:nat, g 0 m = m.
+      Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
+      Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
 
-.. coqtop:: in
+   .. coqtop:: in
 
-   Axiom g0 : forall m:nat, g 0 m = m.
-   Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
-   Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
+      Hint Rewrite g0 g1 g2 using omega : base1.
 
+   .. coqtop:: in
 
-.. coqtop:: in
+      Lemma Resg0 : g 1 110 = 100.
 
-   Hint Rewrite g0 g1 g2 using omega : base1.
+   .. coqtop:: out
 
-.. coqtop:: in
+      Show.
 
-   Lemma Resg0 : g 1 110 = 100.
+   .. coqtop:: all
 
-.. coqtop:: out
+      autorewrite with base1 using reflexivity || simpl.
 
-   Show.
+   .. coqtop:: none
 
-.. coqtop:: all
+      Qed.
 
-   autorewrite with base1 using reflexivity || simpl.
+   .. coqtop:: all
 
-.. coqtop:: all
+      Lemma Resg1 : g 1 95 = 91.
 
-   Lemma Resg1 : g 1 95 = 91.
+   .. coqtop:: all
 
-.. coqtop:: all
+      autorewrite with base1 using reflexivity || simpl.
 
-   autorewrite with base1 using reflexivity || simpl.
+   .. coqtop:: none
 
+      Qed.
 
 .. _quote:
 
@@ -419,7 +433,7 @@ the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``.
 
 Here is an example:
 
-.. coqtop:: in
+.. coqtop:: in reset
 
    Require Import Quote.
 
@@ -461,16 +475,11 @@ corresponding left-hand side and call yourself recursively on sub-
 terms. If there is no match, we are at a leaf: return the
 corresponding constructor (here ``f_const``) applied to the term.
 
-
-Error messages:
-
-
-#. quote: not a simple fixpoint
+.. exn:: quote: not a simple fixpoint
 
    Happens when ``quote`` is not able to perform inversion properly.
 
 
-
 Introducing variables map
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -553,7 +562,13 @@ example, this is the case for the :tacn:`ring` tactic. Then one must provide to
 is ``[O S]`` then closed natural numbers will be considered as constants
 and other terms as variables.
 
-Example:
+.. coqtop:: in reset
+
+   Require Import Quote.
+
+.. coqtop:: in
+
+   Parameters A B C : Prop.
 
 .. coqtop:: in
 
@@ -594,8 +609,9 @@ Example:
 
    quote interp_f [ B C iff ].
 
-Warning: Since function inversion is undecidable in general case,
-don’t expect miracles from it!
+.. warning::
+   Since functional inversion is undecidable in the general case,
+   don’t expect miracles from it!
 
 .. tacv:: quote @ident in @term using @tactic
 
@@ -607,25 +623,28 @@ don’t expect miracles from it!
    Same as above, but will use the additional ``ident`` list to chose
    which subterms are constants (see above).
 
-See also: comments of source file ``plugins/quote/quote.ml``
+.. seealso::
+   Comments from the source file ``plugins/quote/quote.ml``
 
-See also: the :tacn:`ring` tactic.
+.. seealso::
+   The :tacn:`ring` tactic.
 
 
-Using the tactical language
+Using the tactic language
 ---------------------------
 
 
 About the cardinality of the set of natural numbers
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-A first example which shows how to use 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 follows:
+The first example which shows how to use pattern matching over the
+proof context is a proof of the fact that natural numbers have more
+than two elements. This can be done as follows:
 
-.. coqtop:: in
+.. coqtop:: in reset
 
-   Lemma card_nat : ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
+   Lemma card_nat :
+     ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z.
    Proof.
 
 .. coqtop:: in
@@ -637,8 +656,8 @@ elements. The proof of such a lemma can be done as follows:
    elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
 
    match goal with
-   | [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
-            cut (b = c); [ discriminate | transitivity a; auto ]
+       | _ : ?a = ?b, _ : ?a = ?c |- _ =>
+           cut (b = c); [ discriminate | transitivity a; auto ]
    end.
 
 .. coqtop:: in
@@ -651,16 +670,14 @@ solved by a match goal structure and, in particular, with only one
 pattern (use of non-linear matching).
 
 
-Permutation on closed lists
+Permutations of 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 here:
+A more complex example is the problem of permutations of
+lists. The aim is to show that a list is a permutation of
+another list.
 
-.. coqtop:: in
+.. coqtop:: in reset
 
    Section Sort.
 
@@ -670,205 +687,179 @@ First, we define the permutation predicate as shown here:
 
 .. coqtop:: in
 
-   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.
+   Inductive perm : list A -> list A -> Prop :=
+       | perm_refl : forall l, perm l l
+       | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1)
+       | perm_append : forall a l, perm (a :: l) (l ++ a :: nil)
+       | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2.
 
 .. coqtop:: in
 
    End Sort.
 
-A 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 above.
 
-
 .. coqtop:: none
 
    Require Import List.
 
 
-.. coqtop:: all
-
-   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.
-
-
-.. coqtop:: all
-
-   Ltac PermutProve :=
-            match goal with
-            | |- (permut _ ?l1 ?l2) =>
-                match eval compute in (length l1 = length l2) with
-                | (?n = ?n) => Permut n
-                end
-            end.
-
-Next, we can write naturally the tactic and the result can be seen
-above. We can notice that we use two top level definitions
-``PermutProve`` and ``Permut``. The function to be called is
-``PermutProve`` which computes the lengths of the two lists and calls
-``Permut`` with the length if the two lists have the same
-length. ``Permut`` works as expected. If the two lists are equal, it
-concludes. Otherwise, if the lists have identical first elements, it
-applies ``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 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 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 :ref:`ltac-syntax`, 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 eval compute in and we can get the terms
-back by match.
-
-With ``PermutProve``, we can now prove lemmas as follows:
-
 .. coqtop:: in
 
-   Lemma permut_ex1 : permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+   Ltac perm_aux n :=
+   match goal with
+       | |- (perm _ ?l ?l) => apply perm_refl
+       | |- (perm _ (?a :: ?l1) (?a :: ?l2)) =>
+           let newn := eval compute in (length l1) in
+               (apply perm_cons; perm_aux newn)
+       | |- (perm ?A (?a :: ?l1) ?l2) =>
+           match eval compute in n with
+               | 1 => fail
+               | _ =>
+                   let l1' := constr:(l1 ++ a :: nil) in
+                       (apply (perm_trans A (a :: l1) l1' l2);
+                       [ apply perm_append | compute; perm_aux (pred n) ])
+           end
+   end.
 
-.. coqtop:: in
+Next we define an auxiliary tactic ``perm_aux`` which takes an argument
+used to control the recursion depth. This tactic behaves as follows. If
+the lists are identical (i.e. convertible), it concludes. Otherwise, if
+the lists have identical heads, it proceeds to look at their tails.
+Finally, if the lists have different heads, it rotates the first list by
+putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the
+number of performed rotations using the argument ``n``. We do this by
+decrementing ``n`` each time we perform a rotation. It works because
+for a list of length ``n`` we can make exactly ``n - 1`` rotations
+to generate at most ``n`` distinct lists. Notice that we use the natural
+numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know
+that it is possible to use the usual natural numbers, but they are only
+used as arguments for primitive tactics and they cannot be handled, so,
+in particular, we cannot make computations with them. Thus the natural
+choice is to use Coq data structures so that Coq makes the computations
+(reductions) by ``eval compute in`` and we can get the terms back by match.
+
+.. coqtop:: in
+
+   Ltac solve_perm :=
+   match goal with
+       | |- (perm _ ?l1 ?l2) =>
+           match eval compute in (length l1 = length l2) with
+               | (?n = ?n) => perm_aux n
+           end
+   end.
 
-   Proof. PermutProve. Qed.
+The main tactic is ``solve_perm``. It computes the lengths of the two lists
+and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they
+aren't, the lists cannot be permutations of each other). Using this tactic we
+can now prove lemmas as follows:
 
 .. coqtop:: in
 
-   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.
+   Lemma solve_perm_ex1 :
+     perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
+   Proof. solve_perm. Qed.
 
+.. coqtop:: in
 
+   Lemma solve_perm_ex2 :
+     perm nat
+       (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
+         (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
+   Proof. solve_perm. Qed.
 
 Deciding intuitionistic propositional logic
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. _decidingintuitionistic1:
-
-.. coqtop:: all
-
-   Ltac Axioms :=
-            match goal with
-            | |- True => trivial
-            | _:False |- _ => elimtype False; assumption
-            | _:?A |- ?A => auto
-            end.
-
-.. _decidingintuitionistic2:
-
-.. coqtop:: all
-
-   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).
-
-.. coqtop:: all
-
-   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.
-
-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 LJT* of Roy Dyckhoff
-:cite:`Dyc92`, it is quite natural to code such a tactic
-using the tactic language as shown on figures: :ref:`Deciding
-intuitionistic propositions (1) <decidingintuitionistic1>` and
-:ref:`Deciding intuitionistic propositions (2)
-<decidingintuitionistic2>`. The tactic ``Axioms`` tries to conclude
-using usual axioms. The tactic ``DSimplif`` applies all the reversible
-rules of Dyckhoff’s system. Finally, the tactic ``TautoProp`` (the
-main tactic to be called) simplifies with ``DSimplif``, tries to
-conclude with ``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).
-
-For example, with ``TautoProp``, we can prove tautologies like those:
-
-.. coqtop:: in
-
-   Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
+Pattern matching on goals allows a powerful backtracking when returning tactic
+values. An interesting application is the problem of deciding intuitionistic
+propositional logic. Considering the contraction-free sequent calculi LJT* of
+Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the
+tactic language as shown below.
 
-.. coqtop:: in
-
-   Proof. TautoProp. Qed.
-
-.. coqtop:: in
+.. coqtop:: in reset
 
-   Lemma tauto_ex2 :
-            forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+   Ltac basic :=
+   match goal with
+       | |- True => trivial
+       | _ : False |- _ => contradiction
+       | _ : ?A |- ?A => assumption
+   end.
 
 .. coqtop:: in
 
-   Proof. TautoProp. Qed.
+   Ltac simplify :=
+   repeat (intros;
+       match goal with
+           | H : ~ _ |- _ => red in H
+           | H : _ /\ _ |- _ =>
+               elim H; do 2 intro; clear H
+           | H : _ \/ _ |- _ =>
+               elim H; intro; clear H
+           | H : ?A /\ ?B -> ?C |- _ =>
+               cut (A -> B -> C);
+                   [ intro | intros; apply H; split; assumption ]
+           | H: ?A \/ ?B -> ?C |- _ =>
+               cut (B -> C);
+                   [ cut (A -> C);
+                       [ intros; clear H
+                       | intro; apply H; left; assumption ]
+                   | intro; apply H; right; assumption ]
+           | H0 : ?A -> ?B, H1 : ?A |- _ =>
+               cut B; [ intro; clear H0 | apply H0; assumption ]
+           | |- _ /\ _ => split
+           | |- ~ _ => red
+       end).
+
+.. coqtop:: in
+
+   Ltac my_tauto :=
+     simplify; basic ||
+     match goal with
+         | H : (?A -> ?B) -> ?C |- _ =>
+             cut (B -> C);
+                 [ intro; cut (A -> B);
+                     [ intro; cut C;
+                         [ intro; clear H | apply H; assumption ]
+                     | clear H ]
+                 | intro; apply H; intro; assumption ]; my_tauto
+         | H : ~ ?A -> ?B |- _ =>
+             cut (False -> B);
+                 [ intro; cut (A -> False);
+                     [ intro; cut B;
+                         [ intro; clear H | apply H; assumption ]
+                     | clear H ]
+                 | intro; apply H; red; intro; assumption ]; my_tauto
+         | |- _ \/ _ => (left; my_tauto) || (right; my_tauto)
+     end.
+
+The tactic ``basic`` tries to reason using simple rules involving truth, falsity
+and available assumptions. The tactic ``simplify`` applies all the reversible
+rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main
+tactic to be called) simplifies with ``simplify``, tries to conclude with
+``basic`` 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``).
+
+Having defined ``my_tauto``, we can prove tautologies like these:
+
+.. coqtop:: in
+
+   Lemma my_tauto_ex1 :
+     forall A B : Prop, A /\ B -> A \/ B.
+   Proof. my_tauto. Qed.
+
+.. coqtop:: in
+
+   Lemma my_tauto_ex2 :
+     forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
+   Proof. my_tauto. Qed.
 
 
 Deciding type isomorphisms
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-A more tricky problem is to decide equalities between types and modulo
+A more tricky problem is to decide equalities between types modulo
 isomorphisms. Here, we choose to use the isomorphisms of the simply
 typed λ-calculus with Cartesian product and unit type (see, for
 example, :cite:`RC95`). The axioms of this λ-calculus are given below.
@@ -915,112 +906,104 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below.
 
    End Iso_axioms.
 
+.. coqtop:: in
 
+   Ltac simplify_type ty :=
+   match ty with
+       | ?A * ?B * ?C =>
+           rewrite <- (Ass A B C); try simplify_type_eq
+       | ?A * ?B -> ?C =>
+           rewrite (Cur A B C); try simplify_type_eq
+       | ?A -> ?B * ?C =>
+           rewrite (Dis A B C); try simplify_type_eq
+       | ?A * unit =>
+           rewrite (P_unit A); try simplify_type_eq
+       | unit * ?B =>
+           rewrite (Com unit B); try simplify_type_eq
+       | ?A -> unit =>
+           rewrite (AR_unit A); try simplify_type_eq
+       | unit -> ?B =>
+           rewrite (AL_unit B); try simplify_type_eq
+       | ?A * ?B =>
+           (simplify_type A; try simplify_type_eq) ||
+           (simplify_type B; try simplify_type_eq)
+       | ?A -> ?B =>
+           (simplify_type A; try simplify_type_eq) ||
+           (simplify_type B; try simplify_type_eq)
+   end
+   with simplify_type_eq :=
+   match goal with
+       | |- ?A = ?B => try simplify_type A; try simplify_type B
+   end.
 
-.. _typeisomorphism1:
-
-.. coqtop:: all
-
-   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.
-
-.. coqtop:: all
+.. coqtop:: in
 
-   Ltac Length trm :=
-            match trm with
-            | (_ * ?B) => let succ := Length B in constr:(S succ)
-            | _ => constr:(1)
-            end.
+   Ltac len trm :=
+   match trm with
+       | _ * ?B => let succ := len B in constr:(S succ)
+       | _ => constr:(1)
+   end.
 
-.. coqtop:: all
+.. coqtop:: in
 
    Ltac assoc := repeat rewrite <- Ass.
 
+.. coqtop:: in
 
-.. _typeisomorphism2:
-
-.. coqtop:: all
-
-   Ltac DoCompare n :=
-            match goal with
-            | [ |- (?A = ?A) ] => reflexivity
-            | [ |- (?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.
-
-.. coqtop:: all
+   Ltac solve_type_eq n :=
+   match goal with
+       | |- ?A = ?A => reflexivity
+       | |- ?A * ?B = ?A * ?C =>
+           apply Cons; let newn := len B in solve_type_eq newn
+       | |- ?A * ?B = ?C =>
+           match eval compute in n with
+               | 1 => fail
+               | _ =>
+                   pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (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.
+.. coqtop:: in
 
-.. coqtop:: all
+   Ltac compare_structure :=
+   match goal with
+       | |- ?A = ?B =>
+           let l1 := len A
+           with l2 := len B in
+               match eval compute in (l1 = l2) with
+                   | ?n = ?n => solve_type_eq n
+               end
+   end.
 
-   Ltac IsoProve := MainSimplif; CompareStruct.
+.. coqtop:: in
 
+   Ltac solve_iso := simplify_type_eq; compare_structure.
 
-The tactic to judge equalities modulo this axiomatization can be
-written as shown on these figures: :ref:`type isomorphism tactic (1)
-<typeisomorphism1>` and :ref:`type isomorphism tactic (2)
-<typeisomorphism2>`.  The algorithm is quite simple. Types are reduced
-using axioms that can be oriented (this done by ``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
-``CompareStruct``). The main tactic to be called and realizing this
-algorithm isIsoProve.
+The tactic to judge equalities modulo this axiomatization is shown above.
+The algorithm is quite simple. First types are simplified using axioms that
+can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``).
+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 by the tactic ``compare_structure``. If they have the same
+lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal.
+The main tactic that puts all these components together is called ``solve_iso``.
 
-Here are examples of what can be solved by ``IsoProve``.
+Here are examples of what can be solved by ``solve_iso``.
 
 .. coqtop:: in
 
-   Lemma isos_ex1 :
-       forall A B:Set, A * unit * B = B * (unit * A).
+   Lemma solve_iso_ex1 :
+     forall A B : Set, A * unit * B = B * (unit * A).
    Proof.
-   intros; IsoProve.
+     intros; solve_iso.
    Qed.
 
 .. coqtop:: in
 
-   Lemma isos_ex2 :
-       forall A B C:Set,
-         (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B).
+   Lemma solve_iso_ex2 :
+     forall A B C : Set,
+       (A * unit -> B * (C * unit)) =
+       (A * unit -> (C -> unit) * C) * (unit -> A -> B).
    Proof.
-   intros; IsoProve.
+     intros; solve_iso.
    Qed.