nipkow@8745

1 
(*<*)

nipkow@17326

2 
theory Itrev

nipkow@17326

3 
imports Main

nipkow@17326

4 
begin

wenzelm@42669

5 
declare [[names_unique = false]]

nipkow@8745

6 
(*>*)

nipkow@8745

7 

paulson@10885

8 
section{*Induction Heuristics*}

nipkow@9844

9 

nipkow@9844

10 
text{*\label{sec:InductionHeuristics}

paulson@11458

11 
\index{induction heuristics(}%

nipkow@9844

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

nipkow@9844

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

nipkow@9844

14 
example:

nipkow@9844

15 
\begin{quote}

nipkow@9844

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

nipkow@9844

17 
\end{quote}

nipkow@9844

18 
In case the function has more than one argument

nipkow@9844

19 
\begin{quote}

nipkow@9844

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

nipkow@9844

21 
recursion in argument number $i$.}

nipkow@9844

22 
\end{quote}

paulson@11458

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

paulson@11458

24 
in \S\ref{sec:introproof} we find

paulson@11458

25 
\begin{itemize}

paulson@11458

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

paulson@11458

27 
the first argument

paulson@11458

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

paulson@11458

29 
@{text"@"}

paulson@11458

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

paulson@11458

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

paulson@11458

32 
\end{itemize}

paulson@11458

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

nipkow@9844

34 

nipkow@9844

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

paulson@11458

36 
\emph{generalize the goal before induction}.

paulson@11458

37 
The reason is simple: if the goal is

nipkow@9844

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

nipkow@10971

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

nipkow@9844

40 

paulson@11458

41 
Function \cdx{rev} has quadratic worstcase running time

nipkow@9792

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

nipkow@9792

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

nipkow@9754

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

paulson@11458

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

nipkow@9754

46 
*}

nipkow@8745

47 

nipkow@27015

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

nipkow@27015

49 
"itrev [] ys = ys" 

nipkow@27015

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

nipkow@8745

51 

nipkow@9754

52 
text{*\noindent

paulson@11458

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

nipkow@9493

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

nipkow@9493

55 
and returning that second argument when the first one becomes

paulson@11458

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

nipkow@9493

57 
compiled into a loop.

nipkow@9493

58 

nipkow@9754

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

nipkow@9754

60 
its first argument provided the second one is empty:

nipkow@9754

61 
*};

nipkow@8745

62 

nipkow@8745

63 
lemma "itrev xs [] = rev xs";

nipkow@8745

64 

nipkow@8745

65 
txt{*\noindent

nipkow@8745

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

nipkow@9458

67 
*};

nipkow@8745

68 

nipkow@9689

69 
apply(induct_tac xs, simp_all);

nipkow@8745

70 

nipkow@8745

71 
txt{*\noindent

paulson@11458

72 
Unfortunately, this attempt does not prove

paulson@11458

73 
the induction step:

nipkow@10971

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

paulson@11458

75 
The induction hypothesis is too weak. The fixed

paulson@11458

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

paulson@11458

77 
This example suggests a heuristic:

paulson@11458

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

nipkow@9754

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

nipkow@8745

80 
\end{quote}

nipkow@9754

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

paulson@11458

82 
just not true. The correct generalization is

nipkow@9458

83 
*};

nipkow@8745

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

nipkow@8745

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

nipkow@10362

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

nipkow@8745

87 
txt{*\noindent

nipkow@9754

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

paulson@11458

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

nipkow@8745

90 

paulson@11458

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

paulson@11458

92 
Other situations can require a good deal of creativity.

nipkow@8745

93 

nipkow@9754

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

paulson@11458

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

nipkow@8745

96 
not there:

nipkow@10362

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

nipkow@8745

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

nipkow@9754

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

nipkow@8745

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

nipkow@9754

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

nipkow@9754

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

nipkow@9458

103 
*};

nipkow@8745

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

nipkow@10362

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

nipkow@9844

106 
(*<*)

nipkow@9844

107 
by(induct_tac xs, simp_all);

nipkow@9844

108 
(*>*)

nipkow@8745

109 

nipkow@9844

110 
text{*\noindent

nipkow@9754

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

nipkow@8745

112 
leads to another heuristic for generalization:

nipkow@8745

113 
\begin{quote}

nipkow@9754

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

nipkow@8745

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

nipkow@8745

116 
\end{quote}

paulson@11458

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

paulson@11458

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

paulson@11458

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

nipkow@13081

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

paulson@11458

121 
those that change in recursive calls.

nipkow@9644

122 

nipkow@9844

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

haftmann@15905

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

nipkow@9844

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

nipkow@9844

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

nipkow@9844

127 
\begin{quote}

nipkow@9844

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

nipkow@9844

129 
than the lefthand side.}

nipkow@9844

130 
\end{quote}

nipkow@9844

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

nipkow@9844

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

nipkow@9844

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

nipkow@10971

134 

paulson@11458

135 
If you have tried these heuristics and still find your

nipkow@10971

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

nipkow@10971

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

paulson@11458

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

paulson@11458

139 
Additionally, you can read \S\ref{sec:advancedind}

paulson@11458

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

paulson@11458

141 
\index{induction heuristics)}

nipkow@9844

142 
*}

nipkow@8745

143 
(*<*)

wenzelm@42669

144 
declare [[names_unique = true]]

nipkow@8745

145 
end

nipkow@8745

146 
(*>*)
