aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-ind.tex
blob: 43bd2419f0b3c1b5230d04246bfccdbcf9042111 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510

%\documentstyle[11pt]{article}
%\input{title}

%\include{macros}
%\makeindex

%\begin{document}
%\coverpage{The module {\tt Equality}}{Cristina CORNES}

%\tableofcontents

\chapter[Tactics for inductive types and families]{Tactics for inductive types and families\label{Addoc-equality}}

This chapter details a few special tactics useful for inferring facts
from inductive hypotheses. They can be considered as tools that
macro-generate complicated uses of the basic elimination tactics for
inductive types. 

Sections \ref{inversion_introduction} to \ref{inversion_using}  present
inversion tactics and Section~\ref{scheme} describes
a command {\tt Scheme} for automatic generation of induction schemes
for mutual inductive types.

%\end{document}
%\documentstyle[11pt]{article}
%\input{title}

%\begin{document}
%\coverpage{Module Inv: Inversion Tactics}{Cristina CORNES}

\section[Generalities about inversion]{Generalities about inversion\label{inversion_introduction}}
When working with (co)inductive predicates, we are very often faced to
some of these situations:
\begin{itemize}
\item we have an inconsistent instance of an inductive predicate in the
  local context of hypotheses. Thus, the current goal can be trivially
  proved by absurdity. 

\item we have a hypothesis that is an instance of an inductive
  predicate, and the instance has some variables whose constraints we
  would like to derive.
\end{itemize}

The inversion tactics are very useful to simplify the work in these
cases. Inversion tools can be classified in three groups:
\begin{enumerate}
\item tactics for inverting an instance without stocking the inversion
  lemma in the context: 
  (\texttt{Dependent})  \texttt{Inversion} and
 (\texttt{Dependent}) \texttt{Inversion\_clear}.
\item commands for generating and stocking in the context the inversion
  lemma corresponding to an instance: \texttt{Derive}
  (\texttt{Dependent}) \texttt{Inversion}, \texttt{Derive}
  (\texttt{Dependent}) \texttt{Inversion\_clear}.
\item tactics for inverting an instance using an already defined
  inversion lemma: \texttt{Inversion \ldots using}.
\end{enumerate}

These tactics work for inductive types of arity $(\vec{x}:\vec{T})s$ 
where $s \in \{Prop,Set,Type\}$. Sections \ref{inversion_primitive},
\ref{inversion_derivation} and \ref{inversion_using} 
describe respectively each group of tools.

As inversion proofs may be large in size, we recommend the user to
stock the lemmas whenever the same instance needs to be inverted
several times.\\

Let's consider the relation \texttt{Le} over natural numbers and the
following variables:

\begin{coq_eval}
Restore State "Initial".
\end{coq_eval}

\begin{coq_example*}
Inductive Le : nat -> nat -> Set :=
  | LeO : forall n:nat, Le 0%N n
  | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
Variable P : nat -> nat -> Prop.
Variable Q : forall n m:nat, Le n m -> Prop.
\end{coq_example*}

For example purposes we defined  \verb+Le: nat->nat->Set+
 but we may have defined
it \texttt{Le} of type \verb+nat->nat->Prop+ or \verb+nat->nat->Type+.


\section[Inverting an instance]{Inverting an instance\label{inversion_primitive}}
\subsection{The non dependent case}
\begin{itemize}

\item \texttt{Inversion\_clear} \ident~\\
\index{Inversion-clear@{\tt Inversion\_clear}}
  Let the type of \ident~ in the local context be $(I~\vec{t})$,
  where $I$ is a (co)inductive predicate. Then,
  \texttt{Inversion} applied to \ident~ derives for each possible
  constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary
  conditions that should hold for the instance $(I~\vec{t})$ to be
  proved by $c_i$. Finally it erases \ident~ from the context.



For example, consider the goal:
\begin{coq_eval}
Lemma ex : forall n m:nat, Le (S n) m -> P n m.
intros.
\end{coq_eval}

\begin{coq_example}
Show.
\end{coq_example}

To prove the goal we may need to reason by cases on \texttt{H} and to 
 derive that \texttt{m}  is necessarily of
the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$.  
Deriving these conditions corresponds to prove that the
only possible constructor of \texttt{(Le (S n) m)}  is
\texttt{LeS} and that we can invert the 
\texttt{->} in the type  of \texttt{LeS}.  
This inversion is possible because \texttt{Le} is the smallest set closed by
the constructors \texttt{LeO} and \texttt{LeS}.


\begin{coq_example}
inversion_clear H.
\end{coq_example}

Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)}
and that the hypothesis \texttt{(Le n m0)} has been added to the
context.

\item \texttt{Inversion} \ident~\\
\index{Inversion@{\tt Inversion}}
  This tactic differs from   {\tt Inversion\_clear} in the fact that
  it adds the equality constraints in the context and
  it does not erase  the hypothesis \ident.


