5 Function \isa{rev} has quadratic worst-case running time
6 because it calls function \isa{{\isacharat}} for each element of the list and
7 \isa{{\isacharat}} is linear in its first argument. A linear time version of
8 \isa{rev} reqires an extra argument where the result is accumulated
9 gradually, using only \isa{{\isacharhash}}:%
11 \isacommand{consts}\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
12 \isacommand{primrec}\isanewline
13 {\isachardoublequote}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
14 {\isachardoublequote}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequote}%
15 \begin{isamarkuptext}%
17 The behaviour of \isa{itrev} is simple: it reverses
18 its first argument by stacking its elements onto the second argument,
19 and returning that second argument when the first one becomes
20 empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
23 Naturally, we would like to show that \isa{itrev} does indeed reverse
24 its first argument provided the second one is empty:%
26 \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
29 There is no choice as to the induction variable, and we immediately simplify:%
31 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
34 Unfortunately, this is not a complete success:
36 ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
38 Just as predicted above, the overall goal, and hence the induction
39 hypothesis, is too weak to solve the induction step because of the fixed
40 \isa{{\isacharbrackleft}{\isacharbrackright}}. The corresponding heuristic:
42 \emph{Generalize goals for induction by replacing constants by variables.}
44 Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
45 just not true---the correct generalization is%
47 \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
50 If \isa{ys} is replaced by \isa{{\isacharbrackleft}{\isacharbrackright}}, the right-hand side simplifies to
51 \isa{rev\ xs}, just as required.
53 In this particular instance it was easy to guess the right generalization,
54 but in more complex situations a good deal of creativity is needed. This is
55 the main source of complications in inductive proofs.
57 Although we now have two variables, only \isa{xs} is suitable for
58 induction, and we repeat our above proof attempt. Unfortunately, we are still
61 ~1.~{\isasymAnd}a~list.\isanewline
62 ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
63 ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
65 The induction hypothesis is still too weak, but this time it takes no
66 intuition to generalize: the problem is that \isa{ys} is fixed throughout
67 the subgoal, but the induction hypothesis needs to be applied with
68 \isa{a\ {\isacharhash}\ ys} instead of \isa{ys}. Hence we prove the theorem
69 for all \isa{ys} instead of a fixed one:%
71 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
74 This time induction on \isa{xs} followed by simplification succeeds. This
75 leads to another heuristic for generalization:
77 \emph{Generalize goals for induction by universally quantifying all free
78 variables {\em(except the induction variable itself!)}.}
80 This prevents trivial failures like the above and does not change the
81 provability of the goal. Because it is not always required, and may even
82 complicate matters in some cases, this heuristic is often not
85 In general, if you have tried the above heuristics and still find your
86 induction does not go through, and no obvious lemma suggests itself, you may
87 need to generalize your proposition even further. This requires insight into
88 the problem at hand and is beyond simple rules of thumb. In a nutshell: you
89 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
90 to learn about some advanced techniques for inductive proofs.%
95 %%% TeX-master: "root"