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 :
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 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and