Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors



On Fri, 1 May 2020 at 17:59, Miguel Pagano <miguel.pagano at gmail.com> wrote:

>
>
> On Fri, 1 May 2020 at 17:58, Richard Waldinger <waldinger at ai.sri.com>
> wrote:
>
>> isn’t the “size” theorem true for any function, not just size?  or am i
>> missing something?
>>
> It shouldn't be true for non-injective functions.
>
I'm embarrased, please discard my stupid answer.


>
>> > On May 1, 2020, at 1:51 PM, Manuel Eberl <eberlm at in.tum.de> wrote:
>> >
>> >> Firstly, I don't think these theorem is especially useful. You might
>> >> have planned to add this to the simplifier, but its term net doesn't do
>> >> any magic here. It will end up checking every term that matches "Cons x
>> >> xs = ys" for whether "xs" can match "ys". I'm not sure if that matching
>> >> is equality, alpha-equivalent or unifiable.
>> >
>> > I honestly never think /that/ much about the performance implications of
>> > simp rules (as long as they're unconditional). At least for lists, by
>> > the way, this is already a simp rule by default though, and lists are
>> > probably by far the most prevalent data type in the Isabelle universe.
>> >
>> > But you're certainly right that it would make sense to keep a look at
>> > this performance impact if one wanted to add these to the simp set for
>> > all datatypes by default, and I agree that the rules are probably not
>> > helpful /that/ often. Still, it might be nice to have them available
>> > nonetheless.
>> >
>> >> Secondly, you can prove these theorems by using this handy trivial
>> >> theorem : "size x ~= size y ==> x ~= y". Apparently that theorem has
>> the
>> >> name  Sledgehammer.size_ne_size_imp_ne - presumably the sledgehammer
>> >> uses it to prove such inequalities.
>> >
>> > It's even easier to prove it by induction. Plus, in fact, the "size"
>> > thing only works if the data type even has a sensible size function.
>> > That is not always the case, e.g. when you nest the datatype through a
>> > function.
>> >
>> > My main point however is that when you have a datatype with a dozen
>> > binary constructors, there's quite a bit of copying & pasting involved
>> > before you've proven all those theorems. Since it can (probably) be
>> > automated very easily, why not do that? Whether or not these should be
>> > simp lemmas by default is another question.
>> >
>> > Manuel
>>
>>
>>



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