In the previous example, {\tt Inversion\_clear} 
has substituted \texttt{m} by \texttt{(S m0)}. Sometimes it is
interesting to have the equality \texttt{m=(S m0)} in the
context to use it after. In that case we can use  \texttt{Inversion} that
does not clear the equalities:

\begin{coq_example*}
Undo.
\end{coq_example*}
\begin{coq_example}
inversion H.
\end{coq_example}

\begin{coq_eval}
Undo.
\end{coq_eval}

Note that the hypothesis \texttt{(S m0)=m} has been deduced and 
\texttt{H} has not been cleared from the context.

\end{itemize}

\begin{Variants}

\item \texttt{Inversion\_clear } \ident~ \texttt{in} \ident$_1$ \ldots
  \ident$_n$\\ 
\index{Inversion_clear...in@{\tt Inversion\_clear...in}}
  Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This
  tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing
  {\tt Inversion\_clear}.

\item \texttt{Inversion } \ident~ \texttt{in} \ident$_1$ \ldots \ident$_n$\\
\index{Inversion ... in@{\tt Inversion ... in}}
  Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This
  tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing
  \texttt{Inversion}.


\item \texttt{Simple Inversion} \ident~ \\
\index{Simple Inversion@{\tt Simple Inversion}}
  It is a very primitive inversion tactic that derives all the necessary
  equalities  but it does not simplify
  the  constraints as \texttt{Inversion} and
  {\tt Inversion\_clear} do.

\end{Variants}


\subsection{The dependent case}
\begin{itemize}
\item \texttt{Dependent Inversion\_clear} \ident~\\
\index{Dependent Inversion-clear@{\tt Dependent Inversion\_clear}}
  Let the type of \ident~ in the local context be $(I~\vec{t})$,
  where $I$ is a (co)inductive predicate, and let the goal  depend both on
  $\vec{t}$ and \ident. Then, 
  \texttt{Dependent Inversion\_clear} applied to \ident~ derives 
   for each possible constructor $c_i$ of $(I~\vec{t})$, {\bf all} the
  necessary conditions that should hold for the instance $(I~\vec{t})$ to be
  proved by $c_i$. It also substitutes  \ident~ for the corresponding
  term  in the goal and  it erases \ident~ from the context.


For example, consider the  goal:
\begin{coq_eval}
Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H.
intros.
\end{coq_eval}

\begin{coq_example}
Show.
\end{coq_example}

As \texttt{H} occurs in the goal, we may want to reason by cases on its
structure and so, we would like  inversion tactics to
substitute \texttt{H} by the corresponding term in constructor form. 
Neither \texttt{Inversion} nor  {\tt Inversion\_clear} make such a
substitution. To have such a behavior we use the dependent inversion tactics:

\begin{coq_example}
dependent inversion_clear H.
\end{coq_example}

Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
\texttt{m} by \texttt{(S m0)}.


\end{itemize}

\begin{Variants}

\item \texttt{Dependent Inversion\_clear } \ident~ \texttt{ with } \term\\
\index{Dependent Inversion_clear...with@{\tt Dependent Inversion\_clear...with}}
 \noindent Behaves as \texttt{Dependent Inversion\_clear} but allows giving
  explicitly the good generalization of the goal. It is useful when
  the system fails to generalize the goal automatically. If
  \ident~ has type $(I~\vec{t})$ and $I$ has type
  $(\vec{x}:\vec{T})s$,   then \term~  must be of type
  $I:(\vec{x}:\vec{T})(I~\vec{x})\rightarrow s'$ where $s'$ is the
  type of the goal.



\item \texttt{Dependent Inversion} \ident~\\
\index{Dependent Inversion@{\tt Dependent Inversion}}
 This tactic differs from   \texttt{Dependent Inversion\_clear} in the fact that
  it also  adds the equality constraints in the context and
  it does not erase  the hypothesis \ident~.

\item \texttt{Dependent Inversion } \ident~ \texttt{ with } \term \\
\index{Dependent Inversion...with@{\tt Dependent Inversion...with}}
  Analogous to \texttt{Dependent Inversion\_clear .. with..} above. 
\end{Variants}



\section[Deriving the inversion lemmas]{Deriving the inversion lemmas\label{inversion_derivation}}
\subsection{The non dependent case}

The tactics (\texttt{Dependent}) \texttt{Inversion} and (\texttt{Dependent})
{\tt Inversion\_clear} work on a
certain instance $(I~\vec{t})$ of an inductive predicate. At each
application, they inspect the given instance and derive the
corresponding inversion lemma.  If we have to invert the same
instance several times it is recommended to stock the lemma in the
context and to reuse it whenever we need it.

