Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

David,

On 28/10/2019 02:39, David Topham wrote:
Hello Rob,Roger, et al. Hope you are doing well. I am still trying to 
apply ProofPower to forward proofs.

Glad to hear that.

I am working on proof by induction and came across this:

induction_thm

In the notes, there is an intriguing statement that we could use 
"forall_elim" to do forward proofs using the thm, but no specific example.


e.g. I would like to show the sum of the integers from 1...n = n(n+1)/2

but not sure how to notate the "infinite sequence" or to
remove the implied "forall" using
rewrite_rule (or prove_rule)

Do you have a sample of that technique somewhere?

There are not so many examples in general of forward proof methods, 
because in practice it is usually easier and faster to use the goal 
package to obtain proofs, even though an understanding of forward proof 
is pretty essential and bits of forward proof are often handy within a 
larger goal-oriented proof or when programming new proof automation.


So I'm not able to point you to an example of forward induction.

However, I can give you some clues about how to go about it.

There are examples of backwards inductive proofs in the HOL Tutorial 
Notes, which it would be worthwhile you looking at first.
You could look at those proofs and ask "how would I do this as a forward 
proof?"
They have the advantage that they are about concepts which are already 
defined in the theory of list, particularly concatenation of lists.


Typically inductive proofs involve inductively defined concepts or 
functions.
The one you want to prove is about natural numbers (which are 
inductively defined) and the function "sum of the numbers up to n" (you 
don't need to do anything with /infinite/ sequences) which needs to be 
defined inductively, but has not been defined in the theory of natural 
numbers.
So to address that inductive proof, you must first master inductive 
definitions, and define the sum of a finite sequence.
There are examples of inductive definitions, for example plus_def and 
times_def, in the HOL theories.
Then you need to identify the property of natural numbers which you are 
trying to show, by induction, is true of all natural numbers.
This is the thing with which you must instantiate induction_thm using 
forall_elim.


Do you think you could define the summation op you need to get to a 
formal statement of the theorem you wish to prove, and then use this in 
formally stating the property you want to prove of all numbers?


Roger

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

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

> David,

Good to hear you are still moving forward.

If the transformation you seek is a propositional tautology, the following 
general prescription should work.

1. Formulate the transformation as an equivalence using propositional (Boolean) 
variables, with the starting point on the left of the equivalence and the 
desired form on the right, and universally quantify the equivalence over all 
the Boolean variables.

2. Prove this sentence using “prove_rule[]”.

3. Use rewrite_rule with the resulting theorem to effect the transformation in 
a forward proof.

I’m not in a position to check any specific examples at the moment, but if you 
have any difficulties I will be better placed later in the week.

Roger Jones

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

Re: [ProofPower] ProofPower and Discrete Math

[David Topham]

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  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  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  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 *)
>

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

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 > 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 mailto: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;
  

Re: [ProofPower] ProofPower and Discrete Math

[David Topham]

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  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  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  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)
>> 

Re: [ProofPower] ProofPower and Discrete Math

[David Topham]

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  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  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 
> wrote:
>
>>
>> On 14/08/2016 08:44, David Topham wrote:
>>
>>> Thanks Roger, I am using slides he distributes.  He  has false
>>> introduction ru

Re: [ProofPower] ProofPower and Discrete Math

[Rob Arthan]

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  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  > 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 .
> 
> 
> ___
> 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

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

David,

There is a reason why the ProofPower tutorials don't say much about the 
forward proof tools you are trying to use.
I have given courses on ProofPower HOL and on ProofPower Z and wrote the 
tutorials.
What I did in the courses was to teach just enough about forward proof 
for the students to understand the basics of how proof in ProofPower 
works, before teaching them how to use the goal package to accomplish 
proofs.
Goal oriented proof is much easier in virtually all applications (though 
it does often involve small fragments of forward proof).
Compared with using the goal package, contruction of forward proofs is 
like pulling teeth.


The example given by Woodcock on page 42 can be proven using the goal 
package by the following script:


set_goal([], %<%(%exists%x:'a%spot% %exists%y:'b%spot% P(x,y)) ´ 
(%exists%y:'b%spot% %exists%x:'a%spot% P(x,y))%>%);

a (REPEAT strip_tac);
a (%exists%_tac %<%y%>% THEN %exists%_tac %<%x%>% THEN strip_tac);

or just (not quite so easy to understand):

