*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*: Mon, 4 May 2020 17:06:32 +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*: <6D44FCB7-C07C-4E17-AF1F-2F1805CA3D08@inf.ethz.ch>*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> <a0887c6e-2030-8648-2443-31dfbf949e05@in.tum.de> <2196b1bf-b197-213d-84dd-2fc26587182a@in.tum.de> <6D44FCB7-C07C-4E17-AF1F-2F1805CA3D08@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0

On 03/05/2020 11:46, Traytel Dmitriy wrote: > while your code works for the examples you show, it does not seem to handle nested recursion. Yes, I am aware of that. Nested datatypes make things considerably more complicated, so I'd rather not support that for now. I'd have to 1. somehow figure out /all/ the other datatypes involved in the definition of my datatype and 2. figure out a robust way to expand their size functions. I have no idea how to do 1 with the information provided by the BNF package (other than inspecting the types of the constructors to figure out the nesting). I also have no idea how to do 2 properly – the "size" plugin provides some information with BNF_LFP_Size.size_of, but oddly enough it only provides the equations for the "regular" size function "size", but not for the generalised one (e.g. "size_list"), which appear in the size functions of nested datatypes. Note that I really do want to do 2, because relying on the simplifier itself to solve the precondition "size lhs ≠ size rhs" is fragile and breaks at least in some cases in the AFP. > I am sympathetic to the proposal of having a 'proper > subexpression' ordering defined for > all datatypes (e.g., via a plugin similarly to size). > Its usefulness goes beyond the > acyclicity rules which this thread is about. Absolutely! It's probably no surprise to you when I say that I won't implement this. But if you (or one of our other datatype experts) ever does it, do let me know! > But one would like to have some reasonable simp rules for subexp_x > (which may be as hard as the original problem that you are trying to solve). > In particular, if F is itself a datatype that belongs to the subexp type class, > its notion of subexp should be linked to the one of x. Already for mutual and nested datatypes, you would probably need an entire family of relations for each combination of types (e.g. if you have mutually recursive datatypes A and B, you would probably need subexpr_A_A, subexpr_A_B, subexpr_B_A, subexpr_B_B). I guess everything gets complicated once you involve nested datatypes… Manuel See code below, with your simproc enabled. Also I would register it only for types that belong to the size class, i.e., > > simproc_setup datatype_no_proper_subterm ("(x :: 'a :: size) = y") = ‹K datatype_no_proper_subterm_simproc› > > Your retrieval of mutual types looks reasonable to me. As usual with Isabelle/ML, the most reliable documentation is the code. > > I am sympathetic to the proposal of having a 'proper subexpression' ordering defined for all datatypes (e.g., via a plugin similarly to size). Its usefulness goes beyond the acyclicity rules which this thread is about. In particular, the 'proper subexpression' ordering can be used for 'strong induction' or to prove termination of functions in cases when size does not exists. (Provided that we also have the fact that this ordering is wellfounded proved.) Something along the following lines: > > class subexp = > fixes subexp :: "'a ⇒ 'a ⇒ bool" (infixl "⊏" 65) > assumes wf: "wfP subexp" > > declare [[typedef_overloaded]] > > bnf_axiomatization 'a F [wits: "'a F"] > > datatype x = Ctor "x F" > > instantiation x :: subexp begin > > definition subexp_x :: "x ⇒ x ⇒ bool" where > "subexp_x = tranclp (λx y. case y of Ctor f ⇒ x ∈ set_F f)" > > instance > apply intro_classes > apply (unfold subexp_x_def) > apply (rule wfP_trancl) > apply (rule wfPUNIVI) > subgoal premises prems for P x > apply (induct x) > apply (rule prems[rule_format]) > apply (simp only: x.case) > done > done > > end > > But one would like to have some reasonable simp rules for subexp_x (which may be as hard as the original problem that you are trying to solve). In particular, if F is itself a datatype that belongs to the subexp type class, its notion of subexp should be linked to the one of x. > > Dmitriy > > datatype 'a rtree = Leaf | Node 'a "'a rtree list" > > lemma "Node x (a # xs) ≠ a" > apply simp? ―‹no_change› > apply (rule size_neq_size_imp_neq) > apply simp > done > > lemma "Node x [c,a,b] ≠ a" > apply simp? ―‹no_change› > apply (rule size_neq_size_imp_neq) > apply simp > done > > > > On 2 May 2020, at 18:04, Manuel Eberl <eberlm at in.tum.de<mailto:eberlm at in.tum.de>> wrote: > > I attached a proof of concept (works with Isabelle 2020) using the > simple size-based approach, including some example applications. > > It works well, although I'm not sure what the proper way to get the > datatype information is (e.g. the list of all the constructors of the > datatype and the associated other datatypes in case of mutual recursion). > > Is the ML interface of the BNF package documented anywhere (in > particular this aspect)? > > Manuel > > > On 02/05/2020 16:19, Manuel Eberl wrote: > 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 > > > > > > <Foo.thy> >

**Follow-Ups**:**Re: [isabelle] Non-idempotence of datatype constructors***From:*Traytel Dmitriy

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

**Re: [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:*Traytel Dmitriy

- Previous by Date: [isabelle] Final call for contributions for the virtual WiL 2020 (4th Women in Logic Worskhop collocated with Petri Nets, IJCAR etc)
- Next by Date: Re: [isabelle] Non-idempotence of datatype constructors
- 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