Detailed examples of tactics¶
This chapter presents detailed examples of certain tactics, to illustrate their behavior.
dependent induction¶
The tactics dependent induction
and dependent destruction
are another
solution for inverting inductive predicate instances and potentially
doing induction at the same time. It is based on the BasicElim
tactic
of Conor McBride which works by abstracting each argument of an
inductive instance by a variable and constraining it by equalities
afterwards. This way, the usual induction and destruct tactics can be
applied to the abstracted instance and after simplification of the
equalities we get the expected goals.
The abstracting tactic is called generalize_eqs and it takes as argument a 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:
 Require Import Coq.Logic.JMeq.
 Inductive Le : nat > nat > Set :=  LeO : forall n:nat, Le 0 n  LeS : forall n m:nat, Le n m > Le (S n) (S m).
 Le is defined Le_rect is defined Le_ind is defined Le_rec is defined
 Variable P : nat > nat > Prop.
 Toplevel input, characters 032: > Variable P : nat > nat > Prop. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: P is declared as a local axiom [localdeclaration,scope] P is declared
 Goal forall n m:nat, Le (S n) m > P n m.
 1 subgoal ============================ forall n m : nat, Le (S n) m > P n m
 intros n m H.
 1 subgoal n, m : nat H : Le (S n) m ============================ P n m
 generalize_eqs H.
 1 subgoal n, m, gen_x : nat H : Le gen_x m ============================ gen_x = S n > P n m
The index S n
gets abstracted by a variable here, but a corresponding
equality is added under the abstract instance so that no information
is actually lost. The goal is now almost amenable to do induction or
case analysis. One should indeed first move n
into the goal to
strengthen it before doing induction, or n
will be fixed in the
inductive hypotheses (this does not matter for case analysis). As a
rule of thumb, all the variables that appear inside constructors in
the indices of the hypothesis should be generalized. This is exactly
what the generalize_eqs_vars
variant does:
 generalize_eqs_vars H.
 induction H.
 2 subgoals n, n0 : nat ============================ 0 = S n > P n n0 subgoal 2 is: S n0 = S n > P n (S m)
As the hypothesis itself did not appear in the goal, we did not need to use an heterogeneous equality to relate the new hypothesis to the old one (which just disappeared here). However, the tactic works just as well in this case, e.g.:
 Abort.
 Variable Q : forall (n m : nat), Le n m > Prop.
 Toplevel input, characters 048: > Variable Q : forall (n m : nat), Le n m > Prop. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Q is declared as a local axiom [localdeclaration,scope] Q is declared
 Goal forall n m (p : Le (S n) m), Q (S n) m p.
 1 subgoal ============================ forall (n m : nat) (p : Le (S n) m), Q (S n) m p
 intros n m p.
 1 subgoal n, m : nat p : Le (S n) m ============================ Q (S n) m p
 generalize_eqs_vars p.
 1 subgoal m, gen_x : nat p : Le gen_x m ============================ forall (n : nat) (p0 : Le (S n) m), gen_x = S n > JMeq p p0 > Q (S n) m p0
One drawback of this approach is that in the branches one will have to
substitute the equalities back into the instance to get the right
assumptions. Sometimes injection of constructors will also be needed
to recover the needed equalities. Also, some subgoals should be
directly solved because of inconsistent contexts arising from the
constraints on 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 axiom K).
This is what the simplify_dep_elim
tactic from Coq.Program.Equality
does. For example, we might simplify the previous goals considerably:
 Require Import Coq.Program.Equality.
 induction p ; simplify_dep_elim.
 1 subgoal n, m : nat p : Le n m IHp : forall (n0 : nat) (p0 : Le (S n0) m), n = S n0 > p ~= p0 > Q (S n0) m p0 ============================ Q (S n) (S m) (LeS n m p)
The higherorder tactic do_depind
defined in Coq.Program.Equality
takes a tactic and combines the building blocks we have seen with it:
generalizing by equalities calling the given tactic with the
generalized induction hypothesis as argument and cleaning the subgoals
with respect to equalities. Its most important instantiations
are 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:
 Abort.
 Lemma ex : forall n m:nat, Le (S n) m > P n m.
 1 subgoal ============================ forall n m : nat, Le (S n) m > P n m
 intros n m H.
 1 subgoal n, m : nat H : Le (S n) m ============================ P n m
 dependent destruction H.
 1 subgoal n, m : nat H : Le n m ============================ P n (S m)
