*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] general commands for rewritting real expressions*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Mon, 25 Jun 2018 12:38:36 -0400*In-reply-to*: <CAKXUXMxGm8FOBc7RJ=3Wk_HdBrV42erUOYudqueC=2prnuttvQ@mail.gmail.com>*References*: <CAGOKs08qjLj33-E4=hH2joGUOs_gAOT9e9Q-JskWmU5KVNEgyg@mail.gmail.com> <CAGOKs0_VVE6v6yvcypYZhmc5vtj2A_P7iwPcVaO-XsbbhdSzgg@mail.gmail.com> <CAGOKs0_08RJ05ayna+BqfyG8-K+uqqzeM+W9yfpWqtk0=LG6Qw@mail.gmail.com> <CAGOKs08xj1wGWNpfBLoLehZ68Y7+Rn7F5U=-BmXAWQi1F40Ghg@mail.gmail.com> <CAGOKs08S-uxnpN0_hV1p5GmO5Gtc-v5FBPpWNwrMgsZDb=mzuA@mail.gmail.com> <CAGOKs08S5RAkyAmbY-sEbX6MG=VcrqxbwGcsKab8iZ0j4oiszQ@mail.gmail.com> <CAGOKs09gshUKmQSg0oPVyW64UTdkCtcm7tdngo2WPMYXu3kiOQ@mail.gmail.com> <CAGOKs0_vLWFhb-7JORU=bZcp1zirqx6jgj_F1tMZPhe6iL8Kow@mail.gmail.com> <CAGOKs09bOzuC9EYrNoJNAoh-xD7EM74eSDa+KZnLQWPuxVo6Ow@mail.gmail.com> <CAGOKs0_NE+k6FL+1DP0Cy_va-1tJobybLGijaC9ymGAE5YPxDg@mail.gmail.com> <CAGOKs0-0Qv-hT3ucODzFScVE-Kjym1sqGDWcH7ir-WorFAFc2g@mail.gmail.com> <CAGOKs09uO1WXYAS8nwAwVJHY6TEmwMdFp5DX9LN7YRaMZ+vf6w@mail.gmail.com> <CAGOKs09D6F9ypRUk+WToFpvjwUHFFyec6oR46LCcVnZfbYxzNA@mail.gmail.com> <CAKXUXMxGm8FOBc7RJ=3Wk_HdBrV42erUOYudqueC=2prnuttvQ@mail.gmail.com>*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.8.0

