HOL4 の証明例（１） - ATPとCASのこと

等比数列の和です．

g `!n. sum(0,SUC n) (\n. &2 pow n) = &2 pow (SUC n) - &1`;
e( Induct_on `n` );
e( RW_TAC(real_ss++REAL_ARITH_ss)[pow, SUM_1] );
e( RW_TAC(real_ss++REAL_ARITH_ss)[pow, sum] );

- g `!n. sum(0,SUC n) (\n. 2 pow n) = 2 pow (SUC n) - 1`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete goalstack:
         Initial goal:

         !n. sum (0,SUC n) (\n. 2 pow n) = 2 pow SUC n - 1


     : proofs
- e( Induct_on `n` );
OK..
2 subgoals:
> val it =

    sum (0,SUC (SUC n)) (\n. 2 pow n) = 2 pow SUC (SUC n) - 1
    ------------------------------------
      sum (0,SUC n) (\n. 2 pow n) = 2 pow SUC n - 1


    sum (0,SUC 0) (\n. 2 pow n) = 2 pow SUC 0 - 1

     : proof
- e( RW_TAC(real_ss++REAL_ARITH_ss)[pow, SUM_1] );
OK..

Goal proved.
 [] |- sum (0,SUC 0) (\n. 2 pow n) = 2 pow SUC 0 - 1

Remaining subgoals:
> val it =

    sum (0,SUC (SUC n)) (\n. 2 pow n) = 2 pow SUC (SUC n) - 1
    ------------------------------------
      sum (0,SUC n) (\n. 2 pow n) = 2 pow SUC n - 1
     : proof
- e( RW_TAC(real_ss++REAL_ARITH_ss)[pow, sum] );
OK..

Goal proved.
 [sum (0,SUC n) (\n. 2 pow n) = 2 pow SUC n - 1]
|- sum (0,SUC (SUC n)) (\n. 2 pow n) = 2 pow SUC (SUC n) - 1
> val it =
    Initial goal proved.
     [] |- !n. sum (0,SUC n) (\n. 2 pow n) = 2 pow SUC n - 1 : proof

HOL Light では

g `!n. sum(0,SUC n) (\n. &2 pow n) = &2 pow (SUC n) - &1`;;
e( INDUCT_TAC );;
e( REWRITE_TAC[pow; sum; REAL_ADD_LID; ADD] THEN REAL_ARITH_TAC );;
e( ASM_REWRITE_TAC[pow; sum; ADD] THEN REAL_ARITH_TAC );;

# g `!n. sum(0,SUC n) (\n. &2 pow n) = &2 pow (SUC n) - &1`;;
val it : goalstack = 1 subgoal (1 total)

`!n. sum (0,SUC n) (\n. &2 pow n) = &2 pow SUC n - &1`

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

  0 [`sum (0,SUC n) (\n. &2 pow n) = &2 pow SUC n - &1`]

`sum (0,SUC (SUC n)) (\n. &2 pow n) = &2 pow SUC (SUC n) - &1`

`sum (0,SUC 0) (\n. &2 pow n) = &2 pow SUC 0 - &1`

# e( REWRITE_TAC[pow; sum; REAL_ADD_LID; ADD] THEN REAL_ARITH_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`sum (0,SUC n) (\n. &2 pow n) = &2 pow SUC n - &1`]

`sum (0,SUC (SUC n)) (\n. &2 pow n) = &2 pow SUC (SUC n) - &1`

# e( ASM_REWRITE_TAC[pow; sum; ADD] THEN REAL_ARITH_TAC );;
val it : goalstack = No subgoals

なので，この程度なら HOL4 の方が簡潔です．

　しかし，分数になると．．．

g `!n. sum(0,SUC n) (\n. (&1/ &2) pow n) = &2 - (&1 / &2) pow n`;;
e( INDUCT_TAC );;
e( REWRITE_TAC[pow; sum; REAL_ADD_LID; ADD] THEN REAL_ARITH_TAC );;
e( ASM_REWRITE_TAC[pow; sum; ADD] THEN REAL_ARITH_TAC );;

# g `!n. sum(0,SUC n) (\n. (&1/ &2) pow n) = &2 - (&1 / &2) pow n`;;
val it : goalstack = 1 subgoal (1 total)

`!n. sum (0,SUC n) (\n. (&1 / &2) pow n) = &2 - (&1 / &2) pow n`

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

  0 [`sum (0,SUC n) (\n. (&1 / &2) pow n) = &2 - (&1 / &2) pow n`]

`sum (0,SUC (SUC n)) (\n. (&1 / &2) pow n) = &2 - (&1 / &2) pow SUC n`

