19 Real analysis (4)

　チェビシェフの多項式を書き下すことは難しくありません．まず，引数の処理に用いる，2以上の整数をn+2の形に書き換えるconvを作ります．

let NUM_ADD2_CONV =
let add_tm = `(+):num->num->num`
and two_tm = `2` in
fun tm ->
let m = mk_numeral(dest_numeral tm -/ Int 2) in
let tm' = mk_comb(mk_comb(add_tm,m),two_tm) in
SYM(NUM_ADD_CONV tm');;

ここで

mk_numeral((dest_numeral tm) -/ Int 2)

は，tmをdest_numeralによりOCamlのIntの元に直して，OCaml上で整数 Int2 を引き算 -/ したものを，mk_numeralでHOL Lightのtermに戻しています（証明内での引数のこのような加工は意外と面倒です）．
　次に，定義に名前を付けます．

# let [pth0;pth1;pth2] = CONJUNCTS cheb;;
Characters 4-20:
Warning P: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
[]
let [pth0;pth1;pth2] = CONJUNCTS cheb;;
^^^^^^^^^^^^^^^^
val pth0 : thm = |- !x. cheb 0 x = &1
val pth1 : thm = |- !x. cheb 1 x = x
val pth2 : thm = |- !n x. cheb (n + 2) x = &2 * x * cheb (n + 1) x - cheb n x

　以下が再帰を用いた関数の定義です．

let rec conv tm =
(GEN_REWRITE_CONV I [pth0; pth1] ORELSEC
(LAND_CONV NUM_ADD2_CONV THENC
GEN_REWRITE_CONV I [pth2]
THENC
COMB2_CONV
(funpow 3 RAND_CONV ( (LAND_CONV NUM_ADD_CONV) THENC conv))
conv THENC
REAL_POLY_CONV) ) tm ;;

全体としては，(n=0,1 のときのconversion ORELSEC n>=2 のときconversion ) tm というもので，前者はcheb 0 x，cheb 1 x の定義を参照したGEN_REWRITE_CONV I であり，DEPTH_CONVなどではなく恒等変換 I を用いることで，定理で書き換えられない際にはエラーとなるので，場合分けが実現できます．後者では，例えば，まず

# (LAND_CONV NUM_ADD2_CONV THENC
GEN_REWRITE_CONV I [pth2])`cheb 5 x`;;
val it : thm = |- cheb 5 x = &2 * x * cheb (3 + 1) x - cheb 3 x

のように 5 = 3 + 2 を n + 2 と見た書き換えを行い，次に COMB2_CONV で `(-) (&2*x*cheb (3+1) x)`，`cheb 3 x` にそれぞれ(funpow 3 RAND_CONV ( (LAND_CONV NUM_ADD_CONV) THENC conv) )，convを作用させます．後は再帰で得られた結果をREAL_POLY_CONVにより

&2 * x * (&2 * x * (&2 * x * (&2 * x * x - &1) - x) - (&2 * x * x - &1)) -
(&2 * x * (&2 * x * x - &1) - x) =
&16 * x pow 5 + -- &20 * x pow 3 + &5 * x

のように整理するだけです．実行してみると

# CHEB_CONV `cheb 10 x`;;
val it : thm =
|- cheb 10 x =
&512 * x pow 10 +
-- &1280 * x pow 8 +
&1120 * x pow 6 +
-- &400 * x pow 4 +
&50 * x pow 2 +
-- &1

などとなります．

　ただし，nに対して処理時間は指数的に増加します．例えば，フィボナッチ数列の場合でも

let rec fib n = if n <= 2 then 1 else fib(n - 1) + fib(n - 2);;

の代わりに，2項ずつ

# let rec fib2 n = if n <= 1 then (1,1) else let a,b = fib2(n-1) in b,a + b;;
val fib2 : int -> int * int =
# let fib n = fst(fib2 n);;
val fib : int -> int =

のように定めれば，OCamlのデフォルトでも，直ちに

# fib 40;;
val it : int = 102334155

とできます．同様のアイデアにより

# let CHEB_2N1 = prove
(`!n x. *1 THEN
CONV_TAC REAL_RING);;
5 basis elements and 8 critical pairs
6 basis elements and 11 critical pairs
7 basis elements and 15 critical pairs
8 basis elements and 21 critical pairs
8 basis elements and 20 critical pairs
9 basis elements and 26 critical pairs
9 basis elements and 25 critical pairs
9 basis elements and 24 critical pairs
10 basis elements and 32 critical pairs
10 basis elements and 31 critical pairs
10 basis elements and 30 critical pairs
10 basis elements and 29 critical pairs
10 basis elements and 28 critical pairs
10 basis elements and 27 critical pairs
10 basis elements and 26 critical pairs
10 basis elements and 25 critical pairs
11 basis elements and 33 critical pairs
11 basis elements and 32 critical pairs
11 basis elements and 31 critical pairs
12 basis elements and 0 critical pairs
5 basis elements and 8 critical pairs
6 basis elements and 11 critical pairs
7 basis elements and 15 critical pairs
8 basis elements and 21 critical pairs
8 basis elements and 20 critical pairs
9 basis elements and 26 critical pairs
9 basis elements and 25 critical pairs
9 basis elements and 24 critical pairs
10 basis elements and 32 critical pairs
10 basis elements and 31 critical pairs
10 basis elements and 30 critical pairs
10 basis elements and 29 critical pairs
10 basis elements and 28 critical pairs
10 basis elements and 27 critical pairs
10 basis elements and 26 critical pairs
10 basis elements and 25 critical pairs
11 basis elements and 33 critical pairs
11 basis elements and 32 critical pairs
11 basis elements and 31 critical pairs
12 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
val ( CHEB_2N1 ) : thm =
|- !n x.
(x - &1) * (cheb (2 * n + 1) x - &1) =
(cheb (n + 1) x - cheb n x) pow 2 /\
&2 * (x pow 2 - &1) * (cheb (2 * n + 2) x - &1) =
(cheb (n + 2) x - cheb n x) pow 2

のような証明も書けますが，この例の係数 x-1，x^2-1が0の場合をHOL Lightで検証することは相応の練習になるでしょう．

*1:x - &1) * (cheb (2 * n + 1) x - &1) = (cheb (n + 1) x - cheb n x) pow 2) /\ (&2 * (x pow 2 - &1) * (cheb (2 * n + 2) x - &1) = (cheb (n + 2) x - cheb n x) pow 2)`, ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN MATCH_MP_TAC CHEB_INDUCT THEN REWRITE_TAC[ARITH; cheb; CHEB_CONV `cheb 2 x`; CHEB_CONV `cheb 3 x`;] THEN REPEAT(CHANGED_TAC (REWRITE_TAC[GSYM ADD_ASSOC; LEFT_ADD_DISTRIB; ARITH] THEN REWRITE_TAC[ARITH_RULE `n + 5 = (n + 3) + 2`; ARITH_RULE `n + 4 = (n + 2) + 2`; ARITH_RULE `n + 3 = (n + 1) + 2`; cheb]