Email Gateway (Aug 22 2022 at 15:10): Email Gateway (Aug 22 2022 at 15:10):From: Michel via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
To understand Isar, I try to write proofs without automation.
I have understood that after the word "proof", PIDE try to apply the implicit rule of the formula to prove and with "r", such a rule does not exists.
But with show "r" using 1, it's worst.
Intuitively, the proof of "r" is simple.
4: "q --> r" by mp (modus ponens) on 1, 3
"r" by mp on 4, 2
Why it's impossible to write this in Isar ?
How to avoid the implicit use of rules?
lemma trivial3isar : "(p ⟶ (q ⟶ r)) ⟶ (q ⟶ (p ⟶ r))"
proof
assume 1: "p ⟶ (q ⟶ r)"
show "q ⟶ (p ⟶ r)"
proof
assume 2: "q"
show "p ⟶ r"
proof
assume 3: "p"
show "r"
using 1
proof
With show "r" using 1, the last proof gives two unsolvable goals
1 (q --> r)==> r
2 p --> (q --> r) ==> p
Email Gateway (Aug 22 2022 at 15:10):From: Peter Lammich <lammich@in.tum.de>
Just note that this highly nested proof structure is very unusual in
practice.
The parenthesis structure of your goal is a bit misleading. Try
term "(p ⟶ (q ⟶ r)) ⟶ (q ⟶ (p ⟶ r))"
to see how it looks with only necessary parenthesis:
"(p ⟶ q ⟶ r) ⟶ q ⟶ p ⟶ r"
Chains of implications are a very common thing in HOL, and usually you
handle them all at once by repeated implication introduction ... there
is no need to open a new nesting level for every single impI:
lemma "(p ⟶ (q ⟶ r)) ⟶ (q ⟶ (p ⟶ r))"
proof (intro impI)
having done this, the proof is almost as easy as you would write it
down on paper. You have several stylistic possibilities here. You could
number your assumptions:
assume 1: "p ⟶ (q ⟶ r)" and 2: "q" and 3: "p"
from 1 have "q⟶r" using 3 by (rule mp)
then show "r" using 2 by (rule mp)
qed
or you could refer to the short assumptions explicitly by fact
antiquotations (note that you have to assume them anyway):
lemma "(p ⟶ (q ⟶ r)) ⟶ (q ⟶ (p ⟶ r))"
proof (intro impI)
assume "q" "p"
assume "p ⟶ (q ⟶ r)"
then have "q⟶r" using ‹p› by (rule mp)
then show "r" using ‹q› by (rule mp)
qed
I posted this email because I feel that this thread has the potential
to scare new Isabelle users and leave them with the impression they
need deeply nested lengthy proofs to handle simple chains of
implications ...
Note to more advanced beginners:
Usually, you never state top-level implications on the HOL level, but
you use the meta-level directly, e.g., you would write:
lemma "(p ⟶ (q ⟶ r)) ⟹ q ⟹ p ⟹ r" or, equivalently:
lemma "⟦(p ⟶ (q ⟶ r)); q; p⟧ ⟹ r"
proof -
assume "q" "p"
assume "p ⟶ (q ⟶ r)"
then have "q⟶r" using ‹p› by (rule mp)
then show "r" using ‹q› by (rule mp)
qed
(whether to use brackets or chains of implications is a matter of
taste, and actually, brackets are just syntactic sugar for chains of
implication. I, personally, find brackets easier to read.)
Even more likely, you would use the long-goal format, which saves you
from re-stating the assumptions in the proof:
lemma
assumes 1: "(p ⟶ (q ⟶ r))" and "q" "p"
shows "r"
proof -
from 1 have "q⟶r" using ‹p› by (rule mp)
then show "r" using ‹q› by (rule mp)
qed
Email Gateway (Aug 22 2022 at 15:10):From: Makarius <makarius@sketis.net>
Here are more examples that you can try: De Morgan laws.
The predicate logic versions are actually simpler than the propositional
ones, but you need to know how to introduce and eliminate quantifiers
(especially the 'obtain' element of Isar).
Makarius
De_Morgan.thy
Email Gateway (Aug 22 2022 at 15:10):From: Lawrence Paulson <lp15@cam.ac.uk>
Absolutely right.
To learn a natural proof style, it’s crucial to use automation. Most proofs involve a string of steps stated using “have” and concluding with “show”. The steps may be connected using “then” or using “moreover/ultimately”. And each justification should involve just a couple of steps involving simp/auto/blast or generated using sledgehammer.
Nesting only arises when one of the intermediate steps is too difficult to prove directly by automation, but even then, the structure of the inner proof would be as described above.
A nesting deeper than three is unusual except in long and complicated proofs.
Try to find an example that goes outside pure logic.
Larry Paulson
Email Gateway (Aug 22 2022 at 15:11):From: Michel via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Thank you really much for your examples. I try to write basic proofs if
it possible without automation and with your suggestion it was possible.
I have written a software <http://teachinglogic.liglab.fr/DN/> (a long
time ago) to produce proof in natural deduction.
This software was originally written in Prolog by Robert Stärk, who was
assistant at ETH Zürich. I try to see if the proofs given by this
software can be translated in Isar. That is the origin of my questions
on Isar.
Lawrence Paulson has said : It’s essential to understand that “proof” by
itself will attempt to use the default proof method. But this default
proof method can lead to an unprovable goal.
If you have to show a not propositional formula, as in the examples
triv1 and triv2 below, you have to give a "by method" or suggest an
hypothesis to eliminate.
In the example triv1 below, the default proof method leads to an
unprovable goal, and there is no hypothesis to eliminate, so you are
obliged to give a "by method". In the example triv2, the default method
leads to an unprovable goal, but we can indicates an hypothesis to
eliminate.
lemma triv1 : "p ⟹ q ∨ p"
(* proof : after the word proof, the new goal produced automatically
by the intro rule disjI1 would be p ⟹ q
which is unprovable. You have to give a method
because you don't have an hypothesis to eliminate
*)
by (rule disjI2)
lemma triv2 : assumes 1: "p ∨ q" shows "q ∨ p"
(* proof : after the word proof, the new goal, produced by
the implicit intro rule disjI1 would be
p ∨ q ⟹ q which is unprovable
so either you give a method (by method) to prove the lemma
or you must indicate, with using, the assumption that can be
eliminated
*)
using 1
proof
assume "p"
then show "q ∨ p" by (rule disjI2)
next
assume "q"
then show "q ∨ p" by (rule disjI1)
qed
In the proof triv3, the thesis is a proposition, so you must use an
hypothesis (or a direct by method).
lemma triv3 : assumes 1: "p ∧ q" shows "p"
using 1
proof
(* you must use the hypothesis 1 because no rule
can be applied to the thesis "p".
The new goal, thanks to the elimination of 1, is the trivial p ⟹ q ⟹ p
*)
show ?thesis by assumption
qed
I think the indication above on how to prove a thesis must be written in
the tutorial prog-prove or an another short tutorial on
the manner to write proofs in Isar.
Sincerely yours.
Email Gateway (Aug 22 2022 at 15:11):From: Makarius <makarius@sketis.net>
On 03/03/17 15:26, Michel via Cl-isabelle-users wrote:
Thank you really much for your examples. I try to write basic proofs if
it possible without automation and with your suggestion it was possible.
I have written a software <http://teachinglogic.liglab.fr/DN/> (a long
time ago) to produce proof in natural deduction.This software was originally written in Prolog by Robert Stärk, who was
assistant at ETH Zürich. I try to see if the proofs given by this
software can be translated in Isar. That is the origin of my questions
on Isar.Lawrence Paulson has said : It’s essential to understand that “proof” by
itself will attempt to use the default proof method. But this default
proof method can lead to an unprovable goal.
The main Isar proof scheme is as follows:
from facts1 have goal
using facts2
proof method1
...
qed method2
The body "..." then consists recursively of sub-proofs, each with a
local context:
fix parameters
assume premises
show conclusion
<proof>
These usually address each sub-goal in turn, but the order is arbitrary.
The "next" command may be used to proceed with a fresh local context;
alternatively it is always possible to use { ... } to indicate context
block structure.
The initial refinement of "proof method1" uses facts = facts1 facts2
(appended in that order) and passes that to the proof method. It is
"standard" by default; "standard" is a bit more than just "rule", but
usually it is sufficient to think of "rule" as the standard step.
The terminal method2 has a chance to finish-off remaining sub-goals (it
may be omitted). Afterwards there is always an implicit stage to finish
everything implicitly by-assumption.
Some important abbreviations:
proof method1 qed method2 == by method1 method2
.. == by standard
. == by this
Proof method "standard" applies a standard rule: the facts are put into
its premises (in that order), the remaining rule is applied to the goal.
Proof method "this" applies all "used" facts directly, without putting a
rule in between.
To apply these Isar principles in practice, I recommend to take all the
Natural Deduction rules for predicate logic as examples, and turn them
into canonical Isar proof outlines, e.g. like this for conjunction:
have "A ∧ B"
proof
show A sorry
show B sorry
qed
next
assume *: "A ∧ B"
then have A ..
from * have B ..
The double projection is a bit awkward. Better eliminate conjunction
simultaneously:
assume "A ∧ B"
then obtain A B ..
Etc. ... Here is
http://teachinglogic.liglab.fr/DN/index.php?formula=p+%26+q+%3D%3E+q+%26+p&action=Prove+Formula
in Isar:
have "A ∧ B ⟶ B ∧ A"
proof
assume "A ∧ B"
then obtain B A ..
then show "B ∧ A" ..
qed
You can enclose the above snippets into "notepad begin ... end", to
avoid having toplevel theorem statements (which have separate syntax).
I also recommend to start Isar without ever writing Pure rule statements
in the text: these somehow belong to the "implementation" of logic and
are rarely needed in proof texts.
I think the indication above on how to prove a thesis must be written in
the tutorial prog-prove or an another short tutorial on
the manner to write proofs in Isar.
After more than 30 years, the situation of Isabelle manuals is very
complex. Everything can be found somewhere, but it might take time to
find it. Moreover, some old materials needs to be ignored, especially
when getting started.
Makarius
Email Gateway (Aug 22 2022 at 15:11):From: Makarius <makarius@sketis.net>
Here is more exercise material based on the above website. It uses
Isabelle/Pure directly, without the huge Isabelle/HOL library. Thus it
is really confined to single-step structure proofs in Isar. Moreover,
classical logic is not assumed globally, but confined to a separate
locale context (in contrast, most Isabelle/HOL tools use classical logic
implicitly).
As Peter has already pointed out before, these proofs are a bit atypical
for practical Isar: there is a fine art to write rule statements in open
form, without too many auxiliary logical connectives getting in between.
This is occasionally called "logic-free reasoning".
Makarius
Pure_Logic.thy
Ex.thy
Last updated: Apr 19 2024 at 01:05 UTC