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.