3 \def\isabellecontext{Itrev}%
5 \isamarkupsection{Induction Heuristics%
9 \label{sec:InductionHeuristics}
10 The purpose of this section is to illustrate some simple heuristics for
11 inductive proofs. The first one we have already mentioned in our initial
14 \emph{Theorems about recursive functions are proved by induction.}
16 In case the function has more than one argument
18 \emph{Do induction on argument number $i$ if the function is defined by
19 recursion in argument number $i$.}
21 When we look at the proof of \isa{{\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}}
22 in \S\ref{sec:intro-proof} we find (a) \isa{{\isacharat}} is recursive in
23 the first argument, (b) \isa{xs} occurs only as the first argument of
24 \isa{{\isacharat}}, and (c) both \isa{ys} and \isa{zs} occur at least once as
25 the second argument of \isa{{\isacharat}}. Hence it is natural to perform induction
28 The key heuristic, and the main point of this section, is to
29 generalize the goal before induction. The reason is simple: if the goal is
30 too specific, the induction hypothesis is too weak to allow the induction
31 step to go through. Let us illustrate the idea with an example.
33 Function \isa{rev} has quadratic worst-case running time
34 because it calls function \isa{{\isacharat}} for each element of the list and
35 \isa{{\isacharat}} is linear in its first argument. A linear time version of
36 \isa{rev} reqires an extra argument where the result is accumulated
37 gradually, using only \isa{{\isacharhash}}:%
39 \isacommand{consts}\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
40 \isacommand{primrec}\isanewline
41 {\isachardoublequote}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
42 {\isachardoublequote}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequote}%
43 \begin{isamarkuptext}%
45 The behaviour of \isa{itrev} is simple: it reverses
46 its first argument by stacking its elements onto the second argument,
47 and returning that second argument when the first one becomes
48 empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
51 Naturally, we would like to show that \isa{itrev} does indeed reverse
52 its first argument provided the second one is empty:%
54 \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
57 There is no choice as to the induction variable, and we immediately simplify:%
59 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
62 Unfortunately, this is not a complete success:
64 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
65 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
67 Just as predicted above, the overall goal, and hence the induction
68 hypothesis, is too weak to solve the induction step because of the fixed
69 argument, \isa{{\isacharbrackleft}{\isacharbrackright}}. This suggests a heuristic:
71 \emph{Generalize goals for induction by replacing constants by variables.}
73 Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
74 just not true --- the correct generalization is%
76 \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
79 If \isa{ys} is replaced by \isa{{\isacharbrackleft}{\isacharbrackright}}, the right-hand side simplifies to
80 \isa{rev\ xs}, just as required.
82 In this particular instance it was easy to guess the right generalization,
83 but in more complex situations a good deal of creativity is needed. This is
84 the main source of complications in inductive proofs.
86 Although we now have two variables, only \isa{xs} is suitable for
87 induction, and we repeat our above proof attempt. Unfortunately, we are still
90 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
91 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
92 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
94 The induction hypothesis is still too weak, but this time it takes no
95 intuition to generalize: the problem is that \isa{ys} is fixed throughout
96 the subgoal, but the induction hypothesis needs to be applied with
97 \isa{a\ {\isacharhash}\ ys} instead of \isa{ys}. Hence we prove the theorem
98 for all \isa{ys} instead of a fixed one:%
100 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
101 \begin{isamarkuptext}%
103 This time induction on \isa{xs} followed by simplification succeeds. This
104 leads to another heuristic for generalization:
106 \emph{Generalize goals for induction by universally quantifying all free
107 variables {\em(except the induction variable itself!)}.}
109 This prevents trivial failures like the above and does not change the
110 provability of the goal. Because it is not always required, and may even
111 complicate matters in some cases, this heuristic is often not
113 The variables that require generalization are typically those that
114 change in recursive calls.
116 A final point worth mentioning is the orientation of the equation we just
117 proved: the more complex notion (\isa{itrev}) is on the left-hand
118 side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
119 another, albeit weak heuristic that is not restricted to induction:
121 \emph{The right-hand side of an equation should (in some sense) be simpler
122 than the left-hand side.}
124 This heuristic is tricky to apply because it is not obvious that
125 \isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
126 happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!
128 In general, if you have tried the above heuristics and still find your
129 induction does not go through, and no obvious lemma suggests itself, you may
130 need to generalize your proposition even further. This requires insight into
131 the problem at hand and is beyond simple rules of thumb. You
132 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
133 to learn about some advanced techniques for inductive proofs.%
138 %%% TeX-master: "root"