Examples (1)

　これまでの知識＋αを用いて，帰納法による証明を幾つか作って見ましょう．

■　:num 上の不等式についてのthm

　|- !n. 2 EXP n >= 1 + n

　ポイントは

# EXP;;
val it : thm = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP SUC n = m * m EXP n)

および，帰納法の仮定の利用の際に |- y>=1+n==>y>=1+n+1をARITH_RULEで導く点です．

g ( `!n. 2 EXP n >= 1 + n` );;
e ( INDUCT_TAC );;
e ( SIMP_TAC[EXP;ARITH] ) ;;
e ( SIMP_TAC[EXP;ARITH;ADD1] ) ;;
e ( ASM_SIMP_TAC[ARITH_RULE`x>=1+n==>2*x>=1+n+1`] ) ;;

実行すると

# g ( `!n. 2 EXP n >= 1 + n` );;
val it : goalstack = 1 subgoal (1 total)

`!n. 2 EXP n >= 1 + n`

# e ( INDUCT_TAC );;
val it : goalstack = 2 subgoals (2 total)

0 [`2 EXP n >= 1 + n`]

`2 EXP SUC n >= 1 + SUC n`

`2 EXP 0 >= 1 + 0`

# e ( SIMP_TAC[EXP;ARITH] ) ;;
val it : goalstack = 1 subgoal (1 total)

0 [`2 EXP n >= 1 + n`]

`2 EXP SUC n >= 1 + SUC n`

# e ( SIMP_TAC[EXP;ARITH;ADD1] ) ;;
val it : goalstack = 1 subgoal (1 total)

0 [`2 EXP n >= 1 + n`]

`2 * 2 EXP n >= 1 + n + 1`

# e ( ASM_SIMP_TAC[ARITH_RULE`x>=1+n==>2*x>=1+n+1`] ) ;;
val it : goalstack = No subgoals

　まとめて実行すると，inductionの2つのsubgoalsに並行してtacticが作用します．

# prove ( `!n. 2 EXP n >= 1 + n` ,
INDUCT_TAC THEN SIMP_TAC[EXP;ARITH;ADD1] THEN
ASM_SIMP_TAC[ARITH_RULE`x>=1+n==>2*x>=1+n+1`] );;
val it : thm = |- !n. 2 EXP n >= 1 + n

　また，ADD1をARITH_RULEに任せて

# prove ( `!n. 2 EXP n >= 1 + n` ,
INDUCT_TAC THEN
ASM_SIMP_TAC[EXP;ARITH;ARITH_RULE`x>=1+n==>2*x>=1+SUC n`] );;
val it : thm = |- !n. 2 EXP n >= 1 + n

とまとめることも出来ます．

■　:real 上の不等式についてのthm（Bernoulli）

　|- !x. &0 <= x ==> (!n. &1 + &n * x <= (&1 + x) pow n)

　非線形不等式なのでREAL_SOSを用いるのがよいでしょう．ただし，:num の元 n の :real への包含写像 & による像 &n が &0 以上であること，つまり

# REAL_POS;;
val it : thm = |- !n. &0 <= &n

を明示しないと，REAL_SOSには通じません．
　powについては

# real_pow;;
val it : thm = |- x pow 0 = &1 /\ (!n. x pow SUC n = x * x pow n)

& の和への分配については

# GSYM REAL_ADD;;
val it : thm = |- !m n. &(m + n) = &m + &n

を用います．

g `!x. &0 <= x ==> !n. &1 + &n * x <= (&1 + x) pow n` ;;
e( STRIP_TAC THEN STRIP_TAC );;
e( INDUCT_TAC );;
e( REAL_ARITH_TAC );;
e( MP_TAC (SPEC `n:num` REAL_POS) THEN SIMP_TAC [ADD1; pow; GSYM REAL_ADD] );;
e( ASM_REAL_SOS_TAC );;

実行すると

# g `!x. &0 <= x ==> !n. &1 + &n * x <= (&1 + x) pow n` ;;
val it : goalstack = 1 subgoal (1 total)

`!x. &0 <= x ==> (!n. &1 + &n * x <= (&1 + x) pow n)`

# e( STRIP_TAC THEN STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

0 [`&0 <= x`]

`!n. &1 + &n * x <= (&1 + x) pow n`

# e( INDUCT_TAC );;
val it : goalstack = 2 subgoals (2 total)

0 [`&0 <= x`]
1 [`&1 + &n * x <= (&1 + x) pow n`]

`&1 + &(SUC n) * x <= (&1 + x) pow SUC n`

