src/Doc/Tutorial/Misc/Itrev.thy
 author wenzelm Sat Nov 01 14:20:38 2014 +0100 (2014-11-01) changeset 58860 fee7cfa69c50 parent 48985 5386df44a037 child 67406 23307fd33906 permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)

     2 theory Itrev

     3 imports Main

     4 begin

     5 declare [[names_unique = false]]

     6 (*>*)

     7

     8 section{*Induction Heuristics*}

     9

    10 text{*\label{sec:InductionHeuristics}

    11 \index{induction heuristics|(}%

    12 The purpose of this section is to illustrate some simple heuristics for

    13 inductive proofs. The first one we have already mentioned in our initial

    14 example:

    15 \begin{quote}

    16 \emph{Theorems about recursive functions are proved by induction.}

    17 \end{quote}

    18 In case the function has more than one argument

    19 \begin{quote}

    20 \emph{Do induction on argument number $i$ if the function is defined by

    21 recursion in argument number $i$.}

    22 \end{quote}

    23 When we look at the proof of @{text"(xs@ys) @ zs = xs @ (ys@zs)"}

    24 in \S\ref{sec:intro-proof} we find

    25 \begin{itemize}

    26 \item @{text"@"} is recursive in

    27 the first argument

    28 \item @{term xs}  occurs only as the first argument of

    29 @{text"@"}

    30 \item both @{term ys} and @{term zs} occur at least once as

    31 the second argument of @{text"@"}

    32 \end{itemize}

    33 Hence it is natural to perform induction on~@{term xs}.

    34

    35 The key heuristic, and the main point of this section, is to

    36 \emph{generalize the goal before induction}.

    37 The reason is simple: if the goal is

    38 too specific, the induction hypothesis is too weak to allow the induction

    39 step to go through. Let us illustrate the idea with an example.

    40

    41 Function \cdx{rev} has quadratic worst-case running time

    42 because it calls function @{text"@"} for each element of the list and

    43 @{text"@"} is linear in its first argument.  A linear time version of

    44 @{term"rev"} reqires an extra argument where the result is accumulated

    45 gradually, using only~@{text"#"}:

    46 *}

    47

    48 primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

    49 "itrev []     ys = ys" |

    50 "itrev (x#xs) ys = itrev xs (x#ys)"

    51

    52 text{*\noindent

    53 The behaviour of \cdx{itrev} is simple: it reverses

    54 its first argument by stacking its elements onto the second argument,

    55 and returning that second argument when the first one becomes

    56 empty. Note that @{term"itrev"} is tail-recursive: it can be

    57 compiled into a loop.

    58

    59 Naturally, we would like to show that @{term"itrev"} does indeed reverse

    60 its first argument provided the second one is empty:

    61 *}

    62

    63 lemma "itrev xs [] = rev xs"

    64

    65 txt{*\noindent

    66 There is no choice as to the induction variable, and we immediately simplify:

    67 *}

    68

    69 apply(induct_tac xs, simp_all)

    70

    71 txt{*\noindent

    72 Unfortunately, this attempt does not prove

    73 the induction step:

    74 @{subgoals[display,indent=0,margin=70]}

    75 The induction hypothesis is too weak.  The fixed

    76 argument,~@{term"[]"}, prevents it from rewriting the conclusion.

    77 This example suggests a heuristic:

    78 \begin{quote}\index{generalizing induction formulae}%

    79 \emph{Generalize goals for induction by replacing constants by variables.}

    80 \end{quote}

    81 Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is

    82 just not true.  The correct generalization is

    83 *}

    84 (*<*)oops(*>*)

    85 lemma "itrev xs ys = rev xs @ ys"

    86 (*<*)apply(induct_tac xs, simp_all)(*>*)

    87 txt{*\noindent

    88 If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to

    89 @{term"rev xs"}, as required.

    90

    91 In this instance it was easy to guess the right generalization.

    92 Other situations can require a good deal of creativity.

    93

    94 Although we now have two variables, only @{term"xs"} is suitable for

    95 induction, and we repeat our proof attempt. Unfortunately, we are still

    96 not there:

    97 @{subgoals[display,indent=0,goals_limit=1]}

    98 The induction hypothesis is still too weak, but this time it takes no

    99 intuition to generalize: the problem is that @{term"ys"} is fixed throughout

   100 the subgoal, but the induction hypothesis needs to be applied with

   101 @{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem

   102 for all @{term"ys"} instead of a fixed one:

   103 *}

   104 (*<*)oops(*>*)

   105 lemma "\<forall>ys. itrev xs ys = rev xs @ ys"

   106 (*<*)

   107 by(induct_tac xs, simp_all)

   108 (*>*)

   109

   110 text{*\noindent

   111 This time induction on @{term"xs"} followed by simplification succeeds. This

   112 leads to another heuristic for generalization:

   113 \begin{quote}

   114 \emph{Generalize goals for induction by universally quantifying all free

   115 variables {\em(except the induction variable itself!)}.}

   116 \end{quote}

   117 This prevents trivial failures like the one above and does not affect the

   118 validity of the goal.  However, this heuristic should not be applied blindly.

   119 It is not always required, and the additional quantifiers can complicate

   120 matters in some cases. The variables that should be quantified are typically

   121 those that change in recursive calls.

   122

   123 A final point worth mentioning is the orientation of the equation we just

   124 proved: the more complex notion (@{const itrev}) is on the left-hand

   125 side, the simpler one (@{term rev}) on the right-hand side. This constitutes

   126 another, albeit weak heuristic that is not restricted to induction:

   127 \begin{quote}

   128   \emph{The right-hand side of an equation should (in some sense) be simpler

   129     than the left-hand side.}

   130 \end{quote}

   131 This heuristic is tricky to apply because it is not obvious that

   132 @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what

   133 happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!

   134

   135 If you have tried these heuristics and still find your

   136 induction does not go through, and no obvious lemma suggests itself, you may

   137 need to generalize your proposition even further. This requires insight into

   138 the problem at hand and is beyond simple rules of thumb.

   139 Additionally, you can read \S\ref{sec:advanced-ind}

   140 to learn about some advanced techniques for inductive proofs.%

   141 \index{induction heuristics|)}

   142 *}

   143 (*<*)

   144 declare [[names_unique = true]]

   145 end

   146 (*>*)