2013-03-01から1ヶ月間の記事一覧
# map(fun t-> MATCH_MP t (ARITH_RULE `~(5=0)`))[MOD_MOD_REFL; MOD_ADD_MO D; MOD_MULT_MOD2];; val it : thm list = [|- !m. m MOD 5 MOD 5 = m MOD 5; |- !a b. (a MOD 5 + b MOD 5) MOD 5 = (a + b) MOD 5; |- !m p. (m MOD 5 * p MOD 5) MOD 5 = (m *…
EXPAND_CASES_CONV http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/EXPAND_CASES_CONV.html は `!n. n<N ==> P(n)`;; を「n # EXPAND_CASES_CONV`!n.n<5==>0<(n EXP 2+n+1)MOD 5`;; val it : thm = |- (!n. n < 5 ==> 0 < (n EXP 2 + n + 1) MOD 5) <=> 0 < (0 EX</n>…
前回程度なら参照する定理を与えるだけで．．． # MESON [FACT_LE; ARITH_RULE `1 <= f ==> ~(f + 1 = 1)`; PRIME_FACTOR; DIVIDES_FA CT_PRIME; COPRIME_PLUS1; coprime; prime; NOT_LE] `!n. ?p. prime p /\ n < p` ;; 0..0..0..6..16..39..92..171..316..…
g `~(?n. !p. prime p ==> p <= n)` ;; e( STRIP_TAC THEN ABBREV_TAC `k = FACT n + 1` );; e( SUBGOAL_THEN `?p. prime p /\ p divides k` MP_TAC );; e( ASM_MESON_TAC [FACT_LE; ARITH_RULE `1 <= f ==> ~(f + 1 = 1)`; PRIME_FACTOR] );; e( STRIP_TAC …
miz3 http://arxiv.org/abs/1201.3601 はメモリー（Unixのみ）に常駐して mizar のような natural language declarative style の証明を書く為の自動入力ツールで，インストールは cp miz3/exrc ~/.exrc export PATH = $PATH:~/CAS/hol_light/miz3/bin とし…
ASM 系のタクティックの負担軽減の為，不要な仮定を消去する目的で作りました．for HOL Light let DEL_TAC n = ASSUM_LIST (fun al-> UNDISCH_THEN ( concl ((el((length al)-1-n)al)) ) (K ALL_TAC) );; for HOL4 fun DEL_TAC n = ASSUM_LIST (fn al => UND…
と言うわけで，Examples/prover9.ml にある PROVER9 とのインターフェイスを定理リスト参照型のプルーバー PV9，および，タクティック PV9_TAC として実装すると．．．コーシー・ラグランジュの恒等式 # let ths = [REAL_POW_2; REAL_ADD_LDISTRIB; REAL_ADD…
HOL Light には Prover9 という頼もしい友がいます． # #use "Examples/prover9.ml" ;; val prover9 : string = "prover9" val prover9_debugging : bool ref = {contents = false} val prover9_options : string ref = {contents = "clear(auto_inference).…
METIS があります．HOL Light には MESON しかなく，口惜しい限りです． load "dividesTheory"; open dividesTheory; val ARITH_RULE = SIMP_CONV(arith_ss++ARITH_ss)[divides_def]; val lem = ARITH_RULE ``~(9=0:num) /\ ~(2=0:num) /\ ~(4=0:num) /\ ~(5…
等比数列の和です． 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 (…
前回紹介したライブラリーのロード，オープン以外にも，グローバル変数の設定や，自作の定理，tacticなどを起動時に読み込ませるには，ホームディレクトリ（WindowsではC:\Users\ユーザー名）にhol-config.sml hol-config.ML .hol-config .hol-config.sml .h…
HOL4 のインストールスクリプトは http://d.hatena.ne.jp/ehito/20130219/1361260859 に書きましたが，システムとして HOL Light と大きく異なる点を幾つか述べます．まず，ライブラリーのロードとオープンについてです．デフォルトでの起動では，例えば - I…
# #use "Rqe/make.ml";; ... # time REAL_QELIM_CONV`!a b c. (?x. &0<=x pow 3 +a* x pow 2+ b*x+c) `;; CPU time (user): 614.655 val it : thm = |- (!a b c. ?x'. &0 <= x' pow 3 + a * x' pow 2 + b * x' + c) <=> T
http://d.hatena.ne.jp/ehito/20130313/1363131870 の定理の HOL4 による証明です． - g `!s t a b:real. 0<=s /\ 0<=t /\ (s+t=1) /\ 0<=a /\ 0<=b ==> !n. (s*a+t*b) pow n <= s*a pow n + t*b pow n` ; > val it = Proof manager status: 1 proof. 1. Inc…
適当な tactics を用いて論理記号を外し，atomic formula に分解する作業にそれほどの困難はありません．問題は，そのあと，定数，変数，関数，述語記号などからなる式を「計算」により証明する部分にあります．実際，各種の「検証」で高名な HOL4 も他の証…
g `!s t a b. &0<=s /\ &0<=t /\ s+t= &1 /\ &0<=a /\ &0<=b /\ a<=b ==> !n. (s*a+t*b) pow n <= s*a pow n + t*b pow n` ;; e( REPEAT GEN_TAC THEN STRIP_TAC );; e( INDUCT_TAC );; e( ASM_REAL_ARITH_TAC );; e( REWRITE_TAC [pow] );; let lem1 = MESO…
やはり METIS は優秀です． http://www.gilith.com/research/metis/ MESON による PROVE_TAC ではこうは行きません． load "numRingLib"; open arithmeticTheory numLib numRingLib; val def1 = Define `p n = (n*n+n+1) MOD 5 <> 0`; val def2 = Define `p0…
prove (`!n. ~((n EXP 2 + n + 1) MOD 5 = 0)`, GEN_TAC THEN MP_TAC (MP(SPECL[`n:num`;`5`]DIVISION)(ARITH_RULE`~(5=0)`)) THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN MAP_EVERY ABBREV_TAC [`q = n DIV 5`;`r = n MOD 5`] THEN SIMP_TAC [NUM_R…
let def0 = new_definition `f0 n = n EXP 2 + n + 1` ;; let def1 = new_definition `prop1 n <=> ~((f0 n) MOD 5 = 0)` ;; let lem0 = prove (`prop2 0`, SIMP_TAC[def0;def1;def2] THEN ARITH_TAC);; let lem1 = prove (`!n. f0 (SUC (SUC (SUC (SUC (SUC…
let def0 = new_definition `f0 n = n EXP 2 + n + 1` ;; let def1 = new_definition `prop1 n <=> ~((f0 n) MOD 5 = 0)` ;; let def2 = new_definition `prop2 n <=> prop1 n /\ prop1 (SUC n) /\ prop1 (SUC (SUC n)) /\ prop1 (SUC (SUC (SUC n))) /\ pro…
#use "Library/prime.ml" ;; g `!p. prime p ==> !n. (n EXP p == n) (mod p)` ;; e( REPEAT STRIP_TAC );; e( MP_TAC (UNDISCH(SPEC_ALL PRIME_COPRIME_STRONG)) THEN STRIP_TAC );; e( FIRST_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM CONG_0] ) ) );; e( …
仮定が親切過ぎたかと思い formulas(assumptions). all x all y all z (x <= y <-> (x < y | x = y)). all x all y all z (x < y & y < z -> x < z). all x -(x < x). end_of_list. に変更しても，ご覧の通りです． ============================== PROOF ==…
前回の最後に MESON が証明した定理式を Prover9 に与えると．．． 瞬時に以下のように証明してくれます． ============================== Prover9 =============================== Prover9 (32) version Dec-2007, Dec 2007. ===========================…
f は次数，主係数が正の整数係数一変数多項式なら十分ですが，原題の３次式にしました．N は任意の自然数です． let lemma01 = prove (`!x f. f 0 < x /\ (!n. f n < x ==> f (SUC n) < x) ==> !n. f n < x`, REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC…
all,exists の inference rules を証明させます． %for Prover9 ( %LAE ((all y all x (r(y)->q(x,y)))&(all y ((all x q(x,y))->p(y)) )) ->(all y (r(y)->p(y))) )&( %weak LAE LAI (all y ((all x q(x,y))->p(y)) ) <->(all y exists x (q(x,y)->p(y))) )…
