# Re: [isabelle] Quickcheck counter example of "3 < 4"?

```On Thu, 2 Jul 2015, Jason Dagit wrote:

```
```On Wed, Jul 1, 2015 at 11:14 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:

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.
```
```
There are many more possibilities to get into trouble with types that are more general than expected. It used to be a really hard problem to figure that out in the past. Today you just need to C-hover over subspicious variables in the Prover IDE, to get the type information. You have to become active yourself, though.
```
```
One day in the future, the Prover IDE might hilight such suspicious positions spontaneously. (And users will probably run into other problems instead.)
```

Makarius```

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