Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] list_to_set_comprehension simproc crashes

Email Gateway (Aug 19 2022 at 11:54):

From: Dmitriy Traytel <traytel@in.tum.de>
The internal "Tactic failed" can be reproduced in Isabelle2013 as well
as in the repository version 50cc036f1522 by the following example.

datatype x = A | B | C | D

lemma "set (case x of A ⇒ [] | r ⇒ [r]) ⊆ {x}"
using [[simp_debug]] apply simp
oops

With less than 4 constructors the simproc works (by failing properly) as
expected.

Dmitriy

Email Gateway (Aug 19 2022 at 11:54):

From: Makarius <makarius@sketis.net>
I think you could have posted that on isabelle-dev, esp. since you have a
changeset id ready already. (We are again at the verge of an identify
crisis of the mailing lists. Discussing changeset versions should not
become a habit on isabelle-users.)

The canonical question (to be understood in the context of isabelle-dev):
Is there a maintainer of list_to_set_comprehension? This is also relevant
to the coming release.

Makarius

Email Gateway (Aug 19 2022 at 11:55):

From: Dmitriy Traytel <traytel@in.tum.de>
Am 04.09.2013 17:48, schrieb Makarius:

On Wed, 4 Sep 2013, Dmitriy Traytel wrote:

The internal "Tactic failed" can be reproduced in Isabelle2013 as
well as in the repository version 50cc036f1522 by the following example.

datatype x = A | B | C | D

lemma "set (case x of A ⇒ [] | r ⇒ [r]) ⊆ {x}"
using [[simp_debug]] apply simp
oops

With less than 4 constructors the simproc works (by failing properly)
as expected.

I think you could have posted that on isabelle-dev, esp. since you
have a changeset id ready already. (We are again at the verge of an
identify crisis of the mailing lists. Discussing changeset versions
should not become a habit on isabelle-users.)
Maybe it's my own identity crisis, but besides being an Isabelle
developer, my alter ego is also an Isabelle user. In this particular
case I worked as a user on a formalization. After stumbling over the
crash, I have tested the repository version in order to be sure that
this is not fixed yet. Nevertheless, I consider this a perfect match for
isabelle-users.

The canonical question (to be understood in the context of
isabelle-dev): Is there a maintainer of list_to_set_comprehension?
This is also relevant to the coming release.
I looked into the simproc myself and identified the problem. Fix will
follow today. To make the above observation more precise: the simproc
fails properly for an odd number of constructors and crashed for an even
number.

Dmitriy

Last updated: Nov 21 2024 at 12:39 UTC