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

Showing the instantiations for the type variables would be sensible. However, if one knows how quickcheck works, the search scope is pretty small. With the default setup in Isabelle2015, quickcheck with exhaustive search tries only the types Enum.finite_1, Enum.finite_2, and Enum.finite_3.

In this case, its the type finite_2 which produces a counterexample. Interestingly, quickcheck does not find a counterexample for "4 < 5" (because only Enum.finite_2 instantiates the numeral type class and there it holds).


On 02/07/15 08:21, Manuel Eberl wrote:
Should it not at least show the interpretation of the free type variable?


On 02/07/15 08:14, Tobias Nipkow 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.

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.

The fact that you are not shown the model is because only the
interpretation of the free variables is shown, but there are none.


For instantiation with default_type Enum.finite_1:
Enum.finite_1 to be substituted for variable 'a does not have sort
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:

Compared with the type annotation:
lemma "(3::nat) < 4" quickcheck
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found no counterexample.

Note: in the first case it says there is a counter example but that
is the
end of the output in the "Output" tab of jEdit.

Is this to be expected when no types are given? As a new Isabelle
user it
quite surprised me.


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