2012-01-01から1年間の記事一覧
４変数から３変数の場合を導きましょう．まず，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.…
