Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
I am also in favor of the set type-constructor. The issue of compatibility with other HOL provers could very probably be solved by the transfer mechanism. If not immediately from the generic setup, the surely from a tailored one dedicated to this issue, if enough people are concerned. Amine. Am 11/08/2011 14:43, schrieb Florian Haftmann: Hello together, recently in some personal discussions the matter has arisen whether there would be good reason to re-introduce the ancient set type constructor. To open the discussion I have carried together some arguments. I'm pretty sure there are further ones either pro or contra, for which this mailing list seems a good place to collect them. Why (I think) the current state concerning sets is a bad idea: * There are two worlds (sets and predicates) which are logically the same but syntactically different. Although the logic construction suggests that you can switch easily between both, in practice you can't – just do something like (unfold mem_def) and your proof will be a mess since you have switched to the »wrong world«. * Similarly, there is a vast proof search space for automated tools which is not worth exploring since it leads to the »wrong world«, making vain proof attempts lasting longer instead just failing. * The logical identification of sets and predicates prevents some reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x = A x& B x because then expressions like »set xs |inter| set ys« behave strangely if the are eta-expanded (e.g. due to induction). * The missing abstraction for sets prevents straightforward code generation for them (for the moment, the most pressing, but not the only issue). What is your opinion? In a further e-mail I give some estimations I gained through some experiments to figure out how feasible a re-introduction would be in practice. Btw. the history of the set-elimination can be found here: http://isabelle.in.tum.de/repos/isabelle/shortlog/26839 Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Sticking with something merely to avoid change is not a strong argument. This time we know what we go back to and the real benefits (and the few losses). Hence I would be in favour. Tobias Am 11/08/2011 14:43, schrieb Florian Haftmann: > Hello together, > > recently in some personal discussions the matter has arisen whether > there would be good reason to re-introduce the ancient set type > constructor. To open the discussion I have carried together some > arguments. I'm pretty sure there are further ones either pro or > contra, for which this mailing list seems a good place to collect > them. > > Why (I think) the current state concerning sets is a bad idea: * > There are two worlds (sets and predicates) which are logically the > same but syntactically different. Although the logic construction > suggests that you can switch easily between both, in practice you > can't – just do something like (unfold mem_def) and your proof will > be a mess since you have switched to the »wrong world«. * Similarly, > there is a vast proof search space for automated tools which is not > worth exploring since it leads to the »wrong world«, making vain > proof attempts lasting longer instead just failing. * The logical > identification of sets and predicates prevents some reasonable simp > rules on predicates: e.g. you cannot have (A |inf| B) x = A x & B x > because then expressions like »set xs |inter| set ys« behave > strangely if the are eta-expanded (e.g. due to induction). * The > missing abstraction for sets prevents straightforward code generation > for them (for the moment, the most pressing, but not the only > issue). > > What is your opinion? > > In a further e-mail I give some estimations I gained through some > experiments to figure out how feasible a re-introduction would be in > practice. > > Btw. the history of the set-elimination can be found here: > http://isabelle.in.tum.de/repos/isabelle/shortlog/26839 > > Cheers, Florian > > > > > ___ isabelle-dev mailing > list isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] performance regression for simp_all
Hello all, Recently I've been hacking on a bunch of proof scripts using the development version of Isabelle, and I noticed that when processing proof scripts, I often get a noticeable pause at uses of "simp_all". The same pause does not occur with Isabelle2011. Below is a minimal theory file to demonstrate the problem; I ran it with global timing turned on. theory Scratch imports "~~/src/HOL/HOL" begin lemma shows "True" and "True" by (simp, simp) (* 0.001s elapsed time, 0.000s cpu time, 0.000s GC time *) lemma shows "True" and "True" by simp_all (* 0.253s elapsed time, 0.004s cpu time, 0.000s GC time *) I'm using an old, slow machine, so maybe 0.253s is a bit long compared to what most people will see. On the other hand, in terms of the slowdown ratio, 0.1s or even 0.05s would be pretty bad. Here's what I learned by doing "hg bisect": The first bad revision is: changeset: 42372:6cca8d2a79ad user:wenzelm date:Sat Apr 16 23:41:25 2011 +0200 summary: PARALLEL_GOALS for method "simp_all"; http://isabelle.in.tum.de/repos/isabelle/rev/6cca8d2a79ad Was this change supposed to *improve* performance? Was the performance impact tested? Maybe the performance penalty only appears when interactively stepping through proofs, and not in batch mode? - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
I'm strongly in favour of an explicit set type. I've been asked for advice by a number of novice Isabelle users and given the same recommendation: go make the development type-check under the old rules. Then the simplifier will start helping you rather than fighting you. I suppose there might be an alternative strategy involving adapting the simpset or similar to try to standardise blended terms on set operations or function operations. But I don't think this is possible the way Isabelle works - if it were not the default noone then it would not help, and if it were then it would generate years of work in compatibility with the existing proof library. Yours, Thomas. From: isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de [isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de] On Behalf Of Lawrence Paulson [l...@cam.ac.uk] Sent: Thursday, August 11, 2011 11:09 PM To: Florian Haftmann Cc: DEV Isabelle Mailinglist Subject: Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation I hope that my position on this question is obvious. And if we decide to revert to the former setup, I would be happy to help track down and fix some problems in theories. Larry On 11 Aug 2011, at 13:43, Florian Haftmann wrote: > Why (I think) the current state concerning sets is a bad idea: > * There are two worlds (sets and predicates) which are logically the > same but syntactically different. Although the logic construction > suggests that you can switch easily between both, in practice you can't ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Florian: Is your modified Isabelle repo available for cloning, so we can play with it? If so, I might be able to find an answer to my own question... You can clone directly from the http:// location: hg clone http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set or, faster, clone isabelle locally and pull the extra revision. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann wrote: > Hello together, > > recently in some personal discussions the matter has arisen whether > there would be good reason to re-introduce the ancient set type > constructor. To open the discussion I have carried together some > arguments. I'm pretty sure there are further ones either pro or contra, > for which this mailing list seems a good place to collect them. One of the arguments in favor of identifying "'a set" and "'a => bool" was for "compatibility with other HOLs". https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-December/msg00043.html If we make them into separate types again, how will tools that import proofs from other HOLs be affected? I am interested in this question because I have written such a tool myself (I hacked up an importer for Joe Hurd's OpenTheory format a while back). Florian: Is your modified Isabelle repo available for cloning, so we can play with it? If so, I might be able to find an answer to my own question... - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
I hope that my position on this question is obvious. And if we decide to revert to the former setup, I would be happy to help track down and fix some problems in theories. Larry On 11 Aug 2011, at 13:43, Florian Haftmann wrote: > Why (I think) the current state concerning sets is a bad idea: > * There are two worlds (sets and predicates) which are logically the > same but syntactically different. Although the logic construction > suggests that you can switch easily between both, in practice you can't ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
Hi again, as feasibility study I re-introduced the good old set type constructor at a recent revision in the history. The result can be inspected at http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329 This is by no means meant as a thorough treatment of the whole issue, just to get some experience with which problem we would have to cope if we would go ahead. The whole work took approximately seven hours (excluding writing this report). As always which such things, the issue itself (re-introduction of set) took approximately a quarter of the time, solving of not-so-trivial problems (e.g. type check for set type in ML) a third, and the rest was dedicated for re-engineering of poor proofs which hindered the whole matter (btw. this has found its way to the main repository already, e.g. http://isabelle.in.tum.de/reports/Isabelle/rev/b5e7594061ce). A classification of the changes follows: Reintroduction of set type constructor itself: * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l15.7 * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l23.1 * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l15.40 * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l1.16 Correction of bad type annotations: * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l3.8 Correction of predicate/set misfits: * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l8.9 Tuning of metis proofs involving Collect_def or mem_def: * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l5.2 Proof text quality improvement in order to facilitate migration: * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l10.117 * http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l16.15 Ad-hoc adaptations in packages: * Sledgehammer: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l24.1 * Meson: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l19.7 * Quotient: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329#l21.7 These last changesets nicely demonstrate how the situation with sets affects packages: * some (sledgehammer) circumvent problems which would not occur with a set type constructor * for others (quotient) it is not clear how much effort a re-introduction would cost (I doubt that there is any package which inherently depends on the set-predicate identification) The changes above were not systematic, just to get a HOL image built. Then the following sessions fail: HOL-Algebra HOL-Auth HOLCF HOL-ex HOL-Hahn_Banach HOL-Hoare_Parallel HOL-IMP HOL-Imperative_HOL HOL-Induct HOL-Library HOL-Matrix HOL-Metis_Examples HOL-MicroJava HOL-Multivariate_Analysis HOL-Nitpick_Examples HOL-Nominal HOL-NSA HOL-Old_Number_Theory HOL-Predicate_Compile_Examples HOL-Quotient_Examples HOL-TPTP HOL-UNITY HOL-Word-SMT_Examples I estimate that half of these failures are marginal and are just due to use of mem_def or Collect_def in proofs. In particular for HOL-Quotient_Examples an elimination of the failure needs a careful adaptation of the quotient package to the new situation. Other failures are caused by some constructs which somehow exploit the set-predicate identification (Library/Cset.thy "set = member", HOL-Multivariate_Analysis "mono (S :: 'a set ==> _"), but this can be changed with comparably little effort. What can be drawn for that? If there is an agreement that re-introducing set is a good idea, this requires some effort, but it is not unrealistic. A working plan could look like the following: Step A * eliminate predicate / set »misfits« * eliminate proofs with mem_def / Collect_def * repair proofs which fail in this ad-hoc adjustment setup The advantage is that these quality improvements can be committed to Isabelle as it is by now and do not demand a reintroduction of set immediately, but eliminate obstacles later on. Step B * solve problems which existing packages (quotient) * re-construct from relevant changesets what still has to be done to keep the system consistent * re-introduce 'a set Step C * cleaning up the situation: type class instantiations for sets, appropriate simp rules for predicates, … * code generation setup for sets It should be self-evident that nothing beyond Step A can be undertaken before the next release. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy
[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Hello together, recently in some personal discussions the matter has arisen whether there would be good reason to re-introduce the ancient set type constructor. To open the discussion I have carried together some arguments. I'm pretty sure there are further ones either pro or contra, for which this mailing list seems a good place to collect them. Why (I think) the current state concerning sets is a bad idea: * There are two worlds (sets and predicates) which are logically the same but syntactically different. Although the logic construction suggests that you can switch easily between both, in practice you can't – just do something like (unfold mem_def) and your proof will be a mess since you have switched to the »wrong world«. * Similarly, there is a vast proof search space for automated tools which is not worth exploring since it leads to the »wrong world«, making vain proof attempts lasting longer instead just failing. * The logical identification of sets and predicates prevents some reasonable simp rules on predicates: e.g. you cannot have (A |inf| B) x = A x & B x because then expressions like »set xs |inter| set ys« behave strangely if the are eta-expanded (e.g. due to induction). * The missing abstraction for sets prevents straightforward code generation for them (for the moment, the most pressing, but not the only issue). What is your opinion? In a further e-mail I give some estimations I gained through some experiments to figure out how feasible a re-introduction would be in practice. Btw. the history of the set-elimination can be found here: http://isabelle.in.tum.de/repos/isabelle/shortlog/26839 Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Probable bug in let_simp simproc
On Thu, 11 Aug 2011, Thomas Sewell wrote: I spent a bit of yesterday trying to discover why the standard simpset was taking forever to simplify a large term I happen to have. The term is folded down in such a manner that unfolding Let_def will cause it to grow extremely large, which turns out to be what is happening. Deleting the let_simp simproc from the simpset solves the problem. The let_simp simproc is written in two halves. The first bit I can easily understand, and if I produce a simproc with just that code it does what is expected. The second half is commented "Norbert Schirmer's case", and is incomprehensible to me at the moment. Does anyone know, broadly, what it is meant to do? If I knew that I might be able to figure out what the problem was. Here are some further clues from ancient history: http://isabelle.in.tum.de/repos/isabelle/rev/761a4f8e6ad6 In particular the NEWS entry: * Simplifier: new simproc for "let x = a in f x". If a is a free or bound variable or a constant then the let is unfolded. Otherwise first a is simplified to b, and then f b is simplified to g. If possible we abstract b from g arriving at "let x = b in h x", otherwise we unfold the let and arrive at g. The simproc can be enabled/disabled by the reference use_let_simproc. Potential INCOMPATIBILITY since simplification is more powerful by default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
