(* Title: A General Method for the Proof of Theorems on Tail-recursive Functions Author: Pasquale Noce Security Certification Specialist at Arjo Systems - Gep S.p.A. pasquale dot noce dot lavoro at gmail dot com pasquale dot noce at arjowiggins-it dot com *) 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 (*>*)