This gives essentially the same result as inversion. Now if the 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:
 Abort.
 Set Implicit Arguments.
 Variable A : Set.
 Toplevel input, characters 017: > Variable A : Set. > ^^^^^^^^^^^^^^^^^ Warning: A is declared as a local axiom [localdeclaration,scope] A is declared
 Inductive vector : nat > Type :=  vnil : vector 0  vcons : A > forall n, vector n > vector (S n).
 vector is defined vector_rect is defined vector_ind is defined vector_rec is defined
 Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'.
 1 subgoal ============================ forall (n : nat) (v : vector (S n)), exists (v' : vector n) (a : A), v = vcons a v'
 intros n v.
 1 subgoal n : nat v : vector (S n) ============================ exists (v' : vector n) (a : A), v = vcons a v'
 dependent destruction v.
 1 subgoal n : nat a : A v : vector n ============================ exists (v' : vector n) (a0 : A), vcons a v = vcons a0 v'
In this case, the v
variable can be replaced in the goal by the
generalized hypothesis only when it has a type of the form vector (S n)
,
that is only in the second case of the destruct. The first one is
dismissed because S n <> 0
.
A larger example¶
Let’s see how the technique works with induction on inductive predicates on a real example. We will develop an example application to the theory of simplytyped lambdacalculus formalized in a dependentlytyped style:
 Inductive type : Type :=  base : type  arrow : type > type > type.
 type is defined type_rect is defined type_ind is defined type_rec is defined
 Notation " t > t' " := (arrow t t') (at level 20, t' at next level).
 Inductive ctx : Type :=  empty : ctx  snoc : ctx > type > ctx.
 ctx is defined ctx_rect is defined ctx_ind is defined ctx_rec is defined
 Notation " G , tau " := (snoc G tau) (at level 20, tau at next level).
 Fixpoint conc (G D : ctx) : ctx := match D with  empty => G  snoc D' x => snoc (conc G D') x end.
 conc is defined conc is recursively defined (decreasing on 2nd argument)
 Notation " G ; D " := (conc G D) (at level 20).
 Inductive term : ctx > type > Type :=  ax : forall G tau, term (G, tau) tau  weak : forall G tau, term G tau > forall tau', term (G, tau') tau  abs : forall G tau tau', term (G , tau) tau' > term G (tau > tau')  app : forall G tau tau', term G (tau > tau') > term G tau > term G tau'.
 term is defined term_rect is defined term_ind is defined term_rec is defined
We have defined types and contexts which are snoclists of types. We
also have a conc
operation that concatenates two contexts. The term
datatype represents in fact the possible typing derivations of the
calculus, which are isomorphic to the welltyped terms, hence the
name. A term is either an application of:
the axiom rule to type a reference to the first variable in a context
the weakening rule to type an object in a larger context
the abstraction or lambda rule to type a function
the application to type an application of a function to an argument
Once we have this datatype we want to do proofs on it, like weakening:
 Lemma weakening : forall G D tau, term (G ; D) tau > forall tau', term (G , tau' ; D) tau.
 1 subgoal ============================ forall (G D : ctx) (tau : type), term (G; D) tau > forall tau' : type, term ((G, tau'); D) tau
 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:
 Lemma weakening' : forall G' tau, term G' tau > forall G D, (G ; D) = G' > forall tau', term (G, tau' ; D) tau.
 1 subgoal ============================ forall (G' : ctx) (tau : type), term G' tau > forall G D : ctx, G; D = G' > forall tau' : type, term ((G, tau'); D) tau
 Abort.
With this proper separation of the index from the instance and the
right induction loading (putting G
and D
after the inductedon
hypothesis), the proof will go through, but it is a very tedious
process. One is also forced to make a wrapper lemma to get back the
more natural statement. The dependent induction
tactic alleviates this
trouble by doing all of this plumbing of generalizing and substituting
back automatically. Indeed we can simply write:
 Require Import Coq.Program.Tactics.
 Require Import Coq.Program.Equality.
 Lemma weakening : forall G D tau, term (G ; D) tau > forall tau', term (G , tau' ; D) tau.
 1 subgoal ============================ forall (G D : ctx) (tau : type), term (G; D) tau > forall tau' : type, term ((G, tau'); D) tau
 Proof with simpl in * ; simpl_depind ; auto.
 intros G D tau H.
 1 subgoal G, D : ctx tau : type H : term (G; D) tau ============================ forall tau' : type, term ((G, tau'); D) tau
 dependent induction H generalizing G D ; intros.
 4 subgoals G0 : ctx tau : type G, D : ctx x : G0, tau = G; D tau' : type ============================ term ((G, tau'); D) tau subgoal 2 is: term ((G, tau'0); D) tau subgoal 3 is: term ((G, tau'0); D) (tau > tau') subgoal 4 is: term ((G, tau'0); D) tau'
