Roger, Thank you so much! I had not come across rewrite_rule in my reading. It works exactly as I need. -Dave
On Tue, Feb 7, 2017 at 5:01 AM, Roger Bishop Jones <[email protected]> wrote: > David, > > Of course, how to make a rule depends on what rule you are trying to make. > > ¬_∨_thm is an equivalence, i.e. a boolean equation, and the most common > way of using equations is by rewriting. > If you are doing forward proof then you can rewrite using rewrite_rule, so > to use this theorem you might rewrite with it as follows: > > val new_thm = rewrite_rule [¬_∨_thm] old_thm; > > The effect would be to push in negation over any disjunctions to which it > is applied in the old_thm and return the resulting theorem, > > If you wanted a special rule to achieve that effect then: > > val ¬_∨_rule = rewrite_rule [¬_∨_thm]; > > which you would use thus: > > val new_thm = ¬_∨_rule old_thm; > > Roger > > On 07/02/2017 05:29, David Topham wrote: > > I have made some more progress in applying ProofPower to forward proofs in > discrete math. e.g. I can prove DeMorgan's theorem successful > (propositional calculus). I would like to use the newly proved theorem in > other proofs now. What is the best strategy to do that? Is it to create > an SML function that takes an argument of type TERM and returns a THM? > Could you give an example of a proved THM intended to be used as a new rule > of inference? > > I also discovered the not_or_thm in the zed theory, which is DeMorgan's > Law, but that does not seem to be a function, so I am not sure how to apply > it in a forward proof. > > I appreciate any pointers in the right direction (or reference to which > manual might enlighten me). Thanks, Dave > > On Wed, Aug 17, 2016 at 11:06 AM, David Topham <[email protected]> wrote: > >> Thank you both (Rob and Roger) for your "above and beyond the call of >> duty" help in getting me through my attempts to approach using ProofPower >> to teach Discrete Math. I understand your comments that backward proof is >> more economical than forward proof. Yet, I don't think the students will >> learn how to formulate proof thinking skills if ProofPower does it for >> them! True, that learning how to use the mechanized assistance is >> practical, but we (students) need to understand what constitutes valid >> reasoning so have to see the tedious steps one-at-a-time. (e.g. I tried "a >> (prove_tac[]);" and it works perfectly, but does not show me all the steps >> that were used (is there a way for it to do that?)) >> >> I believe the majority of courses teaching DM don't even try to go beyond >> the paper and pencil proofs--maybe that is good enough, but I can't help >> but think that exposure to professional tools (i.e. ProofPower) that force >> us to think carefully about what we are doing and to have the computer not >> allow us to proceed on shaky grounds is beneficial. >> >> Even though ProofPower is designed for math pros and is difficult to >> approach as beginning math novices, it is very well designed in its >> interface and ease of use. I am drawn to it by integration of "literate" >> approaches to documentation, ability to enter math notation, support for >> SML, and Z too (which is my next goal once basic Prop/Pred Calc is under >> our belts). Overall we should be able to derive correct programs and/or >> prove algorithms. >> >> My idea is that application of proofs to software design is the main goal >> of a Discrete Math course (recently changed to Discrete Structures by the >> powers that be). I do recognize the value of your time, and will resist >> asking each time I get stuck unless I am unable to continue. >> -Dave >> >> >> On Wed, Aug 17, 2016 at 3:02 AM, Rob Arthan <[email protected]> wrote: >> >>> 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 <[email protected]> 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 (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 <[email protected]> >>> 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 [email protected] or (510) 659-7333 >>>> <%28510%29%20659-7333>. >>>> >>>> >>> _______________________________________________ >>> Proofpower mailing list >>> [email protected] >>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >>> >>> >>> >> > >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
