Re: [isabelle] Nitpick: Output Syntax for Data Types



On Sun, 2014-05-11 at 21:59 +0200, Jasmin Blanchette wrote:
> > 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".
> 
> 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.

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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.