Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quickcheck problem?

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

From: Thomas Genet <Thomas.Genet@irisa.fr>
True, it fixes the problem. Thanks a lot.

Thomas

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

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

I am playing a bit with Isabelle (MacOSX version, Isabelle2009-2.dmg)
and had the following problem: quickcheck always answers

*** Term to be tested contains type variables
*** At command "quickcheck".

whatever the theorem to be proved. I even tried with the example of the
quickcheck paper:

theory ToyList3
imports Datatype
begin
datatype 'a list= Nil ("[]")
| Cons 'a "'a list" (infix "#" 65)

primrec take::"nat => 'a list => 'a list"
where
"take n [] = []" |
"take n (x # xs) =
(case n of
0 => [] |
Suc m => x # take m xs)"

primrec drop::"nat => 'a list => 'a list"
where
"drop n [] = []"|
"drop n (x # xs) =
(case n of
0 => x # xs |
Suc m => drop m xs)"

theorem "take j (drop i xs) = drop i (take j xs)"
quickcheck

Note that nitpick succeeds to find a counterexample.

What did I do wrong?

Thanks in advance,

Thomas

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

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

The issue is actually located here: in user space, you are always
expected to include the Main theory among you imports (directly or
transitively). The toy list examples in the tutorial are just there to
demonstrate for beginners how lists are done in the system, therefore
they start at a theory which does not contain lists already.

Beneath theory Main there is an intricate bootstrap of various
components which are then plugged together to get the basic tool setup
that the user expects: also quickcheck is not monolithic but can be
thought of as a "microkernel service". The good thing is that as a user
you need not spend much thought on it: start with Main and leave the
issues beneath to developers. An analogy: starting beneath Main is like
using a Unix without init or Upstart.

Hope this helps,
Florian
signature.asc

Last updated: Apr 25 2024 at 08:20 UTC