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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
