2011-11-16

　今回は
　 ${\forall}n.\sum_{k=0}^{n}2k=n(n+1)$
の帰納法による証明です．まず，左辺の和を

# NSUM_CLAUSES_NUMSEG;;
val it : thm =
|- (!m. nsum (m..0) f = (if m = 0 then f 0 else 0)) /\
(!m n. nsum (m..SUC n) f =
(if m <= SUC n then nsum (m..n) f + f (SUC n) else nsum (m..n) f))

という性質を持つnsumで表すと，goalは

# g(`!n. nsum(0..n)(\k.2*k)=n*(n+1)`);;
val it : goalstack = 1 subgoal (1 total)
`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)`

となります．
　NSUM_CLAUSES_NUMSEGにある if p then q else r は，条件による分岐ですが，q，rのhol.typeは数に限らず，:boolでも構いません．

# let f x y =(if x>0 then y else not y );;
val f : int -> bool -> bool =
# f 1 (1=1);;
val it : bool = true
# f 0 (1=1);;
val it : bool = false
# f 0 (1=0);;
val it : bool = true
# f 1 (1=0);;
val it : bool = false

　帰納法は，全称量化の本体をPとして

# num_INDUCTION;;
val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)

を thm_tac MATCH_MP_TAC に渡すことで開始されます．

# e( (MATCH_MP_TAC num_INDUCTION)THEN(CONJ_TAC));;
val it : goalstack = 2 subgoals (2 total)
`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)
==> nsum (0..SUC n) (\k. 2 * k) = SUC n * (SUC n + 1)`
`nsum (0..0) (\k. 2 * k) = 0 * (0 + 1)`

　CONJ_TACで分離した下のsubgoalは，SIMP_TACまたはREWRITE_TACに先のtheorem NSUM_CLAUSES_NUMSEGを参照させれば

# e(REWRITE_TAC[NSUM_CLAUSES_NUMSEG]);;
val it : goalstack = 1 subgoal (2 total)
`2 * 0 = 0 * (0 + 1)`

となりますので

# e(ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)
`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)
==> nsum (0..SUC n) (\k. 2 * k) = SUC n * (SUC n + 1)`

で，次のsubgoalに移ります．しかし，これも

# e(REWRITE_TAC[NSUM_CLAUSES_NUMSEG]);;
val it : goalstack = 1 subgoal (1 total)
`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)
==> (if 0 <= SUC n
then nsum (0..n) (\k. 2 * k) + 2 * SUC n
else nsum (0..n) (\k. 2 * k)) =
SUC n * (SUC n + 1)`
# e(ARITH_TAC);;
val it : goalstack = No subgoals

とできるので，e で並行して適用するなら

# prove(
`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)`,
(MATCH_MP_TAC num_INDUCTION) THEN
(CONJ_TAC) THEN
(REWRITE_TAC[NSUM_CLAUSES_NUMSEG]) THEN
(ARITH_TAC) );;
val it : thm = |- !n. nsum (0..n) (\k. 2 * k) = n * (n + 1)

となります．なお

(MATCH_MP_TAC num_INDUCTION)THEN(CONJ_TAC)

ではなく，INDUCT_TACを用いると

`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)`
# e(INDUCT_TAC);;
val it : goalstack = 2 subgoals (2 total)
0 [`nsum (0..n) (\k. 2 * k) = n * (n + 1)`]
`nsum (0..SUC n) (\k. 2 * k) = SUC n * (SUC n + 1)`
`nsum (0..0) (\k. 2 * k) = 0 * (0 + 1)`

のように，nステップ目からSUC nステップ目を導くsubgoalと0ステップ目のsubgoalとに分離されるので

# prove(
`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)`,
(INDUCT_TAC) THEN
(ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]) THEN
(ARITH_TAC) );;
val it : thm = |- !n. nsum (0..n) (\k. 2 * k) = n * (n + 1)

ともできます．ここでASM_REWRITE_TACは，REWRITE_TACの拡張なので，実際には仮定によらない0ステップに対しても同じtacticで上手くいくことに注意しましょう．勿論，THENL [ tac1 ; tac2 ] を用いて，下から順でsubgoal1，subgoal2に適用するtacticを個別に指定することもでき

# prove(
`!n. nsum (0..n) (\k. 2 * k) = n * (n + 1)`,
(INDUCT_TAC) THENL
[(REWRITE_TAC[NSUM_CLAUSES_NUMSEG]);
(ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG])]
THEN (ARITH_TAC) );;
val it : thm = |- !n. nsum (0..n) (\k. 2 * k) = n * (n + 1)

となり，より複雑な証明にはこうした個別の処理の指定が不可欠になります．
　類題です．

# prove(
`!n. nsum (0..SUC n) (\k. 66*k EXP 10) = (2*n+3)*(n+2)*(n+1)*(n EXP 2+3*n+1)*
(3*n EXP 6+27*n EXP 5+92*n EXP 4+147*n EXP 3+117*n EXP 2+54*n+11)`,
(INDUCT_TAC) THEN
(ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]) THEN
(ARITH_TAC) );;
val it : thm =
|- !n. nsum (0..SUC n) (\k. 66 * k EXP 10) =
(2 * n + 3) *
(n + 2) *
(n + 1) *
(n EXP 2 + 3 * n + 1) *
(3 * n EXP 6 +
27 * n EXP 5 +
92 * n EXP 4 +
147 * n EXP 3 +
117 * n EXP 2 +
54 * n +
11)
# prove(
`!n. nsum (0..n) (\k. 10*k EXP 9+45*k EXP 8+120*k EXP 7+210*k EXP 6+252*k E
XP 5+210*k EXP 4+120*k EXP 3+45*k EXP 2+10*k+1 ) = (SUC n) EXP 10`,
(INDUCT_TAC) THEN
(ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]) THEN
(ARITH_TAC) );;
val it : thm =
|- !n. nsum (0..n)
(\k. 10 * k EXP 9 +
45 * k EXP 8 +
120 * k EXP 7 +
210 * k EXP 6 +
252 * k EXP 5 +
210 * k EXP 4 +
120 * k EXP 3 +
45 * k EXP 2 +
10 * k +
1) =
SUC n EXP 10

　
　この８章までで，HOL Lightの概要は一通りお話したことになります．しかし，木に例えるなら，幹と主な枝，その各枝に葉が２，３枚といった状況ですから，次章からは，色々と拡充して行きたいと思います．

ATPとCASのこと

8.2 Inductive proofs about summations