Email Gateway (Aug 18 2022 at 10:30): Email Gateway (Aug 18 2022 at 10:30):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
Hi there. I normally push this sort of thing via Gerwin, but he's away at
the moment, so here's a direct bug report from me. He also maintains our
local Isabelle version, and I'm afraid I can't be more specific that
Isabelle2005.
It seems that the function package has a real issue with a True or False
term turning up as an explicit assumption thanks to a congruence rule.
For example, try running the following code:
function
recursive :: "nat => nat" where
"recursive (Suc n) = (if True then arbitrary else recursive n)"
"recursive 0 = 0"
In quick-and-dirty mode, this works immediately for me, but when attempted
in strict mode I get a thoroughly self-explanatory "Tactic failed" error.
I haven't looked at any code, but I assume that the problem here is that
the True/Not True assumptions introduced by if's congruence rule are then
eliminated by one of the more interesting simplification rules that
explicitly manipulates PROP. This results in a simpler recursion graph
from which a subsequent tactic has failed to produce the desired recursion
rule.
Obviously, the example above is useless. The example I'm interested in
uses a let expression to put a wrapper around a recursive call, allowing
certain code to be pasted in unmodified but still use the wrapper. In at
least one call site, False is passed as an argument and thus finds its way
into the congruence assumptions. I think I can work around this by
inventing some wrapping constants to befuddle the simplifier, but it would
be nice to see this fixed in future versions.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 10:30):From: Alexander Krauss <krauss@in.tum.de>
Hi Thomas,
Thanks for reporting this. I'll have a closer look.
Alex
Email Gateway (Aug 18 2022 at 10:31):From: Thomas Arthur Leck Sewell <tsewell@cse.unsw.EDU.AU>
I'd like to widen my previous bug report. Having boiled down my example to
a simple construction and explained it, I went and worked around the
problem only to have the system continue to fail ... sigh.
It seems that some of the simps in simp_thms are applied in a simpset deep
in the bowels of the function package, and that if any of them
manipulate the term, it will result in a tactic failure later (when not in
quick-and-dirty mode) when the package tries to produce derivative
results.
For example:
function recursive :: "bool => nat" where
"recursive x = recursive (Not True)"
function recursive :: "bool => nat" where
"recursive x = recursive (Not False)"
function recursive :: "bool => nat" where
"recursive x = recursive (True & x)"
function recursive :: "bool => nat" where
"recursive x = recursive (x & True)"
But not (x | False). This is all rather amusing, and I hope someone has an
idea what I might have come across.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 10:31):From: Alexander Krauss <krauss@in.tum.de>
Thomas,
I'd like to widen my previous bug report. Having boiled down my example
to a simple construction and explained it, I went and worked around the
problem only to have the system continue to fail ... sigh.
You are using a development snapshot of Isabelle, so errors like this
can happen from time to time.
Please send further bug reports for the function package directly to me.
It is good if you produce small self-contained examples like you did, but
you shouldn't try to guess what happens internally, since that
probably just wastes your time.
function recursive :: "bool => nat" where
"recursive x = recursive (Not True)"[...]
These were all instances of the same problem. We fixed this in the
CVS, and the fix should be in tomorrow's development snapshot.
Cheers,
Alex
Last updated: May 03 2024 at 04:19 UTC