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)
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.
It certainly looks like it could be a genuine problem with nitpick.
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.
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.
Thanks, I'll post it to the mailing list.
Last updated: Sep 25 2021 at 09:17 UTC