*To*: Richard Waldinger <waldinger at ai.sri.com>*Subject*: Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors*From*: Miguel Pagano <miguel.pagano at gmail.com>*Date*: Fri, 1 May 2020 18:04:31 -0300*Cc*: Thomas Sewell <sewell at chalmers.se>, Andrew Butterfield <Andrew.Butterfield at cs.tcd.ie>, Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAEHLFpsax_ZugZZDn0m=tPL4Yeiios0iGEy2ZE57fRVpzShavA@mail.gmail.com>*References*: <c589df10-64bc-a330-aa92-7c55a31e23d5@in.tum.de> <D916632E-8273-4528-9948-73EB0F65840F@cs.tcd.ie> <f7d513d8-be71-33bf-c58d-6055ece0b5ae@in.tum.de> <8fdd816aab574465943b51a475f8af05@chalmers.se> <048a75cb-79d1-e6e4-84ce-f1041bc04706@in.tum.de> <19B9709E-E573-4541-AA06-169CFD9CFB3E@ai.sri.com> <CAEHLFpsax_ZugZZDn0m=tPL4Yeiios0iGEy2ZE57fRVpzShavA@mail.gmail.com>

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 >> >> >>

**Follow-Ups**:**Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors***From:*Manuel Eberl

**References**:**[isabelle] Non-idempotence of datatype constructors***From:*Manuel Eberl

**Re: [isabelle] Non-idempotence of datatype constructors***From:*Manuel Eberl

**Re: [isabelle] Non-idempotence of datatype constructors***From:*Thomas Sewell

**Re: [isabelle] Non-idempotence of datatype constructors***From:*Manuel Eberl

**Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors***From:*Richard Waldinger

**Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors***From:*Miguel Pagano

- Previous by Date: Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors
- Next by Date: Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors
- Previous by Thread: Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors
- Next by Thread: Re: [isabelle] [EXTERNAL] Non-idempotence of datatype constructors
- Cl-isabelle-users May 2020 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list