Re: [isabelle] isar in PIDE : strange behavior



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   Â


--
 Peter


On Do, 2017-03-02 at 18:21 +0100, Michel via Cl-isabelle-users wrote:
> 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
> 
> 
> Le 02/03/2017 Ã 16:41, Lawrence Paulson a Ãcrit :
> > 
> > > 
> > > On 2 Mar 2017, at 15:03, Michel via Cl-isabelle-users <cl-isabell
> > > e-users at lists.cam.ac.uk> wrote:
> > > 
> > > As a beginner, I tried another elementary proof with jedit.
> > > 
> > > But during the proof, I have strange messages in the output
> > > window and 4 proof and only 3 qed.
> > > 
> > > lemma trivial3isar : "(p â (q â r)) â (q â (p â r))"
> > > Â proof
> > > ÂÂÂÂassume "p â (q â r)"
> > > ÂÂÂÂshow "q â (p â r)"
> > > ÂÂÂÂproof
> > > ÂÂÂÂÂÂassume "q"
> > > ÂÂÂÂÂÂshow "p â r"
> > > ÂÂÂÂÂÂproof
> > > ÂÂÂÂÂÂÂÂassumeÂÂ"p"
> > > ÂÂÂÂÂÂÂÂshow "r"
> > > ÂÂÂÂÂÂÂÂproof
> > Itâs essential to understand that âproofâ by itself will attempt to
> > use the default proof method, but there is none for the formula r.
> > 
> > At this stage, you have two alternatives. One is to continue in
> > this single-step style by feeding in one of your previous
> > assumptions; the other is finally to use a little automation. So
> > possibly this (note the introduced label):
> > 
> > Â lemma trivial3isar : "(p â (q â r)) â (q â (p â r))"
> > Â proof
> > ÂÂÂÂassume 1: "p â (q â r)"
> > ÂÂÂÂshow "q â (p â r)"
> > ÂÂÂÂproof
> > ÂÂÂÂÂÂassume "q"
> > ÂÂÂÂÂÂshow "p â r"
> > ÂÂÂÂÂÂproof
> > ÂÂÂÂÂÂÂÂassumeÂÂ"p"
> > ÂÂÂÂÂÂÂÂshow "r"
> > ÂÂÂÂÂÂÂÂÂÂusing 1
> > ÂÂÂÂÂÂÂÂproof
> > 
> > Alternatively, this:
> > 
> > ÂÂÂÂÂÂÂÂshow "r"
> > ÂÂÂÂÂÂÂÂÂÂby (simp add: "1" âpâ âqâ)
> > 
> > Larry Paulson
> > 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.