[isabelle-dev] quickcheck on type real

[Amine Chaieb]

This is perhaps an occasion to advertise Library/Executable_real.thy, 
which contains a verified implementation of rational numbers to be have 
like HOL --- So here you would no get an exception when dividing by 
zero, but just zero as you expect.

Florian integrated this into the CVS to work with his code generator, 
but trying the first lemma with quickcheck, I get the error

*** Unable to generate code for term:
*** of_int a / of_int b
*** required by:
*** Abstract_Rat.INum, Executable_Real.Real, HOL.inverse_class.divide 
def1, <Top>
*** At command "quickcheck".

Maybe this is good motivation to get these theories work for Stefan's 
Code generator and quickcheck.

Amine.


Brian Huffman wrote:
> 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
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev