Email Gateway (Aug 22 2022 at 09:58): Email Gateway (Aug 22 2022 at 09:58):From: Denis Lohner <denis.lohner@kit.edu>
Dear Nitpick developers,
a student of mine recently came up with an example where Nitpick
produces a genuine counterexample for the following (easily provable) lemma:
theory Scratch imports "$AFP/Coinductive/Coinductive" begin
lemma "ltake ∞ xs = xs"
nitpick [expect = none]
by (rule ltake_all) simp
end
I'm not sure if this case is covered by Section 8 "Known Bugs and
Limitations" in the Nitpick Userguide, so I decided to post the example
anyway.
Denis
smime.p7s
Email Gateway (Aug 22 2022 at 09:58):From: David Cock <david.cock@inf.ethz.ch>
Do you mean a spurious counterexample? If it's a lemma, there shouldn't
be any genuine counterexamples.
David
Email Gateway (Aug 22 2022 at 09:59):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Denis,
Thanks for posting it! It is indeed a genuine counterexample to the soundness of Nitpick. I will look into it.
Appeal to the mailing list: Nitpick is not supposed to produce spurious counterexamples (except when it warns you about a “potentially spurious” counterexample in its message already). If you run into cases like the one reported by Denis, this is not normal and I would love to have a reproducible example.
Jasmin
Email Gateway (Aug 22 2022 at 10:01):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Denis,
The issue is related to “enat”. When “Coinductive” is loaded, “enat” is suddenly viewed as a codatatype, with two constructors (0 and eSuc). However, the old constructors and the old case constant still lie around and confuse Nitpick.
This aspect of the Nitpick code is very messy, and there has been a long history of bugs related to types that present several views to their users (starting with the user-level typedef definition). I looked into it for about one hour but couldn’t find a satisfactory solution — I could solve the unsoundness, but only at the cost of gross imprecision that maybe causes more harm than good.
Instead, I am more inclined to leave things as they are and to think through the issue for Nitpick’s planned successor, Nunchaku. But perhaps I’ll find a solution for Nitpick too.
Thank you nonetheless for your report, and please report any future Nitpick bugs you run into on problems not involving “enat”.
Cheers,
Jasmin
Last updated: Apr 18 2024 at 12:27 UTC