1 (*<*) |
1 (*<*) |
2 theory Itrev = Main:; |
2 theory Itrev = Main:; |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{* |
5 section{*Induction heuristics*} |
|
6 |
|
7 text{*\label{sec:InductionHeuristics} |
|
8 The purpose of this section is to illustrate some simple heuristics for |
|
9 inductive proofs. The first one we have already mentioned in our initial |
|
10 example: |
|
11 \begin{quote} |
|
12 \emph{Theorems about recursive functions are proved by induction.} |
|
13 \end{quote} |
|
14 In case the function has more than one argument |
|
15 \begin{quote} |
|
16 \emph{Do induction on argument number $i$ if the function is defined by |
|
17 recursion in argument number $i$.} |
|
18 \end{quote} |
|
19 When we look at the proof of @{term[source]"(xs @ ys) @ zs = xs @ (ys @ zs)"} |
|
20 in \S\ref{sec:intro-proof} we find (a) @{text"@"} is recursive in |
|
21 the first argument, (b) @{term xs} occurs only as the first argument of |
|
22 @{text"@"}, and (c) both @{term ys} and @{term zs} occur at least once as |
|
23 the second argument of @{text"@"}. Hence it is natural to perform induction |
|
24 on @{term xs}. |
|
25 |
|
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 |
|
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. |
|
30 |
6 Function @{term"rev"} has quadratic worst-case running time |
31 Function @{term"rev"} has quadratic worst-case running time |
7 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 |
8 @{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 |
9 @{term"rev"} reqires an extra argument where the result is accumulated |
34 @{term"rev"} reqires an extra argument where the result is accumulated |
10 gradually, using only @{text"#"}: |
35 gradually, using only @{text"#"}: |
34 |
59 |
35 apply(induct_tac xs, simp_all); |
60 apply(induct_tac xs, simp_all); |
36 |
61 |
37 txt{*\noindent |
62 txt{*\noindent |
38 Unfortunately, this is not a complete success: |
63 Unfortunately, this is not a complete success: |
39 \begin{isabelle} |
64 \begin{isabelle}\makeatother |
40 ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]% |
65 ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]% |
41 \end{isabelle} |
66 \end{isabelle} |
42 Just as predicted above, the overall goal, and hence the induction |
67 Just as predicted above, the overall goal, and hence the induction |
43 hypothesis, is too weak to solve the induction step because of the fixed |
68 hypothesis, is too weak to solve the induction step because of the fixed |
44 @{term"[]"}. The corresponding heuristic: |
69 @{term"[]"}. The corresponding heuristic: |
60 the main source of complications in inductive proofs. |
85 the main source of complications in inductive proofs. |
61 |
86 |
62 Although we now have two variables, only @{term"xs"} is suitable for |
87 Although we now have two variables, only @{term"xs"} is suitable for |
63 induction, and we repeat our above proof attempt. Unfortunately, we are still |
88 induction, and we repeat our above proof attempt. Unfortunately, we are still |
64 not there: |
89 not there: |
65 \begin{isabelle} |
90 \begin{isabelle}\makeatother |
66 ~1.~{\isasymAnd}a~list.\isanewline |
91 ~1.~{\isasymAnd}a~list.\isanewline |
67 ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline |
92 ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline |
68 ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys |
93 ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys |
69 \end{isabelle} |
94 \end{isabelle} |
70 The induction hypothesis is still too weak, but this time it takes no |
95 The induction hypothesis is still too weak, but this time it takes no |
73 @{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem |
98 @{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem |
74 for all @{term"ys"} instead of a fixed one: |
99 for all @{term"ys"} instead of a fixed one: |
75 *}; |
100 *}; |
76 (*<*)oops;(*>*) |
101 (*<*)oops;(*>*) |
77 lemma "\\<forall>ys. itrev xs ys = rev xs @ ys"; |
102 lemma "\\<forall>ys. itrev xs ys = rev xs @ ys"; |
|
103 (*<*) |
|
104 by(induct_tac xs, simp_all); |
|
105 (*>*) |
78 |
106 |
79 txt{*\noindent |
107 text{*\noindent |
80 This time induction on @{term"xs"} followed by simplification succeeds. This |
108 This time induction on @{term"xs"} followed by simplification succeeds. This |
81 leads to another heuristic for generalization: |
109 leads to another heuristic for generalization: |
82 \begin{quote} |
110 \begin{quote} |
83 \emph{Generalize goals for induction by universally quantifying all free |
111 \emph{Generalize goals for induction by universally quantifying all free |
84 variables {\em(except the induction variable itself!)}.} |
112 variables {\em(except the induction variable itself!)}.} |
92 induction does not go through, and no obvious lemma suggests itself, you may |
120 induction does not go through, and no obvious lemma suggests itself, you may |
93 need to generalize your proposition even further. This requires insight into |
121 need to generalize your proposition even further. This requires insight into |
94 the problem at hand and is beyond simple rules of thumb. In a nutshell: you |
122 the problem at hand and is beyond simple rules of thumb. In a nutshell: you |
95 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
123 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
96 to learn about some advanced techniques for inductive proofs. |
124 to learn about some advanced techniques for inductive proofs. |
97 *}; |
|
98 |
125 |
|
126 A final point worth mentioning is the orientation of the equation we just |
|
127 proved: the more complex notion (@{term itrev}) is on the left-hand |
|
128 side, the simpler one (@{term rev}) on the right-hand side. This constitutes |
|
129 another, albeit weak heuristic that is not restricted to induction: |
|
130 \begin{quote} |
|
131 \emph{The right-hand side of an equation should (in some sense) be simpler |
|
132 than the left-hand side.} |
|
133 \end{quote} |
|
134 This heuristic is tricky to apply because it is not obvious that |
|
135 @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what |
|
136 happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}! |
|
137 *} |
99 (*<*) |
138 (*<*) |
100 by(induct_tac xs, simp_all); |
|
101 end |
139 end |
102 (*>*) |
140 (*>*) |