David,

I endorse what Roger said about forward v. backwards proof.
There is definitely a tension between teaching proof theory
and teaching practical mechanised proof.

For the record, the problem was that you had the two theorem
arguments of ∃_elim the wrong way round and you seemed
to have misunderstood the role of the term argument: it is
the variable that is free in the assumption of the second theorem
that is going to be discharged by the first theorem (the one
with the existential conclusion). Here is the complete proof
with the output you should see in the comments.

val L1 = asm_rule ⌜p(x,y):BOOL⌝;
(* val L1 = p (x, y) ⊢ p (x, y): THM *)
val L2 = ⌜∃x:'a⦁p(x,y)⌝;
(* val L2 = ⌜∃ x⦁ p (x, y)⌝: TERM *)
val L3 = ∃_intro L2 L1;
(* val L3 = p (x, y) ⊢ ∃ x⦁ p (x, y): THM *)
val L4 = ⌜∃y:'b⦁∃x:'a⦁p(x,y)⌝;
(* val L4 = ⌜∃ y x⦁ p (x, y)⌝: TERM *)
val L5 = ∃_intro L4 L3;
(* val L5 = p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L6 = asm_rule ⌜∃y:'b⦁p(x,y)⌝;
(* val L6 = ∃ y⦁ p (x, y) ⊢ ∃ y⦁ p (x, y): THM *)
val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
(* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L8 = asm_rule ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝;
(* val L8 = ∃ x y⦁ p (x, y) ⊢ ∃ x y⦁ p (x, y): THM *)
val L9 = ∃_elim ⌜x:'a⌝ L8 L7;
(* val L9 = ∃ x y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L10 = ⇒_intro ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝ L9;
(* val L10 = ⊢ (∃ x y⦁ p (x, y)) ⇒ (∃ y x⦁ p (x, y)): THM *)

The documentation and the error messages talk about varstructs
meaning either variables or  things formed from variables using pairing
(like ∃_elim will work on theorems with conclusions like ∃(x, y)⦁ p (x, y)).
You can just read “variable” for “varstruct” in simple examples.

Regards,

Rob.

> On 16 Aug 2016, at 21:24, David Topham <dtop...@ohlone.edu> wrote:
> 
> Since the slides for this book use slightly different notation, I am back to 
> trying to implement the proofs in the main book:  UsingZ from
> www.usingz.com <http://www.usingz.com/>  (in text link, it is zedbook)
> 
> On page 42, the proof is using nested existentials, and I am trying
> to get past my lack of understanding in applying E-elim
> (Roger already helped me with E-intro)
> 
> Here are two of my attempts (using ASCII since I can't attach pdf here)
> val L1 = asm_rule %<%p(x,y):BOOL%>%;
> val L2 = %<%%exists%x:'a%spot%p(x,y)%>%;
> val L3 = %exists%_intro L2 L1;
> val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p(x,y)%>%;
> val L5 = %exists%_intro L4 L3;
> val L6 = asm_rule %<%%exists%y:'b%spot%p(x,y)%>%;
> val L7 = %exists%_elim L4 L5 L6; 
> 
> val L1 = asm_rule %<%p:BOOL%>%;
> val L2 = %<%%exists%x:'a%spot%p%>%;
> val L3 = %exists%_intro L2 L1;
> val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p%>%;
> val L5 = %exists%_intro L4 L3;
> val L6 = asm_rule %<%%exists%y:'b%spot%p%>%;
> val L7 = %exists%_elim L4 L5 L6; 
> 
> The error I get is "does not match the bound varstruct" 
> 
> Does anyone have a suggestion to get me past this roadblock?
> 
> -Dave
> 
> On Sun, Aug 14, 2016 at 2:21 AM, Roger Bishop Jones <r...@rbjones.com 
> <mailto:r...@rbjones.com>> wrote:
> 
> On 14/08/2016 08:44, David Topham wrote:
> Thanks Roger, I am using slides he distributes.  He  has false introduction 
> rules starting on page 24 (attached).
> Sorry about my poor example, please ignore that since is a confused use of 
> this technique anyway!  -Dave
> 
> Looks like he changed the name.
> 
> In fact the original name (the one he uses in the book) is good in ProofPower.
> ¬_elim is available in ProofPower and does what you want (though it is 
> sligftly more general, it proves anything from a contradiction so you have to 
> tell it what result you are after).
> Details in reference manual.
> 
> Roger
> 
> 
> This message did not originate from Ohlone College  and must be viewed with 
> caution. Viruses and phishing attempts can be transmitted via email.
> E-mail transmission cannot be guaranteed to be secure or error-free as 
> information could be intercepted, corrupted, lost, destroyed, arrive late or 
> incomplete, or contain viruses.
> 
> If you have any concerns, please contact the Ohlone College IT Service Desk 
> at itserviced...@ohlone.edu <mailto:itserviced...@ohlone.edu>  or (510) 
> 659-7333 <tel:%28510%29%20659-7333>.
> 
> 
> _______________________________________________
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to