Email Gateway (Aug 22 2022 at 10:52): Email Gateway (Aug 22 2022 at 10:52):From: Julian Brunner <julianbrunner@gmail.com>
Dear all,
I came across some interesting behavior with respect to the auto proof
method. In the attached theory, auto has to be applied twice in a row in
order to solve the goal. The first invocation solves the first subgoal and
transforms the second, with the second invocation solving what remains of
the second subgoal. So far, I was under the impression that when invoking
auto, it solves/transforms the subgoals until it cannot do anything else,
guaranteeing that a second invocation fails immediately. Any clues on what
is happening here?
Julian
Scratch.thy
Email Gateway (Aug 22 2022 at 10:52):From: Joachim Breitner <breitner@kit.edu>
Hi Julian,
auto has a limit as to how deeply it searches for proofs, and with a
complicated goal, you might well hit that limit, leaving the proof
state in a semi-proven goal a second invocation of auto can solve.
auto has some parameters whose semantics I do not know, but from
experience (auto 4 4), works in these cases. Or try something like
fastforce+.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 10:52):From: Julian Brunner <julianbrunner@gmail.com>
That was also Manuel's first idea when I told him about it. However, it
doesn't seem to have any effect here, as even (auto 100 100) doesn't solve
the goal. Also, my interest here is less about finding a convenient proof
(auto+ does it just fine, after all), and more about figuring out what is
going on.
Email Gateway (Aug 22 2022 at 10:52):From: Quentin Hibon <quentin.hibon@polytechnique.edu>
apply auto+ also works (the + repeats the given command until it no
longer succeeds).
Email Gateway (Aug 22 2022 at 10:52):From: Lars Noschinski <noschinl@in.tum.de>
auto is designed such that it is usually idempotent, but without
guarantees. It calls first the simplifier and then safe, before trying
some classical reasoning. Sometimes, the simplifier needs a call to safe
first.
Last updated: Apr 25 2024 at 04:18 UTC