a (contr_tac THEN asm_fc_tac[]);

or even:

a (prove_tac[]);

(in a reasonable proof context such as "hol")

You might consider pointing your students to the Woodcock forward proof 
and then showing them a ProofPower goal oriented proof, then they will 
be learning a more intelligible and economic method of proof.


I could look closely at how to do this by forward proof and debug your 
attempts, but I have never myself had occasion to do this kind of 
forward proof, its not a necessary skill.
Of course, the forward proof facilities are used, but in rather 
different ways, by the people who programmed the goal package, and by 
people writing higher level proof facilities such as tactics, tacticals 
etc., but for applications, the goal package makes things simpler both 
to understand and to execute.


By way of further comment on why your proofs are not working, the term 
required as a parameter to exists elim is one which matches just the 
variable over which the existential quantifies, and so not a predicate.
It will only work one quantifier at a time (and %exists% x y %spot% is 
two nested quantifiers), so you would have to do the proof in two stages 
one for each of the quantified variables, unless you put them together 
in the theorem as in %exists% (x,y) %spot%, which of course, is not 
quite the same theorem.

So it really is a lot more complicated to do this by forward proof.

Roger


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

Re: [ProofPower] ProofPower and Discrete Math

[David Topham]

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  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.
>
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

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

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

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

David,

I don't quite understand what you are trying to do here.
On the face of it you want a rule:

p
-- false-intro
   false

But this is not possible, because it is not sound.

As far as I can see Woodcock does not have a false-intro rule,
he has only a false-elim rule, is that what you want to reproduce?
Woodcock, so far as I can see, introduces false by using ¬-elim.

Could you clarify what you are looking for?

Roger

On 14/08/2016 01:21, David Topham wrote:
Roger (or Rob), I have been studying "UsingZ" by Jim Woodcock and JIm 
Davies. They use the "sequent" method and show a proof that derives 
"false".  In looking through the inference rules in USR029 I don't see 
a rule that matches "false-intro".  Can you suggest how to approach 
this type of proof  (it is for my Discrete Match course).  -Dave

i.e. What rule would I replace  ??? with for L6

​



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

Re: [ProofPower] ProofPower and Discrete Math

[David Topham]

My first successful results of the mapping from Discrete Math rules of
inference to ProofPower are attached in case they are useful to anyone else
working on a similar project.

a mapping from discrete math "rules of inference" to ProofPower
<https://www.dropbox.com/s/mtdejdpgzziz6g5/mapping_rules_of_inference.pdf?dl=0>


On Sat, Feb 28, 2015 at 11:47 PM, David Topham  wrote:

