# Re: [ProofPower] ProofPower and Discrete Math

```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 <r...@rbjones.com> 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 <dtop...@ohlone.edu> 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 <r...@lemma-one.com> 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 <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  (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>
>>> 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  or (510) 659-7333
>>>> <%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
```