This call to dependent induction has an additional arguments which is a list of variables appearing in the instance that should be generalized in the goal, so that they can vary in the induction hypotheses. By default, all variables appearing inside constructors (except in a parameter position) of the instantiated hypothesis will be generalized automatically but one can always give the list explicitly.
 Show.
 4 subgoals G0 : ctx tau : type G, D : ctx x : G0, tau = G; D tau' : type ============================ term ((G, tau'); D) tau subgoal 2 is: term ((G, tau'0); D) tau subgoal 3 is: term ((G, tau'0); D) (tau > tau') subgoal 4 is: term ((G, tau'0); D) tau'
The simpl_depind
tactic includes an automatic tactic that tries to
simplify equalities appearing at the beginning of induction
hypotheses, generally using trivial applications of reflexivity
. In
cases where the equality is not between constructor forms though, one
must help the automation by giving some arguments, using the
specialize
tactic for example.
 destruct D... apply weak; apply ax.
 5 subgoals G0 : ctx tau, tau' : type ============================ term ((G0, tau), tau') tau subgoal 2 is: term (((G, tau'); D), t) t subgoal 3 is: term ((G, tau'0); D) tau subgoal 4 is: term ((G, tau'0); D) (tau > tau') subgoal 5 is: term ((G, tau'0); D) tau' 4 subgoals G, D : ctx t, tau' : type ============================ term (((G, tau'); D), t) t subgoal 2 is: term ((G, tau'0); D) tau subgoal 3 is: term ((G, tau'0); D) (tau > tau') subgoal 4 is: term ((G, tau'0); D) tau'
 apply ax.
 3 subgoals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall G D : ctx, G0 = G; D > forall tau' : type, term ((G, tau'); D) tau G, D : ctx x : G0, tau' = G; D tau'0 : type ============================ term ((G, tau'0); D) tau subgoal 2 is: term ((G, tau'0); D) (tau > tau') subgoal 3 is: term ((G, tau'0); D) tau'
 destruct D...
 4 subgoals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall G D : ctx, G0 = G; D > forall tau' : type, term ((G, tau'); D) tau tau'0 : type ============================ term ((G0, tau'), tau'0) tau subgoal 2 is: term (((G, tau'0); D), t) tau subgoal 3 is: term ((G, tau'0); D) (tau > tau') subgoal 4 is: term ((G, tau'0); D) tau'
 Show.
 4 subgoals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall G D : ctx, G0 = G; D > forall tau' : type, term ((G, tau'); D) tau tau'0 : type ============================ term ((G0, tau'), tau'0) tau subgoal 2 is: term (((G, tau'0); D), t) tau subgoal 3 is: term ((G, tau'0); D) (tau > tau') subgoal 4 is: term ((G, tau'0); D) tau'
 specialize (IHterm G0 empty eq_refl).
 4 subgoals G0 : ctx tau : type H : term G0 tau tau' : type IHterm : forall tau' : type, term ((G0, tau'); empty) tau tau'0 : type ============================ term ((G0, tau'), tau'0) tau subgoal 2 is: term (((G, tau'0); D), t) tau subgoal 3 is: term ((G, tau'0); D) (tau > tau') subgoal 4 is: term ((G, tau'0); D) tau'
Once the induction hypothesis has been narrowed to the right equality, it can be used directly.
 apply weak, IHterm.
 3 subgoals tau : type G, D : ctx IHterm : forall G0 D0 : ctx, G; D = G0; D0 > forall tau' : type, term ((G0, tau'); D0) tau H : term (G; D) tau t, tau'0 : type ============================ term (((G, tau'0); D), t) tau subgoal 2 is: term ((G, tau'0); D) (tau > tau') subgoal 3 is: term ((G, tau'0); D) tau'
Now concluding this subgoal is easy.
 constructor; apply IHterm; reflexivity.
 2 subgoals G, D : ctx tau, tau' : type H : term ((G; D), tau) tau' IHterm : forall G0 D0 : ctx, (G; D), tau = G0; D0 > forall tau'0 : type, term ((G0, tau'0); D0) tau' tau'0 : type ============================ term ((G, tau'0); D) (tau > tau') subgoal 2 is: term ((G, tau'0); D) tau'
autorewrite¶
Here are two examples of autorewrite
use. The first one ( Ackermann
function) shows actually a quite basic use where there is no
conditional rewriting. The second one ( Mac Carthy function)
involves conditional rewritings and shows how to deal with them using
the optional tactic of the Hint Rewrite
command.
Example: Ackermann function
 Require Import Arith.
 [Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... done]
 Variable Ack : nat > nat > nat.
 Toplevel input, characters 033: > Variable Ack : nat > nat > nat. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: Ack is declared as a local axiom [localdeclaration,scope] Ack is declared
 Axiom Ack0 : forall m:nat, Ack 0 m = S m.
 Ack0 is declared
 Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
 Ack1 is declared
 Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
 Ack2 is declared
 Hint Rewrite Ack0 Ack1 Ack2 : base0.
 Lemma ResAck0 : Ack 3 2 = 29.
 1 subgoal ============================ Ack 3 2 = 29
 autorewrite with base0 using try reflexivity.
 No more subgoals.
Example: MacCarthy function
 Require Import Omega.
 [Loading ML file omega_plugin.cmxs ... done]
 Variable g : nat > nat > nat.
 Toplevel input, characters 031: > Variable g : nat > nat > nat. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning: g is declared as a local axiom [localdeclaration,scope] g is declared
 Axiom g0 : forall m:nat, g 0 m = m.
 g0 is declared
 Axiom g1 : forall n m:nat, (n > 0) > (m > 100) > g n m = g (pred n) (m  10).
 g1 is declared
 Axiom g2 : forall n m:nat, (n > 0) > (m <= 100) > g n m = g (S n) (m + 11).
 g2 is declared
 Hint Rewrite g0 g1 g2 using omega : base1.
 Lemma Resg0 : g 1 110 = 100.
 1 subgoal ============================ g 1 110 = 100
 Show.
 1 subgoal ============================ g 1 110 = 100
 autorewrite with base1 using reflexivity  simpl.
 No more subgoals.
 Qed.
 Resg0 is defined
 Lemma Resg1 : g 1 95 = 91.
 1 subgoal ============================ g 1 95 = 91
 autorewrite with base1 using reflexivity  simpl.
 No more subgoals.
 Qed.
 Resg1 is defined
quote¶
The tactic quote
allows using Barendregt’s socalled 2level approach
without writing any ML code. Suppose you have a language L
of
'abstract terms' and a type A
of 'concrete terms' and a function f : L > A
.
If L
is a simple inductive datatype and f
a simple fixpoint,
quote f
will replace the head of current goal by a convertible term of
the form (f t)
. L
must have a constructor of type: A > L
.
Here is an example:
 Require Import Quote.
 Parameters A B C : Prop.
 A is declared B is declared C is declared
 Inductive formula : Type :=  f_and : formula > formula > formula  f_or : formula > formula > formula  f_not : formula > formula  f_true : formula  f_const : Prop > formula .
 formula is defined formula_rect is defined formula_ind is defined formula_rec is defined
 Fixpoint interp_f (f:formula) : Prop := match f with  f_and f1 f2 => interp_f f1 /\ interp_f f2  f_or f1 f2 => interp_f f1 \/ interp_f f2  f_not f1 => ~ interp_f f1  f_true => True  f_const c => c end.
 interp_f is defined interp_f is recursively defined (decreasing on 1st argument)
 Goal A /\ (A \/ True) /\ ~ B /\ (A <> A).
 1 subgoal ============================ A /\ (A \/ True) /\ ~ B /\ (A <> A)
 quote interp_f.
 1 subgoal ============================ interp_f (f_and (f_const A) (f_and (f_or (f_const A) f_true) (f_and (f_not (f_const B)) (f_const (A <> A)))))
The algorithm to perform this inversion is: try to match the term with
righthand sides expression of f
. If there is a match, apply the
corresponding lefthand 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.
When quote
is not able to perform inversion properly, it will error out with
quote: not a simple fixpoint
.
Introducing variables map¶
The normal use of quote is to make proofs by reflection: one defines a
function simplify : formula > formula
and proves a theorem
simplify_ok: (f:formula)(interp_f (simplify f)) > (interp_f f)
. Then,
one can simplify formulas by doing:
 quote interp_f.
 1 subgoal ============================ interp_f (f_const (interp_f (f_and (f_const A) (f_and (f_or (f_const A) f_true) (f_and (f_not (f_const B)) (f_const (A <> A)))))))
 apply simplify_ok.
 Toplevel input, characters 617: > apply simplify_ok. > ^^^^^^^^^^^ Error: The reference simplify_ok was not found in the current environment.
 compute.
 1 subgoal ============================ A /\ (A \/ True) /\ (B > False) /\ (A > A) /\ (A > A)
But there is a problem with leafs: in the example above one cannot
write a function that implements, for example, the logical
simplifications \(A \wedge A \rightarrow A\) or \(A \wedge
\lnot A \rightarrow \mathrm{False}\). This is because Prop
is
impredicative.
It is better to use that type of formulas:
 Require Import Quote.
 Parameters A B C : Prop.
 A is declared B is declared C is declared
 Inductive formula : Set :=  f_and : formula > formula > formula  f_or : formula > formula > formula  f_not : formula > formula  f_true : formula  f_atom : index > formula.
 formula is defined formula_rect is defined formula_ind is defined formula_rec is defined
index
is defined in module Quote
. Equality on that type is
decidable so we are able to simplify \(A \wedge A\) into \(A\)
at the abstract level.
When there are variables, there are bindings, and quote
also
provides a type (varmap A)
of bindings from index to any set
A
, and a function varmap_find
to search in such maps. The
interpretation function also has another argument, a variables map:
 Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := match f with  f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2  f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2  f_not f1 => ~ interp_f vm f1  f_true => True  f_atom i => varmap_find True i vm end.
 interp_f is defined interp_f is recursively defined (decreasing on 2nd argument)
quote
handles this second case properly:
 Goal A /\ (B \/ A) /\ (A \/ ~ B).
 1 subgoal ============================ A /\ (B \/ A) /\ (A \/ ~ B)
 quote interp_f.
 1 subgoal ============================ interp_f (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop)) (f_and (f_atom (Left_idx End_idx)) (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx))) (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
It builds vm
and t
such that (f vm t)
is convertible with the
conclusion of current goal.
Combining variables and constants¶
One can have both variables and constants in abstracts terms; for
example, this is the case for the ring
tactic. Then one must provide to
quote
a list of constructors of constants. For example, if the list
is [O S]
then closed natural numbers will be considered as constants
and other terms as variables.
 Require Import Quote.
 Parameters A B C : Prop.
 A is declared B is declared C is declared
 Inductive formula : Type :=  f_and : formula > formula > formula  f_or : formula > formula > formula  f_not : formula > formula  f_true : formula  f_const : Prop > formula  f_atom : index > formula.
 formula is defined formula_rect is defined formula_ind is defined formula_rec is defined
 Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := match f with  f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2  f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2  f_not f1 => ~ interp_f vm f1  f_true => True  f_const c => c  f_atom i => varmap_find True i vm end.
 interp_f is defined interp_f is recursively defined (decreasing on 2nd argument)
 Goal A /\ (A \/ True) /\ ~ B /\ (C <> C).
 1 subgoal ============================ A /\ (A \/ True) /\ ~ B /\ (C <> C)
 quote interp_f [ A B ].
 1 subgoal ============================ interp_f (Node_vm (C <> C) (Empty_vm Prop) (Empty_vm Prop)) (f_and (f_const A) (f_and (f_or (f_const A) f_true) (f_and (f_not (f_const B)) (f_atom End_idx))))
 Undo.
 1 subgoal ============================ A /\ (A \/ True) /\ ~ B /\ (C <> C)
 quote interp_f [ B C iff ].
 1 subgoal ============================ interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_and (f_atom End_idx) (f_and (f_or (f_atom End_idx) f_true) (f_and (f_not (f_const B)) (f_const (C <> C)))))
警告
Since functional inversion is undecidable in the general case, don’t expect miracles from it!

Variant
quote ident in term using tactic
tactic
must be a functional tactic (starting withfun x =>
) and will be called with the quoted version of term according toident
.

Variant
quote ident [ident+] in term using tactic
Same as above, but will use the additional
ident
list to chose which subterms are constants (see above).
参考
Comments from the source file plugins/quote/quote.ml
参考
The ring
tactic.
Using the tactic language¶
About the cardinality of the set of natural numbers¶
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:
 Lemma card_nat : ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z.
 1 subgoal ============================ ~ (exists x y : nat, forall z : nat, x = z \/ y = z)
 Proof.
 red; intros (x, (y, Hy)).
 1 subgoal x, y : nat Hy : forall z : nat, x = z \/ y = z ============================ False
 elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; match goal with  _ : ?a = ?b, _ : ?a = ?c  _ => cut (b = c); [ discriminate  transitivity a; auto ] end.
 No more subgoals.
 Qed.
 card_nat is defined
We can notice that all the (very similar) cases coming from the three eliminations (with three distinct natural numbers) are successfully solved by a match goal structure and, in particular, with only one pattern (use of nonlinear matching).
Permutations of lists¶
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.
 Section Sort.
 Variable A : Set.
 A is declared
 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.
 perm is defined perm_ind is defined
 End Sort.
First, we define the permutation predicate as shown above.
 Require Import List.
 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.
 perm_aux is defined
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 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.
 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.
 solve_perm is defined
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:
 Lemma solve_perm_ex1 : perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
 1 subgoal ============================ perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil)
 Proof.
 solve_perm.
 No more subgoals.
 Qed.
 solve_perm_ex1 is defined
 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).
 1 subgoal ============================ 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.
 No more subgoals.
 Qed.
 solve_perm_ex2 is defined
Deciding intuitionistic propositional logic¶
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 contractionfree sequent calculi LJT* of Roy Dyckhoff [Dyc92], it is quite natural to code such a tactic using the tactic language as shown below.
 Ltac basic := match goal with   True => trivial  _ : False  _ => contradiction  _ : ?A  ?A => assumption end.
 basic is defined
 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).
 simplify is defined
 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.
 my_tauto is defined
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:
 Lemma my_tauto_ex1 : forall A B : Prop, A /\ B > A \/ B.
 1 subgoal ============================ forall A B : Prop, A /\ B > A \/ B
 Proof.
 my_tauto.
 No more subgoals.
 Qed.
 my_tauto_ex1 is defined
 Lemma my_tauto_ex2 : forall A B : Prop, (~ ~ B > B) > (A > B) > ~ ~ A > B.
 1 subgoal ============================ forall A B : Prop, (~ ~ B > B) > (A > B) > ~ ~ A > B
 Proof.
 my_tauto.
 No more subgoals.
 Qed.
 my_tauto_ex2 is defined
