Email Gateway (Aug 19 2022 at 09:34): Email Gateway (Aug 19 2022 at 09:34):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
When I type...
lemma assumes "A ∧ B" shows "A" "B"
using assms
apply rule
...I obtain the following proof state...
goal (2 subgoals):
1. A ⟹ B ⟹ A
2. B
... which is insoluble. I think the "apply rule" step is using the conjE rule. Which rule should I apply in order to obtain the preferred proof state below? I briefly tried conjunctionI but that doesn't seem quite to fit.
goal (2 subgoals):
1. A ⟹ B ⟹ A
2. A ⟹ B ⟹ B
By the way, I know I can solve this lemma via auto; my question is pedagogical rather than practical.
cheers,
john
Email Gateway (Aug 19 2022 at 09:34):From: Joachim Breitner <breitner@kit.edu>
Hi,
I was told, but don’t understand the reasons, that this works as an
intro rule for &&&:
lemma assumes "A ∧ B" shows "A" "B"
using assms
apply -
goal (2 subgoals):
But I’m also looking forward for pedagogical enlightenment.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:35):From: Makarius <makarius@sketis.net>
Automated tools are indeed obstructing the understanding how formal proof
really works. Here is my version of the above example:
notepad
begin
assume ab: "A & B"
from ab have A and A
apply rule
apply assumption
using ab
apply rule
apply assumption
done
from ab obtain A and B ..
end
General notes on it:
* 'notepad' is better for experimentation than old-fashioned 'lemma',
because it gives you the full proof language. In top-level theorem
statements your possibilities to indicate proof structure are more
limited and one has to simulate things, and obscure the main points
more than necessary. There is also the initial goal hanging around,
but proof is not primarily about goals.
* The fact "ab" (or your assms) need to be eliminated twice to work on
the two goals "A" and "B". The "rule" method implicitly refers to
conjE, but it works on the head goal only. Note that in old-fashioned
tactical reasoning, you would simulate a local fact like "ab" via some
goal premise "A & B ==> ...", and "apply (erule conjE)" would consume
that, and the result would indeed become insoluble as you've said.
In proper Isar, the context grows monotonically, and things can be
used again as required.
* My second proof above via 'obtain' does the elimination of fact "ab"
in a single step, saying that it is possible to assume A and B
simultaneously thanks to the (implicit) conjE rule. Recall that ".."
abbreviates "by rule" (actually "by default", which is a bit more).
Formally, there is only one goal behind 'obtain', so it works in a
single rule application step, not two. It would be more awkward to
prove:
from ab have A and B sorry
which are two goals again.
Since the context of assumptions is commutative, you may swap the
obtain result in-place like this:
from ab obtain B and A ..
Putting it all together, here is my canonical starter proof for Isar:
assume "A & B"
then obtain B and A ..
then have "B & A" ..
You can also make implicit rules explicit like this:
assume "A & B"
then obtain B and A by (rule conjE)
then have "B & A" by (rule conjI)
Using the projections conjD1/conjD2 instead, it becomes a bit more awkward
and artificial:
assume ab: "A & B"
from ab have a: A by (rule conjD1)
from ab have b: B by (rule conjD2)
from b and a have "B & A" by (rule conjI)
To be more fair, here is another variant that minimizes the spaghetti of
fact references:
assume "A & B"
then have B ..
from A & B have A ..
with B have "B & A" ..
I usually prefer the first-class support of eliminations in Isar via
'obtain' to reduce the formal noise and expose the reasoning more
directly.
Makarius
Email Gateway (Aug 19 2022 at 09:35):From: Makarius <makarius@sketis.net>
&&& is merely funny Pure notation to say that there are several
simultaneous goals to be proven.
The system needs to retain this structure for advanced methods like
"induct", so it cannot be split into several goals by default. The
splitting happends implicitly for any other proof method like "rule",
which then acts on the first resulting subgoal only. There are other
proof methods like "auto" that operate on all available subgoals, and
consequently insert used facts into all of them at the start, so the above
example will work here.
You can see the difference again in "simp" vs. "simp_all", which is the
same tool acting either on the head goal or all goals: "apply simp_all"
will solve the above, but not "apply simp".
Further fine points:
assume "A & B"
then have A and B by (simp, simp) -- works
assume "A & B"
then have A and B by simp simp -- fails
assume "A & B"
then have A and B apply simp apply simp done -- fails
assume "A & B"
then have A and B
apply simp
using A & B
apply simp
done -- works
The first one works, because the method expression with sequential
composition "," uses the same facts each time: both simp steps will insert
the given facts into the respective head subgoal before doing
simplification.
The second version puts one simp in the "initial" slot of 'by', and the
other in the "terminal" slot. Only the initial method expressions sees
the used facts, they are reset afterwards.
The third version imitates the same operationally, using two separate
'apply' steps. The 'apply' command essentially "consumes" the used facts,
so the second simp won't see them and fail.
The fourth version refreshes the consumed facts by explicit 'using' in the
apply script, so it works again.
This illustrates that "by method1 method2" is structurally different from
"by (method1, method2). I always emphasize the importance to do canonical
"by induct auto" or "by cases auto" steps that way, and not "optimize"
special cases where old-fashioned sequential composition via "," happens
to work. The latter is merely an odd imitation of tactical proof style in
Isar, and should have disappeared already 10 years ago.
Makarius
Last updated: Apr 23 2024 at 16:19 UTC