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



While we're on the topic of quickcheck, why does it fail to show a counterexample for this?

    lemma "set [(1::nat)] â set [2]"
      quickcheck

    (* Outputs the following, but no actual example:
     *   Quickchecking...
     *   Testing conjecture with Quickcheck-exhaustive...
     *   Quickcheck found a counterexample:
     *)

On 02/07/15 16:51, Andreas Lochbihler wrote:
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).

Andreas

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

Manuel


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
(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





________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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