Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with quickcheck in Isabelle2015

view this post on Zulip Email Gateway (Aug 22 2022 at 11:15):

From: Thomas Genet <thomas.genet@irisa.fr>
Dear all Isabelle users,

I have the following strange behavior of quickcheck on the following
simple theory:

datatype t= A | B "(t list)"

value "B [A,A]"

fun f:: "t ⇒ bool"
where
"f _= True"

lemma "f (x::t)= True"
quickcheck
quickcheck [tester=narrowing]

All the quickcheck calls fail. The last one fails with the following
error message:

Type unification failed: No type arity t :: narrowing

Type error in application: incompatible operand type

Operator: ??.Quickcheck_Narrowing.ensure_testable :: ??'a ⇒ ??'a
Operand: λx. equal_bool_inst.equal_bool (f x) True :: t ⇒ bool

Note that the same example works fine with Isabelle2012.

Thanks in advance for any hint,

Best regards,

Thomas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:16):

From: Lars Hupel <hupel@in.tum.de>
Dear Thomas,

the "datatype" command has been replaced with a newer implementation since
Isabelle2012. That replacement also meant reimplementation of the old
facilities. Unfortunately, not everything was/could be implemented. I've
stumbled over the same problem before*: Quickcheck generators will only be
installed for datatypes without nested recursion.

Note that the old "datatype" command is still around:

theory Scratch
imports "~~/src/HOL/Library/Old_Datatype"
begin

old_datatype t= A | B "(t list)"

fun f:: "t ⇒ bool" where "f _= True"

lemma "f (x::t)= True"
quickcheck

There, the call succeeds. I wouldn't recommend using it, though.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 11:17):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Lars, Thomas,

the "datatype" command has been replaced with a newer implementation since
Isabelle2012.

I guess Lars meant Isabelle2015.

That replacement also meant reimplementation of the old
facilities. Unfortunately, not everything was/could be implemented. I've
stumbled over the same problem before*: Quickcheck generators will only be
installed for datatypes without nested recursion.

This is unfortunate. Having done the transition myself, I didn't realized I introduced this limitation (and the conversation between Andreas and Lars didn't wake me up). I will look into this.

Cheers,

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 11:20):

From: Thomas Genet <thomas.genet@irisa.fr>
Dear Lars and Jasmin,

thank you for your answers.
The old_datatype is, at least, a workaround that I can use for some time
until Jasmin successfully fix it ;-)

Best regards,

Thomas

Last updated: Apr 25 2024 at 08:20 UTC