0 [`&0 <= x`]

`&1 + &0 * x <= (&1 + x) pow 0`

# e( REAL_ARITH_TAC );;
val it : goalstack = 1 subgoal (1 total)

0 [`&0 <= x`]
1 [`&1 + &n * x <= (&1 + x) pow n`]

`&1 + &(SUC n) * x <= (&1 + x) pow SUC n`

# e( MP_TAC (SPEC `n:num` REAL_POS) THEN SIMP_TAC [ADD1; pow; GSYM REAL_ADD]

val it : goalstack = 1 subgoal (1 total)

0 [`&0 <= x`]
1 [`&1 + &n * x <= (&1 + x) pow n`]

`&0 <= &n ==> &1 + (&n + &1) * x <= (&1 + x) * (&1 + x) pow n`

# e( ASM_REAL_SOS_TAC );;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
val it : goalstack = No subgoals

まとめると

# prove
(`!x. &0 <= x ==> !n. &1 + &n * x <= (&1 + x) pow n`,
STRIP_TAC THEN STRIP_TAC THEN
INDUCT_TAC THEN
MP_TAC (SPEC `n:num` REAL_POS) THEN SIMP_TAC [ADD1; pow; GSYM REAL_ADD] THEN

ASM_REAL_SOS_TAC);;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
val it : thm = |- !x. &0 <= x ==> (!n. &1 + &n * x <= (&1 + x) pow n)

となります．

■　簡単な差分方程式の解
　:num 上でのcutoffに注意します．また，ARITH_RULEでは扱えない2 EXP nを文字においてthmを作り参照する点も重要です．

g (`!x. x 0 = 0 /\ (!n. x (n + 1) = 2 * x n + 1) ==> (!n. x n = 2 EXP n - 1)` );;
e ( STRIP_TAC THEN STRIP_TAC );;
e ( INDUCT_TAC );;
e ( ASM_SIMP_TAC[EXP;ARITH] ) ;;
e ( SIMP_TAC[EXP;ARITH;ADD1] ) ;;
e ( FIRST_X_ASSUM( ASSUME_TAC o SPECL[`n:num`] ) );;
e ( ASSUME_TAC (MESON[EXP_LT_0;EXP;ARITH]`0<2 EXP n`) );;
e ( ASM_SIMP_TAC[ARITH_RULE`02*(x-1)+1=2*x-1`] );;

実行すると

# g( `!x:num->num. x(0)=0 /\ (!n. x(n+1)=2*x(n)+1) ==> !n. x(n)=2 EXP n - 1` );
;
val it : goalstack = 1 subgoal (1 total)

`!x. x 0 = 0 /\ (!n. x (n + 1) = 2 * x n + 1) ==> (!n. x n = 2 EXP n - 1)`

# e ( STRIP_TAC THEN STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = 0`]
1 [`!n. x (n + 1) = 2 * x n + 1`]

`!n. x n = 2 EXP n - 1`

# e ( INDUCT_TAC );;
val it : goalstack = 2 subgoals (2 total)

0 [`x 0 = 0`]
1 [`!n. x (n + 1) = 2 * x n + 1`]
2 [`x n = 2 EXP n - 1`]

`x (SUC n) = 2 EXP SUC n - 1`

0 [`x 0 = 0`]
1 [`!n. x (n + 1) = 2 * x n + 1`]

`x 0 = 2 EXP 0 - 1`

# e ( ASM_SIMP_TAC[EXP;ARITH] ) ;;
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = 0`]
1 [`!n. x (n + 1) = 2 * x n + 1`]
2 [`x n = 2 EXP n - 1`]

`x (SUC n) = 2 EXP SUC n - 1`

# e ( SIMP_TAC[EXP;ARITH;ADD1] ) ;;
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = 0`]
1 [`!n. x (n + 1) = 2 * x n + 1`]
2 [`x n = 2 EXP n - 1`]

`x (n + 1) = 2 * 2 EXP n - 1`

# e ( FIRST_X_ASSUM( ASSUME_TAC o SPECL[`n:num`] ) );;
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = 0`]
1 [`x n = 2 EXP n - 1`]
2 [`x (n + 1) = 2 * x n + 1`]

`x (n + 1) = 2 * 2 EXP n - 1`

# e ( ASSUME_TAC (MESON[EXP_LT_0;EXP;ARITH]`0<2 EXP n`) );;
0..0..16..102..615..solved at 1746
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = 0`]
1 [`x n = 2 EXP n - 1`]
2 [`x (n + 1) = 2 * x n + 1`]
3 [`0 < 2 EXP n`]

