Sander van Rijnswou (Mar 02 2021 at 10:12): 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)
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.
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: Dec 21 2024 at 16:20 UTC