Stream: Beginner Questions

Topic: Nitpick and Sledgehammer both succesfull


view this post on Zulip Sander van Rijnswou (Mar 02 2021 at 10:12):

Hi,

I ran into a case where Nitpick finds a counterexample to a true lemma. The proof checks out, so apparently I can't use Nitpick in this situation? I don't understand why though.

Thanks for your comments,

lemma
  fixes   a b:: int
  assumes "b≠0"
  shows "rat_of_int a  * (Fract 1 b) = (Fract  a b)"
    (* nitpick find a counterexample; sometimes a=0, b=3 sometimes a=2, b=2*)
    nitpick
    (* sledgehammer finds a proof *)
    by (metis Fract_of_int_eq mult.commute mult.left_neutral mult_rat)

question.thy

view this post on Zulip Manuel Eberl (Mar 02 2021 at 12:01):

You might have better luck asking about this on the mailing list – I'm not sure if Jasmin reads Zulip, and he is the nitpick expert.

view this post on Zulip Manuel Eberl (Mar 02 2021 at 12:01):

It certainly looks like it could be a genuine problem with nitpick.

view this post on Zulip Manuel Eberl (Mar 02 2021 at 12:03):

Note however that nitpick is not a ‘trusted’ tool. It doesn't prove that the counterexamples it produces are genuine, it's not the same as actually proving a theorem that this is a counterexample. Nitpick is more like a diagnostic tool to find potential counterexamples. There is no inconsistency in the system when it produces wrong ones – at most, there is a big in Nitpick.

view this post on Zulip Manuel Eberl (Mar 02 2021 at 12:03):

But as I said, do report it on the mailing list, please. Maybe there is some genuine problem with Nitpick here that Jasmin should look into.

view this post on Zulip Sander van Rijnswou (Mar 02 2021 at 14:29):

Thanks, I'll post it to the mailing list.


Last updated: Sep 25 2021 at 09:17 UTC