Email Gateway (Aug 22 2022 at 09:13): Email Gateway (Aug 22 2022 at 09:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF experts,
In the attached theory, the primcorec definition of a function does not terminate (tested
with both Isabelle2014 and Isabelle2015-RC0). Is is because my definition is erroneous or
a shortcoming of the primcorec implementation?
Best,
Andreas
Scratch.thy
Email Gateway (Aug 22 2022 at 09:13):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andreas,
in any case primcorec should always terminate. Here, you definition
looks fine to me. It seems that one of the primcorec tactics is
spinning. I guess we'll need Jasmin's expertise here when he is back
from vacation.
Temporarily, you can use quick_and_dirty to get this definition through.
Best wishes,
Dmitriy
Email Gateway (Aug 22 2022 at 09:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
Thanks for the hint with quick_and_dirty. Now I can continue my work without having to
define the function manually.
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:18):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Andreas,
In the attached theory, the primcorec definition of a function does not terminate (tested with both Isabelle2014 and Isabelle2015-RC0). Is is because my definition is erroneous or a shortcoming of the primcorec implementation?
It is, indeed, a shortcoming of the selector-theorem generating tactic — I think it might eventually have terminated, given enough resources.
The tactic doesn’t look easy to fix. I’ll need to dig into it more deeply, which is unlikely to happen in the very near future. However, an easy workaround is to add an explicit case
| LCons (Inr x) xs’ => Nil_call)”
to deal with the missing unspecified case. (Otherwise, “primcorec” expands the resulting implicit “undefined” into a trivial “case”, which complicates the destructor view — cf. our ITP 2014 paper.)
I’ll let you know if and when I improved the tactic.
Jasmin
Email Gateway (Aug 22 2022 at 09:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,
Thanks for the hint of fully specifying the function. This is certainly better than taking
the quick_and_dirty road.
When I use primcorec, I usually either define it using the destructor view (and then
manually derive a suitable code view -- the automatically generated one is usually not
idiomatic) or specify the code view with cases (from which I derive pattern-matching
equations using simps_of_case) and then manually derive the destructor rules, as the
generated theorems use cases rather than selectors and discriminators. So I am not so
worried about these generated theorems becoming more complex (although undefined indeed
does add some problems, but I am not planning to call my function on arguments that result
in undefined.
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:19):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
When I use primcorec, I usually either define it using the destructor view (and then manually derive a suitable code view -- the automatically generated one is usually not idiomatic) or specify the code view with cases (from which I derive pattern-matching equations using simps_of_case) and then manually derive the destructor rules, as the generated theorems use cases rather than selectors and discriminators.
Using selectors and discriminators for these is also on my TODO list.
Jasmin
Last updated: Apr 25 2024 at 08:20 UTC