isahipster: 3595916fce63dfbbd88d6b1678fdf68bc107820e

     1: \label{sec:rec-ind}
     2: 
     3: A recursion induction scheme is specific for and associated to a function's definition.
     4: %
     5: This stronger induction scheme corresponds closer to the originating definition and, hence, the cases considered in its simplification rules.
     6: %
     7: We further explain recursion induction in this section and the benefit in considering these schemata.
     8: 
     9: \subsection{Recursion induction}
    10: 
    11: When defining a recursive function over an inductive datatype one might traverse arguments following a different pattern to the strictly structural one (the one arising from a datatype's definition).
    12: %
    13: This pattern could be more specific, or even less so, than following the datatype.
    14: 
    15: For instance, take the functions on lists \isaCode{sorted} and \isaCode{last}:
    16: 
    17: \begin{lstlisting}[ mathescape, columns=fullflexible,keepspaces, basicstyle=\fontfamily{lmvtt}\selectfont, ]
    18: fun sorted :: "Nat List $\Rightarrow$ Bool" where
    19:   "sorted [] = True"
    20: | "sorted ([_]) = True"
    21: | "sorted (r # (t # ts)) = (r $\le$ t & sorted (t # ts))"
    22: 
    23: fun last :: "'a List $\Rightarrow$ 'a" where
    24:   "last ([t]) = t"
    25: | "last (_ # ts) = last ts"
    26: \end{lstlisting}
    27: 
    28: \noindent From these definitions' structures one can derive a new induction principle.
    29: %
    30: Structural induction on lists considers the base-case \isaCode{[]} (the empty list) and step-case \isaCode{t \# ts} (a list with an element inserted at the front).
    31: %
    32: In the case of \isaCode{sorted}, cases are broken down into more detailed ones by including an additional base-case \isaCode{[t]} (the singleton list) and restricting the step-case to lists with at least two elements \isaCode{r \# t \# ts}.
    33: %
    34: Meanwhile \isaCode{last} is not defined for the case \isaCode{[]} and hence partially defined, meaning the induction scheme it gives rise to is to be completed with such a case.
    35: %
    36: This, in fact, results in the same recursion induction scheme derived from \isaCode{sorted}:
    37: 
    38: % TODO: update?
    39: % For longer version: insert recursion induction scheme and how it becomes even more specific
    40: %\inferrule [InsertInd]
    41: %  {\forall r\;\; P\;(r,\; []) \\ \forall r, \; t, \; ts\;\; ((\not (r \le t) \Longrightarrow P\;(r, \; ts)) \; \Longrightarrow\;P\;(r, \; (t\;\#\; ts))) }
    42: %  {\forall x,\; ys \;\; P\;(x,\; ys)}
    43: 
    44: \vspace{2 mm}
    45: 
    46: \inferrule [SortedInd]
    47:   {P\;([]) \\ \forall u\;\; P\;(u \;\#\; []) \\ \forall r, \; t, \; ts\;\; (P\;(r \;\#\; ts) \; \Longrightarrow\;P\;(t\;\#\; (r\;\#\; ts)))}
    48:   {\forall x \;\; P\;(x)}
    49: 
    50: \inferrule [LastInd]
    51:   {\forall u\;\; P\;(u \;\#\; []) \\ \forall r, \; t, \; ts\;\; (P\;(r\;\#\; ts) \; \Longrightarrow\;P\;(t \;\#\; (r\;\#\; ts))) \\ P\;([])}
    52:   {\forall x \;\; P\;(x)}
    53: 
    54: \vspace{2 mm}
    55: 
    56: 
    57: Induction determined by these schemata is called \emph{recursion induction} or \emph{computation induction}.
    58: %
    59: They can isolate sub-units not represented in a datatype's structure as being atomic, such as lists with at least two elements in the scheme for \isaCode{sorted}.
    60: %
    61: Recursion induction hence provides an immediate and more specific structure for reasoning about other recursion patterns where a simple structural induction would fail to set appropriate base cases for the inductive step to succeed.
    62: 
    63: Particularly, within Isabelle/HOL these schemata are automatically derived as theorems from recursive functions' termination order \cite{krauss-term}. % From the PROOF! of those
    64: 
    65: \subsubsection*{Recursion induction in a proof}
    66: 
    67: %% Example from presentation on difference
    68: 
    69: To exemplify the potential difference between recursion and structural induction, let us take the already introduced conditional lemma \isaCode{sorted xs $\Longrightarrow$ sorted (insert x xs)}.
    70: %
    71: Applying structural induction on the list \isaCode{xs} would produce the subgoals:
    72: 
    73: \begin{lstlisting}[ mathescape, columns=fullflexible,keepspaces, basicstyle=\fontfamily{lmvtt}\selectfont, ]
    74: 1. sorted [] $\Longrightarrow$ sorted (insert x [])
    75: 2. $\wedge$ a y. (sorted y $\Longrightarrow$ sorted (insert x y)) $\Longrightarrow$ sorted (a # y) $\Longrightarrow$
    76:             sorted (insert x (a # y))
    77: \end{lstlisting}
    78: 
    79: \noindent Whilst \isaCode{sorted}'s recursion induction scheme would yield:
    80: 
    81: \begin{lstlisting}[ mathescape, columns=fullflexible,keepspaces, basicstyle=\fontfamily{lmvtt}\selectfont, ]
    82: 1. sorted [] $\Longrightarrow$ sorted (insert x [])
    83: 2. $\wedge$ u. sorted [u] $\Longrightarrow$ sorted (insert x [u])
    84: 3. $\wedge$ r t ts. (sorted (t # ts) $\Longrightarrow$ sorted (insert x (t # ts))) $\Longrightarrow$ sorted (r # t # ts) $\Longrightarrow$
    85:                sorted (insert x (r # t # ts))
    86: \end{lstlisting}
    87: 
    88: The latter set of subgoals leads to an immediate proof of the main lemma thanks to its steps mirroring the actual predicate definition, hence having a correspondence with its simplification rules.
    89: %
    90: In contrast, the former, even though it intuitively looks immediate to prove, is not sufficiently generalised nor does it specify any intermediate result on inserting an element on a concrete non-empty list (in our case, the singleton list) which would enable to prove the second subgoal for any arbitrary list. Structural induction is in some way a weaker scheme and additional case-splits or lemmas would be required to close the proof employing it in our example.
    91: 
    92: 
    93: \subsection{A tactic (not only) for conditionals}
    94: 
    95: Recursion induction is a way of dealing with more complicated recursive structures, many may occur in conditional statements but the advantage in considering recursion induction is broader.
    96: 
    97: \subsubsection*{Simultaneous induction}
    98: 
    99: The final tactic for Hipster explores the proofs one could attain by recursion inductions derived from functions occurring in the conjecture.
   100: %
   101: As a side-result, this increases the scope of Hipster's original approach for equational lemmas too.
   102: 
   103: A notable gain, affecting both conditional and equational lemmas, is that of having the capability of performing simultaneous induction, whereas previously only structural inductions on a single variable were performed by Hipster.
   104: %
   105: Simultaneous induction schemata are those inducting over more than one variable at a time, whether those variables are of the same type or not.
   106: %
   107: Such is the case for the list function \isaCode{zip}'s recursion induction scheme, which corresponds to parallel induction on lists:
   108: 
   109: \begin{lstlisting}[   mathescape,   columns=fullflexible,   basicstyle=\fontfamily{lmvtt}\selectfont, ]
   110: fun zip :: "'a list $\Rightarrow$ 'b list $\Rightarrow$ ('a $\times$ 'b) list" where
   111:   "zip [] y = []"
   112: | "zip (x # xs) [] = []"
   113: | "zip (x # xs) (y # ys) = (x, y) # (zip xs ys)"
   114: \end{lstlisting}
   115: 
   116: \vspace{2 mm}
   117: 
   118: \inferrule [ZipInd]
   119:   {\forall ts\;\; P\;([],\; ts) \\ \forall z,\; rs\;\; P\;(z\;\#\; rs, [])  \\ \forall z,\; y,\; rs,\; ts\;\; (P\;(rs,\;ts) \Longrightarrow\; P\;(z\; \# \; rs,\; y\;\#\; ts))}
   120:   {\forall xs, \; ys \;\; P\;(xs,\; ys)}
   121: 
   122: \vspace{2 mm}
   123: 
   124: \noindent This scheme, along with some initial theory exploration, allows theorems like the following to be provable automatically:
   125: 
   126: \begin{lstlisting}[   mathescape,   columns=fullflexible,   basicstyle=\fontfamily{lmvtt}\selectfont, ]
   127: zip (xs @ ys) zs = (zip xs (take (len xs) zs)) @ (zip ys (drop (len xs) zs))
   128: \end{lstlisting}
   129: 
   130: \noindent Or even the alternative related conditional lemma to be immediately provable:
   131: 
   132: \begin{lstlisting}[   mathescape,   columns=fullflexible,   basicstyle=\fontfamily{lmvtt}\selectfont, ]
   133: len a = len b $\Longrightarrow$ (zip a b) @ (zip c d) = zip (a @ c) (b @ d)
   134: \end{lstlisting}
   135: 
   136: Neither of these lemmas was provable before, even having done exploration for all the occurring functions in them.
   137: %
   138: Hipster's prior structural induction approach could not capture in a scheme the relation between two variables.
   139: %
   140: In these two cases, \isaCode{zip} traverses its arguments taking steps on both at the same time, a pattern we can only capture with some form of simultaneous induction.
   141: %
   142: Instead of synthesising a series of possible simultaneous induction schemata, recursion induction gives us an immediate choice which is also closer to the problem at hand.
   143: 
   144: 
   145: % Unnecessary here. Maybe expand in longer?
   146: % \subsubsection*{Flexibilising Hipster}
   147: 
   148: % Include or not?
   149: 
   150: % Very brief overview of other aspects more interaction-oriented that improve Hipster
   151: 
   152: 
   153: