*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Manuel Eberl <eberlm at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Quickcheck counter example of "3 < 4"?*From*: Matthew Fernandez <matthew.fernandez at nicta.com.au>*Date*: Thu, 2 Jul 2015 22:09:46 +1000*In-reply-to*: <5594DF60.5030101@inf.ethz.ch>*References*: <CAJ-DSyzHTYYeHT3DqUotjs10cwwpj3SkskSTmoQoY7aWz63Aow@mail.gmail.com> <5594D6B7.1080109@in.tum.de> <5594D879.6050905@in.tum.de> <5594DF60.5030101@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

While we're on the topic of quickcheck, why does it fail to show a counterexample for this? lemma "set [(1::nat)] â set [2]" quickcheck (* Outputs the following, but no actual example: * Quickchecking... * Testing conjecture with Quickcheck-exhaustive... * Quickcheck found a counterexample: *) On 02/07/15 16:51, Andreas Lochbihler wrote:

Showing the instantiations for the type variables would be sensible. However, if one knows how quickcheck works, the search scope is pretty small. With the default setup in Isabelle2015, quickcheck with exhaustive search tries only the types Enum.finite_1, Enum.finite_2, and Enum.finite_3. In this case, its the type finite_2 which produces a counterexample. Interestingly, quickcheck does not find a counterexample for "4 < 5" (because only Enum.finite_2 instantiates the numeral type class and there it holds). Andreas On 02/07/15 08:21, Manuel Eberl wrote:Should it not at least show the interpretation of the free type variable? Manuel On 02/07/15 08:14, Tobias Nipkow wrote:On 02/07/2015 07:48, Jason Dagit wrote:I forgot to add a type annotation and ended up with the following (Isabelle 2015 on Windows 7): lemma "3 < 4" quickcheckNo type constraints. Because 3, 4 and < are polymorphic, quickcheck is free to build a type/model with an interpretation for < where 3 < 4 does not hold. There used to be a time when the interface alerted you to polymorphic numerals, which are almost always not what one wants. But we have moved on from that. The fact that you are not shown the model is because only the interpretation of the free variables is shown, but there are none. TobiasQuickchecking... For instantiation with default_type Enum.finite_1: Enum.finite_1 to be substituted for variable 'a does not have sort {numeral,ord} Testing conjecture with Quickcheck-exhaustive... Quickcheck found a counterexample: Compared with the type annotation: lemma "(3::nat) < 4" quickcheck Quickchecking... Testing conjecture with Quickcheck-exhaustive... Quickcheck found no counterexample. Note: in the first case it says there is a counter example but that is the end of the output in the "Output" tab of jEdit. Is this to be expected when no types are given? As a new Isabelle user it quite surprised me. Thanks, Jason

________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

**Follow-Ups**:**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Lars Noschinski

**References**:**[isabelle] Quickcheck counter example of "3 < 4"?***From:*Jason Dagit

**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Tobias Nipkow

**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Manuel Eberl

**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Work on a new theorem prover
- Next by Date: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Previous by Thread: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Thread: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list