9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{Itrev}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
17175
|
10 |
\isamarkupfalse%
|
17056
|
11 |
%
|
|
12 |
\endisatagtheory
|
|
13 |
{\isafoldtheory}%
|
|
14 |
%
|
|
15 |
\isadelimtheory
|
|
16 |
%
|
|
17 |
\endisadelimtheory
|
8749
|
18 |
%
|
10878
|
19 |
\isamarkupsection{Induction Heuristics%
|
10397
|
20 |
}
|
11866
|
21 |
\isamarkuptrue%
|
9844
|
22 |
%
|
8749
|
23 |
\begin{isamarkuptext}%
|
9844
|
24 |
\label{sec:InductionHeuristics}
|
11458
|
25 |
\index{induction heuristics|(}%
|
9844
|
26 |
The purpose of this section is to illustrate some simple heuristics for
|
|
27 |
inductive proofs. The first one we have already mentioned in our initial
|
|
28 |
example:
|
|
29 |
\begin{quote}
|
|
30 |
\emph{Theorems about recursive functions are proved by induction.}
|
|
31 |
\end{quote}
|
|
32 |
In case the function has more than one argument
|
|
33 |
\begin{quote}
|
|
34 |
\emph{Do induction on argument number $i$ if the function is defined by
|
|
35 |
recursion in argument number $i$.}
|
|
36 |
\end{quote}
|
11458
|
37 |
When we look at the proof of \isa{{\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys{\isacharat}zs{\isacharparenright}}
|
|
38 |
in \S\ref{sec:intro-proof} we find
|
|
39 |
\begin{itemize}
|
|
40 |
\item \isa{{\isacharat}} is recursive in
|
|
41 |
the first argument
|
|
42 |
\item \isa{xs} occurs only as the first argument of
|
|
43 |
\isa{{\isacharat}}
|
|
44 |
\item both \isa{ys} and \isa{zs} occur at least once as
|
|
45 |
the second argument of \isa{{\isacharat}}
|
|
46 |
\end{itemize}
|
|
47 |
Hence it is natural to perform induction on~\isa{xs}.
|
9844
|
48 |
|
|
49 |
The key heuristic, and the main point of this section, is to
|
11458
|
50 |
\emph{generalize the goal before induction}.
|
|
51 |
The reason is simple: if the goal is
|
9844
|
52 |
too specific, the induction hypothesis is too weak to allow the induction
|
10971
|
53 |
step to go through. Let us illustrate the idea with an example.
|
9844
|
54 |
|
11458
|
55 |
Function \cdx{rev} has quadratic worst-case running time
|
9792
|
56 |
because it calls function \isa{{\isacharat}} for each element of the list and
|
|
57 |
\isa{{\isacharat}} is linear in its first argument. A linear time version of
|
9493
|
58 |
\isa{rev} reqires an extra argument where the result is accumulated
|
11458
|
59 |
gradually, using only~\isa{{\isacharhash}}:%
|
8749
|
60 |
\end{isamarkuptext}%
|
17175
|
61 |
\isamarkuptrue%
|
|
62 |
\isacommand{consts}\isamarkupfalse%
|
|
63 |
\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
|
|
64 |
\isacommand{primrec}\isamarkupfalse%
|
|
65 |
\isanewline
|
|
66 |
{\isachardoublequoteopen}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequoteclose}\isanewline
|
|
67 |
{\isachardoublequoteopen}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequoteclose}%
|
8749
|
68 |
\begin{isamarkuptext}%
|
9792
|
69 |
\noindent
|
11458
|
70 |
The behaviour of \cdx{itrev} is simple: it reverses
|
9493
|
71 |
its first argument by stacking its elements onto the second argument,
|
|
72 |
and returning that second argument when the first one becomes
|
17100
|
73 |
empty. Note that \isa{Itrev{\isachardot}itrev} is tail-recursive: it can be
|
9493
|
74 |
compiled into a loop.
|
|
75 |
|
17100
|
76 |
Naturally, we would like to show that \isa{Itrev{\isachardot}itrev} does indeed reverse
|
9493
|
77 |
its first argument provided the second one is empty:%
|
8749
|
78 |
\end{isamarkuptext}%
|
17175
|
79 |
\isamarkuptrue%
|
|
80 |
\isacommand{lemma}\isamarkupfalse%
|
|
81 |
\ {\isachardoublequoteopen}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequoteclose}%
|
17056
|
82 |
\isadelimproof
|
|
83 |
%
|
|
84 |
\endisadelimproof
|
|
85 |
%
|
|
86 |
\isatagproof
|
16069
|
87 |
%
|
|
88 |
\begin{isamarkuptxt}%
|
|
89 |
\noindent
|
|
90 |
There is no choice as to the induction variable, and we immediately simplify:%
|
|
91 |
\end{isamarkuptxt}%
|
17175
|
92 |
\isamarkuptrue%
|
|
93 |
\isacommand{apply}\isamarkupfalse%
|
|
94 |
{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
|
16069
|
95 |
\begin{isamarkuptxt}%
|
|
96 |
\noindent
|
|
97 |
Unfortunately, this attempt does not prove
|
|
98 |
the induction step:
|
|
99 |
\begin{isabelle}%
|
|
100 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
|
17100
|
101 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\isanewline
|
|
102 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
|
16069
|
103 |
\end{isabelle}
|
|
104 |
The induction hypothesis is too weak. The fixed
|
|
105 |
argument,~\isa{{\isacharbrackleft}{\isacharbrackright}}, prevents it from rewriting the conclusion.
|
|
106 |
This example suggests a heuristic:
|
|
107 |
\begin{quote}\index{generalizing induction formulae}%
|
|
108 |
\emph{Generalize goals for induction by replacing constants by variables.}
|
|
109 |
\end{quote}
|
17100
|
110 |
Of course one cannot do this na\"{\i}vely: \isa{Itrev{\isachardot}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
|
16069
|
111 |
just not true. The correct generalization is%
|
|
112 |
\end{isamarkuptxt}%
|
17175
|
113 |
\isamarkuptrue%
|
|
114 |
\isamarkupfalse%
|
17056
|
115 |
%
|
|
116 |
\endisatagproof
|
|
117 |
{\isafoldproof}%
|
|
118 |
%
|
|
119 |
\isadelimproof
|
|
120 |
%
|
|
121 |
\endisadelimproof
|
17175
|
122 |
\isacommand{lemma}\isamarkupfalse%
|
|
123 |
\ {\isachardoublequoteopen}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}%
|
17056
|
124 |
\isadelimproof
|
|
125 |
%
|
|
126 |
\endisadelimproof
|
|
127 |
%
|
|
128 |
\isatagproof
|
17175
|
129 |
\isamarkupfalse%
|
16069
|
130 |
%
|
|
131 |
\begin{isamarkuptxt}%
|
|
132 |
\noindent
|
|
133 |
If \isa{ys} is replaced by \isa{{\isacharbrackleft}{\isacharbrackright}}, the right-hand side simplifies to
|
|
134 |
\isa{rev\ xs}, as required.
|
|
135 |
|
|
136 |
In this instance it was easy to guess the right generalization.
|
|
137 |
Other situations can require a good deal of creativity.
|
|
138 |
|
|
139 |
Although we now have two variables, only \isa{xs} is suitable for
|
|
140 |
induction, and we repeat our proof attempt. Unfortunately, we are still
|
|
141 |
not there:
|
|
142 |
\begin{isabelle}%
|
|
143 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
|
17100
|
144 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
|
|
145 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Itrev{\isachardot}itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
|
16069
|
146 |
\end{isabelle}
|
|
147 |
The induction hypothesis is still too weak, but this time it takes no
|
|
148 |
intuition to generalize: the problem is that \isa{ys} is fixed throughout
|
|
149 |
the subgoal, but the induction hypothesis needs to be applied with
|
|
150 |
\isa{a\ {\isacharhash}\ ys} instead of \isa{ys}. Hence we prove the theorem
|
|
151 |
for all \isa{ys} instead of a fixed one:%
|
|
152 |
\end{isamarkuptxt}%
|
17175
|
153 |
\isamarkuptrue%
|
|
154 |
\isamarkupfalse%
|
17056
|
155 |
%
|
|
156 |
\endisatagproof
|
|
157 |
{\isafoldproof}%
|
|
158 |
%
|
|
159 |
\isadelimproof
|
|
160 |
%
|
|
161 |
\endisadelimproof
|
17175
|
162 |
\isacommand{lemma}\isamarkupfalse%
|
|
163 |
\ {\isachardoublequoteopen}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}%
|
17056
|
164 |
\isadelimproof
|
|
165 |
%
|
|
166 |
\endisadelimproof
|
|
167 |
%
|
|
168 |
\isatagproof
|
17175
|
169 |
\isamarkupfalse%
|
17056
|
170 |
%
|
|
171 |
\endisatagproof
|
|
172 |
{\isafoldproof}%
|
|
173 |
%
|
|
174 |
\isadelimproof
|
|
175 |
%
|
|
176 |
\endisadelimproof
|
11866
|
177 |
%
|
9844
|
178 |
\begin{isamarkuptext}%
|
8749
|
179 |
\noindent
|
|
180 |
This time induction on \isa{xs} followed by simplification succeeds. This
|
|
181 |
leads to another heuristic for generalization:
|
|
182 |
\begin{quote}
|
9754
|
183 |
\emph{Generalize goals for induction by universally quantifying all free
|
8749
|
184 |
variables {\em(except the induction variable itself!)}.}
|
|
185 |
\end{quote}
|
11458
|
186 |
This prevents trivial failures like the one above and does not affect the
|
|
187 |
validity of the goal. However, this heuristic should not be applied blindly.
|
|
188 |
It is not always required, and the additional quantifiers can complicate
|
13081
|
189 |
matters in some cases. The variables that should be quantified are typically
|
11458
|
190 |
those that change in recursive calls.
|
9644
|
191 |
|
9844
|
192 |
A final point worth mentioning is the orientation of the equation we just
|
17100
|
193 |
proved: the more complex notion (\isa{Itrev{\isachardot}itrev}) is on the left-hand
|
9844
|
194 |
side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
|
|
195 |
another, albeit weak heuristic that is not restricted to induction:
|
|
196 |
\begin{quote}
|
|
197 |
\emph{The right-hand side of an equation should (in some sense) be simpler
|
|
198 |
than the left-hand side.}
|
|
199 |
\end{quote}
|
|
200 |
This heuristic is tricky to apply because it is not obvious that
|
17100
|
201 |
\isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{Itrev{\isachardot}itrev\ xs\ ys}. But see what
|
|
202 |
happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ Itrev{\isachardot}itrev\ xs\ ys}!
|
10971
|
203 |
|
11458
|
204 |
If you have tried these heuristics and still find your
|
10971
|
205 |
induction does not go through, and no obvious lemma suggests itself, you may
|
|
206 |
need to generalize your proposition even further. This requires insight into
|
11458
|
207 |
the problem at hand and is beyond simple rules of thumb.
|
|
208 |
Additionally, you can read \S\ref{sec:advanced-ind}
|
10971
|
209 |
to learn about some advanced techniques for inductive proofs.%
|
11458
|
210 |
\index{induction heuristics|)}%
|
9844
|
211 |
\end{isamarkuptext}%
|
17175
|
212 |
\isamarkuptrue%
|
17056
|
213 |
%
|
|
214 |
\isadelimtheory
|
|
215 |
%
|
|
216 |
\endisadelimtheory
|
|
217 |
%
|
|
218 |
\isatagtheory
|
17175
|
219 |
\isamarkupfalse%
|
17056
|
220 |
%
|
|
221 |
\endisatagtheory
|
|
222 |
{\isafoldtheory}%
|
|
223 |
%
|
|
224 |
\isadelimtheory
|
|
225 |
%
|
|
226 |
\endisadelimtheory
|
9722
|
227 |
\end{isabellebody}%
|
9145
|
228 |
%%% Local Variables:
|
|
229 |
%%% mode: latex
|
|
230 |
%%% TeX-master: "root"
|
|
231 |
%%% End:
|