Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] context-sensitive termination proof

Email Gateway (Aug 18 2022 at 11:56):

From: Andrei Popescu <uuomul@yahoo.com>
Hello,

I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following:

typedecl A  typedecl B  typedecl C

consts
 u :: "A => C => B"
 v :: "C => A"
 w :: "C => B"
 P :: "A => C => bool"
 size :: "A => nat"

axioms conditional_decrease:
"P a c ==> size (v c) < size a"

function f :: "A => B set" where
"f a = {u a c| c. P a c  &  w c : f (v c)}"

The only tool I see available for proving termination of f is the lemma

f.termination: "[|wf ?R; !! a x c. (v c, a) : ?R|] ==> ALL x. f_dom x"

while I would need something like:

f.context_sensitive_termination:
"[|wf ?R; !! a x c. P a c ==> (v c, a) : ?R|] ==> ALL x. f_dom x"

or rather

"[|wf (?R Int {(v c,a)| a c. P a c}); !! a x c. (v c, a) : ?R|] ==> ALL x. f_dom x"

Thanks in advance for any hint on how to handle this.

   Andrei Popescu

Email Gateway (Aug 18 2022 at 11:56):

From: Alexander Krauss <krauss@in.tum.de>
Andrei,

I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following:
[...]
The only tool I see available for proving termination of f is the lemma

f.termination: "[|wf ?R; !! a x c. (v c, a) : ?R|] ==> ALL x. f_dom x"

while I would need something like:

f.context_sensitive_termination:
"[|wf ?R; !! a x c. P a c ==> (v c, a) : ?R|] ==> ALL x. f_dom x"

You need to add a congruence rule (here: conj_cong for the conjunction)
to the definition. See the attached theory (and the function tutorial
for some more explanation on congruence rules).

Hope this helps
Alex
Scratch.thy

Email Gateway (Aug 18 2022 at 11:57):

From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
The function package does build up context information for you.

The algorithm for doing so involves using congruence rules, in a similar
manner to the use of congruence rules in the simplifier. Essentially these
congruence rules define the assumptions that may be made while rewriting
inner contexts of the goals.

You seem to need to exploit the fact that P a c holds for the right hand side
of the conjunction to matter. I suspect that declaring
conj_cong[fundef_cong] before defining your recursive function may add the
necessary fact to the termination rule.

This is a powerful technique - we have managed to use it to define what
are essentially recursive imperative programs and state their termination
property in terms of progressive state transformation. We had to add a
great many rules to the set, but we got there. Good luck!

Yours,
Thomas.

Last updated: Nov 21 2024 at 12:39 UTC