*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Quickcheck counter example of "3 < 4"?*From*: Jason Dagit <dagitj at gmail.com>*Date*: Thu, 2 Jul 2015 10:12:53 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5594D6B7.1080109@in.tum.de>*References*: <CAJ-DSyzHTYYeHT3DqUotjs10cwwpj3SkskSTmoQoY7aWz63Aow@mail.gmail.com> <5594D6B7.1080109@in.tum.de>

On Wed, Jul 1, 2015 at 11:14 PM, Tobias Nipkow <nipkow at in.tum.de> 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" quickcheck >> > > No 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. > I see. Thanks! > > 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. > I think I've been bitten by this several times. Most recently (and where I discovered the above example), I was proving the follow lemma, using the induction lemma described in [1]: lemma "(n::nat) > 1 â nâ2 > n + 1" In the case of n = 2, I had this: case 2 show "2 + 1 < 2â2" by auto This was giving me a message saying: show 2 + 1 < 2â2 Successful attempt to solve goal by exported rule: (1 < 2) â 2 + 1 < 2â2 But also saying: Failed to finish proofâ: goal (1 subgoal): 1. 3 < 2â2 Of course, if I manually simplified the expression in my `show` to match the goal, then I get an error about refining the goal. As you might have already guessed, the solution is rather simple, I have to add a type annotation somewhere in the `show`. So having an alert about polymorphic numerals would have been helpful here for this beginner. Lesson learned. [1] http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/10660

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

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

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

- Previous by Date: Re: [isabelle] Cannot solve all subgoals
- Next by Date: Re: [isabelle] Work on a new theorem prover
- 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