Re: [isabelle] general commands for rewritting real expressions



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
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.