There are many others on this list with much more experience than I have, but FWIW here are some techniques that I have found useful: * "try" is quite useful, not only for finding out about relevant facts, but also for finding out what proof methods are most likely to work in various situations. Surprisingly often, "try" will come up with a proof if you let it run for a little while. A disadvantage is that sometimes it seems to explode and cause the system to embark on very long garbage collections that put you out of business for many minutes (this is a major peeve I have, which I wish could be improved). Other times it will claim to produce a proof, but you will find that it doesn't actually work. However, by looking at the list of facts that it thinks are relevant, you can select the ones you agree with, add them to your "using" list, and re-run "try". Sometimes you can converge on a proof in this way. At least you are getting an idea of what facts the system has that might be relevant. "Try" will quite often find startling proofs by "smt" that are mostly incomprehensible by just looking at the list of facts used. In working out first versions of a development, I will use these as a quick demonstration that what I am trying to prove is actually true, but later I will go back and expand into something understandable. Infrequently, you can replace "smt" by "metis" or "metis (no_types, lifting)" to avoid the use of "smt". Sometimes "try" will claim to produce proofs by "smt" that mention "everything but the kitchen sink" and will say that "smt" timed out. I throw these away and try something else. * "try0" is useful if you have a pretty good idea of a superset of the facts needed to prove something, but you don't know which proof method is going to work. The "try0" command has a time limit, which avoids spamming the system like "try" can do, so it is not a bad idea to try it first, "just in case". A disadvantage of "try0" is that it will miss long-running proofs by "force" and "fastforce" because they will time out. That is, you might have a sufficient list of facts, but a proof by "force" or "fastforce" will take longer than "try0" allows. This can be frustrating. * As a first strategy when automatic attempts to find a proof fail, look at the output from using "apply simp" on your goal. Try to get an idea why the simplifier only gets as far as it does. This can help to identify missing hypotheses or to try to get an idea of what kind of additional facts should be supplied. If "apply simp" makes substantial progress, but fails to complete the proof, take the result it produces and work on it as a subgoal. If you succeed in proving this subgoal, then you can complete the original proof by adding one additional "by simp" step. * If a goal refuses to succumb to your first attempts, your main recourse is to try to break it into simpler subgoals. The output of "apply auto" is one way of doing this, but the goals might not be very natural. In other cases, you have to apply your understanding of how the proof should go to figure out how to reduce the original goal to subgoals that are likely to be easier to solve. Sometimes if you look around you can find introduction or elimination rules that were not applied automatically, and you can explicitly invoke them in the first step of the proof. * Another strategy that can be helpful when you think you have a set of facts that ought to prove the result but you can't see why the system will not find a proof, is to start specifying the required instances of the facts using the [of ...] construct. While doing this, keep an eye on the output window to make sure that you are in fact specifying the correct instances (this can be done by comparing terms in the instances of the facts being used with terms in the goal). If you get the instances wrong, then you will waste a lot of time on a proof that can't work, so it is best to be careful here. In some cases, specifying partial or full instantiations will provide the boost needed for one of the proof methods to succeed. In general, "force" and "fastforce" often require that instances be specified, whereas "auto" and "simp" seem to be able to find the required instances automatically more often. If I find a proof in this way, I then generally attempt to reduce the instance information to the bare minimum needed for the proof to succeed. The reason for this is, even though the instance information is useful documentation for a human reader, if a change is made later to the facts that have been instantiated, the order in which the terms have to be specified will often change, which will cause the proof to break. So a proof with as few instances specified as possible will generally be more robust to later changes in the statements of the facts it uses. * One of the most difficult things for me in trying to learn how to produce proofs in the system was to come to understand the "personalities" of the various proof methods. Probably knowing how each of them is implemented would be very useful, but I don't have such knowledge, and probably most normal users wouldn't, either. From trying to do proofs lots of different ways and using "try" and observing the results, the following seem to me to be true: * "simp" is perhaps the main workhorse. It takes facts, treats them as rewrite rules, applies the rules to the goal, accumulates consequences of the rules, and ultimately attempts to rewrite the goal to "True". When equations are used as rules, the orientation is important: if the rules do not produce something "simpler" (it can be hard to figure out what this ought to mean in a given situation) then "simp" will not work well. "Simp" can loop when presented with incompatibly oriented rules; the symptom of this is "by simp" remaining a purple color, rather than turning pink (indicating failure) after some time. One can sometimes glean some information about why the looping has occurred by adding [[simp_trace]] and perhaps also [[simp_trace_depth_limit=5]] (or whatever depth is desired) to the "using" list and then hovering the mouse over the "by simp" or "apply simp" to see the simplifier trace. The output can be voluminous and is not that easy to understand. Another important thing to understand about "simp" is how it uses implications P1 ==> P2 ==> ... ==> Q as rewrite rules. It uses such an implication by unifying Q with the goal, then recursively attempting to simplify the obtained instances of P1, P2, ..., to "True". If a subgoal fails to simplify, then backtracking occurs, and the simplifier gives up on that rule and tries another. As far as I can see, the simplifier considers "success" to have occurred whenever *some* simplification is made. Once this occurs, backtracking is apparently suppressed for that subgoal. What this means is that sometimes having "too many" simplification rules can cause the simplifier to miss things that it actually has rules for. This can seem mysterious unless you are able to examine the simplifier trace, and even then it can take time to figure out. So it is important to be able to control the facts the simplifier has and when failure occurs to try to understand the reason for it. * "auto" extends "simp" by doing things like splitting cases and canonicalizing the goal in various ways. Whereas "simp" will not increase the number of subgoals, "auto" will often do so. As far as I know, if something can be proved by "simp", it can also be proved by "auto", though the proof might take slightly longer. Just as looking at the output of "apply simp" can be helpful to understanding, looking at the output of "apply auto" can, as well, though because of the case splitting and other transformations that "auto" makes to the goal it can be more difficult to understand the result. The output of "apply simp" or "apply auto" will show a failed subgoal of the form P1 ==> P2 ==> ... ==> Q. I typically focus first on Q, as that is generally where the essence of what is going on is located. Then work back, looking at the Pi to see among them are rules that would unify with Q and try to see whether there is sufficient information to verify their hypotheses. In some cases, Q will be obviously untrue, in which case "False" needs to be derivable from the Pi. * "force" and "fastforce" will use simplification, but they seem to restrict the simplifications that are used in some sense that I don't really understand well. They will also generally use introduction and elimination rules in more general contexts than what "auto" will do. For example, "auto" seems unwilling to consider the use of an elimination rule if the term to which the rule applies happens to be conjoined with other terms, but it will use the elimination rule if the term stands alone. On the other hand "force" and "fastforce" seem to be able to apply the elimination rule regardless. Guessing from the names, "force" and "fastforce" probably also do a certain amount of brute-force search. This seems to make them useful in situations where there are permutative facts that need to be applied that have no suitable orientations as rewrite rules. On the other hand, this means that these methods may succumb to combinatorial explosion in certain situations, and so will run for a very long time, perhaps effectively forever. * "blast" is a general-purpose method that seems to often succeed when "auto" fails, and vice-versa. Again, I don't understand this well, but when there are rules that cause the simplifier to loop, "blast" can succeed where "auto" fails, whereas conversely there are other situations in which "auto" succeeds where "blast" does not. "Blast" is generally one of the fastest methods for doing relatively routine things, such as the final transitivity step in a "have...also have...finally have" proof. "Fast" seems to me to be related to "blast" but I don't know for sure. * An advantage (and disadvantage) of "metis" is that it requires all the relevant facts to be specified explicitly. So when a proof is done by "metis" you know what you have -- there are no implicit simplification or introduction or elimination rules that come into play. On the other hand, it can be very tedious and verbose to list every single fact used in every single proof, so it is probably desirable to encode a lot of routine reasoning by annotating the facts as rules, so that they can be used automatically by other proof methods. In a proof "by (metis F1 F2 ...)", "metis" will indicate if any of the facts F1 F2 ... are unused. It is usually right about that, and the unused facts can be deleted. In occasional situations it lies, which will leave annoying yellow-orange warning bars on the side of your editor window. "Metis" generally seems to be slow, but it will often "get the job done" in situations where the proof just does not follow any particular structure known to the other methods. * Other methods (e.g. "meson") are more infrequently reported by "try" and "try0". I don't have much of an understanding of these, except that it seems to me that "meson" can be useful when you have to prove somewhat complex general logical facts that are then to be used as lemmas. Once I have a proof by some method, I will typically use "try0" to see what other methods can also do the proof using the same facts, and how much time is required. Then I will usually select the proof method that is the fastest, if there is no other reason not to do so. One reason not to do this is that if you can get several steps in a proof to be performed by the same proof method (e.g. "auto"), then you can often shorten the proof by combining those steps into one. The combined proof might actually take less time than the one with the individual steps, though in some cases, it takes much longer because the system has to search to find out the information that was present in the steps you deleted. So you have to make a decision about whether you want a shorter proof that takes longer to verify or a longer proof that verifies more quickly. There is probably not a good reason to replace a bit longer proof by a somewhat shorter one that takes much longer to verify, but if the time difference is not too much then the abbreviated proof might be preferable. I have made only minimal use of the search features that allow you to look up facts by name or by statement. Based on my own experience, if you find "try" is pointing you regularly to facts from a certain theory, it is worth going and having a look at the source for that theory to try to understand what is there. For what I have been doing, I found that I needed to look at HilbertChoice and FuncSet. Note that I have not done very many proofs that involve reasoning about arithmetic or real numbers. >From the few that I have done, it strikes me that there are many more relevant theories that one would have to find out about in order to construct such proofs efficiently. Well, I wrote a bit more here than what I started out to, but I hope this might help the learning curve for others to be a little flatter than what it has been for me. On 06/25/2018 10:31 AM, Lukas Bulwahn wrote: > Hi Noam, > > On Sun, Jun 24, 2018 at 4:54 AM, noam neer <noamneer at gmail.com> wrote: >> >> Since these solutions are somewhat tedious, my question is - are there >> other general commands I can try at this point? Or maybe something like >> 'field_simps' that is more appropriate for real expressions? Any advice >> would be appreciated. >> > > In addition to Larry's answer: > > I believe you should be made aware of try, try0 and sledgehammer, > these commands invoke generally powerful methods; they are not silver > bullets but are as automatic as it gets in Isabelle and in interactive > theorem provers in general. > > Other than that, you have the right strategy of decomposing the goal, > looking for useful theorems and trying to identify useful lemma sets, > such as field_simps, divide_simps etc. > > Lukas >

**References**:**[isabelle] general commands for rewritting real expressions***From:*noam neer

**Re: [isabelle] general commands for rewritting real expressions***From:*Lukas Bulwahn

- Previous by Date: Re: [isabelle] general commands for rewritting real expressions
- Next by Date: [isabelle] new AFP entry: Pell's Equation
- Previous by Thread: Re: [isabelle] general commands for rewritting real expressions
- Next by Thread: Re: [isabelle] general commands for rewritting real expressions
- Cl-isabelle-users June 2018 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