doc-src/TutorialI/Misc/document/Itrev.tex
author nipkow
Tue, 31 Oct 2000 08:53:12 +0100
changeset 10362 c6b197ccf1f1
parent 9924 3370f6aa3200
child 10395 7ef380745743
permissions -rw-r--r--
*** empty log message ***
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Itrev}%
     4 %
     5 \isamarkupsection{Induction heuristics}
     6 %
     7 \begin{isamarkuptext}%
     8 \label{sec:InductionHeuristics}
     9 The purpose of this section is to illustrate some simple heuristics for
    10 inductive proofs. The first one we have already mentioned in our initial
    11 example:
    12 \begin{quote}
    13 \emph{Theorems about recursive functions are proved by induction.}
    14 \end{quote}
    15 In case the function has more than one argument
    16 \begin{quote}
    17 \emph{Do induction on argument number $i$ if the function is defined by
    18 recursion in argument number $i$.}
    19 \end{quote}
    20 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}}
    21 in \S\ref{sec:intro-proof} we find (a) \isa{{\isacharat}} is recursive in
    22 the first argument, (b) \isa{xs} occurs only as the first argument of
    23 \isa{{\isacharat}}, and (c) both \isa{ys} and \isa{zs} occur at least once as
    24 the second argument of \isa{{\isacharat}}. Hence it is natural to perform induction
    25 on \isa{xs}.
    26 
    27 The key heuristic, and the main point of this section, is to
    28 generalize the goal before induction. The reason is simple: if the goal is
    29 too specific, the induction hypothesis is too weak to allow the induction
    30 step to go through. Let us now illustrate the idea with an example.
    31 
    32 Function \isa{rev} has quadratic worst-case running time
    33 because it calls function \isa{{\isacharat}} for each element of the list and
    34 \isa{{\isacharat}} is linear in its first argument.  A linear time version of
    35 \isa{rev} reqires an extra argument where the result is accumulated
    36 gradually, using only \isa{{\isacharhash}}:%
    37 \end{isamarkuptext}%
    38 \isacommand{consts}\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    39 \isacommand{primrec}\isanewline
    40 {\isachardoublequote}itrev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ ys\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
    41 {\isachardoublequote}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequote}%
    42 \begin{isamarkuptext}%
    43 \noindent
    44 The behaviour of \isa{itrev} is simple: it reverses
    45 its first argument by stacking its elements onto the second argument,
    46 and returning that second argument when the first one becomes
    47 empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
    48 compiled into a loop.
    49 
    50 Naturally, we would like to show that \isa{itrev} does indeed reverse
    51 its first argument provided the second one is empty:%
    52 \end{isamarkuptext}%
    53 \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
    54 \begin{isamarkuptxt}%
    55 \noindent
    56 There is no choice as to the induction variable, and we immediately simplify:%
    57 \end{isamarkuptxt}%
    58 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
    59 \begin{isamarkuptxt}%
    60 \noindent
    61 Unfortunately, this is not a complete success:
    62 \begin{isabelle}\makeatother
    63 ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
    64 \end{isabelle}
    65 Just as predicted above, the overall goal, and hence the induction
    66 hypothesis, is too weak to solve the induction step because of the fixed
    67 \isa{{\isacharbrackleft}{\isacharbrackright}}. The corresponding heuristic:
    68 \begin{quote}
    69 \emph{Generalize goals for induction by replacing constants by variables.}
    70 \end{quote}
    71 Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
    72 just not true---the correct generalization is%
    73 \end{isamarkuptxt}%
    74 \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
    75 \begin{isamarkuptxt}%
    76 \noindent
    77 If \isa{ys} is replaced by \isa{{\isacharbrackleft}{\isacharbrackright}}, the right-hand side simplifies to
    78 \isa{rev\ xs}, just as required.
    79 
    80 In this particular instance it was easy to guess the right generalization,
    81 but in more complex situations a good deal of creativity is needed. This is
    82 the main source of complications in inductive proofs.
    83 
    84 Although we now have two variables, only \isa{xs} is suitable for
    85 induction, and we repeat our above proof attempt. Unfortunately, we are still
    86 not there:
    87 \begin{isabelle}%
    88 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
    89 \ \ \ \ \ \ \ itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
    90 \ \ \ \ \ \ \ itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
    91 \end{isabelle}
    92 The induction hypothesis is still too weak, but this time it takes no
    93 intuition to generalize: the problem is that \isa{ys} is fixed throughout
    94 the subgoal, but the induction hypothesis needs to be applied with
    95 \isa{a\ {\isacharhash}\ ys} instead of \isa{ys}. Hence we prove the theorem
    96 for all \isa{ys} instead of a fixed one:%
    97 \end{isamarkuptxt}%
    98 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
    99 \begin{isamarkuptext}%
   100 \noindent
   101 This time induction on \isa{xs} followed by simplification succeeds. This
   102 leads to another heuristic for generalization:
   103 \begin{quote}
   104 \emph{Generalize goals for induction by universally quantifying all free
   105 variables {\em(except the induction variable itself!)}.}
   106 \end{quote}
   107 This prevents trivial failures like the above and does not change the
   108 provability of the goal. Because it is not always required, and may even
   109 complicate matters in some cases, this heuristic is often not
   110 applied blindly.
   111 
   112 In general, if you have tried the above heuristics and still find your
   113 induction does not go through, and no obvious lemma suggests itself, you may
   114 need to generalize your proposition even further. This requires insight into
   115 the problem at hand and is beyond simple rules of thumb. In a nutshell: you
   116 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
   117 to learn about some advanced techniques for inductive proofs.
   118 
   119 A final point worth mentioning is the orientation of the equation we just
   120 proved: the more complex notion (\isa{itrev}) is on the left-hand
   121 side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
   122 another, albeit weak heuristic that is not restricted to induction:
   123 \begin{quote}
   124   \emph{The right-hand side of an equation should (in some sense) be simpler
   125     than the left-hand side.}
   126 \end{quote}
   127 This heuristic is tricky to apply because it is not obvious that
   128 \isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
   129 happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!%
   130 \end{isamarkuptext}%
   131 \end{isabellebody}%
   132 %%% Local Variables:
   133 %%% mode: latex
   134 %%% TeX-master: "root"
   135 %%% End: