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



Hey, don't worry about it. I had to think for a few seconds to be sure
myself.

A colleague of mine who shall not be named once spent an embarrassingly
long time trying to prove that the "fst" function is injective. ;)

Happens to all of us!

Manuel

On 01/05/2020 23:04, Miguel Pagano wrote:
>
>
> On Fri, 1 May 2020 at 17:59, Miguel Pagano <miguel.pagano at gmail.com
> <mailto:miguel.pagano at gmail.com>> wrote:
>
>
>
>     On Fri, 1 May 2020 at 17:58, Richard Waldinger
>     <waldinger at ai.sri.com <mailto: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
>         <mailto: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.