Email Gateway (Aug 19 2022 at 14:04): Email Gateway (Aug 19 2022 at 14:04):From: Gergely Buday <gbuday@gmail.com>
Hi,
sledgehammer returns a number of lemmas that can be fed to metis to verify
a lemma.
auto is sometimes better finding the proof, but it does not return any
information on the lemmas used. Has anybody been thinking on the idea of
extending auto's implementation to return with the list of lemmas?
Possibly, the non-trivial lemmas.
This would yield more readable scripts, but there might be a reason that
this is not done.
Email Gateway (Aug 19 2022 at 14:05):From: Lawrence Paulson <lp15@cam.ac.uk>
These two tools work in very different ways. The idea behind sledgehammer is to use a lot of very powerful tools to search for proof, but not to trust the result; instead, we merely extract the list of relevant lemmas to give to a weak but trustworthy internal prover. It is true that this list is very interesting in its own right, especially when it is shorter than one might expect.
Auto uses Isabelle’s internal reasoners. As you have guessed, they use an enormous number of basic lemmas in order to traverse formulas, and it might be interesting to identify the less trivial ones by somehow processing the proof object. This might be a good student project.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:05):From: Gottfried Barrow <igbi@gmx.com>
On 14-03-26 03:31, Gergely Buday wrote:
(Skip past the first 4 paragraphs to get an algorithm for how to
sometimes be able to narrow down what auto is doing, and for a list of
traces to help you do that, and get trace info about other things.)
I'm all for automated tools which give me good information, so, when
needed, I can understand the logic for a proof step, or to make explicit
in a document what lemmas are being used for a proof step.
If Larry Paulson is sympathetic with a request like this, that can't be
a bad thing. I'll do my part and pull strings for grant money, with my
personal friends at Intel, Google, Microsoft, Apple, IBM and all the big
USA defense companies, that should have lots of money after 14 years of
war, like Raytheon which I didn't get a job with, General Dynamics,
Lockheed Martin, and Hughes which I didn't get a job with.
And Motorola, which lost out to Intel, but which has been on my mind
lately, because of num. Is a num big endian or little endian? The
order of the num binary digits is reversed, so in my mind it's big
endian, because binary digits are permanently embedded in my mind as
being little endian, because of thinking about binary digits in relation
to Intel microprocessors, for a long time.
However, Wiki relates endianess to how you read things from left to
right, and if Num.One is considered memory location 0, then maybe num
is little endian, because then, the reading of a num number is
reversed from how it's stored in memory. I'm looking around the room
right now for someone to engage with in thoughtful, intellectual
discourse about the endianness of num. There is no one in the room but
me. That's okay. There's the little kid next door, but he just wants me
to throw him the football, the football not being a soccer ball, the
football being related to chronic brain injury for those who bash their
heads against 280 pound men, pound not being a form of British currency
in this context, and bitcoin not being currency in the context of the
IRS, but merely property.
auto is sometimes better finding the proof, but it does not return any
information on the lemmas used.
The traces give you info about how auto proves a lemma. If it's doing a
lot for a proof step, it's not easy to tell what it did, but then that's
because it did a lot. If you want to narrow down how auto proves a proof
step, you study the trace to the extent you want to, and then apply
other automatic methods directly, such as blast and arith, and from the
simp rules you see in the trace experiment with simp, you do things like
the following, while looking at the output panel trace:
(1) apply(simp only:) and apply(auto simp only:), where if this prevents
auto from proving the lemma, you can start adding back rules you see in
the simp trace with only, or start deleting simp rules using del to
see if you can find simp rules it has to have, as shown next.
(2) apply(simp only: foo bar) and apply(auto simp only: foo bar).
(3) apply(simp del: foo bar) and apply(auto simp del: foo bar).
(4) apply(blast), (apply arith).
If
(1) apply(auto simp only:) or apply(simp only:) shuts it down,
(2) apply(auto simp only: foo1 foo2 foo3) or apply(simp only: foo1
foo2 foo3)proves it,
(3) the blast trace shows it didn't call blast,
(5) the linarith_trace shows it didn't use linear arithmetic,
(6) in the trace it looks like all other rewrites are trivial
simplifications,
(7) or rewrites based on unknown rewrite rules that come from your
lemma assumptions,
then there's some chance logically, if there aren't other traces you
need to enable, that (2) above is the non-trivial lemma info that you're
requesting.
Here are some traces I've accumulated over several years, that I either
insert with a macro, or have in an imported helper file. You use
declare to enable them globally and using to declare them in a
proof. For auto, I'm interested in the simp, blast, and linarith traces
because that's the only ones I know about that will tell what auto is doing:
declare[[blast_trace=false, blast_stats=false]]
declare[[simp_trace=false, simp_trace_depth_limit=100]]
declare[[linarith_trace=false]]
declare[[rule_trace=false]]
declare[[metis_trace=false]]
declare[[simp_debug=false]]
declare[[metis_verbose = false]]
declare[[unify_trace_simp=false]] (*controls tracing of the
simplification phase of higher-order unification*)
declare[[unify_trace_types=false]]
My standard insertion for traces is this:
using[[simp_trace, simp_trace_depth_limit=100, linarith_trace, rule_trace]]
using[[blast_trace, blast_stats]]
To use the blast traces, you use the following, which was most helpfully
provided by Makarius Wenzel:
attribute_setup blast_trace = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace
b)))
*}
attribute_setup blast_stats = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.stats
b)))
*}
Has anybody been thinking on the idea of extending auto's implementation to return with the list of lemmas? Possibly, the non-trivial lemmas.
Personally, I wish I could always shut down simp and auto with
only, other than trivial rewrites being done, like symmetry and
negation of False rewrites, which are generally obnoxious things to have
to manually take care of.
But, if there would be a huge performance hit, even when the traces
aren't enabled, because it would slow down doing the thousands of
low-level things it always has do, that would be bad.
Regards,
GB
Last updated: Apr 26 2024 at 16:20 UTC