`sum (0,SUC 0) (\n. (&1 / &2) pow n) = &2 - (&1 / &2) pow 0`

# e( REWRITE_TAC[pow; sum; REAL_ADD_LID; ADD] THEN REAL_ARITH_TAC );;
val it : goalstack = 1 subgoal (1 total)

  0 [`sum (0,SUC n) (\n. (&1 / &2) pow n) = &2 - (&1 / &2) pow n`]

`sum (0,SUC (SUC n)) (\n. (&1 / &2) pow n) = &2 - (&1 / &2) pow SUC n`

# e( ASM_REWRITE_TAC[pow; sum; ADD] THEN REAL_ARITH_TAC );;
val it : goalstack = No subgoals

のように HOL Light が全く動じないのに対して，HOL4 は大変です．

g `!n. sum(0,SUC n) (\n. (1/ 2) pow n) = 2 - (1 / 2) pow n`;
e( Induct_on `n` );
e(RW_TAC(real_ss++REAL_ARITH_ss)[pow, SUM_1]);
val lem0 = METIS_PROVE[POW_NZ, REAL_ARITH``2<>0:real``, REAL_ENTIRE, mult_ratr, REAL_DIV_LMUL_CANCEL]``(2 * (1 / (2 * 2 pow n)))=(1 / 2 pow n)``;
val lem1 = REAL_ARITH``(2 - 1 / 2 pow n + 1 / (2 * 2 pow n) = 2 - 1 / (2 * 2 pow n))<=>(2 * (1 / (2 * 2 pow n)) = 1 / 2 pow n)``;
e(RW_TAC(real_ss++REAL_ARITH_ss)[pow, sum, POW_ONE, lem0, lem1]);

- g `!n. sum(0,SUC n) (\n. (1/ 2) pow n) = 2 - (1 / 2) pow n`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete goalstack:
         Initial goal:

         !n. sum (0,SUC n) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow n


     : proofs
- e( Induct_on `n` );
OK..
2 subgoals:
> val it =

    sum (0,SUC (SUC n)) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow SUC n
    ------------------------------------
      sum (0,SUC n) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow n


    sum (0,SUC 0) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow 0

     : proof
- e(RW_TAC(real_ss++REAL_ARITH_ss)[pow, SUM_1]);
OK..

Goal proved.
 [] |- sum (0,SUC 0) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow 0

Remaining subgoals:
> val it =

    sum (0,SUC (SUC n)) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow SUC n
    ------------------------------------
      sum (0,SUC n) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow n
     : proof
- val lem0 = METIS_PROVE[POW_NZ, REAL_ARITH``2<>0:real``, REAL_ENTIRE, mult_ratr, REAL_DIV_LMUL_CANCEL]``(2 * (1 / (2 * 2 pow n)))=(1 / 2 pow n)``;
metis: r[+0+10]+0+0+0+0+0+0+0+2+7+2+0+4+3+6+7+1+11+13+11+10+13r+5+11+16+9+1
2+2+3+13+1#
> val lem0 =  [] |- 2 * (1 / (2 * 2 pow n)) = 1 / 2 pow n : thm
- val lem1 = REAL_ARITH``(2 - 1 / 2 pow n + 1 / (2 * 2 pow n) = 2 - 1 / (2 * 2 pow n))<=>(2 * (1 / (2 * 2 pow n)) = 1 / 2 pow n)``;
> val lem1 =
     []
    |- (2 - 1 / 2 pow n + 1 / (2 * 2 pow n) = 2 - 1 / (2 * 2 pow n)) <=>
       (2 * (1 / (2 * 2 pow n)) = 1 / 2 pow n) : thm
- e(RW_TAC(real_ss++REAL_ARITH_ss)[pow, sum, POW_ONE, lem0, lem1]);
OK..

Goal proved.
 [sum (0,SUC n) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow n]
|- sum (0,SUC (SUC n)) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow SUC n
> val it =
    Initial goal proved.
     [] |- !n. sum (0,SUC n) (\n. (1 / 2) pow n) = 2 - (1 / 2) pow n : proof

これを HOL4 の力不足と見るか，計算をブラックボックスにしない高潔な理念の現われと見るかは．．．

おまけ

- TOP_DEPTH_CONV num_CONV ``5:num``;
> val it =  [] |- 5 = SUC (SUC (SUC (SUC (SUC 0)))) : thm

- (TOP_DEPTH_CONV num_CONV THENC REWRITE_CONV[pow, REAL_MUL_RID]) ``x pow 5``;
> val it =  [] |- x pow 5 = x * (x * (x * (x * x))) : thm