24 on @{term xs}. |
24 on @{term xs}. |
25 |
25 |
26 The key heuristic, and the main point of this section, is to |
26 The key heuristic, and the main point of this section, is to |
27 generalize the goal before induction. The reason is simple: if the goal is |
27 generalize the goal before induction. The reason is simple: if the goal is |
28 too specific, the induction hypothesis is too weak to allow the induction |
28 too specific, the induction hypothesis is too weak to allow the induction |
29 step to go through. Let us now illustrate the idea with an example. |
29 step to go through. Let us illustrate the idea with an example. |
30 |
30 |
31 Function @{term"rev"} has quadratic worst-case running time |
31 Function @{term"rev"} has quadratic worst-case running time |
32 because it calls function @{text"@"} for each element of the list and |
32 because it calls function @{text"@"} for each element of the list and |
33 @{text"@"} is linear in its first argument. A linear time version of |
33 @{text"@"} is linear in its first argument. A linear time version of |
34 @{term"rev"} reqires an extra argument where the result is accumulated |
34 @{term"rev"} reqires an extra argument where the result is accumulated |
59 |
59 |
60 apply(induct_tac xs, simp_all); |
60 apply(induct_tac xs, simp_all); |
61 |
61 |
62 txt{*\noindent |
62 txt{*\noindent |
63 Unfortunately, this is not a complete success: |
63 Unfortunately, this is not a complete success: |
64 @{subgoals[display,indent=0,margin=65]} |
64 @{subgoals[display,indent=0,margin=70]} |
65 Just as predicted above, the overall goal, and hence the induction |
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 |
66 hypothesis, is too weak to solve the induction step because of the fixed |
67 argument, @{term"[]"}. This suggests a heuristic: |
67 argument, @{term"[]"}. This suggests a heuristic: |
68 \begin{quote} |
68 \begin{quote} |
69 \emph{Generalize goals for induction by replacing constants by variables.} |
69 \emph{Generalize goals for induction by replacing constants by variables.} |
70 \end{quote} |
70 \end{quote} |
71 Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is |
71 Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is |
72 just not true---the correct generalization is |
72 just not true --- the correct generalization is |
73 *}; |
73 *}; |
74 (*<*)oops;(*>*) |
74 (*<*)oops;(*>*) |
75 lemma "itrev xs ys = rev xs @ ys"; |
75 lemma "itrev xs ys = rev xs @ ys"; |
76 (*<*)apply(induct_tac xs, simp_all)(*>*) |
76 (*<*)apply(induct_tac xs, simp_all)(*>*) |
77 txt{*\noindent |
77 txt{*\noindent |
110 complicate matters in some cases, this heuristic is often not |
110 complicate matters in some cases, this heuristic is often not |
111 applied blindly. |
111 applied blindly. |
112 The variables that require generalization are typically those that |
112 The variables that require generalization are typically those that |
113 change in recursive calls. |
113 change in recursive calls. |
114 |
114 |
115 In general, if you have tried the above heuristics and still find your |
|
116 induction does not go through, and no obvious lemma suggests itself, you may |
|
117 need to generalize your proposition even further. This requires insight into |
|
118 the problem at hand and is beyond simple rules of thumb. You |
|
119 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
|
120 to learn about some advanced techniques for inductive proofs. |
|
121 |
|
122 A final point worth mentioning is the orientation of the equation we just |
115 A final point worth mentioning is the orientation of the equation we just |
123 proved: the more complex notion (@{term itrev}) is on the left-hand |
116 proved: the more complex notion (@{term itrev}) is on the left-hand |
124 side, the simpler one (@{term rev}) on the right-hand side. This constitutes |
117 side, the simpler one (@{term rev}) on the right-hand side. This constitutes |
125 another, albeit weak heuristic that is not restricted to induction: |
118 another, albeit weak heuristic that is not restricted to induction: |
126 \begin{quote} |
119 \begin{quote} |
128 than the left-hand side.} |
121 than the left-hand side.} |
129 \end{quote} |
122 \end{quote} |
130 This heuristic is tricky to apply because it is not obvious that |
123 This heuristic is tricky to apply because it is not obvious that |
131 @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what |
124 @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what |
132 happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}! |
125 happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}! |
|
126 |
|
127 In general, if you have tried the above heuristics and still find your |
|
128 induction does not go through, and no obvious lemma suggests itself, you may |
|
129 need to generalize your proposition even further. This requires insight into |
|
130 the problem at hand and is beyond simple rules of thumb. You |
|
131 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
|
132 to learn about some advanced techniques for inductive proofs. |
133 *} |
133 *} |
134 (*<*) |
134 (*<*) |
135 end |
135 end |
136 (*>*) |
136 (*>*) |