HOL-Theorem-Prover
Extend Definition template for nested recursion
Problem
The current
Definition <name> <attributes>:
<eqns>
Termination
<tactic>
End
template doesn't support nested recursive definitions properly. It does support some "syntactically" nested definitions where the termination argument doesn't have to develop facts about the nested calls, but that's only part of the problem and we'll ignore them here.
Currently a definition of a nested recursion has 5 parts
- Initial definition
- Instantiation of auxiliaries
- Proof of "semantic" lemma(s)
- Termination proof
- Storing results
We'd like to collapse these as much as possible into the nice
Definition ... End presentation. In the following we go through
an example and then discuss some ideas.
Example of how things work now.
Initial definition. Consider the following list reversal algorithm.
val rev_defn = Hol_defn
"rev"
‘rev [] = [] /\
rev (x::xs) =
case rev xs
of [] => [x]
| y::ys => y :: rev (x::rev ys)’
Hol_defn defines rev, extracts termination conditions, and builds
the recursion equations and induction theorem for rev. The latter two facts are constrained
by synthesized termination conditions, which are parametric in the
as-yet-not-specified termination relation R. This information is
packaged up into rev_defn.
Instantiation of auxiliaries.
We now choose a termination relation for R, instantiate the
constrained recursion equations and induction theorem, and simplify.
This has been packaged up into a call to Defn.instantiate_aux:
val [rev_ind, rev_nil, rev_cons] =
Defn.instantiate_aux rev_defn
“measure LENGTH”
(SIMP_RULE arith_ss [] o SRULE[]);
Overload revFn[local] = “rev_aux (measure LENGTH)”
We use overloading to make the formulas a bit more readable.
Proof of "semantic" lemma(s)
A key part of most proofs of termination for nested functions is the
use of so-called "semantic lemmas" in the termination proof. Such a
lemma is a fact about the behaviour of the defined function. Somewhat
mind-bendingly, we are proving a fact about the function before
finishing its termination proof, which is ordinarily the point after
which the equations and induction can be validly used. However, the
attached applicability conditions on the (instantiated, simplified)
auxiliary definitions means this is OK. In this case, the semantic
lemma asserts that invocation of revFn doesn't change the length of
its input.
Theorem revFn_length_eq[local]:
∀L. LENGTH (revFn L) = LENGTH L
Proof
recInduct rev_ind >> rw[]
>- rw[rev_nil]
>- (mp_tac rev_cons >> CASE_TAC >> gvs[])
QED
Termination proof
The termination proof is set up interactively with
Defn.tgoal rev_defn and usually initiated with a call to
WF_REL_TAC <reln>. Once the interactive proof is finished,
it has to be packaged up with Defn.tprove:
val (def, ind) = Defn.tprove
(rev_defn,
WF_REL_TAC ‘measure LENGTH’ >>
rw[GSYM measure_length] >>
rule_assum_tac $ Q.AP_TERM ‘LENGTH’ >>
gvs [revFn_length_eq])
Storing results
Since Defn.tprove doesn't store its results in the current segment,
we finish with the following simple calls:
Theorem rev_def = def;
Theorem rev_ind = ind;
Discussion.
The introductory definition part and the termination part have to be separated so that the semantic lemmas can be proved. Something like
Definition rev_def [nested]:
rev [] = [] /\
rev (x::xs) =
case rev xs
of [] => [x]
| y::ys => y :: rev (x::rev ys)
End
could result in rev_defn being created and bound in the SML top-level.
Then, for now, the user would invoke the instantiation of auxiliaries,
declare the Overload and prove the semantic lemmas.
[It's possible that the instantiation of auxiliaries could be done by the system instead of the user, but that could be addressed in a later revision.]
This would also set up a goalstack with Defn.tgoal rev_defn and tell
the user about it. The user would interactively prove termination.
Then something like
Termination [rev]
WF_REL_TAC ‘measure LENGTH’ >>
rw[GSYM measure_length] >>
rule_assum_tac $ Q.AP_TERM ‘LENGTH’ >>
gvs [revFn_length_eq]
End
would run the Defn.tprove(rev,defn, <tactic>) and bind the results
to rev_def and rev_ind.
Actually, the "detached Termination block" idea could be useful for other definitions too. For example, if a function needed to define a bespoke "weighting" function (aka polynomial interpretation) to be used as the measure, there could be intermediate proofs that need to be done before the termination goal can be proved. In that case, doing a
Definition <name>:
<equations>
End
.... definition of weighting function, proofs about it if necessary ...
Termination <name> :
....
End
would provide a neat way to "bracket" the entirely local weighting stuff, even though it could be moved to come before the initial definition.
Yes! Perhaps the magic attribute for this situation should be deferred rather than nested.
We could also contemplate nice front-end syntax for new_specification and new_type_definition. Both of these have witness theorems that have to be proved in order for the new specification or type definition to happen. So
Definition <name>[spec(s1,...,sn)]:
P[v1,...,vn]
Witness
<proof>
End
supplies a formula P with n free variables and the witness proof will be to show the existence of suitable t1,...,tn making P[t1,...,tn] true. The resulting definition gets made once the proof is successful. NB: when the Definition ...Witness ... End form is repeated (say when the enclosing file gets replayed to the SML top-level), the introduced constants need to be hidden. Hence the inclusion of the names s1,...,sn in the attribute. Maybe something nicer can be found.
Also
Definition <name>[type]:
P (* closed *)
Witness
<proof>
End
can encapsulate the introduction of a new type operator, going up to and including an invocation of new_type_bijections.
For both forms, a first step is to add a new category for it to the DefnBase and to define the analogues of tgoal and tprove for it.