1
\chapter{Detailed examples of tactics}
2
\label{Tactics-examples}
4
This chapter presents detailed examples of certain tactics, to
5
illustrate their behavior.
11
This tactic applies to any goal. It behaves like {\tt exact} with a
12
big difference : the user can leave some holes (denoted by \texttt{\_} or
13
{\tt (\_:}{\it type}{\tt )}) in the term.
14
{\tt refine} will generate as many
15
subgoals as they are holes in the term. The type of holes must be
16
either synthesized by the system or declared by an
17
explicit cast like \verb|(\_:nat->Prop)|. This low-level
18
tactic can be useful to advanced users.
24
Inductive Option : Set :=
26
| Ok : bool -> Option.
29
Definition get : forall x:Option, x <> Fail -> bool.
32
match x return x <> Fail -> bool with
36
intros; absurd (Fail = Fail); trivial.
42
% \example{Using Refine to build a poor-man's ``Cases'' tactic}
44
% \texttt{Refine} is actually the only way for the user to do
45
% a proof with the same structure as a {\tt Cases} definition. Actually,
46
% the tactics \texttt{case} (see \ref{case}) and \texttt{Elim} (see
47
% \ref{elim}) only allow one step of elementary induction.
49
% \begin{coq_example*}
57
% Definition one_two_or_five := [x:nat]
64
% Goal (x:nat)(Is_true (one_two_or_five x)) -> x=(1)\/x=(2)\/x=(5).
67
% A traditional script would be the following:
69
% \begin{coq_example*}
82
% Intros; Inversion H.
85
% With the tactic \texttt{Refine}, it becomes quite shorter:
87
% \begin{coq_example*}
92
% <[y:nat](Is_true (one_two_or_five y))->(y=(1)\/y=(2)\/y=(5))>
97
% | n => [H](False_ind ? H)
106
\label{eapply-example}
108
Assume we have a relation on {\tt nat} which is transitive:
111
Variable R : nat -> nat -> Prop.
112
Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z.
113
Variables n m p : nat.
114
Hypothesis Rnm : R n m.
115
Hypothesis Rmp : R m p.
118
Consider the goal {\tt (R n p)} provable using the transitivity of
125
The direct application of {\tt Rtrans} with {\tt apply} fails because
126
no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}:
129
Set Printing Depth 50.
130
(********** The following is not correct and should produce **********)
131
(**** Error: generated subgoal (R n ?17) has metavariables in it *****)
137
A solution is to rather apply {\tt (Rtrans n m p)}.
140
apply (Rtrans n m p).
147
More elegantly, {\tt apply Rtrans with (y:=m)} allows to only mention
152
apply Rtrans with (y := m).
159
Another solution is to mention the proof of {\tt (R x y)} in {\tt
164
apply Rtrans with (1 := Rnm).
171
... or the proof of {\tt (R y z)}:
175
apply Rtrans with (2 := Rmp).
182
On the opposite, one can use {\tt eapply} which postpone the problem
183
of finding {\tt m}. Then one can apply the hypotheses {\tt Rnm} and {\tt
184
Rmp}. This instantiates the existential variable and completes the proof.
196
\section{{\tt Scheme}}
198
\label{Scheme-examples}
201
\example{Induction scheme for \texttt{tree} and \texttt{forest}}
203
The definition of principle of mutual induction for {\tt tree} and
204
{\tt forest} over the sort {\tt Set} is defined by the command:
213
Inductive tree : Set :=
214
node : A -> forest -> tree
217
| cons : tree -> forest -> forest.
219
Scheme tree_forest_rec := Induction for tree Sort Set
220
with forest_tree_rec := Induction for forest Sort Set.
223
You may now look at the type of {\tt tree\_forest\_rec}:
226
Check tree_forest_rec.
229
This principle involves two different predicates for {\tt trees} and
230
{\tt forests}; it also has three premises each one corresponding to a
231
constructor of one of the inductive definitions.
233
The principle {\tt tree\_forest\_rec} shares exactly the same
234
premises, only the conclusion now refers to the property of forests.
237
Check forest_tree_rec.
240
\example{Predicates {\tt odd} and {\tt even} on naturals}
242
Let {\tt odd} and {\tt even} be inductively defined as:
246
Open Scope nat_scope.
250
Inductive odd : nat -> Prop :=
251
oddS : forall n:nat, even n -> odd (S n)
252
with even : nat -> Prop :=
254
| evenS : forall n:nat, odd n -> even (S n).
257
The following command generates a powerful elimination
261
Scheme odd_even := Minimality for odd Sort Prop
262
with even_odd := Minimality for even Sort Prop.
265
The type of {\tt odd\_even} for instance will be:
271
The type of {\tt even\_odd} shares the same premises but the
272
conclusion is {\tt (n:nat)(even n)->(Q n)}.
274
\section{{\tt Functional Scheme} and {\tt functional induction}}
275
\comindex{Functional Scheme}\tacindex{functional induction}
276
\label{FunScheme-examples}
279
\example{Induction scheme for \texttt{div2}}
281
We define the function \texttt{div2} as follows:
288
Require Import Arith.
289
Fixpoint div2 (n:nat) : nat :=
293
| S (S n') => S (div2 n')
297
The definition of a principle of induction corresponding to the
298
recursive structure of \texttt{div2} is defined by the command:
301
Functional Scheme div2_ind := Induction for div2 Sort Prop.
304
You may now look at the type of {\tt div2\_ind}:
310
We can now prove the following lemma using this principle:
314
Lemma div2_le' : forall n:nat, div2 n <= n.
316
pattern n , (div2 n).
321
apply div2_ind; intros.
327
simpl; auto with arith.
331
We can use directly the \texttt{functional induction}
332
(\ref{FunInduction}) tactic instead of the pattern/apply trick:
336
Lemma div2_le : forall n:nat, div2 n <= n.
341
functional induction (div2 n).
351
\Rem There is a difference between obtaining an induction scheme for a
352
function by using \texttt{Function} (section~\ref{Function}) and by
353
using \texttt{Functional Scheme} after a normal definition using
354
\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
358
\example{Induction scheme for \texttt{tree\_size}}
364
We define trees by the following mutual inductive type:
368
Inductive tree : Set :=
369
node : A -> forest -> tree
372
| cons : tree -> forest -> forest.
375
We define the function \texttt{tree\_size} that computes the size
376
of a tree or a forest. Note that we use \texttt{Function} which
377
generally produces better principles.
380
Function tree_size (t:tree) : nat :=
382
| node A f => S (forest_size f)
384
with forest_size (f:forest) : nat :=
387
| cons t f' => (tree_size t + forest_size f')
391
Remark: \texttt{Function} generates itself non mutual induction
392
principles {\tt tree\_size\_ind} and {\tt forest\_size\_ind}:
398
The definition of mutual induction principles following the recursive
399
structure of \texttt{tree\_size} and \texttt{forest\_size} is defined
403
Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
404
with forest_size_ind2 := Induction for forest_size Sort Prop.
407
You may now look at the type of {\tt tree\_size\_ind2}:
410
Check tree_size_ind2.
416
\section{{\tt inversion}}
418
\label{inversion-examples}
420
\subsection*{Generalities about inversion}
422
When working with (co)inductive predicates, we are very often faced to
423
some of these situations:
425
\item we have an inconsistent instance of an inductive predicate in the
426
local context of hypotheses. Thus, the current goal can be trivially
428
\item we have a hypothesis that is an instance of an inductive
429
predicate, and the instance has some variables whose constraints we
430
would like to derive.
433
The inversion tactics are very useful to simplify the work in these
434
cases. Inversion tools can be classified in three groups:
437
\item tactics for inverting an instance without stocking the inversion
438
lemma in the context; this includes the tactics
439
(\texttt{dependent}) \texttt{inversion} and
440
(\texttt{dependent}) \texttt{inversion\_clear}.
441
\item commands for generating and stocking in the context the inversion
442
lemma corresponding to an instance; this includes \texttt{Derive}
443
(\texttt{Dependent}) \texttt{Inversion} and \texttt{Derive}
444
(\texttt{Dependent}) \texttt{Inversion\_clear}.
445
\item tactics for inverting an instance using an already defined
446
inversion lemma; this includes the tactic \texttt{inversion \ldots using}.
449
As inversion proofs may be large in size, we recommend the user to
450
stock the lemmas whenever the same instance needs to be inverted
454
\example{Non-dependent inversion}
456
Let's consider the relation \texttt{Le} over natural numbers and the
464
Inductive Le : nat -> nat -> Set :=
465
| LeO : forall n:nat, Le 0 n
466
| LeS : forall n m:nat, Le n m -> Le (S n) (S m).
467
Variable P : nat -> nat -> Prop.
468
Variable Q : forall n m:nat, Le n m -> Prop.
471
For example, consider the goal:
474
Lemma ex : forall n m:nat, Le (S n) m -> P n m.
482
To prove the goal we may need to reason by cases on \texttt{H} and to
483
derive that \texttt{m} is necessarily of
484
the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$.
485
Deriving these conditions corresponds to prove that the
486
only possible constructor of \texttt{(Le (S n) m)} is
487
\texttt{LeS} and that we can invert the
488
\texttt{->} in the type of \texttt{LeS}.
489
This inversion is possible because \texttt{Le} is the smallest set closed by
490
the constructors \texttt{LeO} and \texttt{LeS}.
496
Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)}
497
and that the hypothesis \texttt{(Le n m0)} has been added to the
501
interesting to have the equality \texttt{m=(S m0)} in the
502
context to use it after. In that case we can use \texttt{inversion} that
503
does not clear the equalities:
517
\example{Dependent Inversion}
519
Let us consider the following goal:
522
Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H.
530
As \texttt{H} occurs in the goal, we may want to reason by cases on its
531
structure and so, we would like inversion tactics to
532
substitute \texttt{H} by the corresponding term in constructor form.
533
Neither \texttt{Inversion} nor {\tt Inversion\_clear} make such a
535
To have such a behavior we use the dependent inversion tactics:
538
dependent inversion_clear H.
541
Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
542
\texttt{m} by \texttt{(S m0)}.
544
\example{using already defined inversion lemmas}
550
For example, to generate the inversion lemma for the instance
551
\texttt{(Le (S n) m)} and the sort \texttt{Prop} we do:
554
Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort
562
Then we can use the proven inversion lemma:
569
inversion H using leminv.
576
\section{\tt autorewrite}
577
\label{autorewrite-example}
579
Here are two examples of {\tt autorewrite} use. The first one ({\em Ackermann
580
function}) shows actually a quite basic use where there is no conditional
581
rewriting. The second one ({\em Mac Carthy function}) involves conditional
582
rewritings and shows how to deal with them using the optional tactic of the
583
{\tt Hint~Rewrite} command.
586
\example{Ackermann function}
587
%Here is a basic use of {\tt AutoRewrite} with the Ackermann function:
590
Require Import Arith.
594
forall m:nat, Ack 0 m = S m.
595
Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
596
Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
600
Hint Rewrite Ack0 Ack1 Ack2 : base0.
603
autorewrite with base0 using try reflexivity.
610
\example{Mac Carthy function}
611
%The Mac Carthy function shows a more complex case:
614
Require Import Omega.
618
forall m:nat, g 0 m = m.
622
(n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
626
(n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
630
Hint Rewrite g0 g1 g2 using omega : base1.
633
autorewrite with base1 using reflexivity || simpl.
641
Lemma Resg1 : g 1 95 = 91.
642
autorewrite with base1 using reflexivity || simpl.
651
\label{quote-examples}
653
The tactic \texttt{quote} allows to use Barendregt's so-called
654
2-level approach without writing any ML code. Suppose you have a
655
language \texttt{L} of
656
'abstract terms' and a type \texttt{A} of 'concrete terms'
657
and a function \texttt{f : L -> A}. If \texttt{L} is a simple
658
inductive datatype and \texttt{f} a simple fixpoint, \texttt{quote f}
659
will replace the head of current goal by a convertible term of the form
660
\texttt{(f t)}. \texttt{L} must have a constructor of type: \texttt{A
666
Require Import Quote.
667
Parameters A B C : Prop.
668
Inductive formula : Type :=
669
| f_and : formula -> formula -> formula (* binary constructor *)
670
| f_or : formula -> formula -> formula
671
| f_not : formula -> formula (* unary constructor *)
672
| f_true : formula (* 0-ary constructor *)
673
| f_const : Prop -> formula (* contructor for constants *).
674
Fixpoint interp_f (f:
677
| f_and f1 f2 => interp_f f1 /\ interp_f f2
678
| f_or f1 f2 => interp_f f1 \/ interp_f f2
679
| f_not f1 => ~ interp_f f1
683
Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A).
687
The algorithm to perform this inversion is: try to match the
688
term with right-hand sides expression of \texttt{f}. If there is a
689
match, apply the corresponding left-hand side and call yourself
690
recursively on sub-terms. If there is no match, we are at a leaf:
691
return the corresponding constructor (here \texttt{f\_const}) applied
695
\item \errindex{quote: not a simple fixpoint} \\
696
Happens when \texttt{quote} is not able to perform inversion properly.
699
\subsection{Introducing variables map}
701
The normal use of \texttt{quote} is to make proofs by reflection: one
702
defines a function \texttt{simplify : formula -> formula} and proves a
703
theorem \texttt{simplify\_ok: (f:formula)(interp\_f (simplify f)) ->
704
(interp\_f f)}. Then, one can simplify formulas by doing:
710
But there is a problem with leafs: in the example above one cannot
711
write a function that implements, for example, the logical simplifications
712
$A \land A \ra A$ or $A \land \lnot A \ra \texttt{False}$. This is
713
because the \Prop{} is impredicative.
715
It is better to use that type of formulas:
721
Inductive formula : Set :=
722
| f_and : formula -> formula -> formula
723
| f_or : formula -> formula -> formula
724
| f_not : formula -> formula
726
| f_atom : index -> formula.
729
\texttt{index} is defined in module \texttt{quote}. Equality on that
730
type is decidable so we are able to simplify $A \land A$ into $A$ at
733
When there are variables, there are bindings, and \texttt{quote}
734
provides also a type \texttt{(varmap A)} of bindings from
735
\texttt{index} to any set \texttt{A}, and a function
736
\texttt{varmap\_find} to search in such maps. The interpretation
737
function has now another argument, a variables map:
740
Fixpoint interp_f (vm:
741
varmap Prop) (f:formula) {struct f} : Prop :=
743
| f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
744
| f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
745
| f_not f1 => ~ interp_f vm f1
747
| f_atom i => varmap_find True i vm
751
\noindent\texttt{quote} handles this second case properly:
754
Goal A /\ (B \/ A) /\ (A \/ ~ B).
758
It builds \texttt{vm} and \texttt{t} such that \texttt{(f vm t)} is
759
convertible with the conclusion of current goal.
761
\subsection{Combining variables and constants}
763
One can have both variables and constants in abstracts terms; that is
764
the case, for example, for the \texttt{ring} tactic (chapter
765
\ref{ring}). Then one must provide to \texttt{quote} a list of
766
\emph{constructors of constants}. For example, if the list is
767
\texttt{[O S]} then closed natural numbers will be considered as
768
constants and other terms as variables.
776
Inductive formula : Type :=
777
| f_and : formula -> formula -> formula
778
| f_or : formula -> formula -> formula
779
| f_not : formula -> formula
781
| f_const : Prop -> formula (* constructor for constants *)
782
| f_atom : index -> formula.
784
(vm: (* constructor for variables *)
785
varmap Prop) (f:formula) {struct f} : Prop :=
787
| f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
788
| f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
789
| f_not f1 => ~ interp_f vm f1
792
| f_atom i => varmap_find True i vm
795
A /\ (A \/ True) /\ ~ B /\ (C <-> C).
799
quote interp_f [ A B ].
801
quote interp_f [ B C iff ].
804
\Warning Since function inversion
805
is undecidable in general case, don't expect miracles from it!
807
% \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}
809
\SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
811
\SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring})
815
\section{Using the tactical language}
817
\subsection{About the cardinality of the set of natural numbers}
819
A first example which shows how to use the pattern matching over the proof
820
contexts is the proof that natural numbers have more than two elements. The
821
proof of such a lemma can be done as %shown on Figure~\ref{cnatltac}.
827
Require Import Arith.
832
~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z).
834
red; intros (x, (y, Hy)).
835
elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
837
| [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
838
cut (b = c); [ discriminate | apply trans_equal with a; auto ]
843
%\caption{A proof on cardinality of natural numbers}
847
We can notice that all the (very similar) cases coming from the three
848
eliminations (with three distinct natural numbers) are successfully solved by
849
a {\tt match goal} structure and, in particular, with only one pattern (use
850
of non-linear matching).
852
\subsection{Permutation on closed lists}
854
Another more complex example is the problem of permutation on closed lists. The
855
aim is to show that a closed list is a permutation of another one.
857
First, we define the permutation predicate as shown in table~\ref{permutpred}.
864
Inductive permut : list A -> list A -> Prop :=
865
| permut_refl : forall l, permut l l
867
forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
868
| permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
870
forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
874
\caption{Definition of the permutation predicate}
878
A more complex example is the problem of permutation on closed lists.
879
The aim is to show that a closed list is a permutation of another one.
880
First, we define the permutation predicate as shown on
881
Figure~\ref{permutpred}.
888
| |- (permut _ ?l ?l) => apply permut_refl
889
| |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
890
let newn := eval compute in (length l1) in
891
(apply permut_cons; Permut newn)
892
| |- (permut ?A (?a :: ?l1) ?l2) =>
893
match eval compute in n with
896
let l1' := constr:(l1 ++ a :: nil) in
897
(apply (permut_trans A (a :: l1) l1' l2);
898
[ apply permut_append | compute; Permut (pred n) ])
903
| |- (permut _ ?l1 ?l2) =>
904
match eval compute in (length l1 = length l2) with
905
| (?n = ?n) => Permut n
910
\caption{Permutation tactic}
914
Next, we can write naturally the tactic and the result can be seen on
915
Figure~\ref{permutltac}. We can notice that we use two toplevel
916
definitions {\tt PermutProve} and {\tt Permut}. The function to be
917
called is {\tt PermutProve} which computes the lengths of the two
918
lists and calls {\tt Permut} with the length if the two lists have the
919
same length. {\tt Permut} works as expected. If the two lists are
920
equal, it concludes. Otherwise, if the lists have identical first
921
elements, it applies {\tt Permut} on the tail of the lists. Finally,
922
if the lists have different first elements, it puts the first element
923
of one of the lists (here the second one which appears in the {\tt
924
permut} predicate) at the end if that is possible, i.e., if the new
925
first element has been at this place previously. To verify that all
926
rotations have been done for a list, we use the length of the list as
927
an argument for {\tt Permut} and this length is decremented for each
928
rotation down to, but not including, 1 because for a list of length
929
$n$, we can make exactly $n-1$ rotations to generate at most $n$
930
distinct lists. Here, it must be noticed that we use the natural
931
numbers of {\Coq} for the rotation counter. On Figure~\ref{ltac}, we
932
can see that it is possible to use usual natural numbers but they are
933
only used as arguments for primitive tactics and they cannot be
934
handled, in particular, we cannot make computations with them. So, a
935
natural choice is to use {\Coq} data structures so that {\Coq} makes
936
the computations (reductions) by {\tt eval compute in} and we can get
937
the terms back by {\tt match}.
939
With {\tt PermutProve}, we can now prove lemmas as
940
% shown on Figure~\ref{permutlem}.
947
permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
948
Proof. PermutProve. Qed.
951
(0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
952
(0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
953
Proof. PermutProve. Qed.
956
%\caption{Examples of {\tt PermutProve} use}
961
\subsection{Deciding intuitionistic propositional logic}
969
| _:False |- _ => elimtype False; assumption
974
\caption{Deciding intuitionistic propositions (1)}
986
| id:(~ _) |- _ => red in id
987
| id:(_ /\ _) |- _ =>
988
elim id; do 2 intro; clear id
989
| id:(_ \/ _) |- _ =>
990
elim id; intro; clear id
991
| id:(?A /\ ?B -> ?C) |- _ =>
993
[ intro | intros; apply id; split; assumption ]
994
| id:(?A \/ ?B -> ?C) |- _ =>
998
| intro; apply id; left; assumption ]
999
| intro; apply id; right; assumption ]
1000
| id0:(?A -> ?B),id1:?A |- _ =>
1001
cut B; [ intro; clear id0 | apply id0; assumption ]
1002
| |- (_ /\ _) => split
1009
| id:((?A -> ?B) -> ?C) |- _ =>
1011
[ intro; cut (A -> B);
1013
[ intro; clear id | apply id; assumption ]
1015
| intro; apply id; intro; assumption ]; TautoProp
1016
| id:(~ ?A -> ?B) |- _ =>
1018
[ intro; cut (A -> False);
1020
[ intro; clear id | apply id; assumption ]
1022
| intro; apply id; red; intro; assumption ]; TautoProp
1023
| |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
1027
\caption{Deciding intuitionistic propositions (2)}
1031
The pattern matching on goals allows a complete and so a powerful
1032
backtracking when returning tactic values. An interesting application
1033
is the problem of deciding intuitionistic propositional logic.
1034
Considering the contraction-free sequent calculi {\tt LJT*} of
1035
Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic
1036
using the tactic language as shown on Figures~\ref{tautoltaca}
1037
and~\ref{tautoltacb}. The tactic {\tt Axioms} tries to conclude using
1038
usual axioms. The tactic {\tt DSimplif} applies all the reversible
1039
rules of Dyckhoff's system. Finally, the tactic {\tt TautoProp} (the
1040
main tactic to be called) simplifies with {\tt DSimplif}, tries to
1041
conclude with {\tt Axioms} and tries several paths using the
1042
backtracking rules (one of the four Dyckhoff's rules for the left
1043
implication to get rid of the contraction and the right or).
1045
For example, with {\tt TautoProp}, we can prove tautologies like
1047
% on Figure~\ref{tautolem}.
1048
%\begin{figure}[tbp]
1049
%\begin{centerframe}
1050
\begin{coq_example*}
1051
Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
1052
Proof. TautoProp. Qed.
1054
forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
1055
Proof. TautoProp. Qed.
1058
%\caption{Proofs of tautologies with {\tt TautoProp}}
1062
\subsection{Deciding type isomorphisms}
1064
A more tricky problem is to decide equalities between types and modulo
1065
isomorphisms. Here, we choose to use the isomorphisms of the simply typed
1066
$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
1067
\cite{RC95}). The axioms of this $\lb{}$-calculus are given by
1075
\begin{coq_example*}
1076
Open Scope type_scope.
1078
Variables A B C : Set.
1079
Axiom Com : A * B = B * A.
1080
Axiom Ass : A * (B * C) = A * B * C.
1081
Axiom Cur : (A * B -> C) = (A -> B -> C).
1082
Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
1083
Axiom P_unit : A * unit = A.
1084
Axiom AR_unit : (A -> unit) = unit.
1085
Axiom AL_unit : (unit -> A) = A.
1086
Lemma Cons : B = C -> A * B = A * C.
1088
intro Heq; rewrite Heq; apply refl_equal.
1093
\caption{Type isomorphism axioms}
1097
A more tricky problem is to decide equalities between types and modulo
1098
isomorphisms. Here, we choose to use the isomorphisms of the simply typed
1099
$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
1100
\cite{RC95}). The axioms of this $\lb{}$-calculus are given on
1101
Figure~\ref{isosax}.
1106
Ltac DSimplif trm :=
1109
rewrite <- (Ass A B C); try MainSimplif
1110
| (?A * ?B -> ?C) =>
1111
rewrite (Cur A B C); try MainSimplif
1112
| (?A -> ?B * ?C) =>
1113
rewrite (Dis A B C); try MainSimplif
1115
rewrite (P_unit A); try MainSimplif
1117
rewrite (Com unit B); try MainSimplif
1119
rewrite (AR_unit A); try MainSimplif
1121
rewrite (AL_unit B); try MainSimplif
1123
(DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
1125
(DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
1129
| |- (?A = ?B) => try DSimplif A; try DSimplif B
1133
| (_ * ?B) => let succ := Length B in constr:(S succ)
1136
Ltac assoc := repeat rewrite <- Ass.
1139
\caption{Type isomorphism tactic (1)}
1148
| [ |- (?A = ?A) ] => apply refl_equal
1149
| [ |- (?A * ?B = ?A * ?C) ] =>
1150
apply Cons; let newn := Length B in
1152
| [ |- (?A * ?B = ?C) ] =>
1153
match eval compute in n with
1156
pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
1159
Ltac CompareStruct :=
1161
| [ |- (?A = ?B) ] =>
1163
with l2 := Length B in
1164
match eval compute in (l1 = l2) with
1165
| (?n = ?n) => DoCompare n
1168
Ltac IsoProve := MainSimplif; CompareStruct.
1171
\caption{Type isomorphism tactic (2)}
1175
The tactic to judge equalities modulo this axiomatization can be written as
1176
shown on Figures~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
1177
simple. Types are reduced using axioms that can be oriented (this done by {\tt
1178
MainSimplif}). The normal forms are sequences of Cartesian
1179
products without Cartesian product in the left component. These normal forms
1180
are then compared modulo permutation of the components (this is done by {\tt
1181
CompareStruct}). The main tactic to be called and realizing this algorithm is
1184
% Figure~\ref{isoslem} gives
1185
Here are examples of what can be solved by {\tt IsoProve}.
1187
%\begin{centerframe}
1188
\begin{coq_example*}
1190
forall A B:Set, A * unit * B = B * (unit * A).
1197
(A * unit -> B * (C * unit)) =
1198
(A * unit -> (C -> unit) * C) * (unit -> A -> B).
1204
%\caption{Type equalities solved by {\tt IsoProve}}
1208
%%% Local Variables:
1210
%%% TeX-master: "Reference-Manual"
added
removed
refman/RefMan-tacex.tex
