*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Non-idempotence of datatype constructors*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Sat, 2 May 2020 16:19:41 +0200*Autocrypt*: addr=eberlm at in.tum.de; prefer-encrypt=mutual; keydata= mQINBFnXYyYBEADCLx1xTJEx34IA2n1uH2xGOXNlYA5MRecNLArLyF1bOx5Gjex1ilmZJzj2 mhonPfwpP98QsQDL4N4Nbi+MFpBJGrDATN56GPBQh8a4ttndlp0+srOeNA4kLSE48gp4YdTX zUCXeutse3eHBRtBSqelCoU9VwFc0QmAyiHnnwVy4AgZwiMCbrSvgBSvx/gcyZhYYuOVekTg JN1aZCGpedpTwhH2f7XH8X1Bw4AhjexHPSRZYI+E7eek+QFJTdXndXApHWGQajswrFZQ5W5p q3zS2XAOSMZdquAu0XC7CZzJHV8xzoWQC9XLdV7DltOmASWrLMi2FUrNr/O/uPV08ZIzZxZX 9T+WynujrWwEZPwkcNFM1EUyxIMqaOvJNA5r1Is89SL4rArk8M3MzpF4xqVguAYFxSHyCpZ5 Ijjn1XrYgR/VCqTAhDNXSeOlomd6fFxdDmIo35g/GZZs7giQGi7XocnZegnleeHyJwZdPkie 7zz5cjvFuwrSTvEHybfMIA4pyC2XnVFpCS4y5sCOSemHNEbXQYwJqG1pIj+tH0ncF/O2e9x6 ygW4dKp43aY7E+CMHzQBEuZZo4JLDMmnoGuPPWrjFZA6EmJNIvHUf4uzzdiFJVEuRNqh82R6 HvDvxQkjhuRQvC8cP31pRbf51M8j5W77f0WZ/rFnkIx9hh53EQARAQABtB9NYW51ZWwgRWJl cmwgPGViZXJsbUBpbi50dW0uZGU+iQJUBBMBCAA+FiEEN1tratkE0f8X2q+Y59G0ZJvnKoQF AlnXY18CGwMFCQlmAYAFCwkIBwIGFQgJCgsCBBYCAwECHgECF4AACgkQ59G0ZJvnKoTDEA/+ KY5vnLMwy/WhMaV3r3sl8+L2r75zmIVvatyevVEnfLYunghOO6AurT9S5egwNqOGjuW2FXju NVukQ2/sFqjodUNBdkeMjCSgBG0puGEdTkf9JA2dWAs5cCzQRyFVzwYx9SuHO+gdpxliV/ba 6tHQewoV0BZNtgvu4dlLAaOQw5JPip38tEa0FdMCwpaoPtOTdhwCcDOTDf0sLivi5Eo7zTjP 8edhJoxa0UuWAMWTaPE8UlXSJqN/ufFS5MP1n1eCuSJOkM3ELewjmKddm4/TycxUtvrd4aHp jqJfbm5gh0Xj3l6K7clykqtvrnv5PSydaZvi/THwvlcqlRSekKfBlRYbZUykzZ8xryjNToh/ tbCv19vPlLDm1K2hPfljrMfr5PZj35Ca7v1o2WYQRlYFSIbmY5amUyptsUi1934clybq8lhg lwQCIO4w0gpcMEKyq1hZK4PNvpnac9IcW2G48vjoMCyEJpTrJLO23eEVYGqRBpJGl94b2H6A eWek1Z/3znr+ph0S4tddcfe1Tz5qCOeD5UI0BCMHYw+6uM4Q6NMVwXz1+czcgMJUzbT0FYti EqXMOnh/DC5C1evV1lcyHuI/jEOfpOMfgjKwN/bTQkmzXf3d/Cyf2h4+K4JKZUjT4Wteac+o 3tHLX/2MamTXcqsaU2vrMz+Q6OlDEwY4GXO5Ag0EWddjJgEQANO9foaUMRzjVeniynCTLul/ gDztIR3G9d0aYM4sQ2Sv1hV3xcV+EWyrEPmOjhOYfCEtzW4MBhAKvKFHGMyTz1fIFYvEeBFH AflFnpD5r69B38nv/TkDx2hcrY7ZJ98/2YkE2l5pz8aAU4B2NSgLwpr2eISpAMDZ+Y7Y+G1d n6g5tdlZTdPBSBXVIam1axbKJdRLlAdL4yZNRAqiVaC6kfwkB0O3+4Zhh6NbL8vEkKQB/tOv 6QkJZLBO7kNGtoJP5dc4UnlbSgu5Gq3csbbJsdFFdJETqSDgVrO/2gVxulQjmA6UCzYoXBcn fOioSJQ+4Zu76kBFPRotQ5goAA7JjtHWoLdZ7hTorBy4M5o02OqA9VayZsmiA060oINaS+Kp UQZEUq7i/G+Al5FNqcG8Gq5GBZSAuORYP2KGaAJcrv0tVDbF3BBEdtkPQeLBxb2mVqn8rLQI NDZUdzKr6S19qj2knJFA0dY/jceFSHG4EV8Fr0oEoAfD9opyaduGAJDmO/Zq4xOOJPvIYalB aekPxMbWNmrDmeuK7HQ1IqOx65EoNoOzqqYHnae21NyMSV+h3Wsqq7DJAWiDFqx/ebHpRS25 SyD5Pe89iaC9Cr9X2h3gK2dfgd3UpOTUjRJE1A82c1jEZCvSNDouFY6fiUgFycBrxKa5XzrC nWF7c8soh+YJABEBAAGJAjwEGAEIACYWIQQ3W2tq2QTR/xfar5jn0bRkm+cqhAUCWddjJgIb DAUJCWYBgAAKCRDn0bRkm+cqhIJFEACpRkf/NC+OeYyXmWUja0fVDKoTOmXcBVNdeptnz2Rr QrDZy8Di+DfWmz8VqEkI6PomAWjO3xDU/5yCs7A+gQrt8ioTPJbUCSQNRJGmFSEiLJ0/l9Sq iqjQsUjZbTNYAt2F/RDj7eQYh6c1smXpkbIyCQUfkOtafW9QFCnq06EPuuLOZeh35cphZ7W0 AcCrel2KLvX7PDNQxPmLuP/y2E787YySA/2f7dDjEgvrpNS9WOnWUekFSc3oWtN/dnmn0kXw AK6TYV1C9jUdGVQmjI8JcK4NUEJhVHV4N205EWivBU74L5QMXHHsA3YukYQTYXQOUWlP4x7G Jr4whSKeVh3xZpl2EvF/9Rp9rbwhqTxcBe/oAOeWR98puguCcKQkgANETArKLd3+e1KLeimT OMtgEA4srbuqBh7BtTcbdz4bbjIfKyYFxH/I9ZKpaO6J8DJxNJYQKZfpfs86tv9znfpYWJcB HeSN3ilKW0CBcboQ3Zcs0qycWYLHgMH7DNB49DTCfSMMKGLFmvarAtjkaX5NZraY32PgPvlT ZFTM2SHd14WlC8lwDQgEsYvcItKWped2+XRYfgxGX9SDWwAKr4q/yUAmBaXQyPf519IEcmNe qtIOXZlrjgSw1Kgk1JRlbFkMnlJ5EEkEdBsXP1RCQ8hkwYBzdZURPSeRM+CU2IKREg==*In-reply-to*: <8c84b763-4696-0821-682d-d18ad57d66d4@in.tum.de>*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> <9cf305b5-706c-2e79-5627-b22707c221d4@in.tum.de> <93a5ac2a-9f71-ec10-5b42-5a9e9484baa9@in.tum.de> <8c84b763-4696-0821-682d-d18ad57d66d4@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0

