先のJENSEN_LT_INFを用いて，変数の相加平均と相乗平均の不等式を証明します． let lemma0 = prove (`!n s x. (!i. i <= n ==> &0 <= s i) /\ sum (0..n) s = &1 /\ (!i. i <= n ==> &0 < x i) ==> sum (0..n) (\i. s i * ln (x i)) <= ln (sum (0..n) (\i. …

HOL LightはOcamlのToplevel Loop上のプログラムですから，Ocamlが動くならOSは問いませんが，周辺プログラムとの連携という観点に立つなら何といってもUnixです． それはMaximaやPARI/GPを呼ぶmlファイル内のシステムコマンドによるものだけではなく，一般…

普通の数学ならTaylorの定理が簡単ですが，HOL Lightで書いてみると予想外に長くなりましたので，MVTを二重に使う方針にしました． (* f(x)<=f(p)+(x-p)*f'(p) *) let ass = ASM_SIMP_TAC[] THEN STRIP_TAC;; g`!a b:real f f' f'':real->real. a<b /\ (!x. a<=x /\ x<=b ==> (f diffl f</b>…

今回は私がHOL Lightで証明を書く際の環境？をご紹介します． OSはWindows，エディターは秀丸，OcamlはDOS窓内です． 秀丸はシェアウエアですが，軽快な作動と柔軟なカスタマイズ性，Cライクなマクロが特徴で，私は例えば，カーソルのある論理行をクリップボ…

かなり刹那的ですが，とりあえず２変数の場合です．MVT_ALTではなくMVTを参照すれば端点での可微分性は不要なのですが，その分contlを付さねばならず煩雑？なので，この形にしました（transc.mlのMCLAURINの証明にもWe could weaken the hypotheses slightly…

次回からは，一変数級関数上の数列についてのJensenの不等式を証明します．

ある論文で紹介されていた排中律によるトリック？です． # g `!p:A->bool. ?x:A. (p x ==> !y. p y)`;; val it : goalstack = 1 subgoal (1 total) `!p. ?x. p x ==> (!y. p y)` # e(GEN_TAC);; val it : goalstack = 1 subgoal (1 total) `?x. p x ==> (!y.…

これで積分の第一平均値定理が通常の形で証明できます． let CONT_ATTAINS3 = prove (`!f:real->real a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?L. (!x. a <= x /\ x <= b ==> L <= f x) /\ (?x1. a <= x1 /\ x1 <= b /\ f x1 = L)) /\ (?…

落穂ひろい気味ですが，先のthm15から&0 積分の第一平均値定理を得るための補題の証明です． let INTEGRAL_CONST_LE = prove (`!c g a b. a <= b /\ integrable (a,b) g /\ (!x. a <= x /\ x <= b ==> c <= g x) ==> c * (b - a) <= integral (a,b) g`, GEN_…

以上をまとめると次のようになります． g `!f (z:num->num->real). (!x. &0 <= x /\ x <= &1 ==> f contl x) ==> (?z. !N. 1 <= N ==> (!n. if n < N then &n / &N <= z N n /\ z N n <= &(n + 1) / &N else z N n = &1) /\ integral (&0,&1) (\x. f x * abs…

tagged division用のlemmaを幾つか用意すれば，区分求積の公式が証明できます． g`(!n. n < N ==> (if n < N then &n / &N else &1) < (if n + 1 < N then &(n + 1) / &N else &1)) /\ (!n. n >= N ==> (if n < N then &n / &N else &1) = &1)`;; e(REPEAT S…

そして，Kurzweil-Henstock積分ですので，区分求積の為に通常のRiemann積分の理論を自作します． let rdefint = new_definition `(!a b f k. rdefint (a,b) f k <=> (!e. &0 < e ==> (?g. &0 < g /\ (!D p. ((D 0 = a /\ (?N. (!n. n < N ==> D n < D (SUC n…

得られた結果をもとの式に適用します． g `!f n k. 1 <= n /\ 1 <= k /\ k <= n /\ (!x. &(k - 1) / &n <= x /\ x <= &k / &n ==> f contl x) ==> ?z. &(k - 1) / &n <= z /\ z <= &k / &n /\ integral (&(k - 1) / &n,&k / &n) (\x. f x * abs (sin (&n * p…

前回の結果とDIFF_CONV，更に微積分の基本定理（その１）FTC1を用いて，定積分の値を具体化します． let lemma01 = MESON[REAL_LE; REAL_ARITH `&1 <= &n ==> &0 < &n`; REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; PI_POS; REAL_LE_LMUL_EQ; REAL_MUL_AC] `1 <= n =…

の絶対値の積分において，絶対値記号を外に出すには定符号を言えば良いわけです．もし変数変換が使えるならに帰着する道もありそうですが，それらしいthmは見当たりませんので，の偶奇により場合を分けて行きます． g `!m y. (&2 * &m) * pi <= y /\ y <= (&…

次は積分の平均値定理ですが，第２はありますが，簡単な第１が見当たらないので，CONT_ATTAINS_ALLとIVTなどから証明しました． let thm12 = MESON[thm05; REAL_LE_TRANS] `(!x. &0 <= x /\ x <= &1 ==> f contl x) ==> !n. 1 <= n ==> !k. 1 <= k /\ k <= n…

まずは，区間の等分です．単調列での分割を帰納法で示した後，を固定した列により等分します． needs "Library/transc.ml";; g `!n f x i. (!j k. j <= k /\ k <= n ==> x j <= x k) /\ (!k. 1 <= k /\ k <= n ==> defint (x (k -1),x k) f (i k)) ==> defin…

次回からは，が区間[0,1]で連続のとき の証明を進めます． 証明の流れは，区間を等分して，積分の平均値定理，絶対値との順序交換，リーマン和の極限といったものです． 本格的な積分の証明には，"Multivariate/realanalysis.ml"あたりが入用ですが，今回程…

今回は，床関数の性質の一つです．定義に近い形で進めるなら g `!x m. floor (x + &m) = floor x + &m`;; e(REPEAT GEN_TAC);; e(MAP_EVERY ASSUME_TAC [SPEC`x + &m`FLOOR; SPEC`x:real`FLOOR]);; e(SUBGOAL_TAC""`integer (floor x + &m)`[ASM_SIMP_TAC[IN…

MESONは非常に優秀なproverであり，例えば # let lemma = `!x:real. ?n:num. &1 <= x ==> &1 <= &n /\ floor x = &n`;; val lemma : term = `!x. ?n. &1 <= x ==> &1 <= &n /\ floor x = &n`の証明に必要な # [FLOOR; integer; ABS_REFL; REAL_LE_FLOOR; INT…

既出の本家筋以外は中々見当たらないのですが，次の論文の補足Ｂに入門的な解説があります． http://rudar.ruc.dk/bitstream/1800/6890/1/8%20-%20Automatization%20of%20the%20semantic%20tableau%20method.pdf なお，取り上げられている例をただ証明するだ…

ご覧のように，HOL Light は，数学科の学部程度の定理(Pre-proved Theorems)とそれを用いて新たな定理の証明を作成する為の関数(Pre-de ned ML Identi ers)からなる，所謂，proof assistantですが，MizarやCoqよりも知名度が低いように思えます．その理由の…

あるサイトに出ていた計算機による証明の課題です． # prove (`!n. 1 + nsum (0..n) (\k. 2 EXP k) = 2 EXP (n + 1)`, INDUCT_TAC THENL [SIMP_TAC [NSUM_CLAUSES_NUMSEG; EXP; GSYM ADD1; MULT_CLAUSES; TWO]; ASM_SIMP_TAC [NSUM_CLAUSES_NUMSEG; LE_0; EX…

以上を利用して次に至ります． g`~(?n N. 2 <= n /\ sum(1..n)(\k. &1 / &k) = &N)`;; e(REPEAT STRIP_TAC);; e(MP_TAC (SPEC_ALL floor2) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);; e(MP_TAC (SPEC`xn:num`thm4) THEN ASM_SIMP_TAC[] THEN REPEAT STRI…

同様に第２の和も表せることの証明です．thm8_2はthm7_2を含んだ形になりました． g`!n xn k. n < 2 EXP SUC xn /\ 1 <= xn /\ 2 EXP xn + 1 <= k /\ k <= n ==> ?x y. &2 pow xn / &k = &x / &y /\ EVEN x /\ ODD y`;; e(REPEAT STRIP_TAC);; e(MP_TAC( pro…

先の補題を用いて，thm5で分割した第１の和が奇数分の分数と表せることを証明します． g`!xn k. 1 <= xn /\ 1 <= k /\ k <= 2 EXP xn - 1 ==> ?x y. &2 pow xn / &k = &x / &y /\ EVEN x /\ ODD y`;; e(REPEAT STRIP_TAC);; e(MP_TAC( prove(`k <= 2 EXP xn …

今回は，奇数分の偶数と表せる有理数が加法について閉じていることの証明です． let lemma01 = MESON[ODD_EXISTS; LT_0; REAL_LT]`!x. ODD x ==> &0 < &x`;; g`!a b c d. EVEN a /\ EVEN c /\ ODD b /\ ODD d ==> ?x y. &a / &b + &c / &d = &x / &y /\ EVEN…

今回は，先の和にを掛けてになる項と残りの和に分割する補題です． let lemma01 = MP (SPECL[`\k. &2 pow xn / &k`;`1`;`2 EXP xn`;`n - 2 EXP xn`]SUM_ADD_SPLIT) (prove(`1 <= 2 EXP xn + 1`,MP_TAC(MESON[TWO; ZERO_LESS_EXP]`0 < 2 EXP n`) THEN ARITH_T…

今回は，先の和の各項の分母の中での指数がに等しいものは唯一つであり，その他のの指数はより小さいことの証明です． g`!x y n. ODD y /\ 2 EXP x * y < 2 EXP (SUC n) ==> x <= n`;; e(REPEAT STRIP_TAC);; e(ASSUME_TAC(UNDISCH(MESON[ODD_EXISTS; LT_0; …

今回からは，以上の任意の整数に対して， は整数にならないことを証明していきます．方針は，この和を整数とおき，となる偶数を掛けると，適当な偶数，奇数が存在してとなり不合理というものです． 最初は，任意の正の整数に対して，適当な非負の整数，正の…