[isabelle-dev] quickcheck on type real

[Brian Huffman]

Hello all,

I would like to report some bugs I found when using quickcheck on lemmas 
involving division on reals. When auto_quickcheck is enabled (which it is by 
default) these bugs cause the "lemma" command to fail, preventing me from 
even attempting a proof.

The first bug is that sometimes quickcheck fails with a DIVZERO exception. 
This could probably be fixed by changing rat.ML to return zero when dividing 
by zero.

ML {* Codegen.auto_quickcheck := false; *}

lemma "(a::real) = 1 / (1 / a)"
  quickcheck

*** DIVZERO
*** At command "quickcheck".

The same error is also appears with other, more useful lemmas like this one:

lemma real_divide_cancel_lemma:
  "(b = 0  ==> a = 0)  ==> (a / b::real) * (b / c) = a / c"

The other bug is a false counterexample; I have no idea what causes it:

lemma "inverse (a::real) = (1 / a)"
  quickcheck

Test data size: 0

Test data size: 1


Counterexample found:
a = -1

I am using the current CVS version of Isabelle, by the way.

- Brian