Email Gateway (Aug 18 2022 at 13:35): 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
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: May 03 2024 at 04:19 UTC