`x (n + 1) = 2 * 2 EXP n - 1`

# e ( ASM_SIMP_TAC[ARITH_RULE`02*(x-1)+1=2*x-1`] );;
val it : goalstack = No subgoals

proveにまとめると

g( `!x:num->num. x(0)=0 /\ (!n. x(n+1)=2*x(n)+1) ==> !n. x(n)=2 EXP n - 1` );;
e ( STRIP_TAC THEN STRIP_TAC );;
e ( INDUCT_TAC );;
e ( ASM_SIMP_TAC[EXP;ARITH] ) ;;
e ( SIMP_TAC[EXP;ARITH;ADD1] ) ;;
e ( FIRST_X_ASSUM( ASSUME_TAC o SPECL[`n:num`] ) );;
e ( ASSUME_TAC (MESON[EXP_LT_0;EXP;ARITH]`0<2 EXP n`) );;
e ( ASM_SIMP_TAC[ARITH_RULE`02*(x-1)+1=2*x-1`] );;

となります．
　:real 上で扱えば引き算も自由にできます．

g `!x. x 0 = &0 /\ (!n. x (n + 1) = &2 * x n + &1) ==> (!n. x n = &2 pow n - &1)` ;;
e( STRIP_TAC THEN STRIP_TAC );;
e( INDUCT_TAC );;
e( ASM_REAL_ARITH_TAC );;
e( ASM_SIMP_TAC [pow; ADD1] );;
e( REAL_ARITH_TAC );;

実行すると

# g `!x. x 0 = &0 /\ (!n. x (n + 1) = &2 * x n + &1) ==> (!n. x n = &2 pow n - &
1)` ;;
val it : goalstack = 1 subgoal (1 total)

`!x. x 0 = &0 /\ (!n. x (n + 1) = &2 * x n + &1)
==> (!n. x n = &2 pow n - &1)`

# e( STRIP_TAC THEN STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = &0`]
1 [`!n. x (n + 1) = &2 * x n + &1`]

`!n. x n = &2 pow n - &1`

# e( INDUCT_TAC );;
val it : goalstack = 2 subgoals (2 total)

0 [`x 0 = &0`]
1 [`!n. x (n + 1) = &2 * x n + &1`]
2 [`x n = &2 pow n - &1`]

`x (SUC n) = &2 pow SUC n - &1`

0 [`x 0 = &0`]
1 [`!n. x (n + 1) = &2 * x n + &1`]

`x 0 = &2 pow 0 - &1`

# e( ASM_REAL_ARITH_TAC );;
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = &0`]
1 [`!n. x (n + 1) = &2 * x n + &1`]
2 [`x n = &2 pow n - &1`]

`x (SUC n) = &2 pow SUC n - &1`

# e( ASM_SIMP_TAC [pow; ADD1] );;
val it : goalstack = 1 subgoal (1 total)

0 [`x 0 = &0`]
1 [`!n. x (n + 1) = &2 * x n + &1`]
2 [`x n = &2 pow n - &1`]

`&2 * (&2 pow n - &1) + &1 = &2 * &2 pow n - &1`

# e( REAL_ARITH_TAC );;
val it : goalstack = No subgoals

まとめると

# prove
(`!x. x 0 = &0 /\ (!n. x (n + 1) = &2 * x n + &1) ==> (!n. x n = &2 pow n - &
1)`,
STRIP_TAC THEN STRIP_TAC THEN
INDUCT_TAC THEN
ASM_SIMP_TAC [pow; ADD1] THEN
ASM_REAL_ARITH_TAC);;
val it : thm =
|- !x. x 0 = &0 /\ (!n. x (n + 1) = &2 * x n + &1)
==> (!n. x n = &2 pow n - &1)

となります．

■　等比数列の和

g ( `!n:num. sum(0..n)(\k. &2 pow k)= &2 pow (SUC n) - &1` );;
e ( INDUCT_TAC );;
e ( ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;pow] THEN REAL_ARITH_TAC );;
e ( ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;pow;LE_0] THEN REAL_ARITH_TAC );;

　まとめて

# prove ( `!n:num. sum(0..n)(\k. &2 pow k)= &2 pow (SUC n) - &1` ,
INDUCT_TAC THEN
ASM_SIMP_TAC[SUM_CLAUSES_NUMSEG;pow;LE_0] THEN REAL_ARITH_TAC );;
val it : thm = |- !n. sum (0..n) (\k. &2 pow k) = &2 pow SUC n - &1

となります．