PV9
と言うわけで，Examples/prover9.ml にある PROVER9 とのインターフェイスを定理リスト参照型のプルーバー PV9，および，タクティック PV9_TAC として実装すると．．．
# let ths = [REAL_POW_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB;
REAL_SUB_LDISTRIB; REAL_SUB_RDISTRIB;
REAL_ARITH `a + (b - c) = (a + b) - c`;
REAL_ARITH `a - (b - c) = a + (c - b)`;
REAL_ARITH `(a - b) + c = (a + c) - b`;
REAL_ARITH `(a - b) - c = a - (b + c)`;
REAL_ARITH `(a - b = c) = (a = b + c)`;
REAL_ARITH `(a = b - c) = (a + c = b)`;
REAL_ADD_AC; REAL_MUL_AC];;
val ths : thm list =
[|- !x. x pow 2 = x * x; |- !x y z. x * (y + z) = x * y + x * z;
|- !x y z. (x + y) * z = x * z + y * z;
|- !x y z. x * (y - z) = x * y - x * z;
|- !x y z. (x - y) * z = x * z - y * z; |- a + b - c = (a + b) - c;
|- a - (b - c) = a + c - b; |- a - b + c = (a + c) - b;
|- a - b - c = a - (b + c); |- a - b = c <=> a = b + c;
|- a = b - c <=> a + c = b;
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p;
|- m * n = n * m /\ (m * n) * p = m * n * p /\ m * n * p = n * m * p]
# let tm = `(x pow 2 + y pow 2) * (a pow 2 + b pow 2) =
(a * x + b * y) pow 2 + (a * y - b * x) pow 2`;;
val tm : term =
`(x pow 2 + y pow 2) * (a pow 2 + b pow 2) =
(a * x + b * y) pow 2 + (a * y - b * x) pow 2`
# PV9 ths tm;;
-------- Proof 1 --------
THEOREM PROVED
------ process 4040 exit (max_proofs) ------
val it : thm =
|- (x pow 2 + y pow 2) * (a pow 2 + b pow 2) =
(a * x + b * y) pow 2 + (a * y - b * x) pow 2
# MESON ths tm;;
0..0..1..3..8..20..43..226..787..2703..13876..64565..293047..
\log_{2}{3}は有理数ではない
# g `!n. 1<=n ==> EVEN( 2 EXP n )` ;; val it : goalstack = 1 subgoal (1 total) `!n. 1 <= n ==> EVEN (2 EXP n)` # e( INDUCT_TAC );; val it : goalstack = 2 subgoals (2 total) 0 [`1 <= n ==> EVEN (2 EXP n)`] `1 <= SUC n ==> EVEN (2 EXP SUC n)` `1 <= 0 ==> EVEN (2 EXP 0)` # e( ARITH_TAC );; val it : goalstack = 1 subgoal (1 total) 0 [`1 <= n ==> EVEN (2 EXP n)`] `1 <= SUC n ==> EVEN (2 EXP SUC n)` # e( ASM_PV9_TAC [ARITH_RULE `EVEN 2`; EXP; EVEN_MULT] );; -------- Proof 1 -------- THEOREM PROVED ------ process 1676 exit (max_proofs) ------ val it : goalstack = No subgoals # let lem2 = top_thm () ;; val lem2 : thm = |- !n. 1 <= n ==> EVEN (2 EXP n) # let lem3 =PV9 [NOT_EVEN; LE_1; lem1; lem2; EXP; EXP_EQ_1; ARITH_RULE `~(3=1)` ] `3 EXP m = 2 EXP n ==> m=0 /\ n=0` ;; -------- Proof 1 -------- THEOREM PROVED ------ process 7248 exit (max_proofs) ------ val lem3 : thm = |- 3 EXP m = 2 EXP n ==> m = 0 /\ n = 0 # prove ( `~ (?m n. ln (&3) / ln (&2) = &n / &m )`, let lem01 = PV9[real_div; REAL_INV_EQ_0; LN_POS_LT; REAL_ARITH `&1 < &2 /\ &1 < &3`; REAL_POS_NZ; REAL_ENTIRE; REAL_INJ] `ln (&3) / ln (&2) = &n / &m ==> ~(m=0)` in let lem02 = PV9[RAT_LEMMA5; LE_1; REAL_LT; LN_POS_LT; REAL_ARITH `&1 < &2`; REAL_MUL_SYM; lem01] `ln (&3) / ln (&2) = &n / &m ==> &m * ln (&3) = &n * ln (&2)` in let lem03 = PV9[REAL_ARITH `&0 < &2 /\ &0 < &3`; LN_POW; REAL_OF_NUM_POW; LN_INJ; REAL_POW_LT; REAL_INJ] `&m * ln (&3) = &n * ln (&2) ==> 3 EXP m = 2 EXP n` in PV9_TAC [lem01; lem02; lem03; lem3] ) ;; -------- Proof 1 -------- THEOREM PROVED ------ process 10060 exit (max_proofs) ------ -------- Proof 1 -------- THEOREM PROVED ------ process 6024 exit (max_proofs) ------ -------- Proof 1 -------- THEOREM PROVED ------ process 9728 exit (max_proofs) ------ -------- Proof 1 -------- THEOREM PROVED ------ process 4892 exit (max_proofs) ------ val it : thm = |- ~(?m n. ln (&3) / ln (&2) = &n / &m)
