Email Gateway (Aug 22 2022 at 10:43): Email Gateway (Aug 22 2022 at 10:43):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,
sometimes when I prove a lemma with multiple subgoals one after the
other, the number of subgoals does not shrink and in the end there are
unsolved subgoals that I don't understand.
The following is a minimal example of what happened:
theory Test imports Main begin
lemma foo:
assumes "R = {}"
shows "⋀x y. (x, y) ∈ R ⟹ x = y" "⋀x y. (y, x) ∈ R ⟹ (x, y) ∈ R" proof-
show "⋀x y. (x, y) ∈ R ⟹ x = y" sorry
show "⋀x y. (y, x) ∈ R ⟹ (x, y) ∈ R" sorry
(* 2 remaining subgoals at this point:
1. ⋀x y. (x, y) ∈ R ⟹ (y, x) ∈ R
2. ⋀x y. (y, x) ∈ R ⟹ (x, y) ∈ R
*)
qed
(*
Failed to finish proof:
goal (2 subgoals):
1. ⋀x y. (x, y) ∈ R ⟹ (y, x) ∈ R
2. ⋀x y. (y, x) ∈ R ⟹ (x, y) ∈ R
*)
end
In the lemma, after positioning the cursor in jedit behind proof-, it
shows me the two subgoals I expect. After solving these two subgoals,
there are now still 2 goals remaining and the proof fails.
The last unsolved subgoal looks to me exactly like the one I proved
explicitly with the second show line, so I am somewhat puzzled as to why
it remains.
Where did I go wrong? Is this the expected behavior?
(In case it is relevant, I work with Isabelle2015.)
Thanks,
Christoph
Email Gateway (Aug 22 2022 at 10:44):From: Lars Hupel <hupel@in.tum.de>
Hi Christoph,
Where did I go wrong? Is this the expected behavior?
the short answer: yes, this is expected behaviour.
The longer answer: The statement
show "P ⟹ Q"
doesn't do what you think it does. Let's say, your goal state looks like
this:
When you prove something with "show", then the goal state gets
resolved against what you proved. This allows you e.g. to prove
something more general than what the subgoal says.
In this particular case, you would end up with the new subgoal
However, you can easily avoid that behaviour. You can structure your
proof as follows:
proof -
assume assm: P
show Q
using assm ...
next
assume assm: Q
show P
using assm ...
qed
By explicitly stating "P" as an assumption, the system knows – sloppily
speaking – that it should solve the whole subgoal.
The whole situation is a little bit more complex and it's going to
change (it has already changed in the development version), but the
above is how you would generally structure your proof.
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:45):From: Lars Noschinski <noschinl@in.tum.de>
The short answer is: Don't use "_ ==> _" in show statements. For a
longer explanation, see the following answer on Stackoverflow:
http://stackoverflow.com/questions/25285797/taming-meta-implication-in-isar-proofs/25442787#25442787
-- Lars
Email Gateway (Aug 22 2022 at 10:45):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Thank you and also Lars Hupel for your answers. This list is indeed
very helpful!
I was using show statements with ==> mostly because I had lots of them
from unfolding a locale and most of them were rather trivial one-line
proofs. So I was looking for a way to avoid Isar style verbose proofs
in this specific case without resorting to apply scripts.
Christoph
Email Gateway (Aug 22 2022 at 10:45):From: Lars Noschinski <noschinl@in.tum.de>
When they are really trivial, you might also be able to solve them by
giving a single proof method to the closing "qed".
-- Lars
Last updated: Apr 26 2024 at 04:17 UTC