Email Gateway (Aug 22 2022 at 13:00): Email Gateway (Aug 22 2022 at 13:00):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
sometimes I get
Successful attempt to solve goal by exported rule:
and
goal:
No subgoals!
but with
Failed to apply initial proof method
and Isabelle/Jedit does not accept the proof. Where does it get the formula referred as "exported rule" from
and why the system says No subgoals! when despite of this it does not accept the proof?
Email Gateway (Aug 22 2022 at 13:00):From: Makarius <makarius@sketis.net>
On Thu, 17 Mar 2016, Buday Gergely wrote:
sometimes I get
Successful attempt to solve goal by exported rule:
and
goal:
No subgoals!
This means a certain fix-assume-show refinement has worked out.
but with
Failed to apply initial proof method
and Isabelle/Jedit does not accept the proof.
This means that proof method application has failed, e.g. a "by method"
step for the proof of "show" above.
and why the system says No subgoals! when despite of this it does not
accept the proof?
The message stems from really ancient time where there was a linear,
unstructured goal state.
In Isabelle2016 the default split into Output vs. State panel should make
the situation a bit clearer. Did you use that default? Or did you switch
back to the old way?
Makarius
Email Gateway (Aug 22 2022 at 13:00):From: Buday Gergely <gbuday@karolyrobert.hu>
I used Proof state, yes. Switching it off I see
show ∃Ys::form list. Ys cf⇒ (A::form) → (C::form)
Successful attempt to solve goal by exported rule:
( (?A2::form) # (?Xsa2::form list) ⇒ (?C2::form) ) ⟹
(∃Ys::form list. Ys cf⇒ ?C2 ) ⟹ ∃Ys::form list. Ys cf⇒ ?A2 → ?C2
Failed to apply initial proof method⌂:
using this:
∃Ys::form list. Ys cf⇒ (C::form)
goal (1 subgoal):
Is the above "exported rule" a fact, and, where does it come from? Can I use it to prove the goal, or it is a hypothetical fact that would prove the goal?
And, is there a reference of Output and State messages? The Isabelle/jEdit manual does not seem to contain one.
Email Gateway (Aug 22 2022 at 13:01):From: Lars Hupel <hupel@in.tum.de>
Is the above "exported rule" a fact, and, where does it come from? Can I use it to prove the goal, or it is a hypothetical fact that would prove the goal?
Let's say you need to show a HOL implication "A --> B".
lemma "A ⟶ B"
proof
(* The proof command applies a standard rule. As a result,
the state panel shows an unstructured goal state A ⟹ B. *)
assume A
show B
sorry
qed
Do you agree that this is a syntactically correct proof "template"? This
is what the system tells you:
Successful attempt to solve goal by exported rule
It could use the locally fixed variables, assumptions, and shown
propositions to (partly) discharge a subgoal in the goal state.
When you replace the "sorry" with a subproof which doesn't work, the
outer proof is still syntactically correct. But the system also tells
you that the subproof itself is incorrect ("Failed to apply ...").
It may help to think of Isar as a compiler with error recovery. Even if
a part of a program (= proof) does not type check, the compiler
"assumes" correctness and lets you go on with the rest. It'll only
report the error where it actually occurred.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:01):From: Makarius <makarius@sketis.net>
The GUI panels merely display what certain prover commands produce, so the
place to look is the isar-ref manual. For command 'show' it says:
➧ @{command "show"}~‹a: φ› is like @{command "have"}~‹a: φ› plus a second
stage to refine some pending sub-goal for each one of the finished result,
after having been exported into the corresponding context (at the head of
the sub-proof of this @{command "show"} command).
To accommodate interactive debugging, resulting rules are printed before
being applied internally. Even more, interactive execution of @{command
"show"} predicts potential failure and displays the resulting error as a
warning beforehand. Watch out for the following message:
@{verbatim [display] ‹Local statement fails to refine any pending goal›}
Makarius
Last updated: Apr 25 2024 at 12:23 UTC