Discussion:
[isabelle] Proof failed for datatype
(too old to reply)
C***@data61.csiro.au
2016-09-15 10:34:00 UTC
Permalink
Hi all,

As far as I can tell, I seem to have run into an issue with the datatype
package. After slightly increasing the complexity of an existing
datatype I get a 'Proof failed' error message.

The problematic datatype is
datatype ('s, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list"

Cheers,
Corey
Jasmin Blanchette
2016-09-15 10:41:32 UTC
Permalink
Dear Corey,
Post by C***@data61.csiro.au
As far as I can tell, I seem to have run into an issue with the datatype
package. After slightly increasing the complexity of an existing
datatype I get a 'Proof failed' error message.
The problematic datatype is
datatype ('s, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list"
The bug appears to be already fixed in the development version of Isabelle, and hence in the forthcoming release (expected before the end of the year). There should be easy (but ugly) workarounds, e.g. by using a type isomorphic to ×. Let me know if you want a patch for Isabelle2016.

Cheers,

Jasmin
Dmitriy Traytel
2016-09-15 20:07:46 UTC
Permalink
Dear Corey,
Post by Jasmin Blanchette
Dear Corey,
Post by C***@data61.csiro.au
As far as I can tell, I seem to have run into an issue with the datatype
package. After slightly increasing the complexity of an existing
datatype I get a 'Proof failed' error message.
The problematic datatype is
datatype ('s, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list"
The bug appears to be already fixed in the development version of Isabelle, and hence in the forthcoming release (expected before the end of the year). There should be easy (but ugly) workarounds, e.g. by using a type isomorphic to ×. Let me know if you want a patch for Isabelle2016.
another (much simpler) workaround is to put a “dead” annotation on ’s (it is dead anyway since it occurs as a parameter to set):

datatype (dead 's, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list”

Cheers,
Dmitriy
C***@data61.csiro.au
2016-09-16 02:17:04 UTC
Permalink
Awesome, thanks Dmitriy! That solves my problem nicely.

Cheers,
Corey
Post by Jasmin Blanchette
Dear Corey,
Post by Jasmin Blanchette
Dear Corey,
Post by C***@data61.csiro.au
As far as I can tell, I seem to have run into an issue with the datatype
package. After slightly increasing the complexity of an existing
datatype I get a 'Proof failed' error message.
The problematic datatype is
datatype ('s, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list"
The bug appears to be already fixed in the development version of Isabelle, and hence in the forthcoming release (expected before the end of the year). There should be easy (but ugly) workarounds, e.g. by using a type isomorphic to ×. Let me know if you want a patch for Isabelle2016.
datatype (dead 's, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list”
Cheers,
Dmitriy
Loading...