> The first successful results of the mapping from Discrete Math rules of
> inference to ProofPower are attached in case they are useful to anyone else
> working on a similar project.
>
> On Thu, Feb 5, 2015 at 9:00 AM,  wrote:
>
>> Send Proofpower mailing list submissions to
>> proofpower@lemma-one.com
>>
>> To subscribe or unsubscribe via the World Wide Web, visit
>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>> or, via email, send a message with subject or body 'help' to
>> proofpower-requ...@lemma-one.com
>>
>> You can reach the person managing the list at
>> proofpower-ow...@lemma-one.com
>>
>> When replying, please edit your Subject line so it is more specific
>> than "Re: Contents of Proofpower digest..."
>>
>>
>> Today's Topics:
>>
>>1. Re: ProofPower and Discrete Math (David Topham)
>>2. Re: ProofPower and Discrete Math (Rob Arthan)
>>
>>
>> --------------
>>
>> Message: 1
>> Date: Wed, 4 Feb 2015 12:49:47 -0800
>> From: David Topham 
>> To: Roger Bishop Jones 
>> Cc: ProofPower List 
>> Subject: Re: [ProofPower] ProofPower and Discrete Math
>> Message-ID:
>> <
>> cad034bgcumtxj3nkvjjpcxdspsd5s_7ipw+tli0mfu6htwo...@mail.gmail.com>
>> Content-Type: text/plain; charset="utf-8"
>>
>> Roger, Thank you very much! This example got me past my mental block and I
>> see how to work with these proofs much better now. I appreciate your time
>> in helping me. Now I see one of my tasks is to map the names I use (such
>> as
>> hypothetical syllogism) to the names used within ProofPower (such as
>> =>_trans_rule). I will work on that mapping...  -Dave
>>
>> On Tue, Feb 3, 2015 at 7:29 AM, Roger Bishop Jones <
>> postmas...@rbjones.com>
>> wrote:
>>
>> > On 03/02/15 13:55, David Topham wrote:
>> > >
>> > >
>> > > I am interested in using ProofPower to aid in the teaching of Discrete
>> > > Math. I would like to assist the students in developing proofs using
>> > > specific rules of inference. e.g. in the attached proof from our
>> > > textbook the proof uses Hypothetical Syllogism to prove a
>> > > Propositional expression. I don't quite see yet from the tutorials how
>> > > to direct ProofPower in this way. Is it possible? Does anyone have
>> > > experience using ProofPower like this? If so, I would appreciate some
>> > > guidance. It seems so far in my observations, that pp is used by
>> > > selecting some "tactics" which then guide pp to find  a proof, but we
>> > > would need to direct each step as part of the learning process.
>> > > Thanks, Dave
>> > >
>> > The proof you exhibit is what we would call a "forward proof".
>> > The subgoal package is used for what we call "backward" (or goal
>> > oriented) proofs.
>> >
>> > A forward proof for the result you require runs like this:
>> >
>> > val L1 = asm_rule ?P ? Q?;
>> > val L2 = asm_rule ?Q ? R?;
>> > val L3 = ?_trans_rule L1 L2;
>> > val L4 = asm_rule ?R ? P?;
>> > val L5 = ?_intro L3 L4;
>> >
>> > Except that the characters are a mess because I just copied
>> > and pasted from the xpp window which doesn't work.
>> >
>> > The value of L5 will be the desired result/
>> >
>> > I attach a proofpower document  containing the proof.
>> >
>> > The documentation for the inference rules is in the reference manual
>> > USR029 section 8.1.
>> >
>> > The HOL Tutorial Notes USR013 has perhaps more accessible descriptions
>> of
>> > a selection of rules in Chapter 5.
>> >
>> > Roger Jones
>> >
>> >
>> >
>> >
>> >
>> -- next part --
>> An HTML attachment was scrubbed...
>> URL: <
>> http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20150204/341a13e6/attachmen

Re: [ProofPower] ProofPower and Discrete Math

[Rob Arthan]

On 3 Feb 2015, at 21:16, Roger Bishop Jones  wrote:

> On 03/02/15 13:55, David Topham wrote:
>> 
>> 
>> I am interested in using ProofPower to aid in the teaching of Discrete
>> Math. I would like to assist the students in developing proofs using
>> specific rules of inference. e.g. in the attached proof from our
>> textbook the proof uses Hypothetical Syllogism to prove a
>> Propositional expression. I don't quite see yet from the tutorials how
>> to direct ProofPower in this way. Is it possible? Does anyone have
>> experience using ProofPower like this? If so, I would appreciate some
>> guidance. It seems so far in my observations, that pp is used by
>> selecting some "tactics" which then guide pp to find  a proof, but we
>> would need to direct each step as part of the learning process.
>> Thanks, Dave
>> 
> The proof you exhibit is what we would call a "forward proof".
> The subgoal package is used for what we call "backward" (or goal
> oriented) proofs.
> 
> A forward proof for the result you require runs like this:
> 
> val L1 = asm_rule ¬P ´ Q®;
> val L2 = asm_rule ¬Q ´ R®;
> val L3 = ´_trans_rule L1 L2;
> val L4 = asm_rule ¬R ´ P®;
> val L5 = ¤_intro L3 L4;
> 
> Except that the characters are a mess because I just copied
> and pasted from the xpp window which doesn't work.
> 

For the record, here it is in Unicode:

val L1 = asm_rule ⌜P ⇒ Q⌝;
val L2 = asm_rule ⌜Q ⇒ R⌝;
val L3 = ⇒_trans_rule L1 L2;
val L4 = asm_rule ⌜R ⇒ P⌝;
val L5 = ⇔_intro L3 L4;

> The value of L5 will be the desired result/
> 
> I attach a proofpower document  containing the proof.
> 
> The documentation for the inference rules is in the reference manual
> USR029 section 8.1.
> 
Another way of finding all the forward inference rules provided is
to browse the entries for “rule”, “elim”,  “intro” and “conv"
in the keyword in context index.

> The HOL Tutorial Notes USR013 has perhaps more accessible descriptions of
> a selection of rules in Chapter 5.

