Email Gateway (Aug 19 2022 at 12:24): Email Gateway (Aug 19 2022 at 12:24):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
It was using "declare[[blast_trace=false]]" and
"declare[[blast_stats=false]]" with Isabelle2013 that showed me that
auto sometimes calls blast, but those traces cause an error now. Did
anything replace them?
I use that as an excuse to point out that these traces can help educate
a man, and I ask here if there's some kind of trace that will give me
some details about what the "assumption" method is doing.
I give here two proofs of the same statement:
(1)
theorem "(P ==> (Q ==> ((P ==> (Q ==> (!!(P::prop). PROP P))) ==>
(!!(P::prop). PROP P))))"
by(assumption)
(2)
theorem "(P ==> (Q ==> ((P ==> (Q ==> (!!(P::prop). PROP P))) ==>
(!!(P::prop). PROP P))))"
apply(simp del: True_implies_equals)
by(simp only: True_implies_equals)
(* lemma True_implies_equals: "(True ==> PROP P) == PROP P" *)
The formula "(P ==> (Q ==> (!!(P::prop). PROP P))) ==> (!!(P::prop).
PROP P)))" is a conjunction, and I'm having to work hard to try and
prevent the automatic proof methods from proving things using too much HOL.
The proof for (2) is undesirable, but the proof for (1) seems okay
because it doesn't look like it's resorting to any HOL other than some
Trueprop coercion.
However, I don't know the details of what's happening, so I could be wrong.
What I'm guessing is something like this:
There's 3 assumptions: P, Q, and "(P ==> (Q ==> (!!(P::prop). PROP
P)))". The assumption method starts by using P and Q to reduce the third
assumption to "(!!(P::prop). PROP P))", which can then be used as an
assumption for the final conclusion.
If I had a trace to tell me what the assumption method is doing, I might
could stare at it a long time, and figure out what "assumption" is
doing, and also do that with future problems.
Regards,
GB
Email Gateway (Aug 19 2022 at 12:25):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I'll state the obvious again, but the more traces the better, though
there's already a lot of tools to give feedback.
blast_trace looked like it was going to be useful to me. It's main use
was that it was telling me when auto was resorting to something more
than simplification, but I would try some to understand the details it
was returning.
I've searched in NEWS and in isar-ref.pdf, but I didn't find anything
about what would replace blast_trace.
Doing these simple exercises can help make obvious simple things that
aren't obvious at first, and it's the feedback tools that help out.
Talking to myself is fine when I have tools to eventually lead me to the
answers.
In the proof of (2) that I gave, the simp trace was doing some
substitution of "True", and that contributed to my impression that my
false, "(!!(P::prop). PROP P)" was actually important. But then when I
used "assumption", it eventually became clear that I was simply doing:
theorem "(P ==> (Q ==> ((P ==> (Q ==> R)) ==> R)))"
Modus ponens came to mind, and "Auto solve_direct", for the unexpanded
formula, says "meta_impE" can be used, which is based on "meta_mp", but
not quite the same, because of "meta_impE = meta_mp [elim_format]".
All that to say, one thing leads to another, and all the different
routes can lead to a better understanding. I could assume I know what
"assumption" is doing, but assuming I know the details when I don't,
even with something simple, leads to being wrong a significant number of
times.
I guess it's not a big deal, but the more access we have to the
low-level details, to try and understand them and verify what we think
is happening, the better. As I said, there's already a lot of feedback.
Regards,
GB
Email Gateway (Aug 19 2022 at 12:25):From: Makarius <makarius@sketis.net>
These options are a leftover when Larry implemented the tool, and were not
meant for end-user consumption, as far as I can tell.
In Isabelle2013-1-RC2 you can refer to them nonetheless, using regular ML
operations for configuration options:
setup "Config.put_global Blast.trace true"
That is a rather indirect way to see when blast happens to be invoked by
other proof tools. Generally, producing a meaningful trace is very
difficult for anything non-trivial.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC