David,
On 29/10/2019 22:55, David Topham wrote:
Thanks Roger, I do have some pure SML code that checks the summation
to the explicit formula but not so sure how to express summation in
ProofPower. I did find this interesting reference
http://www.rbjones.com/rbjpub/pp/rda001.html
Which has things that seem useful for this such as
arithmetic_sum_thm
but those don't seem to work--so far I have only loaded xpp with -d hol
maybe I need some other database for those functions?
Some of those theorems are in the maths_egs contrib, which you download
separately,
but not the ones you are interested in.
However the definitions you want are quite simple, so easily entered.
Your SML is interesting, but what you want is simpler.
These are the triangular numbers, so lets call the function "tri",
and this suffices to define them in SML:
fun tri 0 = 0 | tri n = tri(n-1) + n;
In HOL you have to do this slightly differently (see HOL Tutorial Notes
section 4.3 for more examples of inductive definitions):
ⓈHOLCONST
│ tri : ℕ → ℕ
├──────────────────────
│ ∀n⦁ tri 0 = 0
│ ∧ tri (n+1) = (tri n)+n+1
■
Your conjecture is then:
⌜∀n⦁ tri n = n*(n+1) Div 2⌝;
To use induction_thm in proving this you need to get the property which
is asserted of all numbers, which is :
val tri_p = ⌜λn⦁ tri n = n*(n+1) Div 2⌝;
Which is used to instantiate induction_thm thus:
∀_elim tri_p induction_thm;
Giving:
val it =
⊢ (λ n⦁ tri n = n * (n + 1) Div 2) 0
∧ (∀ m
⦁ (λ n⦁ tri n = n * (n + 1) Div 2) m
⇒ (λ n⦁ tri n = n * (n + 1) Div 2) (m + 1))
⇒ (∀ n⦁ (λ n⦁ tri n = n * (n + 1) Div 2) n): THM
more easily digested if you do a few beta reductions:
val lemma1 = rewrite_rule [] it;
which gives:
val lemma1 =
⊢ tri 0 = 0
∧ (∀ m
⦁ tri m = m * (m + 1) Div 2
⇒ tri (m + 1) = (m + 1) * ((m + 1) + 1) Div 2)
⇒ (∀ n⦁ tri n = n * (n + 1) Div 2): THM
Now you see that your conjecture appears on the last line and can be
obtained by
Modus Ponens if you can prove the two conjuncts on the left of the
implication
(the base case and the step case).
Roger
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