Indeed.

Regards,

Rob.

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

Re: [ProofPower] ProofPower and Discrete Math

[David Topham]

Roger, Thank you very much! This example got me past my mental block and I
see how to work with these proofs much better now. I appreciate your time
in helping me. Now I see one of my tasks is to map the names I use (such as
hypothetical syllogism) to the names used within ProofPower (such as
=>_trans_rule). I will work on that mapping...  -Dave

On Tue, Feb 3, 2015 at 7:29 AM, Roger Bishop Jones 
wrote:

> On 03/02/15 13:55, David Topham wrote:
> >
> >
> > I am interested in using ProofPower to aid in the teaching of Discrete
> > Math. I would like to assist the students in developing proofs using
> > specific rules of inference. e.g. in the attached proof from our
> > textbook the proof uses Hypothetical Syllogism to prove a
> > Propositional expression. I don't quite see yet from the tutorials how
> > to direct ProofPower in this way. Is it possible? Does anyone have
> > experience using ProofPower like this? If so, I would appreciate some
> > guidance. It seems so far in my observations, that pp is used by
> > selecting some "tactics" which then guide pp to find  a proof, but we
> > would need to direct each step as part of the learning process.
> > Thanks, Dave
> >
> The proof you exhibit is what we would call a "forward proof".
> The subgoal package is used for what we call "backward" (or goal
> oriented) proofs.
>
> A forward proof for the result you require runs like this:
>
> val L1 = asm_rule ¬P ´ Q®;
> val L2 = asm_rule ¬Q ´ R®;
> val L3 = ´_trans_rule L1 L2;
> val L4 = asm_rule ¬R ´ P®;
> val L5 = ¤_intro L3 L4;
>
> Except that the characters are a mess because I just copied
> and pasted from the xpp window which doesn't work.
>
> The value of L5 will be the desired result/
>
> I attach a proofpower document  containing the proof.
>
> The documentation for the inference rules is in the reference manual
> USR029 section 8.1.
>
> The HOL Tutorial Notes USR013 has perhaps more accessible descriptions of
> a selection of rules in Chapter 5.
>
> Roger Jones
>
>
>
>
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower and Discrete Math

[Roger Bishop Jones]

On 03/02/15 13:55, David Topham wrote:
>
>
> I am interested in using ProofPower to aid in the teaching of Discrete
> Math. I would like to assist the students in developing proofs using
> specific rules of inference. e.g. in the attached proof from our
> textbook the proof uses Hypothetical Syllogism to prove a
> Propositional expression. I don't quite see yet from the tutorials how
> to direct ProofPower in this way. Is it possible? Does anyone have
> experience using ProofPower like this? If so, I would appreciate some
> guidance. It seems so far in my observations, that pp is used by
> selecting some "tactics" which then guide pp to find  a proof, but we
> would need to direct each step as part of the learning process.
> Thanks, Dave
>
The proof you exhibit is what we would call a "forward proof".
The subgoal package is used for what we call "backward" (or goal
oriented) proofs.

A forward proof for the result you require runs like this:

val L1 = asm_rule ¬P ´ Q®;
val L2 = asm_rule ¬Q ´ R®;
val L3 = ´_trans_rule L1 L2;
val L4 = asm_rule ¬R ´ P®;
val L5 = ¤_intro L3 L4;

Except that the characters are a mess because I just copied
and pasted from the xpp window which doesn't work.

The value of L5 will be the desired result/

I attach a proofpower document  containing the proof.

The documentation for the inference rules is in the reference manual
USR029 section 8.1.

The HOL Tutorial Notes USR013 has perhaps more accessible descriptions of
a selection of rules in Chapter 5.

Roger Jones



forwardproof.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[ProofPower] ProofPower and Discrete Math

[David Topham]

I am interested in using ProofPower to aid in the teaching of Discrete
Math. I would like to assist the students in developing proofs using
specific rules of inference. e.g. in the attached proof from our textbook
the proof uses Hypothetical Syllogism to prove a Propositional expression.
I don't quite see yet from the tutorials how to direct ProofPower in this
way. Is it possible? Does anyone have experience using ProofPower like
this? If so, I would appreciate some guidance. It seems so far in my
observations, that pp is used by selecting some "tactics" which then guide
pp to find  a proof, but we would need to direct each step as part of the
learning process. Thanks, Dave
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com