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




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.

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.

Tobias

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

Compared with the type annotation:
lemma "(3::nat) < 4" quickcheck
Quickchecking...
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.

Thanks,
Jason


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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