Email Gateway (Aug 18 2022 at 12:13): Email Gateway (Aug 18 2022 at 12:13):From: John Matthews <matthews@galois.com>
Hi,
Our Cryptol->Isabelle translator generates recursive function
definitions that don't always terminate, but should terminate when the
inputs satisfy certain conditions known to the user but not
necessarily to the translator, i.e. the functions are partially
terminating.
Here is a non-Cryptol example of what I'm talking about:
function (domintros)
fac_int :: "int => int" where
"fac_int n = (if n = 0 then 1 else n * fac_int (n - 1))"
by pat_completeness auto
I'd like to prove the following partial termination lemma for fac_int:
lemma "0 <= n ==> fac_int_dom n"
However, the termination rule for fac_int_dom seems to be too weak:
lemma fac_int.termination:
"[|wf ?R;
!!n. n ~= 0 ==> (n - 1, n) \<in> ?R|]
==> !x. fac_int_dom x"
What I really need is a rule like this, where ?P is an arbitrary
precondition on input ?x:
lemma fac_int.partial_termination:
"[|wf ?R;
!!n. [|?P n; n ~= 0|] ==> (n - 1, n) \<in> ?R;
?P ?x|]
==> fac_int_dom ?x"
I know I could generate a rule like this by changing the definition of
fac_int, but we don't want the user to have to muck with Cryptol-
generated definitions just to prove partial termination.
Is it possible to have the function package generate a partial
termination rule for recursive functions?
Thanks,
-john
Email Gateway (Aug 18 2022 at 12:13):From: Alexander Krauss <krauss@in.tum.de>
Hi John,
function (domintros)
fac_int :: "int => int" where
"fac_int n = (if n = 0 then 1 else n * fac_int (n - 1))"
by pat_completeness autoI'd like to prove the following partial termination lemma for fac_int:
lemma "0 <= n ==> fac_int_dom n"
Here is a proof:
lemma "0 <= n ==> fac_int_dom n"
proof (induct rule: int_ge_induct)
case base show ?case
by (auto intro: accpI elim: fac_int_rel.cases)
next
case (step i)
show ?case
by (rule accpI) (auto intro: step elim!: fac_int_rel.cases )
qed
However, the termination rule for fac_int_dom seems to be too weak:
lemma fac_int.termination:
The ".termination" rule can only prove totality. You have to use the
rules for accessible part and the call relation, as above. Note that
"fac_int_dom" is just an abbreviation for "accp fac_int_rel".
What I really need is a rule like this, where ?P is an arbitrary
precondition on input ?x:lemma fac_int.partial_termination:
"[|wf ?R;
!!n. [|?P n; n ~= 0|] ==> (n - 1, n) \<in> ?R;
?P ?x|]
==> fac_int_dom ?x"
In fact, this rule is wrong: Take P as ">= - 10" and
R as "{(n - 1, n) | n. n >= - 10 }".
For this to work, P must be preserved by recursive calls.
Is it possible to have the function package generate a partial
termination rule for recursive functions?
At the moment, the best way is to use the definition of the domain
directly as above, together with a suitable induction. An alternative to
the "(rule accp) then (erule fac_int_rel.cases)" is the ".domintro"
rule, which makes the above proof much shorter:
lemma "0 <= n ==> fac_int_dom n"
by (induct rule: int_ge_induct) (auto intro: fac_int.domintros)
On the other hand, the domintros are sometimes a little ad-hoc (due to
internal forward simplification), and some users had probolems with it.
But the manual version using the definitions always works.
Alex
Email Gateway (Aug 18 2022 at 12:14):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
Hi John,
We ran in to a problem somewhat like this. In fact, you have all the
information you need - use an ML antiquotation like
ML {* @{term "fac_int_dom"} *}
and you'll see that fac_int_dom is an abbreviation for the accessible part
of fac_int_rel, for which you have far more information. In particular,
you should be able to prove that "n >= 0 ==> fac_int_dom n" from that, and
then you will be able to use the psimps and pinduct rules.
We were considering recommending that the function package produce an
appropriate rule so that you don't have to spot the abbreviation in order
to prove some precondition implies *_dom.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 12:14):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
The confusion about partial termination in the function package could
possibly be solved by modifying the theorem searcher.
Abbreviations such as rec_fun_dom are easily confused for constants. The
problem is that the theorem searcher doesn't help to distinguish them.
When accidentally searching for abbreviations within your own theories it
is usually clear that the theorem searcher is displaying less results
than it should. Constants generated by automatic packages, however, are
assumed to be special cases. It is easy to believe that few rules are
available.
Perhaps the theorem searcher could solve these problems by warning that
one of the input terms is an abbreviation, and that more facts might be
available for its constituent parts. I'm not sure how to implement
this, but I think it would save some confusion.
Another solution would be to have yet another colour scheme in Proof
Genereal to help identify abbreviations. I suspect this might be overkill.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 12:16):From: John Matthews <matthews@galois.com>
Hi Alex,
Here is a proof:
lemma "0 <= n ==> fac_int_dom n"
proof (induct rule: int_ge_induct)
case base show ?case
by (auto intro: accpI elim: fac_int_rel.cases)
next
case (step i)
show ?case
by (rule accpI) (auto intro: step elim!: fac_int_rel.cases )
qed
Thanks. I didn't realize the function package generated these extra
lemmas for fac_int_rel, since I was just using find_theorems on
"fac_int_dom _".
What I really need is a rule like this, where ?P is an arbitrary
precondition on input ?x:
lemma fac_int.partial_termination:
"[|wf ?R;
!!n. [|?P n; n ~= 0|] ==> (n - 1, n) \<in> ?R;
?P ?x|]
==> fac_int_dom ?x"In fact, this rule is wrong: Take P as ">= - 10" and
R as "{(n - 1, n) | n. n >= - 10 }".For this to work, P must be preserved by recursive calls.
Ah, right. I missed that extra constraint.
Thanks,
-john
Email Gateway (Aug 18 2022 at 12:16):From: John Matthews <matthews@galois.com>
Hi Thomas, thanks for your help.
I agree, it would be useful for the function package to automatically
generate a partial termination rule, just not mine! :)
Thanks,
-john
Last updated: Nov 21 2024 at 12:39 UTC