Re: [isabelle] Quickcheck counter example of "3 < 4"?
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
>> 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 :
lemma "(n::nat) > 1 â nâ2 > n + 1"
In the case of n = 2, I had this:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and