The families of commands \texttt{Derive Inversion}, \texttt{Derive
Dependent Inversion}, \texttt{Derive} \\ {\tt Inversion\_clear} and \texttt{Derive Dependent Inversion\_clear}
allow to generate inversion lemmas for given instances and sorts.  Next
section describes the tactic \texttt{Inversion}$\ldots$\texttt{using} that refines the
goal with a specified inversion lemma.

\begin{itemize}

\item \texttt{Derive Inversion\_clear} \ident~ \texttt{with}
  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ 
\index{Derive Inversion_clear...with@{\tt Derive Inversion\_clear...with}}
  Let $I$ be an inductive predicate and $\vec{x}$ the variables
  occurring in $\vec{t}$. This command generates and stocks
  the inversion lemma for the sort  \sort~  corresponding to the instance
  $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf
    global} environment. When applied it is equivalent to have
  inverted the instance with the tactic {\tt Inversion\_clear}.


  For example, to generate the inversion lemma for the instance
 \texttt{(Le (S n) m)} and the sort \texttt{Prop} we do:
\begin{coq_example}
Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort
 Prop.
\end{coq_example}

Let us  inspect the type of the generated lemma:
\begin{coq_example}
Check leminv.
\end{coq_example}



\end{itemize}

%\variants
%\begin{enumerate} 
%\item \verb+Derive Inversion_clear+  \ident$_1$ \ident$_2$ \\ 
%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}}
%  Let \ident$_1$ have type $(I~\vec{t})$ in the local context ($I$
%  an inductive predicate).  Then, this command has the same semantics
%  as \verb+Derive Inversion_clear+ \ident$_2$~ \verb+with+
%  $(\vec{x}:\vec{T})(I~\vec{t})$ \verb+Sort Prop+ where $\vec{x}$ are the free
%  variables of $(I~\vec{t})$ declared in the local context (variables
%  of the global context are considered as constants). 
%\item \verb+Derive Inversion+ \ident$_1$~ \ident$_2$~\\
%\index{Derive Inversion@{\tt Derive Inversion}}
% Analogous to the previous command. 
%\item \verb+Derive Inversion+ $num$ \ident~ \ident~ \\ 
%\index{Derive Inversion@{\tt Derive Inversion}}
%  This command behaves as \verb+Derive Inversion+ \ident~ {\it
%    namehyp} performed on the goal number $num$.
%
%\item \verb+Derive Inversion_clear+ $num$ \ident~ \ident~ \\ 
%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}}
%  This command behaves as \verb+Derive Inversion_clear+ \ident~
%  \ident~ performed on the goal number $num$.
%\end{enumerate}



A derived inversion lemma is  adequate for inverting the instance
with which it was generated,  \texttt{Derive} applied to
different instances yields different lemmas. In general, if we generate
the inversion lemma with 
an instance $(\vec{x}:\vec{T})(I~\vec{t})$ and a sort $s$,  the inversion lemma will
expect a predicate of type $(\vec{x}:\vec{T})s$ as first argument. \\

\begin{Variant}
\item \texttt{Derive Inversion} \ident~ \texttt{with} 
  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort\\ 
\index{Derive Inversion...with@{\tt Derive Inversion...with}}
     Analogous of \texttt{Derive Inversion\_clear .. with ..} but 
 when applied it is equivalent to having
  inverted the instance with the tactic \texttt{Inversion}.
\end{Variant}

\subsection{The dependent case}
\begin{itemize}
\item \texttt{Derive Dependent Inversion\_clear} \ident~ \texttt{with}
  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ 
\index{Derive Dependent Inversion\_clear...with@{\tt Derive Dependent Inversion\_clear...with}}
  Let $I$ be an inductive predicate. This command generates and stocks
  the dependent inversion lemma for the sort  \sort~  corresponding to the instance
  $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf
    global} environment. When applied it is equivalent to having
  inverted the instance with the tactic \texttt{Dependent Inversion\_clear}.
\end{itemize}

\begin{coq_example}
Derive Dependent Inversion_clear leminv_dep with
 (forall n m:nat, Le (S n) m) Sort Prop.
\end{coq_example}

\begin{coq_example}
Check leminv_dep.
\end{coq_example}

\begin{Variants}
\item \texttt{Derive Dependent Inversion} \ident~ \texttt{with}
  $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ 
\index{Derive Dependent Inversion...with@{\tt Derive Dependent Inversion...with}}
  Analogous to \texttt{Derive Dependent Inversion\_clear}, but when
  applied  it is equivalent to having
  inverted the instance with the tactic \texttt{Dependent Inversion}.

\end{Variants}

\section[Using already defined inversion  lemmas]{Using already defined inversion  lemmas\label{inversion_using}}
\begin{itemize}
\item \texttt{Inversion} \ident \texttt{ using} \ident$'$ \\
\index{Inversion...using@{\tt Inversion...using}}
  Let \ident~ have type $(I~\vec{t})$ ($I$ an inductive
  predicate) in the local context, and \ident$'$ be a (dependent) inversion
  lemma. Then, this tactic refines the current goal with the specified
  lemma. 


