doc-src/TutorialI/Misc/document/Itrev.tex

-%
-\begin{isabellebody}%
-\def\isabellecontext{Itrev}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Induction Heuristics%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:InductionHeuristics}
-\index{induction heuristics|(}%
-The purpose of this section is to illustrate some simple heuristics for
-inductive proofs. The first one we have already mentioned in our initial
-example:
-\begin{quote}
-\emph{Theorems about recursive functions are proved by induction.}
-\end{quote}
-In case the function has more than one argument
-\begin{quote}
-\emph{Do induction on argument number $i$ if the function is defined by
-recursion in argument number $i$.}
-\end{quote}
-When we look at the proof of \isa{{\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{40}{\isacharat}}ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{28}{\isacharparenleft}}ys{\isaliteral{40}{\isacharat}}zs{\isaliteral{29}{\isacharparenright}}}
-in \S\ref{sec:intro-proof} we find
-\begin{itemize}
-\item \isa{{\isaliteral{40}{\isacharat}}} is recursive in
-the first argument
-\item \isa{xs}  occurs only as the first argument of
-\isa{{\isaliteral{40}{\isacharat}}}
-\item both \isa{ys} and \isa{zs} occur at least once as
-the second argument of \isa{{\isaliteral{40}{\isacharat}}}
-\end{itemize}
-Hence it is natural to perform induction on~\isa{xs}.
-
-The key heuristic, and the main point of this section, is to
-\emph{generalize the goal before induction}.
-The reason is simple: if the goal is
-too specific, the induction hypothesis is too weak to allow the induction
-step to go through. Let us illustrate the idea with an example.
-
-Function \cdx{rev} has quadratic worst-case running time
-because it calls function \isa{{\isaliteral{40}{\isacharat}}} for each element of the list and
-\isa{{\isaliteral{40}{\isacharat}}} is linear in its first argument.  A linear time version of
-\isa{rev} reqires an extra argument where the result is accumulated
-gradually, using only~\isa{{\isaliteral{23}{\isacharhash}}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\ itrev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ ys\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}xs{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ itrev\ xs\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-The behaviour of \cdx{itrev} is simple: it reverses
-its first argument by stacking its elements onto the second argument,
-and returning that second argument when the first one becomes
-empty. Note that \isa{itrev} is tail-recursive: it can be
-compiled into a loop.
-
-Naturally, we would like to show that \isa{itrev} does indeed reverse
-its first argument provided the second one is empty:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}itrev\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-There is no choice as to the induction variable, and we immediately simplify:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-\noindent
-Unfortunately, this attempt does not prove
-the induction step:
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ list\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ itrev\ list\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}%
-\end{isabelle}
-The induction hypothesis is too weak.  The fixed
-argument,~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, prevents it from rewriting the conclusion.  
-This example suggests a heuristic:
-\begin{quote}\index{generalizing induction formulae}%
-\emph{Generalize goals for induction by replacing constants by variables.}
-\end{quote}
-Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs} is
-just not true.  The correct generalization is%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-If \isa{ys} is replaced by \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, the right-hand side simplifies to
-\isa{rev\ xs}, as required.
-
-In this instance it was easy to guess the right generalization.
-Other situations can require a good deal of creativity.  
-
-Although we now have two variables, only \isa{xs} is suitable for
-induction, and we repeat our proof attempt. Unfortunately, we are still
-not there:
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ list\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ list\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ list\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ ys%
-\end{isabelle}
-The induction hypothesis is still too weak, but this time it takes no
-intuition to generalize: the problem is that \isa{ys} is fixed throughout
-the subgoal, but the induction hypothesis needs to be applied with
-\isa{a\ {\isaliteral{23}{\isacharhash}}\ ys} instead of \isa{ys}. Hence we prove the theorem
-for all \isa{ys} instead of a fixed one:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}ys{\isaliteral{2E}{\isachardot}}\ itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-This time induction on \isa{xs} followed by simplification succeeds. This
-leads to another heuristic for generalization:
-\begin{quote}
-\emph{Generalize goals for induction by universally quantifying all free
-variables {\em(except the induction variable itself!)}.}
-\end{quote}
-This prevents trivial failures like the one above and does not affect the
-validity of the goal.  However, this heuristic should not be applied blindly.
-It is not always required, and the additional quantifiers can complicate
-matters in some cases. The variables that should be quantified are typically
-those that change in recursive calls.
-
-A final point worth mentioning is the orientation of the equation we just
-proved: the more complex notion (\isa{itrev}) is on the left-hand
-side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
-another, albeit weak heuristic that is not restricted to induction:
-\begin{quote}
-  \emph{The right-hand side of an equation should (in some sense) be simpler
-    than the left-hand side.}
-\end{quote}
-This heuristic is tricky to apply because it is not obvious that
-\isa{rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
-happens if you try to prove \isa{rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ itrev\ xs\ ys}!
-
-If you have tried these heuristics and still find your
-induction does not go through, and no obvious lemma suggests itself, you may
-need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb.  
-Additionally, you can read \S\ref{sec:advanced-ind}
-to learn about some advanced techniques for inductive proofs.%
-\index{induction heuristics|)}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: