Email Gateway (Aug 22 2022 at 17:26): Email Gateway (Aug 22 2022 at 17:26):From: noam neer <noamneer@gmail.com>
Hi everybody.
Whenever I have a rewriting problem (usually involving real expressions) I
try first few general commands like
by auto
by simp
by (simp add: field_simps)
by sledgehammer
Sometimes none work, for example for
lemma "(x::real)>0 ==>
((1+x)(1+x)(1+x) powr (1/3))
=
1+x"
In such cases I sometimes decompose the problem to a few simpler ones, and
sometimes delve into the HOL libraries looking for something useful to add
to simp, possibly reversed.
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.
Thanx.
Email Gateway (Aug 22 2022 at 17:28):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm afraid there is no magic bullet for this sort of problem. I often find divide_simps to be more effective than field_simps, but not here. It is obvious how to make that particular example easier to prove. In general though we are all struggling to prove obvious things.
Larry Paulson
Email Gateway (Aug 22 2022 at 17:28):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi Noam,
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
Email Gateway (Aug 22 2022 at 17:28):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
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
cert
[message truncated]
Email Gateway (Aug 22 2022 at 17:29):From: "Nagashima, Yutaka" <Yutaka.Nagashima@uibk.ac.at>
Hi Noam,
If neither "try" or "try0" tries hard enough, why don't you try "try_hard" from PSL [1].
Alternatively, you can write your own proof strategy:
strategy ForNoam =
Thens
[Ors
[Auto,
Simp,
User <simp add: field_simps>,
User <simp add: devide_simps>,
User <simp add: arith>,
User <simp add: algebra>,
User <simp add: ac_simps>,
User <simp add: algebra_simps>,
Hammer
],
IsSolved
]
and apply this strategy as follows:
lemma "True (just an example)"
find_proof ForNoam
oops
Essentially, this strategy keeps applying
If one of them discharges your proof obligation,
PSL shows that proof method with the corresponding arguments
in the output window.
To use PSL, you have to download its source code form GitHub [2] and
import "PSL.thy" using the "import" command as usual with the right
path to "PSL.thy".
It is just a theory file. So, installation should be easy.
The drawback of this approach is that it can be pretty slow at finding a proof script.
But if it finds a proof script, the proof script shown in the output window tends to be efficient.
I attached a small example file (Scratch.thy).
[1] documentation (Springer or arXiv):
https://doi.org/10.1007/978-3-319-63046-5_32
https://arxiv.org/pdf/1606.02941.pdf
[2] source code: https://github.com/data61/PSL/releases/tag/v0.1.1
Regards,
Yutaka
Scratch.thy
Last updated: Apr 25 2024 at 20:15 UTC