\begin{coq_eval}
Abort.
\end{coq_eval}

\begin{coq_example}
Show.
\end{coq_example}
\begin{coq_example}
inversion H using leminv.
\end{coq_example}


\end{itemize}
\variant
\begin{enumerate}
\item \texttt{Inversion} \ident~ \texttt{using} \ident$'$ \texttt{in} \ident$_1$\ldots \ident$_n$\\
\index{Inversion...using...in@{\tt Inversion...using...in}}
This tactic behaves as generalizing  \ident$_1$\ldots \ident$_n$,
then doing \texttt{Use Inversion} \ident~\ident$'$.
\end{enumerate}

\section[\tt Scheme ...]{\tt Scheme ...\index{Scheme@{\tt Scheme}}\label{Scheme}
\label{scheme}}
The {\tt Scheme} command is a high-level tool for generating
automatically (possibly mutual) induction principles for given types
and sorts.  Its syntax follows the schema :

\noindent
{\tt Scheme {\ident$_1$} := Induction for \term$_1$ Sort {\sort$_1$} \\
  with\\
  \mbox{}\hspace{0.1cm} .. \\
        with {\ident$_m$} := Induction for {\term$_m$} Sort
        {\sort$_m$}}\\
\term$_1$ \ldots \term$_m$ are different inductive types belonging to
the same package of mutual inductive definitions. This command
generates {\ident$_1$}\ldots{\ident$_m$} to be mutually recursive
definitions. Each term {\ident$_i$} proves a general principle 
of mutual induction for objects in type {\term$_i$}. 

\Example
The definition of principle of mutual induction for {\tt tree} and
{\tt forest} over the sort {\tt Set} is defined by the command:
\begin{coq_eval}
Restore State "Initial".
Variables A B : Set.
Inductive tree : Set :=
    node : A -> forest -> tree
with forest : Set :=
  | leaf : B -> forest
  | cons : tree -> forest -> forest.
\end{coq_eval}
\begin{coq_example*}
Scheme tree_forest_rec := Induction for tree
  Sort Set
  with forest_tree_rec := Induction for forest Sort Set.
\end{coq_example*}
You may now look at the type of {\tt tree\_forest\_rec} :
\begin{coq_example}
Check tree_forest_rec.
\end{coq_example}
This principle involves two different predicates for {\tt trees} and
{\tt forests}; it also has three premises each one corresponding to a
constructor of one of the inductive definitions.

The principle {\tt tree\_forest\_rec} shares exactly the same
premises, only the conclusion now refers to the property of forests.
\begin{coq_example}
Check forest_tree_rec.
\end{coq_example}

\begin{Variant}
\item {\tt Scheme {\ident$_1$} := Minimality for \term$_1$ Sort {\sort$_1$} \\
  with\\
  \mbox{}\hspace{0.1cm} .. \\
        with {\ident$_m$} := Minimality for {\term$_m$} Sort
        {\sort$_m$}}\\
Same as before but defines a non-dependent elimination principle more
natural in case of inductively defined relations. 
\end{Variant}

\Example
With the predicates {\tt odd} and {\tt even} inductively defined as:
% \begin{coq_eval}
% Restore State "Initial".
% \end{coq_eval}
\begin{coq_example*}
Inductive odd : nat -> Prop :=
    oddS : forall n:nat, even n -> odd (S n)
with even : nat -> Prop :=
  | evenO : even 0%N
  | evenS : forall n:nat, odd n -> even (S n).
\end{coq_example*}
The following command generates a powerful elimination
principle:
\begin{coq_example*}
Scheme odd_even := Minimality for   odd Sort Prop
  with even_odd := Minimality for even Sort Prop.
\end{coq_example*}
The type of {\tt odd\_even} for instance will be:
\begin{coq_example}
Check odd_even.
\end{coq_example}
The type of {\tt even\_odd} shares the same premises but the
conclusion is {\tt (n:nat)(even n)->(Q n)}.

\subsection[\tt Combined Scheme ...]{\tt Combined Scheme ...\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme}
\label{combinedscheme}}
The {\tt Combined Scheme} command is a tool for combining 
induction principles generated by the {\tt Scheme} command.
Its syntax follows the schema :

\noindent
{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\
\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
the same package of mutual inductive principle definitions. This command
generates {\ident$_0$} to be the conjunction of the principles: it is
build from the common premises of the principles and concluded by the
conjunction of their conclusions. For exemple, we can combine the
induction principles for trees and forests:

\begin{coq_example*}
Combined Scheme tree_forest_mutind from tree_ind, forest_ind.
Check tree_forest_mutind.
\end{coq_example*}

%\end{document}