Re: [isabelle] general commands for rewritting real expressions
- 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> <CAGOKs09uO1WXYAS8nwAwVJHY6TEmwMdFp5DX9LN7YRaMZemail@example.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
* 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
* "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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and