## Stream: Beginner Questions

### Topic: Nitpick and Sledgehammer both succesfull

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

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

#### Manuel Eberl (Mar 02 2021 at 12:01):

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

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

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

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