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=65]} |
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 @{term"[]"}. The corresponding 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 |
107 \end{quote} |
107 \end{quote} |
108 This prevents trivial failures like the above and does not change the |
108 This prevents trivial failures like the above and does not change the |
109 provability of the goal. Because it is not always required, and may even |
109 provability of the goal. Because it is not always required, and may even |
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 |
|
113 change in recursive calls. |
112 |
114 |
113 In general, if you have tried the above heuristics and still find your |
115 In general, if you have tried the above heuristics and still find your |
114 induction does not go through, and no obvious lemma suggests itself, you may |
116 induction does not go through, and no obvious lemma suggests itself, you may |
115 need to generalize your proposition even further. This requires insight into |
117 need to generalize your proposition even further. This requires insight into |
116 the problem at hand and is beyond simple rules of thumb. In a nutshell: you |
118 the problem at hand and is beyond simple rules of thumb. You |
117 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
119 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
118 to learn about some advanced techniques for inductive proofs. |
120 to learn about some advanced techniques for inductive proofs. |
119 |
121 |
120 A final point worth mentioning is the orientation of the equation we just |
122 A final point worth mentioning is the orientation of the equation we just |
121 proved: the more complex notion (@{term itrev}) is on the left-hand |
123 proved: the more complex notion (@{term itrev}) is on the left-hand |