author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
8745 | 1 |
(*<*) |
17326 | 2 |
theory Itrev |
3 |
imports Main |
|
4 |
begin |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42358
diff
changeset
|
5 |
declare [[names_unique = false]] |
8745 | 6 |
(*>*) |
7 |
||
67406 | 8 |
section\<open>Induction Heuristics\<close> |
9844 | 9 |
|
67406 | 10 |
text\<open>\label{sec:InductionHeuristics} |
11458 | 11 |
\index{induction heuristics|(}% |
9844 | 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} |
|
69505 | 23 |
When we look at the proof of \<open>(xs@ys) @ zs = xs @ (ys@zs)\<close> |
11458 | 24 |
in \S\ref{sec:intro-proof} we find |
25 |
\begin{itemize} |
|
69505 | 26 |
\item \<open>@\<close> is recursive in |
11458 | 27 |
the first argument |
69597 | 28 |
\item \<^term>\<open>xs\<close> occurs only as the first argument of |
69505 | 29 |
\<open>@\<close> |
69597 | 30 |
\item both \<^term>\<open>ys\<close> and \<^term>\<open>zs\<close> occur at least once as |
69505 | 31 |
the second argument of \<open>@\<close> |
11458 | 32 |
\end{itemize} |
69597 | 33 |
Hence it is natural to perform induction on~\<^term>\<open>xs\<close>. |
9844 | 34 |
|
35 |
The key heuristic, and the main point of this section, is to |
|
11458 | 36 |
\emph{generalize the goal before induction}. |
37 |
The reason is simple: if the goal is |
|
9844 | 38 |
too specific, the induction hypothesis is too weak to allow the induction |
10971 | 39 |
step to go through. Let us illustrate the idea with an example. |
9844 | 40 |
|
11458 | 41 |
Function \cdx{rev} has quadratic worst-case running time |
69505 | 42 |
because it calls function \<open>@\<close> for each element of the list and |
43 |
\<open>@\<close> is linear in its first argument. A linear time version of |
|
69597 | 44 |
\<^term>\<open>rev\<close> reqires an extra argument where the result is accumulated |
69505 | 45 |
gradually, using only~\<open>#\<close>: |
67406 | 46 |
\<close> |
8745 | 47 |
|
27015 | 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)" |
|
8745 | 51 |
|
67406 | 52 |
text\<open>\noindent |
11458 | 53 |
The behaviour of \cdx{itrev} is simple: it reverses |
9493 | 54 |
its first argument by stacking its elements onto the second argument, |
55 |
and returning that second argument when the first one becomes |
|
69597 | 56 |
empty. Note that \<^term>\<open>itrev\<close> is tail-recursive: it can be |
9493 | 57 |
compiled into a loop. |
58 |
||
69597 | 59 |
Naturally, we would like to show that \<^term>\<open>itrev\<close> does indeed reverse |
9754 | 60 |
its first argument provided the second one is empty: |
67406 | 61 |
\<close> |
8745 | 62 |
|
58860 | 63 |
lemma "itrev xs [] = rev xs" |
8745 | 64 |
|
67406 | 65 |
txt\<open>\noindent |
8745 | 66 |
There is no choice as to the induction variable, and we immediately simplify: |
67406 | 67 |
\<close> |
8745 | 68 |
|
58860 | 69 |
apply(induct_tac xs, simp_all) |
8745 | 70 |
|
67406 | 71 |
txt\<open>\noindent |
11458 | 72 |
Unfortunately, this attempt does not prove |
73 |
the induction step: |
|
10971 | 74 |
@{subgoals[display,indent=0,margin=70]} |
11458 | 75 |
The induction hypothesis is too weak. The fixed |
69597 | 76 |
argument,~\<^term>\<open>[]\<close>, prevents it from rewriting the conclusion. |
11458 | 77 |
This example suggests a heuristic: |
78 |
\begin{quote}\index{generalizing induction formulae}% |
|
9754 | 79 |
\emph{Generalize goals for induction by replacing constants by variables.} |
8745 | 80 |
\end{quote} |
69597 | 81 |
Of course one cannot do this na\"{\i}vely: \<^term>\<open>itrev xs ys = rev xs\<close> is |
11458 | 82 |
just not true. The correct generalization is |
67406 | 83 |
\<close> |
58860 | 84 |
(*<*)oops(*>*) |
85 |
lemma "itrev xs ys = rev xs @ ys" |
|
10362 | 86 |
(*<*)apply(induct_tac xs, simp_all)(*>*) |
67406 | 87 |
txt\<open>\noindent |
69597 | 88 |
If \<^term>\<open>ys\<close> is replaced by \<^term>\<open>[]\<close>, the right-hand side simplifies to |
89 |
\<^term>\<open>rev xs\<close>, as required. |
|
8745 | 90 |
|
11458 | 91 |
In this instance it was easy to guess the right generalization. |
92 |
Other situations can require a good deal of creativity. |
|
8745 | 93 |
|
69597 | 94 |
Although we now have two variables, only \<^term>\<open>xs\<close> is suitable for |
11458 | 95 |
induction, and we repeat our proof attempt. Unfortunately, we are still |
8745 | 96 |
not there: |
10362 | 97 |
@{subgoals[display,indent=0,goals_limit=1]} |
8745 | 98 |
The induction hypothesis is still too weak, but this time it takes no |
69597 | 99 |
intuition to generalize: the problem is that \<^term>\<open>ys\<close> is fixed throughout |
8745 | 100 |
the subgoal, but the induction hypothesis needs to be applied with |
69597 | 101 |
\<^term>\<open>a # ys\<close> instead of \<^term>\<open>ys\<close>. Hence we prove the theorem |
102 |
for all \<^term>\<open>ys\<close> instead of a fixed one: |
|
67406 | 103 |
\<close> |
58860 | 104 |
(*<*)oops(*>*) |
105 |
lemma "\<forall>ys. itrev xs ys = rev xs @ ys" |
|
9844 | 106 |
(*<*) |
58860 | 107 |
by(induct_tac xs, simp_all) |
9844 | 108 |
(*>*) |
8745 | 109 |
|
67406 | 110 |
text\<open>\noindent |
69597 | 111 |
This time induction on \<^term>\<open>xs\<close> followed by simplification succeeds. This |
8745 | 112 |
leads to another heuristic for generalization: |
113 |
\begin{quote} |
|
9754 | 114 |
\emph{Generalize goals for induction by universally quantifying all free |
8745 | 115 |
variables {\em(except the induction variable itself!)}.} |
116 |
\end{quote} |
|
11458 | 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 |
|
13081 | 120 |
matters in some cases. The variables that should be quantified are typically |
11458 | 121 |
those that change in recursive calls. |
9644 | 122 |
|
9844 | 123 |
A final point worth mentioning is the orientation of the equation we just |
69597 | 124 |
proved: the more complex notion (\<^const>\<open>itrev\<close>) is on the left-hand |
125 |
side, the simpler one (\<^term>\<open>rev\<close>) on the right-hand side. This constitutes |
|
9844 | 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 |
|
69597 | 132 |
\<^term>\<open>rev xs @ ys\<close> is simpler than \<^term>\<open>itrev xs ys\<close>. But see what |
133 |
happens if you try to prove \<^prop>\<open>rev xs @ ys = itrev xs ys\<close>! |
|
10971 | 134 |
|
11458 | 135 |
If you have tried these heuristics and still find your |
10971 | 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 |
|
11458 | 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|)} |
|
67406 | 142 |
\<close> |
8745 | 143 |
(*<*) |
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42358
diff
changeset
|
144 |
declare [[names_unique = true]] |
8745 | 145 |
end |
146 |
(*>*) |