2012-01-01から1ヶ月間の記事一覧
の絶対値の積分において，絶対値記号を外に出すには定符号を言えば良いわけです．もし変数変換が使えるならに帰着する道もありそうですが，それらしい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; …
今回からは，以上の任意の整数に対して， は整数にならないことを証明していきます．方針は，この和を整数とおき，となる偶数を掛けると，適当な偶数，奇数が存在してとなり不合理というものです． 最初は，任意の正の整数に対して，適当な非負の整数，正の…
４変数から３変数の場合を導きましょう．まず，lemmaを用意します． g`!x. &0 <= x ==> root 3 x = root 4 ( root 3 x * x )`;; e(SIMP_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC);; e(ASM_SIMP_TAC[ARITH_RULE`3 = SUC 2 /\ 4 = SUC 3`; REAL_EXP_POS_LT; REA…
前回のroot4をexpを用いて証明してみます． g`!x. &0 <= x ==> root 4 x = sqrt( sqrt x )`;; e(SIMP_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC);; e(ASM_SIMP_TAC[sqrt; ARITH_RULE`4 = SUC 3 /\ 2 = SUC 1`; ROOT_LN; REAL_EXP_POS_LT; REAL_EXP_INJ]);; e(A…
今回は，２重根号をexpを用いずに，４変数の相加相乗平均の大小関係を証明してみます． (* amgm4 *) (* まず，２変数の場合を証明します．*) g`!a b. &0 <= a /\ &0 <= b ==> (a + b) / &2 >= sqrt(a * b)`;; e(REPEAT GEN_TAC);; e(DISCH_THEN(fun t -> MP_…
先のものでは SQRT_SOS[`a=sqrt x`]`&0 < x ==> (x = sqrt x <=> x = &1)`;;などが処理できないので，少し手を入れました． let SQRT_SOS sqrt tm = prove (tm, REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM (fun t -> ASSUME_TAC (MATCH_MP REAL_LT_IMP_LE…
前回の平方根の消去をconversionにしてみました． let SQRT_SOS sqrt tm = prove (tm, REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP REAL_LT_IMP_LE))) THEN EVERY_ASSUM (MP_TAC o (MATCH_MP SQRT_POS_LE)) THEN MAP_EVERY ABBREV…
今回は平方根を含む不等式の変形です． g`!x y :real. &0 <= x ==> ( y <= sqrt x <=> y < &0 \/ (&0 <= y /\ y pow 2 <= x) )`;; e(REPEAT STRIP_TAC);; e(MP_TAC((UNDISCH o SPEC_ALL)SQRT_POS_LE));; e(ABBREV_TAC`z = sqrt x`);; e(ONCE_ASM_REWRITE_TAC…
let thm20120112=prove (`~(?x y. &x / &y = sqrt (&2) )`, REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o (MATCH_MP lemma08)) THEN SIMP_TAC[REAL_MUL; REAL_INJ] THEN MESON_TAC[thm20120110_2]);; 0..0..1..solved at 4 val thm20120112 : thm = |- ~(?…
let lemma05=MATCH_MP lemma03 lemma04;; g`x = sqrt(&2) * y /\ ~(y = &0) ==> x * x = sqrt(&2) pow 2 * y * y /\ ~(y = &0)`;; e(REPEAT STRIP_TAC);; e(ASM_SIMP_TAC[REAL_MUL_AC; POW_2]);; e(ASM_MESON_TAC[]);; let lemma06=top_thm();; (* MESON[REA…
さらに計算系のproverの利用を控えるなら let lemma01=MESON[real_div; REAL_INV_0; REAL_MUL_RZERO] `x / y = z /\ y = &0 ==> z = &0`;; let lemma02=MESON[REAL_DIV_RMUL] `x / y = z /\ ~(y = &0) ==> x = z * y`;; (* let lemma02=REAL_FIELD `x / y = …
前回の結果をより簡明に表すなら g`~(?x y:num. &x / &y = sqrt (&2) )`;;let lemma01=MESON[real_div; REAL_INV_0; REAL_MUL_RZERO]`x / y = z /\ y = &0 ==> z = &0`;; let lemma02=REAL_FIELD`x / y = z /\ ~(y = &0) ==> x = y * z`;; let lemma012=MESO…
今回は，以前(http://d.hatena.ne.jp/ehito/20111120)，num_WFを用いて証明した が有理数でないこと です． let lemma01=MESON[GCD_ZERO; GCD_COPRIME_EXISTS] `~(a=0) ==> ?x y z. a=x*z /\ b=y*z /\ coprime(x,y)`;; let lemma02=NUM_RING`~(x * z = 0) ==…
前回の実行結果です． # g`!a b c d. &0<a /\ &0<b ==> ( a*c<b*d <=> c/b<d/a )`;; val it : goalstack = 1 subgoal (1 total) `!a b c d. &0 < a /\ &0 < b ==> (a * c < b * d <=> c / b < d / a)` # e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`&0 < a`] 1 [`&0 < b`] `a * c < b * d <=> c / b < d / a…</d/a></b*d></a>
今回は http://as305.dyndns.org/aps/problem/view/50 すなわち [tex:\forall n:num.\, 3\le n \to (n+1)^n g`!a b c d. &0 < a /\ &0 < b ==> ( a*c<b*d <=> c/b<d/a )`;; e(REPEAT STRIP_TAC);; e(ONCE_REWRITE_TAC[ARITH_RULE`x<y<=>x-y< &0`; ]);; e(ASM_SIMP_TAC[RAT_LEMMA3]);; e(ASM_SIMP_TAC[REAL_SOSFIELD`&0<x ==>(a*b* …</x></d/a></b*d>
最終的に # let thm20120104_4=MESON[thm20120104]`!d:num. !c:num->int. (!n:num. ?p:num. isum (0..d) (\i. c i * &n pow i) = &p /\ prime p) ==> (?p:num. !n:num. isum (0..d) (\i. c i * &n pow i) = &p /\ prime p)`;; 0..0..0..1..3..7..13..26..41.…