Deciding type isomorphisms¶
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, [dC95]). The axioms of this λcalculus are given below.
 Open Scope type_scope.
 Section Iso_axioms.
 Variables A B C : Set.
 A is declared B is declared C is declared
 Axiom Com : A * B = B * A.
 Com is declared
 Axiom Ass : A * (B * C) = A * B * C.
 Ass is declared
 Axiom Cur : (A * B > C) = (A > B > C).
 Cur is declared
 Axiom Dis : (A > B * C) = (A > B) * (A > C).
 Dis is declared
 Axiom P_unit : A * unit = A.
 P_unit is declared
 Axiom AR_unit : (A > unit) = unit.
 AR_unit is declared
 Axiom AL_unit : (unit > A) = A.
 AL_unit is declared
 Lemma Cons : B = C > A * B = A * C.
 1 subgoal A, B, C : Set ============================ B = C > A * B = A * C
 Proof.
 intro Heq; rewrite Heq; reflexivity.
 No more subgoals.
 Qed.
 Cons is defined
 End Iso_axioms.
 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.
 simplify_type is defined simplify_type_eq is defined
 Ltac len trm := match trm with  _ * ?B => let succ := len B in constr:(S succ)  _ => constr:(1) end.
 len is defined
 Ltac assoc := repeat rewrite < Ass.
 assoc is defined
 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.
 solve_type_eq is defined
 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.
 compare_structure is defined
 Ltac solve_iso := simplify_type_eq; compare_structure.
 solve_iso is defined
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 solve_iso
.
 Lemma solve_iso_ex1 : forall A B : Set, A * unit * B = B * (unit * A).
 1 subgoal ============================ forall A B : Set, A * unit * B = B * (unit * A)
 Proof.
 intros; solve_iso.
 No more subgoals.
 Qed.
 solve_iso_ex1 is defined
 Lemma solve_iso_ex2 : forall A B C : Set, (A * unit > B * (C * unit)) = (A * unit > (C > unit) * C) * (unit > A > B).
 1 subgoal ============================ forall A B C : Set, (A * unit > B * (C * unit)) = (A * unit > (C > unit) * C) * (unit > A > B)
 Proof.
 intros; solve_iso.
 No more subgoals.
 Qed.
 solve_iso_ex2 is defined