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



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




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