Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] function domains and simplification


view this post on Zulip Email Gateway (Aug 18 2022 at 13:35):

From: Chris Capel <pdf23ds@gmail.com>
theory test
imports Main
begin

(* This function returns some nat based on a list of nats.
If there is a zero in the list, it will sometimes not terminate. *)
function testfun where
"testfun list =
(if (list!0) < length list
then testfun (drop (list ! 0) list)
else length list)"
by pat_completeness auto

lemma simp_loop: "testfun_dom ([0]) ==> testfun [0] = 1"
(* apply (simp) loops *)
sorry

lemma easy: "testfun_dom ([2]) ==> testfun [2] = 1"
apply simp
done

lemma weird: "testfun_dom ([1, 2]) ==> testfun [1, 2] = 1"
apply (simp)

Here the simplifier behaves quite strangely, in my opinion. It
simplifies testfun through one recursive iteration, leaving
"testfun_dom [1, 2] ==> testfun [2] = 1". Why doesn't it simplify the
entire call?

Not surprisingly, adding "testfun_dom ([2])" to the assumptions allows
it to complete. But it doesn't seem like that should be necessary,
since "testfun_dom ([1, 2]) ==> testfun_dom ([2])" due directly to the
definition of testfun. Generally speaking, if arg is the argument to
fun x, for each recursive call x' in x, arg' is in the domain if arg
is. But Isabelle doesn't seem aware of this. Should it be, ideally?

This makes reasoning about potentially non-terminating recursive
functions nearly impossible, in my quite limited experience. Is this
the experience of others?

Chris Capel

view this post on Zulip Email Gateway (Aug 18 2022 at 13:35):

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

function testfun where
"testfun list =
(if (list!0) < length list
then testfun (drop (list ! 0) list)
else length list)"

[...]

lemma weird: "testfun_dom ([1, 2]) ==> testfun [1, 2] = 1"
apply (simp)

Here the simplifier behaves quite strangely, in my opinion. It
simplifies testfun through one recursive iteration, leaving
"testfun_dom [1, 2] ==> testfun [2] = 1". Why doesn't it simplify the
entire call?

Not surprisingly, adding "testfun_dom ([2])" to the assumptions allows
it to complete. But it doesn't seem like that should be necessary,
since "testfun_dom ([1, 2]) ==> testfun_dom ([2])" due directly to the
definition of testfun. Generally speaking, if arg is the argument to
fun x, for each recursive call x' in x, arg' is in the domain if arg
is. But Isabelle doesn't seem aware of this. Should it be, ideally?

Ideally, yes. But it is not trivial to make the simplifier do this in
general, I think...

This makes reasoning about potentially non-terminating recursive
functions nearly impossible, in my quite limited experience. Is this
the experience of others?

In the proofs I did with partial functions, I never had to evaluate a
concrete function more than one or two steps, usually as part of an
induction proof.

If you want to use the simplifier to evaluate a partial function on some
concrete input an arbitrary number of steps automatically, then I guess
you need a special simproc, which automates the domain reasoning along
the way... This hasn't been done yet, and I'd be interested in seeing a
motivating example...

Alex


Last updated: Nov 21 2024 at 12:39 UTC