Email Gateway (Aug 19 2022 at 14:26): Email Gateway (Aug 19 2022 at 14:26):From: Tjark Weber <tjark.weber@it.uu.se>
Jasmin (et al.),
Consider the following minimal example:
theory Scratch imports Main
begin
datatype t = A | B
lemma "(x::t) = y"
nitpick
oops
end
Here, the output that I get from Nitpick is "x = t⇩1 y = t⇩2". I would
have preferred to see, e.g., "x = A y = B".
Incidentally, the latter is what (the now-ancient) Refute prints. And
even Nitpick uses proper constructor names when the lemma is "x = A".
Best,
Tjark
Email Gateway (Aug 19 2022 at 14:26):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Tjark,
This is due to an optimization. If the constructors don't appear in the problem (including definitional axioms etc.), Nitpick treats the datatype as an uninterpreted type (but with the right cardinality constraints), thereby keeping the translation simple. It would be possible for Nitpick to generate some constructor terms instead of t1 and t2, but apart from the fact that it's simpler to generate t1 and t2, I find the added generality nicer, because it indicates that the actual choice of values is irrelevant.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 14:26):From: Tjark Weber <tjark.weber@it.uu.se>
I agree that this is often the more useful bit of information; but it's
less clear to me that when the optimization applies, the user never
wants to see constructor terms. For instance, consider
lemma "(x::bool⇒bool) = y" nitpick oops
versus
datatype t = T "bool ⇒ bool"
lemma "(x::t) = y" nitpick oops
If you had nothing else to do, I would suggest adding an option to show
the constructor terms on demand. But I'll admit that this is not a
particularly important issue.
Best,
Tjark
Last updated: Apr 25 2024 at 08:20 UTC