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
>> (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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.