Stream: Beginner Questions

Topic: Unfold definition for termination proof

Marvin Brieger (Nov 03 2023 at 09:36):

Hey there,

in recursively defined functions I want to use other functions on the rhs, which got an definition elsewhere, as shown by the simple example below.
Note that the function defined elsewhere again takes the recursive function as an argument, which blocks automatic termination proofs.
Can I easily unfold the definition for the termination proof without the need to give a custom termination order by using "function" instead of "fun"?

definition foo :: "nat ⇒ (nat ⇒ nat list) ⇒ nat list"
  where "foo n f = n # f n"

fun bar :: "nat ⇒ nat list" where
  "bar 0 = []"
| "bar (Suc n) = n # foo n bar"

Fabian Huch (Nov 03 2023 at 09:45):

You can register foo_def as termination_simp.

Marvin Brieger (Nov 03 2023 at 09:54):

Sounds like the way to go, but

definition foo :: "nat ⇒ (nat ⇒ nat list) ⇒ nat list"
  where "foo n f = n # f n"

declare foo_def [termination_simp]

fun bar :: "nat ⇒ nat list" where
  "bar 0 = []"
| "bar (Suc n) = n # foo n bar"

is not immediately successful. Do I miss something?

Lukas Stevens (Nov 03 2023 at 09:58):

I have the feeling that something goes wrong in the function package. It says that there is a call Suc n ~> x which is not true

Lukas Stevens (Nov 03 2023 at 10:03):

I think you have to define the function as mutually recursive functions.

Lukas Stevens (Nov 03 2023 at 10:37):

Hm, experimenting with that does not get rid of the problem

Marvin Brieger (Nov 03 2023 at 10:39):

Doing a mutual recursive definition is anyway against what I want to achieve since having a separate definition would allow to prove lemmas about it instead of having the definition always be unfolded directly.
It seems that doing a manual termination proof is the way out.

Lukas Stevens (Nov 03 2023 at 10:42):

I found the problem. This is documented under higher order recursion in the function manual. You need the following lemma:

definition foo :: "nat ⇒ (nat ⇒ nat list) ⇒ nat list"
  where "foo n f = n # f n"

lemma [fundef_cong]:
  "n = m ⟹ f n = g m ⟹ foo n f = foo m g"
  unfolding foo_def by blast

fun bar :: "nat ⇒ nat list" where
  "bar 0 = []"
| "bar (Suc n) = n # foo n bar"

Marvin Brieger (Nov 03 2023 at 11:21):

Great, I could successfully adopt this to my actual (more complex) definition!

Last updated: Dec 21 2024 at 16:20 UTC