Email Gateway (Aug 19 2022 at 17:11): Email Gateway (Aug 19 2022 at 17:11):From: Lars Hupel <hupel@in.tum.de>
I found another problem involving nested case expressions:
lemma "set (if p then case q of (None, u) ⇒ [] | (Some s, u) ⇒ []
else []) = {}"
apply simp
In both Isabelle2014 and Isabelle/adaa430fc0f7, this prints:
Tactic failed
The error(s) above occurred for the goal statement⌂:
set (if p then case q of (None, u) ⇒ [] | (_, u) ⇒ [] else []) =
{x. ∃uu_ uua_. p ∧ (uua_, uu_) = q ∧
x ∈ set (case uua_ of None ⇒ [] | _ ⇒ [])}
A quick look into the simpset reveals that the simproc
'list_to_set_comprehension' is likely at fault. Indeed, after disabling
it, 'simp' goes through (doesn't solve the goal, though). Apparently the
simproc internally sets up some goal via 'Goal.prove' which it cannot solve.
Cheers
Lars
smime.p7s
Email Gateway (Aug 19 2022 at 17:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This seems (again) an indication, that either somebody invests some time
to restore that simproc, or make it optional alternatively.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 09:34):From: Makarius <makarius@sketis.net>
This old thread is still open.
I was at first confused, because the answer by Florian sounded like
another routine breakdown of Set_Comprehension_Pointfree.simproce, but
here it is List_to_Set_Comprehension.simproc, which looks much more
canonical and robust.
Here is again the example causing the crash:
lemma "set (if p then case q of (None, u) ⇒ [] | (Some s, u) ⇒ [] else []) = {}"
apply simp
The point of failure is here in the source
http://isabelle.in.tum.de/repos/isabelle/annotate/879918f4ee0f/src/HOL/List.thy#l639
which may be easily seen by putting a print_tac before and after that
step.
It is not immediately obvious to me, how to improve the simproc, but it
should be possible, after 2-3 rounds of careful study of the source.
In any case this is not relevant for Isabelle2015: the same failure
happens in Isabelle2014, so we don't have a regression.
Makarius
Last updated: Apr 19 2024 at 16:20 UTC