1
\chapter[Detailed examples of tactics]{Detailed examples of tactics\label{Tactics-examples}}
3
This chapter presents detailed examples of certain tactics, to
4
illustrate their behavior.
6
\section[\tt refine]{\tt refine\tacindex{refine}
7
\label{refine-example}}
9
This tactic applies to any goal. It behaves like {\tt exact} with a
10
big difference : the user can leave some holes (denoted by \texttt{\_} or
11
{\tt (\_:}{\it type}{\tt )}) in the term.
12
{\tt refine} will generate as many
13
subgoals as they are holes in the term. The type of holes must be
14
either synthesized by the system or declared by an
15
explicit cast like \verb|(\_:nat->Prop)|. This low-level
16
tactic can be useful to advanced users.
22
Inductive Option : Set :=
24
| Ok : bool -> Option.
27
Definition get : forall x:Option, x <> Fail -> bool.
30
match x return x <> Fail -> bool with
34
intros; absurd (Fail = Fail); trivial.
40
% \example{Using Refine to build a poor-man's ``Cases'' tactic}
42
% \texttt{Refine} is actually the only way for the user to do
43
% a proof with the same structure as a {\tt Cases} definition. Actually,
44
% the tactics \texttt{case} (see \ref{case}) and \texttt{Elim} (see
45
% \ref{elim}) only allow one step of elementary induction.
47
% \begin{coq_example*}
55
% Definition one_two_or_five := [x:nat]
62
% Goal (x:nat)(Is_true (one_two_or_five x)) -> x=(1)\/x=(2)\/x=(5).
65
% A traditional script would be the following:
67
% \begin{coq_example*}
80
% Intros; Inversion H.
83
% With the tactic \texttt{Refine}, it becomes quite shorter:
85
% \begin{coq_example*}
90
% <[y:nat](Is_true (one_two_or_five y))->(y=(1)\/y=(2)\/y=(5))>
95
% | n => [H](False_ind ? H)
102
\section[\tt eapply]{\tt eapply\tacindex{eapply}
103
\label{eapply-example}}
105
Assume we have a relation on {\tt nat} which is transitive:
108
Variable R : nat -> nat -> Prop.
109
Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z.
110
Variables n m p : nat.
111
Hypothesis Rnm : R n m.
112
Hypothesis Rmp : R m p.
115
Consider the goal {\tt (R n p)} provable using the transitivity of
122
The direct application of {\tt Rtrans} with {\tt apply} fails because
123
no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}:
126
Set Printing Depth 50.
127
(********** The following is not correct and should produce **********)
128
(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
134
A solution is to rather apply {\tt (Rtrans n m p)}.
137
apply (Rtrans n m p).
144
More elegantly, {\tt apply Rtrans with (y:=m)} allows to only mention
149
apply Rtrans with (y := m).
156
Another solution is to mention the proof of {\tt (R x y)} in {\tt
161
apply Rtrans with (1 := Rnm).
168
... or the proof of {\tt (R y z)}:
172
apply Rtrans with (2 := Rmp).
179
On the opposite, one can use {\tt eapply} which postpone the problem
180
of finding {\tt m}. Then one can apply the hypotheses {\tt Rnm} and {\tt
181
Rmp}. This instantiates the existential variable and completes the proof.
193
\section[{\tt Scheme}]{{\tt Scheme}\comindex{Scheme}
194
\label{Scheme-examples}}
197
\example{Induction scheme for \texttt{tree} and \texttt{forest}}
199
The definition of principle of mutual induction for {\tt tree} and
200
{\tt forest} over the sort {\tt Set} is defined by the command:
209
Inductive tree : Set :=
210
node : A -> forest -> tree
213
| cons : tree -> forest -> forest.
215
Scheme tree_forest_rec := Induction for tree Sort Set
216
with forest_tree_rec := Induction for forest Sort Set.
219
You may now look at the type of {\tt tree\_forest\_rec}:
222
Check tree_forest_rec.
225
This principle involves two different predicates for {\tt trees} and
226
{\tt forests}; it also has three premises each one corresponding to a
227
constructor of one of the inductive definitions.
229
The principle {\tt forest\_tree\_rec} shares exactly the same
230
premises, only the conclusion now refers to the property of forests.
233
Check forest_tree_rec.
236
\example{Predicates {\tt odd} and {\tt even} on naturals}
238
Let {\tt odd} and {\tt even} be inductively defined as:
242
Open Scope nat_scope.
246
Inductive odd : nat -> Prop :=
247
oddS : forall n:nat, even n -> odd (S n)
248
with even : nat -> Prop :=
250
| evenS : forall n:nat, odd n -> even (S n).
253
The following command generates a powerful elimination
257
Scheme odd_even := Minimality for odd Sort Prop
258
with even_odd := Minimality for even Sort Prop.
261
The type of {\tt odd\_even} for instance will be:
267
The type of {\tt even\_odd} shares the same premises but the
268
conclusion is {\tt (n:nat)(even n)->(Q n)}.
270
\subsection[{\tt Combined Scheme}]{{\tt Combined Scheme}\comindex{Combined Scheme}
271
\label{CombinedScheme-examples}}
273
We can define the induction principles for trees and forests using:
275
Scheme tree_forest_ind := Induction for tree Sort Prop
276
with forest_tree_ind := Induction for forest Sort Prop.
279
Then we can build the combined induction principle which gives the
280
conjunction of the conclusions of each individual principle:
282
Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
285
The type of {\tt tree\_forest\_mutrec} will be:
287
Check tree_forest_mutind.
290
\section[{\tt Functional Scheme} and {\tt functional induction}]{{\tt Functional Scheme} and {\tt functional induction}\comindex{Functional Scheme}\tacindex{functional induction}
291
\label{FunScheme-examples}}
294
\example{Induction scheme for \texttt{div2}}
296
We define the function \texttt{div2} as follows:
303
Require Import Arith.
304
Fixpoint div2 (n:nat) : nat :=
308
| S (S n') => S (div2 n')
312
The definition of a principle of induction corresponding to the
313
recursive structure of \texttt{div2} is defined by the command:
316
Functional Scheme div2_ind := Induction for div2 Sort Prop.
319
You may now look at the type of {\tt div2\_ind}:
325
We can now prove the following lemma using this principle:
329
Lemma div2_le' : forall n:nat, div2 n <= n.
331
pattern n , (div2 n).
336
apply div2_ind; intros.
342
simpl; auto with arith.
346
We can use directly the \texttt{functional induction}
347
(\ref{FunInduction}) tactic instead of the pattern/apply trick:
351
Lemma div2_le : forall n:nat, div2 n <= n.
356
functional induction (div2 n).
366
\Rem There is a difference between obtaining an induction scheme for a
367
function by using \texttt{Function} (see Section~\ref{Function}) and by
368
using \texttt{Functional Scheme} after a normal definition using
369
\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
373
\example{Induction scheme for \texttt{tree\_size}}
379
We define trees by the following mutual inductive type:
383
Inductive tree : Set :=
384
node : A -> forest -> tree
387
| cons : tree -> forest -> forest.
390
We define the function \texttt{tree\_size} that computes the size
391
of a tree or a forest. Note that we use \texttt{Function} which
392
generally produces better principles.
395
Function tree_size (t:tree) : nat :=
397
| node A f => S (forest_size f)
399
with forest_size (f:forest) : nat :=
402
| cons t f' => (tree_size t + forest_size f')
406
Remark: \texttt{Function} generates itself non mutual induction
407
principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
413
The definition of mutual induction principles following the recursive
414
structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
418
Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
419
with forest_size_ind2 := Induction for forest_size Sort Prop.
422
You may now look at the type of {\tt tree\_size\_ind2}:
425
Check tree_size_ind2.
431
\section[{\tt inversion}]{{\tt inversion}\tacindex{inversion}
432
\label{inversion-examples}}
434
\subsection*{Generalities about inversion}
436
When working with (co)inductive predicates, we are very often faced to
437
some of these situations:
439
\item we have an inconsistent instance of an inductive predicate in the
440
local context of hypotheses. Thus, the current goal can be trivially
442
\item we have a hypothesis that is an instance of an inductive
443
predicate, and the instance has some variables whose constraints we
444
would like to derive.
447
The inversion tactics are very useful to simplify the work in these
448
cases. Inversion tools can be classified in three groups:
451
\item tactics for inverting an instance without stocking the inversion
452
lemma in the context; this includes the tactics
453
(\texttt{dependent}) \texttt{inversion} and
454
(\texttt{dependent}) \texttt{inversion\_clear}.
455
\item commands for generating and stocking in the context the inversion
456
lemma corresponding to an instance; this includes \texttt{Derive}
457
(\texttt{Dependent}) \texttt{Inversion} and \texttt{Derive}
458
(\texttt{Dependent}) \texttt{Inversion\_clear}.
459
\item tactics for inverting an instance using an already defined
460
inversion lemma; this includes the tactic \texttt{inversion \ldots using}.
463
As inversion proofs may be large in size, we recommend the user to
464
stock the lemmas whenever the same instance needs to be inverted
468
\example{Non-dependent inversion}
470
Let's consider the relation \texttt{Le} over natural numbers and the
478
Inductive Le : nat -> nat -> Set :=
479
| LeO : forall n:nat, Le 0 n
480
| LeS : forall n m:nat, Le n m -> Le (S n) (S m).
481
Variable P : nat -> nat -> Prop.
482
Variable Q : forall n m:nat, Le n m -> Prop.
485
For example, consider the goal:
488
Lemma ex : forall n m:nat, Le (S n) m -> P n m.
496
To prove the goal we may need to reason by cases on \texttt{H} and to
497
derive that \texttt{m} is necessarily of
498
the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$.
499
Deriving these conditions corresponds to prove that the
500
only possible constructor of \texttt{(Le (S n) m)} is
501
\texttt{LeS} and that we can invert the
502
\texttt{->} in the type of \texttt{LeS}.
503
This inversion is possible because \texttt{Le} is the smallest set closed by
504
the constructors \texttt{LeO} and \texttt{LeS}.
510
Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)}
511
and that the hypothesis \texttt{(Le n m0)} has been added to the
515
interesting to have the equality \texttt{m=(S m0)} in the
516
context to use it after. In that case we can use \texttt{inversion} that
517
does not clear the equalities:
531
\example{Dependent Inversion}
533
Let us consider the following goal:
536
Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H.
544
As \texttt{H} occurs in the goal, we may want to reason by cases on its
545
structure and so, we would like inversion tactics to
546
substitute \texttt{H} by the corresponding term in constructor form.
547
Neither \texttt{Inversion} nor {\tt Inversion\_clear} make such a
549
To have such a behavior we use the dependent inversion tactics:
552
dependent inversion_clear H.
555
Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
556
\texttt{m} by \texttt{(S m0)}.
558
\example{using already defined inversion lemmas}
564
For example, to generate the inversion lemma for the instance
565
\texttt{(Le (S n) m)} and the sort \texttt{Prop} we do:
568
Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort
576
Then we can use the proven inversion lemma:
583
inversion H using leminv.
590
\section[\tt dependent induction]{\tt dependent induction\label{dependent-induction-example}}
591
\def\depind{{\tt dependent induction}~}
592
\def\depdestr{{\tt dependent destruction}~}
594
The tactics \depind and \depdestr are another solution for inverting
595
inductive predicate instances and potentially doing induction at the
596
same time. It is based on the \texttt{BasicElim} tactic of Conor McBride which
597
works by abstracting each argument of an inductive instance by a variable
598
and constraining it by equalities afterwards. This way, the usual
599
{\tt induction} and {\tt destruct} tactics can be applied to the
600
abstracted instance and after simplification of the equalities we get
603
The abstracting tactic is called {\tt generalize\_eqs} and it takes as
604
argument an hypothesis to generalize. It uses the {\tt JMeq} datatype
605
defined in {\tt Coq.Logic.JMeq}, hence we need to require it before.
606
For example, revisiting the first example of the inversion documentation above:
609
Require Import Coq.Logic.JMeq.
612
Require Import Coq.Program.Equality.
616
Inductive Le : nat -> nat -> Set :=
617
| LeO : forall n:nat, Le 0 n
618
| LeS : forall n m:nat, Le n m -> Le (S n) (S m).
619
Variable P : nat -> nat -> Prop.
620
Variable Q : forall n m:nat, Le n m -> Prop.
624
Goal forall n m:nat, Le (S n) m -> P n m.
631
The index {\tt S n} gets abstracted by a variable here, but a
632
corresponding equality is added under the abstract instance so that no
633
information is actually lost. The goal is now almost ammenable to do induction
634
or case analysis. One should indeed first move {\tt n} into the goal to
635
strengthen it before doing induction, or {\tt n} will be fixed in
636
the inductive hypotheses (this does not matter for case analysis).
637
As a rule of thumb, all the variables that appear inside constructors in
638
the indices of the hypothesis should be generalized. This is exactly
639
what the \texttt{generalize\_eqs\_vars} variant does:
645
generalize_eqs_vars H.
649
As the hypothesis itself did not appear in the goal, we did not need to
650
use an heterogeneous equality to relate the new hypothesis to the old
651
one (which just disappeared here). However, the tactic works just a well
659
Goal forall n m (p : Le (S n) m), Q (S n) m p.
660
intros n m p ; generalize_eqs_vars p.
663
One drawback of this approach is that in the branches one will have to
664
substitute the equalities back into the instance to get the right
665
assumptions. Sometimes injection of constructors will also be needed to
666
recover the needed equalities. Also, some subgoals should be directly
667
solved because of inconsistent contexts arising from the constraints on
668
indices. The nice thing is that we can make a tactic based on
669
discriminate, injection and variants of substitution to automatically
670
do such simplifications (which may involve the K axiom).
671
This is what the {\tt simplify\_dep\_elim} tactic from
672
{\tt Coq.Program.Equality} does. For example, we might simplify the
673
previous goals considerably:
676
% Goal forall n m:nat, Le (S n) m -> P n m.
677
% intros n m H ; generalize_eqs_vars H.
681
induction p ; simplify_dep_elim.
684
The higher-order tactic {\tt do\_depind} defined in {\tt
685
Coq.Program.Equality} takes a tactic and combines the
686
building blocks we've seen with it: generalizing by equalities
687
calling the given tactic with the
688
generalized induction hypothesis as argument and cleaning the subgoals
689
with respect to equalities. Its most important instantiations are
690
\depind and \depdestr that do induction or simply case analysis on the
691
generalized hypothesis. For example we can redo what we've done manually
698
Require Import Coq.Program.Equality.
699
Lemma ex : forall n m:nat, Le (S n) m -> P n m.
703
dependent destruction H.
709
This gives essentially the same result as inversion. Now if the
710
destructed hypothesis actually appeared in the goal, the tactic would
711
still be able to invert it, contrary to {\tt dependent
712
inversion}. Consider the following example on vectors:
715
Require Import Coq.Program.Equality.
716
Set Implicit Arguments.
718
Inductive vector : nat -> Type :=
720
| vcons : A -> forall n, vector n -> vector (S n).
721
Goal forall n, forall v : vector (S n),
722
exists v' : vector n, exists a : A, v = vcons a v'.
726
dependent destruction v.
732
In this case, the {\tt v} variable can be replaced in the goal by the
733
generalized hypothesis only when it has a type of the form {\tt vector
734
(S n)}, that is only in the second case of the {\tt destruct}. The
735
first one is dismissed because {\tt S n <> 0}.
737
\subsection{A larger example}
739
Let's see how the technique works with {\tt induction} on inductive
740
predicates on a real example. We will develop an example application to the
741
theory of simply-typed lambda-calculus formalized in a dependently-typed style:
744
Inductive type : Type :=
746
| arrow : type -> type -> type.
747
Notation " t --> t' " := (arrow t t') (at level 20, t' at next level).
748
Inductive ctx : Type :=
750
| snoc : ctx -> type -> ctx.
751
Notation " G , tau " := (snoc G tau) (at level 20, t at next level).
752
Fixpoint conc (G D : ctx) : ctx :=
755
| snoc D' x => snoc (conc G D') x
757
Notation " G ; D " := (conc G D) (at level 20).
758
Inductive term : ctx -> type -> Type :=
759
| ax : forall G tau, term (G, tau) tau
760
| weak : forall G tau,
761
term G tau -> forall tau', term (G, tau') tau
762
| abs : forall G tau tau',
763
term (G , tau) tau' -> term G (tau --> tau')
764
| app : forall G tau tau',
765
term G (tau --> tau') -> term G tau -> term G tau'.
768
We have defined types and contexts which are snoc-lists of types. We
769
also have a {\tt conc} operation that concatenates two contexts.
770
The {\tt term} datatype represents in fact the possible typing
771
derivations of the calculus, which are isomorphic to the well-typed
772
terms, hence the name. A term is either an application of:
774
\item the axiom rule to type a reference to the first variable in a context,
775
\item the weakening rule to type an object in a larger context
776
\item the abstraction or lambda rule to type a function
777
\item the application to type an application of a function to an argument
780
Once we have this datatype we want to do proofs on it, like weakening:
783
Lemma weakening : forall G D tau, term (G ; D) tau ->
784
forall tau', term (G , tau' ; D) tau.
790
The problem here is that we can't just use {\tt induction} on the typing
791
derivation because it will forget about the {\tt G ; D} constraint
792
appearing in the instance. A solution would be to rewrite the goal as:
794
Lemma weakening' : forall G' tau, term G' tau ->
795
forall G D, (G ; D) = G' ->
796
forall tau', term (G, tau' ; D) tau.
802
With this proper separation of the index from the instance and the right
803
induction loading (putting {\tt G} and {\tt D} after the inducted-on
804
hypothesis), the proof will go through, but it is a very tedious
805
process. One is also forced to make a wrapper lemma to get back the
806
more natural statement. The \depind tactic aleviates this trouble by
807
doing all of this plumbing of generalizing and substituting back automatically.
808
Indeed we can simply write:
811
Require Import Coq.Program.Tactics.
812
Lemma weakening : forall G D tau, term (G ; D) tau ->
813
forall tau', term (G , tau' ; D) tau.
814
Proof with simpl in * ; simpl_depind ; auto.
815
intros G D tau H. dependent induction H generalizing G D ; intros.
818
This call to \depind has an additional arguments which is a list of
819
variables appearing in the instance that should be generalized in the
820
goal, so that they can vary in the induction hypotheses. By default, all
821
variables appearing inside constructors (except in a parameter position)
822
of the instantiated hypothesis will be generalized automatically but
823
one can always give the list explicitely.
829
The {\tt simpl\_depind} tactic includes an automatic tactic that tries
830
to simplify equalities appearing at the beginning of induction
831
hypotheses, generally using trivial applications of
832
reflexiviy. In cases where the equality is not between constructor
833
forms though, one must help the automation by giving
834
some arguments, using the {\tt specialize} tactic.
837
destruct D... apply weak ; apply ax. apply ax.
844
specialize (IHterm G empty).
847
Then the automation can find the needed equality {\tt G = G} to narrow
848
the induction hypothesis further. This concludes our example.
854
\SeeAlso The induction \ref{elim}, case \ref{case} and inversion \ref{inversion} tactics.
856
\section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}
858
Here are two examples of {\tt autorewrite} use. The first one ({\em Ackermann
859
function}) shows actually a quite basic use where there is no conditional
860
rewriting. The second one ({\em Mac Carthy function}) involves conditional
861
rewritings and shows how to deal with them using the optional tactic of the
862
{\tt Hint~Rewrite} command.
865
\example{Ackermann function}
866
%Here is a basic use of {\tt AutoRewrite} with the Ackermann function:
869
Require Import Arith.
873
forall m:nat, Ack 0 m = S m.
874
Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
875
Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
879
Hint Rewrite Ack0 Ack1 Ack2 : base0.
882
autorewrite with base0 using try reflexivity.
889
\example{Mac Carthy function}
890
%The Mac Carthy function shows a more complex case:
893
Require Import Omega.
897
forall m:nat, g 0 m = m.
901
(n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
905
(n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
909
Hint Rewrite g0 g1 g2 using omega : base1.
912
autorewrite with base1 using reflexivity || simpl.
920
Lemma Resg1 : g 1 95 = 91.
921
autorewrite with base1 using reflexivity || simpl.
928
\section[\tt quote]{\tt quote\tacindex{quote}
929
\label{quote-examples}}
931
The tactic \texttt{quote} allows to use Barendregt's so-called
932
2-level approach without writing any ML code. Suppose you have a
933
language \texttt{L} of
934
'abstract terms' and a type \texttt{A} of 'concrete terms'
935
and a function \texttt{f : L -> A}. If \texttt{L} is a simple
936
inductive datatype and \texttt{f} a simple fixpoint, \texttt{quote f}
937
will replace the head of current goal by a convertible term of the form
938
\texttt{(f t)}. \texttt{L} must have a constructor of type: \texttt{A
944
Require Import Quote.
945
Parameters A B C : Prop.
946
Inductive formula : Type :=
947
| f_and : formula -> formula -> formula (* binary constructor *)
948
| f_or : formula -> formula -> formula
949
| f_not : formula -> formula (* unary constructor *)
950
| f_true : formula (* 0-ary constructor *)
951
| f_const : Prop -> formula (* contructor for constants *).
952
Fixpoint interp_f (f:
955
| f_and f1 f2 => interp_f f1 /\ interp_f f2
956
| f_or f1 f2 => interp_f f1 \/ interp_f f2
957
| f_not f1 => ~ interp_f f1
961
Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A).
965
The algorithm to perform this inversion is: try to match the
966
term with right-hand sides expression of \texttt{f}. If there is a
967
match, apply the corresponding left-hand side and call yourself
968
recursively on sub-terms. If there is no match, we are at a leaf:
969
return the corresponding constructor (here \texttt{f\_const}) applied
973
\item \errindex{quote: not a simple fixpoint} \\
974
Happens when \texttt{quote} is not able to perform inversion properly.
977
\subsection{Introducing variables map}
979
The normal use of \texttt{quote} is to make proofs by reflection: one
980
defines a function \texttt{simplify : formula -> formula} and proves a
981
theorem \texttt{simplify\_ok: (f:formula)(interp\_f (simplify f)) ->
982
(interp\_f f)}. Then, one can simplify formulas by doing:
988
But there is a problem with leafs: in the example above one cannot
989
write a function that implements, for example, the logical simplifications
990
$A \land A \ra A$ or $A \land \lnot A \ra \texttt{False}$. This is
991
because the \Prop{} is impredicative.
993
It is better to use that type of formulas:
999
Inductive formula : Set :=
1000
| f_and : formula -> formula -> formula
1001
| f_or : formula -> formula -> formula
1002
| f_not : formula -> formula
1004
| f_atom : index -> formula.
1007
\texttt{index} is defined in module \texttt{quote}. Equality on that
1008
type is decidable so we are able to simplify $A \land A$ into $A$ at
1011
When there are variables, there are bindings, and \texttt{quote}
1012
provides also a type \texttt{(varmap A)} of bindings from
1013
\texttt{index} to any set \texttt{A}, and a function
1014
\texttt{varmap\_find} to search in such maps. The interpretation
1015
function has now another argument, a variables map:
1018
Fixpoint interp_f (vm:
1019
varmap Prop) (f:formula) {struct f} : Prop :=
1021
| f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
1022
| f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
1023
| f_not f1 => ~ interp_f vm f1
1025
| f_atom i => varmap_find True i vm
1029
\noindent\texttt{quote} handles this second case properly:
1032
Goal A /\ (B \/ A) /\ (A \/ ~ B).
1036
It builds \texttt{vm} and \texttt{t} such that \texttt{(f vm t)} is
1037
convertible with the conclusion of current goal.
1039
\subsection{Combining variables and constants}
1041
One can have both variables and constants in abstracts terms; that is
1042
the case, for example, for the \texttt{ring} tactic (chapter
1043
\ref{ring}). Then one must provide to \texttt{quote} a list of
1044
\emph{constructors of constants}. For example, if the list is
1045
\texttt{[O S]} then closed natural numbers will be considered as
1046
constants and other terms as variables.
1053
\begin{coq_example*}
1054
Inductive formula : Type :=
1055
| f_and : formula -> formula -> formula
1056
| f_or : formula -> formula -> formula
1057
| f_not : formula -> formula
1059
| f_const : Prop -> formula (* constructor for constants *)
1060
| f_atom : index -> formula.
1062
(vm: (* constructor for variables *)
1063
varmap Prop) (f:formula) {struct f} : Prop :=
1065
| f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
1066
| f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
1067
| f_not f1 => ~ interp_f vm f1
1070
| f_atom i => varmap_find True i vm
1073
A /\ (A \/ True) /\ ~ B /\ (C <-> C).
1077
quote interp_f [ A B ].
1079
quote interp_f [ B C iff ].
1082
\Warning Since function inversion
1083
is undecidable in general case, don't expect miracles from it!
1085
% \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}
1087
\SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
1089
\SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring})
1093
\section{Using the tactical language}
1095
\subsection{About the cardinality of the set of natural numbers}
1097
A first example which shows how to use the pattern matching over the proof
1098
contexts is the proof that natural numbers have more than two elements. The
1099
proof of such a lemma can be done as %shown on Figure~\ref{cnatltac}.
1102
%\begin{centerframe}
1105
Require Import Arith.
1106
Require Import List.
1108
\begin{coq_example*}
1110
~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
1112
red; intros (x, (y, Hy)).
1113
elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
1115
| [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
1116
cut (b = c); [ discriminate | apply trans_equal with a; auto ]
1121
%\caption{A proof on cardinality of natural numbers}
1125
We can notice that all the (very similar) cases coming from the three
1126
eliminations (with three distinct natural numbers) are successfully solved by
1127
a {\tt match goal} structure and, in particular, with only one pattern (use
1128
of non-linear matching).
1130
\subsection{Permutation on closed lists}
1132
Another more complex example is the problem of permutation on closed lists. The
1133
aim is to show that a closed list is a permutation of another one.
1135
First, we define the permutation predicate as shown in table~\ref{permutpred}.
1139
\begin{coq_example*}
1142
Inductive permut : list A -> list A -> Prop :=
1143
| permut_refl : forall l, permut l l
1145
forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
1146
| permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
1148
forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
1152
\caption{Definition of the permutation predicate}
1156
A more complex example is the problem of permutation on closed lists.
1157
The aim is to show that a closed list is a permutation of another one.
1158
First, we define the permutation predicate as shown on
1159
Figure~\ref{permutpred}.
1166
| |- (permut _ ?l ?l) => apply permut_refl
1167
| |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
1168
let newn := eval compute in (length l1) in
1169
(apply permut_cons; Permut newn)
1170
| |- (permut ?A (?a :: ?l1) ?l2) =>
1171
match eval compute in n with
1174
let l1' := constr:(l1 ++ a :: nil) in
1175
(apply (permut_trans A (a :: l1) l1' l2);
1176
[ apply permut_append | compute; Permut (pred n) ])
1181
| |- (permut _ ?l1 ?l2) =>
1182
match eval compute in (length l1 = length l2) with
1183
| (?n = ?n) => Permut n
1188
\caption{Permutation tactic}
1192
Next, we can write naturally the tactic and the result can be seen on
1193
Figure~\ref{permutltac}. We can notice that we use two toplevel
1194
definitions {\tt PermutProve} and {\tt Permut}. The function to be
1195
called is {\tt PermutProve} which computes the lengths of the two
1196
lists and calls {\tt Permut} with the length if the two lists have the
1197
same length. {\tt Permut} works as expected. If the two lists are
1198
equal, it concludes. Otherwise, if the lists have identical first
1199
elements, it applies {\tt Permut} on the tail of the lists. Finally,
1200
if the lists have different first elements, it puts the first element
1201
of one of the lists (here the second one which appears in the {\tt
1202
permut} predicate) at the end if that is possible, i.e., if the new
1203
first element has been at this place previously. To verify that all
1204
rotations have been done for a list, we use the length of the list as
1205
an argument for {\tt Permut} and this length is decremented for each
1206
rotation down to, but not including, 1 because for a list of length
1207
$n$, we can make exactly $n-1$ rotations to generate at most $n$
1208
distinct lists. Here, it must be noticed that we use the natural
1209
numbers of {\Coq} for the rotation counter. On Figure~\ref{ltac}, we
1210
can see that it is possible to use usual natural numbers but they are
1211
only used as arguments for primitive tactics and they cannot be
1212
handled, in particular, we cannot make computations with them. So, a
1213
natural choice is to use {\Coq} data structures so that {\Coq} makes
1214
the computations (reductions) by {\tt eval compute in} and we can get
1215
the terms back by {\tt match}.
1217
With {\tt PermutProve}, we can now prove lemmas as
1218
% shown on Figure~\ref{permutlem}.
1221
%\begin{centerframe}
1223
\begin{coq_example*}
1225
permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
1226
Proof. PermutProve. Qed.
1229
(0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
1230
(0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
1231
Proof. PermutProve. Qed.
1234
%\caption{Examples of {\tt PermutProve} use}
1239
\subsection{Deciding intuitionistic propositional logic}
1246
| |- True => trivial
1247
| _:False |- _ => elimtype False; assumption
1248
| _:?A |- ?A => auto
1252
\caption{Deciding intuitionistic propositions (1)}
1264
| id:(~ _) |- _ => red in id
1265
| id:(_ /\ _) |- _ =>
1266
elim id; do 2 intro; clear id
1267
| id:(_ \/ _) |- _ =>
1268
elim id; intro; clear id
1269
| id:(?A /\ ?B -> ?C) |- _ =>
1271
[ intro | intros; apply id; split; assumption ]
1272
| id:(?A \/ ?B -> ?C) |- _ =>
1276
| intro; apply id; left; assumption ]
1277
| intro; apply id; right; assumption ]
1278
| id0:(?A -> ?B),id1:?A |- _ =>
1279
cut B; [ intro; clear id0 | apply id0; assumption ]
1280
| |- (_ /\ _) => split
1287
| id:((?A -> ?B) -> ?C) |- _ =>
1289
[ intro; cut (A -> B);
1291
[ intro; clear id | apply id; assumption ]
1293
| intro; apply id; intro; assumption ]; TautoProp
1294
| id:(~ ?A -> ?B) |- _ =>
1296
[ intro; cut (A -> False);
1298
[ intro; clear id | apply id; assumption ]
1300
| intro; apply id; red; intro; assumption ]; TautoProp
1301
| |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
1305
\caption{Deciding intuitionistic propositions (2)}
1309
The pattern matching on goals allows a complete and so a powerful
1310
backtracking when returning tactic values. An interesting application
1311
is the problem of deciding intuitionistic propositional logic.
1312
Considering the contraction-free sequent calculi {\tt LJT*} of
1313
Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic
1314
using the tactic language as shown on Figures~\ref{tautoltaca}
1315
and~\ref{tautoltacb}. The tactic {\tt Axioms} tries to conclude using
1316
usual axioms. The tactic {\tt DSimplif} applies all the reversible
1317
rules of Dyckhoff's system. Finally, the tactic {\tt TautoProp} (the
1318
main tactic to be called) simplifies with {\tt DSimplif}, tries to
1319
conclude with {\tt Axioms} and tries several paths using the
1320
backtracking rules (one of the four Dyckhoff's rules for the left
1321
implication to get rid of the contraction and the right or).
1323
For example, with {\tt TautoProp}, we can prove tautologies like
1325
% on Figure~\ref{tautolem}.
1326
%\begin{figure}[tbp]
1327
%\begin{centerframe}
1328
\begin{coq_example*}
1329
Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
1330
Proof. TautoProp. Qed.
1332
forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
1333
Proof. TautoProp. Qed.
1336
%\caption{Proofs of tautologies with {\tt TautoProp}}
1340
\subsection{Deciding type isomorphisms}
1342
A more tricky problem is to decide equalities between types and modulo
1343
isomorphisms. Here, we choose to use the isomorphisms of the simply typed
1344
$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
1345
\cite{RC95}). The axioms of this $\lb{}$-calculus are given by
1353
\begin{coq_example*}
1354
Open Scope type_scope.
1356
Variables A B C : Set.
1357
Axiom Com : A * B = B * A.
1358
Axiom Ass : A * (B * C) = A * B * C.
1359
Axiom Cur : (A * B -> C) = (A -> B -> C).
1360
Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
1361
Axiom P_unit : A * unit = A.
1362
Axiom AR_unit : (A -> unit) = unit.
1363
Axiom AL_unit : (unit -> A) = A.
1364
Lemma Cons : B = C -> A * B = A * C.
1366
intro Heq; rewrite Heq; apply refl_equal.
1371
\caption{Type isomorphism axioms}
1375
A more tricky problem is to decide equalities between types and modulo
1376
isomorphisms. Here, we choose to use the isomorphisms of the simply typed
1377
$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
1378
\cite{RC95}). The axioms of this $\lb{}$-calculus are given on
1379
Figure~\ref{isosax}.
1384
Ltac DSimplif trm :=
1387
rewrite <- (Ass A B C); try MainSimplif
1388
| (?A * ?B -> ?C) =>
1389
rewrite (Cur A B C); try MainSimplif
1390
| (?A -> ?B * ?C) =>
1391
rewrite (Dis A B C); try MainSimplif
1393
rewrite (P_unit A); try MainSimplif
1395
rewrite (Com unit B); try MainSimplif
1397
rewrite (AR_unit A); try MainSimplif
1399
rewrite (AL_unit B); try MainSimplif
1401
(DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
1403
(DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
1407
| |- (?A = ?B) => try DSimplif A; try DSimplif B
1411
| (_ * ?B) => let succ := Length B in constr:(S succ)
1414
Ltac assoc := repeat rewrite <- Ass.
1417
\caption{Type isomorphism tactic (1)}
1426
| [ |- (?A = ?A) ] => apply refl_equal
1427
| [ |- (?A * ?B = ?A * ?C) ] =>
1428
apply Cons; let newn := Length B in
1430
| [ |- (?A * ?B = ?C) ] =>
1431
match eval compute in n with
1434
pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
1437
Ltac CompareStruct :=
1439
| [ |- (?A = ?B) ] =>
1441
with l2 := Length B in
1442
match eval compute in (l1 = l2) with
1443
| (?n = ?n) => DoCompare n
1446
Ltac IsoProve := MainSimplif; CompareStruct.
1449
\caption{Type isomorphism tactic (2)}
1453
The tactic to judge equalities modulo this axiomatization can be written as
1454
shown on Figures~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
1455
simple. Types are reduced using axioms that can be oriented (this done by {\tt
1456
MainSimplif}). The normal forms are sequences of Cartesian
1457
products without Cartesian product in the left component. These normal forms
1458
are then compared modulo permutation of the components (this is done by {\tt
1459
CompareStruct}). The main tactic to be called and realizing this algorithm is
1462
% Figure~\ref{isoslem} gives
1463
Here are examples of what can be solved by {\tt IsoProve}.
1465
%\begin{centerframe}
1466
\begin{coq_example*}
1468
forall A B:Set, A * unit * B = B * (unit * A).
1475
(A * unit -> B * (C * unit)) =
1476
(A * unit -> (C -> unit) * C) * (unit -> A -> B).
1482
%\caption{Type equalities solved by {\tt IsoProve}}
1486
%%% Local Variables:
1488
%%% TeX-master: "Reference-Manual"
added
removed
doc/refman/RefMan-tacex.tex
