27 non-empty list, this lemma looks easy to prove:% |
27 non-empty list, this lemma looks easy to prove:% |
28 \end{isamarkuptext}% |
28 \end{isamarkuptext}% |
29 \isamarkuptrue% |
29 \isamarkuptrue% |
30 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline |
30 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline |
31 \isamarkupfalse% |
31 \isamarkupfalse% |
32 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isamarkupfalse% |
32 \isamarkupfalse% |
33 % |
|
34 \begin{isamarkuptxt}% |
|
35 \noindent |
|
36 But induction produces the warning |
|
37 \begin{quote}\tt |
|
38 Induction variable occurs also among premises! |
|
39 \end{quote} |
|
40 and leads to the base case |
|
41 \begin{isabelle}% |
|
42 \ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% |
|
43 \end{isabelle} |
|
44 Simplification reduces the base case to this: |
|
45 \begin{isabelle} |
|
46 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] |
|
47 \end{isabelle} |
|
48 We cannot prove this equality because we do not know what \isa{hd} and |
|
49 \isa{last} return when applied to \isa{{\isacharbrackleft}{\isacharbrackright}}. |
|
50 |
|
51 We should not have ignored the warning. Because the induction |
|
52 formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises. |
|
53 Thus the case that should have been trivial |
|
54 becomes unprovable. Fortunately, the solution is easy:\footnote{A similar |
|
55 heuristic applies to rule inductions; see \S\ref{sec:rtc}.} |
|
56 \begin{quote} |
|
57 \emph{Pull all occurrences of the induction variable into the conclusion |
|
58 using \isa{{\isasymlongrightarrow}}.} |
|
59 \end{quote} |
|
60 Thus we should state the lemma as an ordinary |
|
61 implication~(\isa{{\isasymlongrightarrow}}), letting |
|
62 \attrdx{rule_format} (\S\ref{sec:forward}) convert the |
|
63 result to the usual \isa{{\isasymLongrightarrow}} form:% |
|
64 \end{isamarkuptxt}% |
|
65 \isamarkuptrue% |
33 \isamarkuptrue% |
66 \isamarkupfalse% |
34 \isamarkupfalse% |
67 \isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse% |
35 \isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse% |
68 \isamarkupfalse% |
36 \isamarkupfalse% |
69 % |
|
70 \begin{isamarkuptxt}% |
|
71 \noindent |
|
72 This time, induction leaves us with a trivial base case: |
|
73 \begin{isabelle}% |
|
74 \ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% |
|
75 \end{isabelle} |
|
76 And \isa{auto} completes the proof. |
|
77 |
|
78 If there are multiple premises $A@1$, \dots, $A@n$ containing the |
|
79 induction variable, you should turn the conclusion $C$ into |
|
80 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \] |
|
81 Additionally, you may also have to universally quantify some other variables, |
|
82 which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format} |
|
83 can remove any number of occurrences of \isa{{\isasymforall}} and |
|
84 \isa{{\isasymlongrightarrow}}. |
|
85 |
|
86 \index{induction!on a term}% |
|
87 A second reason why your proposition may not be amenable to induction is that |
|
88 you want to induct on a complex term, rather than a variable. In |
|
89 general, induction on a term~$t$ requires rephrasing the conclusion~$C$ |
|
90 as |
|
91 \begin{equation}\label{eqn:ind-over-term} |
|
92 \forall y@1 \dots y@n.~ x = t \longrightarrow C. |
|
93 \end{equation} |
|
94 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable. |
|
95 Now you can perform induction on~$x$. An example appears in |
|
96 \S\ref{sec:complete-ind} below. |
|
97 |
|
98 The very same problem may occur in connection with rule induction. Remember |
|
99 that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is |
|
100 some inductively defined set and the $x@i$ are variables. If instead we have |
|
101 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we |
|
102 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as |
|
103 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \] |
|
104 For an example see \S\ref{sec:CTL-revisited} below. |
|
105 |
|
106 Of course, all premises that share free variables with $t$ need to be pulled into |
|
107 the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above. |
|
108 |
|
109 Readers who are puzzled by the form of statement |
|
110 (\ref{eqn:ind-over-term}) above should remember that the |
|
111 transformation is only performed to permit induction. Once induction |
|
112 has been applied, the statement can be transformed back into something quite |
|
113 intuitive. For example, applying wellfounded induction on $x$ (w.r.t.\ |
|
114 $\prec$) to (\ref{eqn:ind-over-term}) and transforming the result a |
|
115 little leads to the goal |
|
116 \[ \bigwedge\overline{y}.\ |
|
117 \forall \overline{z}.\ t\,\overline{z} \prec t\,\overline{y}\ \longrightarrow\ C\,\overline{z} |
|
118 \ \Longrightarrow\ C\,\overline{y} \] |
|
119 where $\overline{y}$ stands for $y@1 \dots y@n$ and the dependence of $t$ and |
|
120 $C$ on the free variables of $t$ has been made explicit. |
|
121 Unfortunately, this induction schema cannot be expressed as a |
|
122 single theorem because it depends on the number of free variables in $t$ --- |
|
123 the notation $\overline{y}$ is merely an informal device.% |
|
124 \end{isamarkuptxt}% |
|
125 \isamarkuptrue% |
37 \isamarkuptrue% |
126 \isamarkupfalse% |
38 \isamarkupfalse% |
127 % |
39 % |
128 \isamarkupsubsection{Beyond Structural and Recursion Induction% |
40 \isamarkupsubsection{Beyond Structural and Recursion Induction% |
129 } |
41 } |
168 be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined |
80 be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined |
169 above, we have to phrase the proposition as follows to allow induction:% |
81 above, we have to phrase the proposition as follows to allow induction:% |
170 \end{isamarkuptext}% |
82 \end{isamarkuptext}% |
171 \isamarkuptrue% |
83 \isamarkuptrue% |
172 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse% |
84 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse% |
173 % |
85 \isamarkuptrue% |
174 \begin{isamarkuptxt}% |
86 \isamarkupfalse% |
175 \noindent |
87 \isamarkuptrue% |
176 To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use |
88 \isamarkupfalse% |
177 the same general induction method as for recursion induction (see |
89 \isamarkupfalse% |
178 \S\ref{sec:recdef-induction}):% |
90 \isamarkupfalse% |
179 \end{isamarkuptxt}% |
91 \isamarkuptrue% |
180 \isamarkuptrue% |
92 \isamarkupfalse% |
181 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% |
|
182 % |
|
183 \begin{isamarkuptxt}% |
|
184 \noindent |
|
185 We get the following proof state: |
|
186 \begin{isabelle}% |
|
187 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i\ {\isasymLongrightarrow}\ {\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
|
188 \end{isabelle} |
|
189 After stripping the \isa{{\isasymforall}i}, the proof continues with a case |
|
190 distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on |
|
191 the other case:% |
|
192 \end{isamarkuptxt}% |
|
193 \isamarkuptrue% |
|
194 \isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline |
|
195 \isamarkupfalse% |
|
196 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ i{\isacharparenright}\isanewline |
|
197 \ \isamarkupfalse% |
|
198 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% |
|
199 % |
|
200 \begin{isamarkuptxt}% |
|
201 \begin{isabelle}% |
|
202 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ i\ nat{\isachardot}\isanewline |
|
203 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}m{\isacharless}n{\isachardot}\ {\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharsemicolon}\ i\ {\isacharequal}\ Suc\ nat{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i% |
|
204 \end{isabelle}% |
|
205 \end{isamarkuptxt}% |
|
206 \isamarkuptrue% |
|
207 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isamarkupfalse% |
|
208 % |
93 % |
209 \begin{isamarkuptext}% |
94 \begin{isamarkuptext}% |
210 \noindent |
95 \noindent |
211 If you find the last step puzzling, here are the two lemmas it employs: |
96 If you find the last step puzzling, here are the two lemmas it employs: |
212 \begin{isabelle} |
97 \begin{isabelle} |