True, but after your suggestion, I realised that the solution with the "proper subexpression" relation (or, alternatively, the size function) combined with a simproc that produces these theorems on the spot is actually the superior approach in every respect. It's simpler, more general, and probably more performant. I can try to come up with a proof-of-concept implementation using the size function approach, since that needs no additional new features from the BNF package. Manuel On 02/05/2020 16:16, Tobias Nipkow wrote: > A first version which only deals with depth 1 would already cover most > of the practical cases. > > Tobias > > On 02/05/2020 15:50, Manuel Eberl wrote: >> That sounds like a good idea. >> >> However, if such a simproc is to work for any nesting of >> constructors,having pre-proven theorems for every constructor will not >> be enough.Instead, I suppose one would have to introduce a >> "proper-subexpression"relation for datatypes (e.g. xs < Cons x xs) along >> with a proof thatthis relation has the obvious properties (irreflexive, >> asymmetric,transitive). >> >> I guess that is something that only a datatype package plugin similar >> tothe one for the "size" function could provide. Having looked at the >> codebriefly, I think only the people who wrote the BNF package could (or >> atleast should) implement that. >> >> Alternatively, one could just use the size function (as someone >> alreadysuggested in this thread) to get pretty much the same thing, >> except thatit won't work for all datatypes (e.g. infinitely branching >> ones). >> >> Manuel >> >> >> On 02/05/2020 15:36, Tobias Nipkow wrote: >>> I do think such rules are useful, esp if they are there by default. I >>> suggest they are best handled by a simproc that is triggered by any >>> "(=)" but that checks immediately if the two argumenst are of the >>> appropriate type and form. That can be done very quickly (there are >>> similar simprocs already). The simproc should work for any datatype and >>> any degree of nesting of the constructors. >>> >>> Tobias >>> >>> >>> On 01/05/2020 22:51, Manuel Eberl 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] 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] Non-idempotence of datatype constructors***From:*Tobias Nipkow

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

**Re: [isabelle] Non-idempotence of datatype constructors***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Non-idempotence of datatype constructors
- Next by Date: [isabelle] SMT 2020: Revised Call for Papers
- Previous by Thread: Re: [isabelle] Non-idempotence of datatype constructors
- Next by Thread: Re: [isabelle] 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