Examples (9)

 sos.mlには,次の定理が含まれています.

# search[name"SOS"];;
val it : (string * thm) list =
[("INT_SOS_EQ_0", |- !x y. x pow 2 + y pow 2 = &0 <=> x = &0 /\ y = &0);
("REAL_SOS_EQ_0", |- !x y. x pow 2 + y pow 2 = &0 <=> x = &0 /\ y = &0)]

 今回はこの個数に対する一般化

# g`!x:num->real n:num. sum (0..n) (\k. x k pow 2) = &0 <=> (!k. k <= n ==> x k = &0)`;;
val it : goalstack = 1 subgoal (1 total)

`!x n. sum (0..n) (\k. x k pow 2) = &0 <=> (!k. k <= n ==> x k = &0)`

の証明です.方針は,==>の基礎は非負数列の和が0なら各項も0という性質ですが,既に

# SUM_POS_EQ_0_NUMSEG;;
val it : thm =
|- !f m n.
(!p. m <= p /\ p <= n ==> &0 <= f p) /\ sum (m..n) f = &0
==> (!p. m <= p /\ p <= n ==> f p = &0)

があるので,f,mを(\k. (x k) pow k),0とSPECLしてもよいのですが

# [LE_0;REAL_LE_POW_2;POW_ZERO];;
val it : thm list =
[|- !n. 0 <= n; |- !x. &0 <= x pow 2; |- !n x. x pow n = &0 ==> x = &0]

も併せて参照すれば,MESON_TACで大丈夫です.

# e (REPEAT GEN_TAC THEN EQ_TAC) ;;
val it : goalstack = 2 subgoals (2 total)

`(!k. k <= n ==> x k = &0) ==> sum (0..n) (\k. x k pow 2) = &0`

`sum (0..n) (\k. x k pow 2) = &0 ==> (!k. k <= n ==> x k = &0)`

# e (MESON_TAC[SUM_POS_EQ_0_NUMSEG;LE_0;REAL_LE_POW_2;POW_ZERO;]);;
0..0..1..3..9..22..53..117..236..452..845..1508..2643..4570..solved at 7094
val it : goalstack = 1 subgoal (1 total)

`(!k. k <= n ==> x k = &0) ==> sum (0..n) (\k. x k pow 2) = &0`

 逆は任意有限個の0の和が0ということで,これにも

# [SUM_EQ_0_NUMSEG; POW_0; TWO;];;
val it : thm list =
[|- !f s. (!i. m <= i /\ i <= n ==> f i = &0) ==> sum (m..n) f = &0;
|- !n. &0 pow SUC n = &0; |- 2 = SUC 1]

があるので

# e(MESON_TAC[SUM_EQ_0_NUMSEG; POW_0; TWO;]);;
0..0..1..5..12..24..56..106..189..302..524..821..1556..2505..5036..solved at 760
6
val it : goalstack = No subgoals

# top_thm();;
val it : thm =
|- !x n. sum (0..n) (\k. x k pow 2) = &0 <=> (!k. k <= n ==> x k = &0)

まとめると

# prove(`!x:num->real n:num. sum (0..n) (\k. x k pow 2) = &0 <=> (!k. k <= n ==> x k = &0)`,
MESON_TAC[SUM_POS_EQ_0_NUMSEG;LE_0;REAL_LE_POW_2;POW_ZERO; SUM_EQ_0_NUMSEG;POW_0; TWO;]);;
0..0..1..3..9..23..61..143..304..623..1234..2300..4161..7441..solved at 11648
0..0..1..6..16..36..91..217..473..916..1823..3442..6654..11981..22581..solved at
32404
val it : thm =
|- !x n. sum (0..n) (\k. x k pow 2) = &0 <=> (!k. k <= n ==> x k = &0)

となります.