Theory Method
section "Method rationale"
theory Method
imports Main
begin
text ‹
Tail-recursive function definitions are sometimes more intuitive and
straightforward than alternatives, and this alone would be enough to make them
preferable in such cases for the mere purposes of functional programming. However,
proving theorems about them with a formal proof assistant like Isabelle may be
roundabout because of the peculiar form of the resulting recursion induction
rules.
Let:
\begin{itemize}
\item
‹f_naive› be a tail-recursive function of type
‹'a⇩1 ⇒ ... ⇒ 'a⇩n ⇒ 'b›.
\item
‹a› be an ‹n›-tuple of values of types ‹'a⇩1›, ...,
‹'a⇩n› such that the computation of ‹f_naive a›, say outputting
value ‹b›, involves at least one recursive call -- which is what happens in
general for significant inputs (e.g. those complying with initial conditions for
accumulator arguments), as otherwise a non-recursive function definition would be
sufficient.
\item
‹a⇩1›, ..., ‹a⇩m› be the sequence of the intermediate
‹n›-tuples of values of types ‹'a⇩1›, ..., ‹'a⇩n› arising from
the computation of ‹f_naive a›.
\item
‹f_naive X⇩1 = f_naive X'⇩1›, ..., ‹f_naive X⇩m = f_naive X'⇩m›,
‹f_naive X = Y› be the sequence (possibly with repetitions) of the
equations involved in the computation of ‹f_naive a› -- which implies
that, putting ‹a⇩0 = a›, they are satisfied for
‹(X⇩1, X'⇩1) = (a⇩0, a⇩1)›, ..., ‹(X⇩m, X'⇩m) = (a⇩m⇩-⇩1, a⇩m)›,
‹(X, Y) = (a⇩m, b)›, respectively.
\end{itemize}
That being stated, suppose that theorem ‹P (f_naive a)› has to be proven.
If recursion induction is applied to such goal, for each ‹i ∈ {1..m}›,
the recursive equation ‹f_naive X⇩i = f_naive X'⇩i› gives rise to subgoal
‹P (f_naive X'⇩i) ⟹ P (f_naive X⇩i)›, trivially discharged by
simplification. On the contrary, the non-recursive equation
‹f_naive X = Y› brings about the generation of subgoal
‹P (f_naive X)›, which is intractable unless it trivially follows from
either the equation or the form of pattern ‹X›.
Indeed, in non-trivial cases such as the case studies examined in this paper, this
formula even fails to be a theorem, thus being hopeless as a goal, since it is
false for some values of its variables. The reason for this is that non-trivial
properties of the output of tail-recursive functions depend on the input as well
as on the whole recursive call pipeline leading from the input to the output, and
all of this information corresponds to missing necessary assumptions in subgoal
‹P (f_naive X)›.
Therefore, for a non-trivial theorem ‹P (f_naive a)›, recursion induction
is rather applicable to some true conditional statement
‹f_inv x ⟶ P (f_naive x)› complying with both of the following
requirements:
\begin{itemize}
\item
subgoal ‹f_inv X ⟶ P (f_naive X)› arising from equation
‹f_naive X = Y› be tractable, and
\item
formula ‹f_inv a› can be shown to be true, so that theorem
‹P (f_naive a)› can be inferred from conditional
‹f_inv a ⟶ P (f_naive a)› by \emph{modus ponens}.
\end{itemize}
Observe that the antecedent of the conditional may not have the form
‹f_inv (f_naive x)›. Otherwise, the latter requirement would ask for
proving formula ‹f_inv (f_naive a)›, which would be at least as hard to
prove as formula ‹P (f_naive a)› being the former a sufficient condition
for the latter. Hence, the same problem as that originating from the proof of
formula ‹P (f_naive a)› would have to be solved again, which would give
rise to a \emph{regressio ad infinitum}.
The latter requirement entails that formula ‹f_inv a⇩0› holds. Moreover,
for each ‹i ∈ {1..m}›, in the proof of conditional
‹f_inv x ⟶ P (f_naive x)› by recursion induction, the recursive equation
‹f_naive X⇩i = f_naive X'⇩i› brings about the generation of subgoal
‹f_inv X'⇩i ⟶ P (f_naive X'⇩i) ⟹ f_inv X⇩i ⟶ P (f_naive X⇩i)›. Assuming
that formula ‹f_inv a⇩i⇩-⇩1› holds, it turns out that the conclusion
antecedent ‹f_inv X⇩i› may not be shown to be false, as ‹n›-tuple
‹a⇩i⇩-⇩1› matches pattern ‹X⇩i›; thus, the conclusion consequent
‹P (f_naive X⇩i)› has to be proven.
In non-trivial cases, this requires that the assumption antecedent
‹f_inv X'⇩i› be derived from the conclusion antecedent ‹f_inv X⇩i›
used as a further assumption, so that the assumption consequent
‹P (f_naive X'⇩i)› -- matching ‹P (f_naive X⇩i)› by virtue of
equation ‹f_naive X⇩i = f_naive X'⇩i› -- can be proven by
\emph{modus ponens}. This in turn requires that ‹f_inv X⇩i› imply
‹f_inv X'⇩i›, i.e. that ‹f_inv x⇩i› imply ‹f_inv x'⇩i› for any
pair of ‹n›-tuples ‹x⇩i›, ‹x'⇩i› matching patterns ‹X⇩i›,
‹X'⇩i› with respect to the same value assignment. But such are
‹n›-tuples ‹a⇩i⇩-⇩1›, ‹a⇩i› as they solve equation
‹f_naive X⇩i = f_naive X'⇩i›, so that the supposed truth of
‹f_inv a⇩i⇩-⇩1› entails that of ‹f_inv a⇩i›.
Hence, by induction, all of formulae ‹f_inv a›, ‹f_inv a⇩1›, ...,
‹f_inv a⇩m› turn out to be true. On the other hand, the former requirement
is verified if either the antecedent ‹f_inv X› can be shown to be false,
which would entail its falsity for any ‹n›-tuple matching pattern ‹X›,
or else the consequent ‹P (f_naive X)› can be shown to be true using the
antecedent as an assumption. Since formula ‹f_inv a⇩m› is true and
‹n›-tuple ‹a⇩m› matches pattern ‹X›, the case that actually
occurs is the second one.
Thus, the former requirement is equivalent to asking for an introduction rule to
be proven -- in fact, a conditional with a contradiction as antecedent may not be
used as an introduction rule -- having the form
‹f_inv X ⟹ P (f_naive X)›, or rather
‹⟦f_inv x; f_form x⟧ ⟹ P (f_naive x)› for a suitable predicate
‹f_form› satisfied by any ‹n›-tuple matching pattern ‹X›. In
the degenerate case in which the rule can be shown to be true for
‹f_form = (λx. True)›, it admits to be put into the simpler equivalent
form ‹f_inv x ⟹ P (f_naive x)›.
An even more important consequence of the previous argument is that in non-trivial
cases, the task of proving conditional ‹f_inv x ⟶ P (f_naive x)› by
recursion induction requires that ‹f_inv X'⇩i› be derived from
‹f_inv X⇩i› for each recursive equation ‹f_naive X⇩i = f_naive X'⇩i›,
where ‹i ∈ {1..m}›.
Let:
\begin{itemize}
\item
‹'a› be the Cartesian product of types ‹'a⇩1›, ..., ‹'a⇩n›.
\item
‹f_set› be the inductive set of type ‹'a ⇒ 'a set› defined by
introduction rules ‹x ∈ f_set x›,
‹X⇩1 ∈ f_set x ⟹ X'⇩1 ∈ f_set x›, ...,
‹X⇩m ∈ f_set x ⟹ X'⇩m ∈ f_set x› -- where patterns ‹X⇩1›,
‹X'⇩1›, ..., ‹X⇩m›, ‹X'⇩m› are now viewed as values of type
‹'a›.
\end{itemize}
Then, the problem of discharging the above proof obligation on predicate
‹f_inv› is at least as hard as that of proving by rule induction
introduction rule ‹⟦y ∈ f_set x; f_inv x⟧ ⟹ f_inv y› -- which states that
for any ‹x› such that ‹f_inv x› is true, ‹f_inv› is an
invariant over inductive set ‹f_set x›, i.e. ‹f_inv y› is true for
each ‹y ∈ f_set x›.
In fact, the application of rule induction to this goal generates subgoals
‹f_inv x ⟹ f_inv x›,
‹⟦X⇩1 ∈ f_set x; f_inv X⇩1; f_inv x⟧ ⟹ f_inv X'⇩1›, ...,
‹⟦X⇩m ∈ f_set x; f_inv X⇩m; f_inv x⟧ ⟹ f_inv X'⇩m›; the first is trivial,
and such would also be the other ones if rules ‹f_inv X⇩1 ⟹ f_inv X'⇩1›,
..., ‹f_inv X⇩m ⟹ f_inv X'⇩m› were available.
Furthermore, suppose that the above invariance property of predicate ‹f_inv›
have been proven; then, the proof of conditional
‹f_inv x ⟶ P (f_naive x)› by recursion induction can be made unnecessary
by slightly refining the definition of function ‹f_naive›, as shown in the
continuation.
Let ‹f_aux› be the tail-recursive function of type ‹'a ⇒ 'a› whose
definition is obtained from that of ‹f_naive› by treating as fixed points
the patterns to which non-recursive equations apply as well as those to which no
equation applies, if any -- i.e. by replacing recursive equation
‹f_naive X⇩i = f_naive X'⇩i› with ‹f_aux X⇩i = f_aux X'⇩i› for each
‹i ∈ {1..m}› and non-recursive equation ‹f_naive X = Y› with
‹f_aux X = X›.
Then, define function ‹f› by means of a non-recursive equation
‹f x = f_out (f_aux (f_in x))›, where:
\begin{itemize}
\item
‹f_in› is a function of type ‹'a' ⇒ 'a›, for a suitable type
‹'a'›, whose range contains all the significant inputs of function
‹f_naive›.
\item
‹f_out› is a function of type ‹'a ⇒ 'b› mapping the outputs of
‹f_aux› to those of ‹f_naive›, i.e. the values of type ‹'a›
matching pattern ‹X› to those of type ‹'b› matching pattern
‹Y› with respect to the same value assignment.
\end{itemize}
The definitions of functions ‹f_aux› and ‹f_out› entail that equation
‹f_naive x = f_out (f_aux x)› holds for any ‹x›. Particularly,
‹f_naive a = f_out (f_aux a)›; thus, being ‹a'› an inverse image of
‹a› under ‹f_in›, viz. ‹a = f_in a'›, it follows that
‹f_naive a = f a'›. As a result, theorem ‹P (f_naive a)› may be
rewritten as ‹P (f a')›.
For any ‹x›, ‹f_set x› is precisely the set of the values
recursively input to function ‹f_aux› in the computation of
‹f_aux x›, including ‹x› itself, and it can easily be ascertained
that ‹f_aux x› is such a value. In fact, the equation invoked last in the
computation of ‹f_aux x› must be a non-recursive one, so that it has the
form ‹f_aux X = X›, since all non-recursive equations in the definition
of ‹f_aux› apply to fixed points. Thus, being ‹f_aux x› the output
of the computation, the right-hand side of the equation, i.e. the pattern
‹X› also input to function ‹f_aux› in the left-hand side, is
instantiated to value ‹f_aux x›.
Therefore, ‹f_aux x ∈ f_set x› for any ‹x›. Observe that the
argument rests on the assumption that whatever ‹x› is given, a sequence of
equations leading from ‹x› to ‹f_aux x› be actually available -- and
what is more, nothing significant could be proven on ‹f_aux x› for any
‹x› for which its value were undefined, and then arbitrary. The trick of
making the definition of ‹f_aux› total by adding equations for the patterns
not covered in the definition of ‹f_naive›, if any, guarantees that this
assumption be satisfied.
An additional consequence of the previous argument is that
‹f_aux (f_aux x) = f_aux x› for any ‹x›, i.e. function ‹f_aux›
is idempotent. If introduction rule ‹⟦f_inv x; f_form x⟧ ⟹ P (f_naive x)›
is rewritten by applying equation ‹f_naive x = f_out (f_aux x)›,
instantiating free variable ‹x› to ‹f_aux x›, and then applying the
idempotence of function ‹f_aux›, the result is formula
‹⟦f_inv (f_aux x); f_form (f_aux x)⟧ ⟹ P (f_out (f_aux x))›, which is
nothing but an instantiation of introduction rule
‹⟦f_inv x; f_form x⟧ ⟹ P (f_out x)›.
Observe that this rule is just a refinement of a rule whose proof is required for
proving conditional ‹f_inv x ⟶ P (f_naive x)› by recursion induction, so
that it does not give rise to any additional proof obligation. Moreover, it
contains neither function ‹f_naive› nor ‹f_aux›, thus its proof does
not require recursion induction with respect to the corresponding induction rules.
The instantiation of such refined introduction rule with value ‹f_aux a›
is ‹⟦f_inv (f_aux a); f_form (f_aux a)⟧ ⟹ P (f_out (f_aux a))›, which by
virtue of equality ‹a = f_in a'› and the definition of function ‹f›
is equivalent to formula
‹⟦f_inv (f_aux a); f_form (f_aux a)⟧ ⟹ P (f a')›. Therefore, the rule is
sufficient to prove theorem ‹P (f a')› -- hence making unnecessary the
proof of conditional ‹f_inv x ⟶ P (f_naive x)› by recursion induction,
as mentioned previously -- provided the instantiated assumptions
‹f_inv (f_aux a)›, ‹f_form (f_aux a)› can be shown to be true.
This actually is the case: the former assumption can be derived from formulae
‹f_aux a ∈ f_set a›, ‹f_inv a› and the invariance of predicate
‹f_inv› over ‹f_set a›, while the latter can be proven by recursion
induction, as by construction goal ‹f_form X› is trivial for any pattern
‹X› to which some non-recursive equation in the definition of function
‹f_naive› applies. If further non-recursive equations whose patterns do not
satisfy predicate ‹f_form› have been added to the definition of
‹f_aux› to render it total, rule inversion can be applied to exclude that
‹f_aux a› may match any of such patterns, again using formula
‹f_aux a ∈ f_set a›.
›
section "Method summary"
text ‹
The general method developed so far can be schematized as follows.
Let ‹f_naive› be a tail-recursive function of type
‹'a⇩1 ⇒ ... ⇒ 'a⇩n ⇒ 'b›, and ‹P (f_naive a⇩1 ... a⇩n)› be a
non-trivial theorem having to be proven on this function.
In order to accomplish such task, the following procedure shall be observed.
\begin{itemize}
\item
\emph{Step 1} --- Refine the definition of ‹f_naive› into that of an
auxiliary tail-recursive function ‹f_aux› of type ‹'a ⇒ 'a›, where
‹'a› is a product or record type with types ‹'a⇩1›, ..., ‹'a⇩n›
as components, by treating as fixed points the patterns to which non-recursive
equations apply as well as those to which no equation applies, if any.
\item
\emph{Step 2} --- Define a function ‹f› of type ‹'a' ⇒ 'b› by means
of a non-recursive equation ‹f x = f_out (f_aux (f_in x))›, where
‹f_in› is a function of type ‹'a' ⇒ 'a› (possibly matching the
identity function) whose range contains all the significant inputs of function
‹f_naive›, and ‹f_out› is a function of type ‹'a ⇒ 'b›
mapping the outputs of ‹f_aux› to those of ‹f_naive›.
\\Then, denoting with ‹a› the value of type ‹'a› with components
‹a⇩1›, ..., ‹a⇩n›, and with ‹a'› an inverse image of ‹a›
under function ‹f_in›, the theorem to be proven takes the equivalent form
‹P (f a')›.
\item
\emph{Step 3} --- Let ‹f_aux X⇩1 = f_aux X'⇩1›, ...,
‹f_aux X⇩m = f_aux X'⇩m› be the recursive equations in the definition of
function ‹f_aux›.
\\Then, define an inductive set ‹f_set› of type ‹'a ⇒ 'a set› with
introduction rules ‹x ∈ f_set x›,
‹X⇩1 ∈ f_set x ⟹ X'⇩1 ∈ f_set x›, ...,
‹X⇩m ∈ f_set x ⟹ X'⇩m ∈ f_set x›.
\\If the right-hand side of some recursive equation contains conditionals in the
form of ‹if› or ‹case› constructs, the corresponding introduction
rule can be split into as many rules as the possible mutually exclusive cases;
each of such rules shall then provide for the related case as an additional
assumption.
\item
\emph{Step 4} --- Prove lemma ‹f_aux x ∈ f_set x›; a general inference
scheme, independent of the specific function ‹f_aux›, applies to this proof.
\\First, prove lemma ‹y ∈ f_set x ⟹ f_set y ⊆ f_set x›, which can easily
be done by rule induction.
\\Next, applying recursion induction to goal ‹f_aux x ∈ f_set x› and then
simplifying, a subgoal ‹X⇩i ∈ f_set X⇩i› arises for each non-recursive
equation ‹f_aux X⇩i = X⇩i›, while a subgoal
‹f_aux X'⇩j ∈ f_set X'⇩j ⟹ f_aux X'⇩j ∈ f_set X⇩j› arises for each recursive
equation ‹f_aux X⇩j = f_aux X'⇩j›.
\\The former subgoals can be proven by introduction rule ‹x ∈ f_set x›, the
latter ones as follows: rule instantiations ‹X⇩j ∈ f_set X⇩j› and
‹X⇩j ∈ f_set X⇩j ⟹ X'⇩j ∈ f_set X⇩j› imply formula ‹X'⇩j ∈ f_set X⇩j›;
thus ‹f_set X'⇩j ⊆ f_set X⇩j› by the aforesaid lemma; from this and subgoal
assumption ‹f_aux X'⇩j ∈ f_set X'⇩j›, subgoal conclusion
‹f_aux X'⇩j ∈ f_set X⇩j› ensues.
\\As regards recursive equations containing conditionals, the above steps have to
be preceded by a case distinction, so as to obtain further assumptions sufficient
for splitting such conditionals.
\item
\emph{Step 5} --- Define a predicate ‹f_inv› of type ‹'a ⇒ bool› in
such a way as to meet the proof obligations prescribed by the following steps.
\item
\emph{Step 6} --- Prove lemma ‹f_inv a›.
\\In case of failure, return to step 5 so as to suitably change the definition of
predicate ‹f_inv›.
\item
\emph{Step 7} --- Prove introduction rule ‹f_inv x ⟹ P (f_out x)›, or
rather ‹⟦f_inv x; f_form x⟧ ⟹ P (f_out x)›, where ‹f_form› is a
suitable predicate of type ‹'a ⇒ bool› satisfied by any pattern to which
some non-recursive equation in the definition of function ‹f_naive› applies.
\\In case of failure, return to step 5 so as to suitably change the definition of
predicate ‹f_inv›.
\item
\emph{Step 8} --- In case an introduction rule of the second form has been proven
in step 7, prove lemma ‹f_form (f_aux a)› by recursion induction.
\\If the definition of function ‹f_aux› resulting from step 1 contains
additional non-recursive equations whose patterns do not satisfy predicate
‹f_form›, rule inversion can be applied to exclude that ‹f_aux a›
may match any of such patterns, using instantiation ‹f_aux a ∈ f_set a› of
the lemma proven in step 4.
\item
\emph{Step 9} --- Prove by rule induction introduction rule
‹⟦y ∈ f_set x; f_inv x⟧ ⟹ f_inv y›, which states the invariance of
predicate ‹f_inv› over inductive set ‹f_set x› for any ‹x›
satisfying ‹f_inv›.
\\In case of failure, return to step 5 so as to suitably change the definition of
predicate ‹f_inv›.
\\Observe that the order in which the proof obligations related to predicate
‹f_inv› are distributed among steps 6 to 9 is ascending in the effort
typically required to discharge them. The reason why this strategy is advisable is
that in case one step fails, which forces to revise the definition of predicate
‹f_inv› and then also the proofs already worked out, such proofs will be the
least demanding ones so as to minimize the effort required for their revision.
\item
\emph{Step 10} --- Prove theorem ‹P (f a')› by means of the following
inference scheme.
\\First, derive formula ‹f_inv (f_aux a)› from introduction rule
‹⟦y ∈ f_set x; f_inv x⟧ ⟹ f_inv y› and formulae
‹f_aux a ∈ f_set a›, ‹f_inv a›.
\\Then, derive formula ‹P (f_out (f_aux a))› from either introduction rule
‹f_inv x ⟹ P (f_out x)› or ‹⟦f_inv x; f_form x⟧ ⟹ P (f_out x)›
and formulae ‹f_inv (f_aux a)›, ‹f_form (f_aux a)› (in the latter
case).
\\Finally, derive theorem ‹P (f a')› from formulae
‹P (f_out (f_aux a))›, ‹a = f_in a'› and the definition of
function ‹f›.
\end{itemize}
In the continuation, the application of this method is illustrated by analyzing
two case studies drawn from an exercise comprised in Isabelle online course
material; see \<^cite>‹"R5"›. The salient points of definitions and proofs are
commented; for additional information see Isabelle documentation, particularly
\<^cite>‹"R1"›, \<^cite>‹"R2"›, \<^cite>‹"R3"›, and \<^cite>‹"R4"›.
›
end