Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] rep_datatype and Datatype exception

view this post on Zulip Email Gateway (Aug 18 2022 at 16:42):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hello all,

I'm trying to use rep_datatype command, however I'm getting an exception
"Datatype" and I'm not sure why.

In the following example, the only difference between Cons2 and Cons2' is the
(un)currying of the parameters but it's OK for the first one while it isn't
for the second.

theory RepDatatype imports Main
begin

typedef 'a list2 = "UNIV:: 'a list set" ..

definition Nil2 :: "'a list2" where "Nil2 = Abs_list2 []"

fun Cons2 :: "'a \<Rightarrow> 'a list2 \<Rightarrow> 'a list2" where
"Cons2 a as = Abs_list2 (a # Rep_list2 as)"

rep_datatype Nil2 Cons2 (* OK *)
oops

fun Cons2' :: "('a * 'a list2) \<Rightarrow> 'a list2" where
"Cons2' (a, as) = Abs_list2 (a # Rep_list2 as)"

rep_datatype Nil2 Cons2' (* exception Datatype raised
(line 218 of "~~/src/HOL/Tools/Datatype/datatype_aux.ML") *)

What does this exception mean ?

Thanks,

Mathieu Giorgino
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:43):

From: Brian Huffman <brianh@cs.pdx.edu>
Hi Mathieu,

This is a bug. "Datatype" is an exception used internally in the
implementation of "rep_datatype"; users are never supposed to see it.

It appears that while "rep_datatype" supports mutual recursion, it has
problems with indirect-recursive datatypes like your "list2" type.
(Indirect recursion means that a recursive type appears as a parameter
of another datatype. In your case, type "'a list2" appears inside a
product type.)

To the Isabelle developers: I was able to get a little further on this
example by modifying HOL/Tools/Datatype/datatype_data.ML like this:

val descr = map_index mk_spec cs;
val injs = Datatype_Prop.make_injs [descr] vs;
val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs);

Now the rep_datatype command produces the right goals for me to prove,
but it raises another Datatype exception after I finish the proof.
Maybe whoever is currently maintaining the datatype package (Stefan or
Florian?) can follow up on this.

view this post on Zulip Email Gateway (Aug 18 2022 at 16:43):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

the issue with rep_datatype is that it started as a semi-official
bootstrap device for HOL and, over the last years, turned more and more
in a user-space command which still carries around restrictions from
that time. For this sake I recommend to prefer datatype, and use
rep_datatype only under special conditions.

Traditionally, Isabelle/HOL is built in a way that there is practically
only one way to introduce a certain type, although there might be a
couple of legitimate views on that type (e.g. multisets either as
typedef with a restriction predicate over 'a => nat or a quotient of 'a
list). This is indeed a constructivism which has no justification
except pragmatism, and maybe future developments should lift that
restriction. For the moment, the only known exception to this is indeed
rep_datatype, which in its current implementation is an
underapproximation of what it should be properly.

Maybe I find some time to have a look at it.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 16:43):

From: Makarius <makarius@sketis.net>
On Fri, 17 Dec 2010, Florian Haftmann wrote:

the issue with rep_datatype is that it started as a semi-official
bootstrap device for HOL and, over the last years, turned more and more
in a user-space command which still carries around restrictions from
that time. For this sake I recommend to prefer datatype, and use
rep_datatype only under special conditions.

Right. And of course there is no "bug" in the package, it merely tells
you via a low-level exception that it cannot handle certain cases.

I have recently had other surprises with 'rep_datatype', which are in fact
to be expected, since the main characterizing theorems that your have
already usually differ from what 'datatype' would produce (induct rule
etc.). This means one should not lean out of the window too much, and use
plain datatype from the very start whenever this is possible.

To the Isabelle developers: I was able to get a little further on this
example by modifying HOL/Tools/Datatype/datatype_data.ML like this:

Now the rep_datatype command produces the right goals for me to prove,
but it raises another Datatype exception after I finish the proof.
Maybe whoever is currently maintaining the datatype package (Stefan or
Florian?) can follow up on this.

The situation of the datatype package is twofold:

(1) It is very complex already.
(2) It still needs to be localized.

Practically this means that I will have to spend quite some time with it
myself, to upgrade it to the current system infrastructure. I hope that
this is still feasible, so that this key component of Isabelle/HOL is not
stuck in the past -- due to a load of features that is too heavy to lift
it again.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 16:44):

From: Alexander Krauss <krauss@in.tum.de>
Makarius wrote:

The situation of the datatype package is twofold:

(I moved this discussion to the isabelle-dev list, since it is getting
into implementation details)

Alex

Last updated: Apr 25 2024 at 08:20 UTC