今回は分数不等式についての証明です． 4変数の3次分数式は，CADによるQEでは難しいようです． Reduce[ForAll[ {a, b, c, d}, a >= 0 && b >= 0 && c >= 0 && d >= 0 && a + b + c + d == 4, a/(a^3 + 8) + b/(b^3 + 8) + c/(c^3 + 8) + d/(d^3 + 8) ... 一…

チェビシェフの多項式を書き下すことは難しくありません．まず，引数の処理に用いる，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_num…

先に定義したチェビシェフの多項式が定める関数による[-1,1]の像が[-1,1]に含まれることは，余弦の逆関数 # ACS;; val it : thm = |- !y. -- &1 ==> &0 acs y /\ acs y acs y) = y についての # ACS_COS;; val it : thm = |- !y. -- &1 cos (acs y) = y から…

では，証明です． # g `!n:num x:real. cheb n (cos(x)) = cos*1 /\ (!x. cheb 1 (cos x) = cos (&1 * x)) /\ (!n. (!x. cheb n (cos x) = cos (&n * x)) /\ (!x. cheb (n + 1) (cos x) = cos (&(n + 1) * x)) ==> (!x. cheb (n + 2) (cos x) = cos (&(n + 2…

次の２つのパッケージの使用例を示します．OCamlの#useの代わりに，HOL Lightのneedsを使うとファイルのリロードが防げます． needs "Library/analysis.ml";; needs "Library/transc.ml";; まずは，チェビシェフの多項式 # let cheb = define `(!x. cheb 0 x…

今回は，任意の集合Aについて，その冪集合2^AからAへの単射が存在しないこと(Cantor)の証明です． 先に示した単射による基数の大小関係の特徴付け # let INJECTIVE_IFF_LEFT_INVERSE = MESON[ MESON`(!a1:A a2:A. f(a1)=f(a2) ==> a1=a2) (!b:B. ?a1:A. !a2:…

等差数列の和の公式の証明です． :num 版 # g`(?a b. !n. x n = a * n + b)==>(!n m. 2 * nsum(m..m+n) x = (SUC n)*( x m + x (m+n) ) )`;; Warning: Free variables in goal: x val it : goalstack = 1 subgoal (1 total)`(?a b. !n. x n = a * n + b) ==>…

今回は，分数関数の和の例です．キーとなるthmは，:realの元の和sumについての # SUM_CLAUSES_NUMSEG;; val it : thm = |- (!m. sum (m..0) f = (if m = 0 then f 0 else &0)) /\ (!m n. sum (m..SUC n) f = (if m です． 先に述べたmからの帰納法，INDUCTm_…

前節の基数の大小関係の2通りの特徴付けのうち，単射Ｎ×Ｎ→Ｎの存在を示して，|Ｎ×Ｎ|≦|Ｎ|を確かめましょう．実際 # let cantor = new_definition `cantor(x,y) = ((x + y) EXP 2 + 3 * x + y) DIV 2`;; val cantor : thm = |- !x y. cantor (x,y) = ((x + …

20世紀の数学の中で最も劇的な進展は，無限集合の体系的利用でしょう．その基礎は，濃度（基数）と順序数の概念です．それらは有限集合の大きさの数え上げと比較のアイデアを無限集合に拡張したものです．■ まず，述語 FINITE で特徴付けられる，有限集合に…

これまで述べなかった述語あるいは集合に対する作用子の一つとして，選択関数@(:(A->bool)->bool)があります．それは，!や?と同じくbinder（従って，括弧付きで用いられるもの）であり，述語 P に対して (@)P は，Pを満たす元があるならその一つ（何れかは不…

■ HOL Lightにおいては，集合は，述語と見做せるよう定義されています． let IN = new_definition `!P:A->bool. !x. x IN P P x`;; ■ 集合のconstantには (typ) (typは:num，:realなどのhol.type) EMPTY or {} UNIV があり，UNIVは # `x+ &1 IN UNIV`;; val …

HOL Light上で関数を定義する道具としては，new_definition(: term -> thm = )は既に述べましたが，例えば # let fib = new_definition `fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;; Exception: Failure "new_definition: term not c…

m:numから始まる帰納法の原理numm_INDUCTIONを証明し，それを適用するtactic，INDUCTm_TACを定義しましょう． まずは肩慣らしに，1から始まるものを証明して見ます． g ( `!P. P 1 /\ (!n. 1 P n ==> P (SUC n) ) ==> (!n. 1 P n)` );; e ( STRIP_TAC THEN S…

これまでの知識＋αを用いて，帰納法による証明を幾つか作って見ましょう．■ :num 上の不等式についてのthm |- !n. 2 EXP n >= 1 + n ポイントは # EXP;; val it : thm = |- (!m. m EXP 0 = 1) /\ (!m n. m EXP SUC n = m * m EXP n) および，帰納法の仮定の…

今回は # g( `!p q. p*p=2*q*q ==> q=0` );; val it : goalstack = 1 subgoal (1 total)`!p q. p * p = 2 * q * q ==> q = 0` をpについての wellfounded induction で証明します．方針は，p*p=2*q*qならばpは偶数，p=2r従って2*r*r=q*qと表せて仮定が使える…

通常の帰納法の原理 # num_INDUCTION;; val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n) を用いて，Wellfounded induction（整礎帰納法）の原理 # num_WF;; val it : thm = |- !P. (!n. (!m. m P m) ==> P n) ==> (!n. P n) を証明して…

今回は，特称量化にも対応した一般の半代数系の prover についてです．■ まず，:num，:intにおける線形系のそれは #use "Examples/cooper.ml";; とロードして使う，Cooperのアルゴリズムに基づく関数，COOPER_RULE，INT_COOPERです． # ARITH_RULE `?x. 0=x`…

では，非線形系の自動処理はどの程度実装されているのでしょう？ まず，変数どうしの積を含む方程式系の評価，つまり，環における prover として，NUM_RING，REAL_RINGがあります（INT_RINGはありませんが，環の構造を提供する関数RINGを用いれば実装可能で…

■ prover ARITH_RULE(: term -> thm = )の:int版，:real版としてINT_ARITH，REAL_ARITHがあるわけですが，それらの特徴は ・代数的な並び替えなら非線形でも扱える # INT_ARITH `!a b a' b' D:int. (a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) = (…

今回は，HOL Lightにおける数の体系のお話です． これまでも多くの例で扱ってきたhol_typeが:numであり，これは自然数（非負整数）全体の集合でした．同様に，hol.mlのロードだけで利用できる:int，:realは整数，実数全体の集合であり #use "./Complex/make.…

今回は の帰納法による証明です．まず，左辺の和を # NSUM_CLAUSES_NUMSEG;; val it : thm = |- (!m. nsum (m..0) f = (if m = 0 then f 0 else 0)) /\ (!m n. nsum (m..SUC n) f = (if m という性質を持つnsumで表すと，goalは # g(`!n. nsum(0..n)(\k.2*k)…

便利なtheorem-tacticとtheorem-tacticalを幾つか述べます． ■ ASSUME_TAC thmとして仮定を追加する代わりに，LABELTAC_TAC "ラベル" thm とすると，その仮定にラベルが付けられます（というより，LABEL_TAC "" がASSUME_TACの実体です）．■ また，結論がimp…

前回残した ... val it : goalstack = 1 subgoal (1 total) 0 [`&0 `&0 &0 は，先のsubgoalのx,yを交換したものなので，同様に # e ( DISJ_CASES_TAC ( REAL_ARITH `&0 &0 0 [`&0 1 [`&0 `&0 &0 # e ( ASM_REWRITE_TAC[] );; val it : goalstack = 1 subgoal…

今回は，量化，論理結合，対称式を含んだ # g `!x y:real. &0 (&0 &0 val it : goalstack = 1 subgoal (1 total)`!x y. &0 (&0 &0 を場合分けを用いて証明します．なお，証明自体は，REAL_FIELDでは # REAL_FIELD `!x y. &0 (&0 &0 と失敗しますが，MESONに …

前回述べたように，HOL Lightでは，goalの集まりであるgoalstackを用いて対話的に証明が作成できます．具体的には，*_TAC の名前を持つ，tactic（戦略関数) を，必要に応じてやり直し・訂正を加えながら，goalstackに段階的に適用することで，その中にある自…

HOL Lightでは，CONJやMPといった推論規則を順次適用する証明作成も原理的には可能ですが，得られる中間結果の授受は少し退屈です．これに対して，証明したい論理式termをgoalとして，それを展開してより簡単なsubgoalsの証明に帰する，下から上への証明作成…

さて，rewritingは数学においてごく普通の処理ですから，HOL Lightは，複数のtheoremsを合わせて参照する，より高度なrewriting conversionを提供します． その最も一般的なものが GEN_REWRITE_CONV convl [th1; ...; thn] (: (conv -> conv) -> thm list ->…