2013年東京大学理科前期第５問 by HOL Light.

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 THEN ASM_MESON_TAC []);;

let lemma02 = MESON [REAL_NOT_LT; lemma01 ] `!x f. f 0 < x /\ (?m. x <= f m) ==> (?m. f m < x /\ x <= f (SUC m))` ;;

let lemma03 = MESON [REAL_NOT_LE; lemma02] `!x y f. x<y ==>  f 0 < x /\  (?m. x <= f m) ==> (!m. ~(x <= f m /\ f m < y) ) ==> (?m. f m < x /\ y <= f (SUC m))` ;;

let lemma04 = MESON[REAL_ARCH_SIMPLE; REAL_POS; REAL_SOS `&0<= &m ==> &m <= &m*(&1+ &m)*(&2+ &m)`; REAL_LE_TRANS] `!x. ?m. x <= &m*(&1+ &m)*(&2+ &m)` ;;


g `!x y. &0<x /\ x<y ==> (!m. ~(x <= &m*(&1+ &m)*(&2+ &m) /\ &m*(&1+ &m)*(&2+ &m) < y) ) ==> (?m. &m*(&1+ &m)*(&2+ &m) < x /\ y <= &(SUC m)*(&1+ &(SUC m))*(&2+ &(SUC m)))` ;;
e( REPEAT STRIP_TAC );;
e( SUBST_ALL_TAC (REAL_ARITH`&0 = &0*(&1+ &0)*(&2+ &0)`) );;
e( ASSUME_TAC (SPEC `x:real` lemma04)  );;
e( ASM_MESON_TAC [SPECL [`x:real`; `y:real`; `(\m. &m*(&1+ &m)*(&2+ &m))`] lemma03] );;
let lemma05 = top_thm () ;;




let lemma0505 = SPECL[`(&N)*(&10 pow n)`;`(&N+ &1)*(&10 pow n)`]lemma05;;

g `!N n.  0<N ==> &0 < &N * &10 pow n /\ &N * &10 pow n < (&N + &1) * &10 pow n` ;;
e( REPEAT STRIP_TAC );;
e( ASM_MESON_TAC [REAL_POW_LT;REAL_OF_NUM_LT;REAL_ARITH `&0< &10`;REAL_LT_MUL] );;
e( ASM_MESON_TAC [REAL_POW_LT;REAL_ARITH`&N< &N+ &1`;REAL_ARITH `&0< &10`;REAL_LT_RMUL] );;
let lemma051 = top_thm () ;;





let lemma055 = MESON [REAL_ARCH; REAL_ARITH `&0< &N + &1`; REAL_MUL_AC] `!N. ?n. &6 + &33 * &N + &54 * ( &N pow 2) + &27 *(&N pow 3) < (&N + &1)*( &n)` ;;

g `!n. &n+ &1 <= &10 pow n` ;;
e( INDUCT_TAC );;
e( REWRITE_TAC [pow] THEN ARITH_TAC );;
e( REWRITE_TAC [pow] THEN REWRITE_TAC [REAL] THEN ASM_REAL_ARITH_TAC );;
let lemma056 = top_thm () ;;

g `!N n.  (&N+ &1)*(&n)<(&N+ &1)*(&10 pow n)` ;;
e( REPEAT GEN_TAC );;
e( MATCH_MP_TAC REAL_LT_LMUL );;
e( CONJ_TAC );;
e( REAL_ARITH_TAC );;
e( MP_TAC (SPEC`n:num`lemma056) THEN REAL_ARITH_TAC );;
let lemma057 = top_thm () ;;

let lemma058 = MESON [lemma055; lemma057; REAL_LT_TRANS] `!N. 0<N ==> ?n. &6 + &33 * &N + &54 * ( &N pow 2) + &27 *(&N pow 3) < (&N + &1)*(&10 pow n)` ;;


g `!N n. 0<N ==> &6 + &33 * &N + &54 * ( &N pow 2) + &27 *(&N pow 3) < (&N + &1)*(&10 pow n) ==> (!m. ~(&N * &10 pow n <= &m * (&1 + &m) * (&2 + &m) /\ &m * (&1 + &m) * (&2 + &m) < (&N + &1) * &10 pow n)) ==> (?m. &m * (&1 + &m) * (&2 + &m) < &N * &10 pow n /\ (&N + &1) * &10 pow n <= &(SUC m) * (&1 + &(SUC m)) * (&2 + &(SUC m)))` ;;
e( MESON_TAC [lemma0505; lemma051]   );;
let lemma059 = top_thm () ;;



let lemma06 = REAL_SOS `&0<= &m /\ &0<= &N ==> &m*(&1+ &m)*(&2+ &m) <  &N * (&10  pow n) /\ (&N+ &1)*(&10  pow n) <= &(SUC m)*(&1+ &(SUC m))*(&2+ &(SUC m)) ==> (&N+ &1)*(&m)*(&1+ &m)*(&2+ &m)< &N*(&(SUC m))*(&1+ &(SUC m))*(&2+ &(SUC m))` ;;
let lemma065 = MESON [REAL] `&(SUC m)*(&1+ &(SUC m))*(&2+ &(SUC m)) = (&m+ &1)*(&1+ (&m+ &1))*(&2+ (&m+ &1))`;;

let lemma07 = REAL_SOS `&0<= &m /\ &0<= &N /\ (&N+ &1)*(&m)*(&1+ &m)*(&2+ &m)< &N*((&m+ &1)*(&1+ (&m+ &1))*(&2+ (&m+ &1))) ==> &m < &3* &N` ;;

let lemma08 = REAL_SOS `&0<= &m /\ &0<= &N /\ &m < &3* &N ==> (&m+ &1)*(&1+ (&m+ &1))*(&2+ (&m+ &1)) < &6 + &33 * &N + &54 * ( &N pow 2) + &27 *(&N pow 3)` ;;


let lemma0679 =MESON[lemma06;lemma065;lemma07;lemma08;REAL_POS] `&m*(&1+ &m)*(&2+ &m) <  &N * (&10  pow n) ==> (&N+ &1)*(&10  pow n) <= &(SUC m)*(&1+ &(SUC m))*(&2+ &(SUC m)) ==> &(SUC m)*(&1+ &(SUC m))*(&2+ &(SUC m)) < &6 + &33 * &N + &54 * ( &N pow 2) + &27 *(&N pow 3)`;;


(* *)

g `!N. 0<N ==> ?n m. &N * (&10 pow n) <= (&m)*(&1+ &m)*(&2+ &m) /\ (&m)*(&1+ &m)*(&2+ &m) < (&N + &1) * (&10 pow n)` ;;
e( REPEAT STRIP_TAC );;
e( MP_TAC (UNDISCH(SPEC`N:num`lemma058)) THEN STRIP_TAC );;
e( REWRITE_TAC [MESON[] `(?n m. P m n) <=> ~(!n m. ~(P m n))`] );;
e( STRIP_TAC );;
e( POP_ASSUM (ASSUME_TAC o (SPEC`n:num`) )  );;
e( ASSUME_TAC (UNDISCH_ALL (SPECL[ `N:num`; `n:num`] lemma059 ) )  );;
e( POP_ASSUM MP_TAC THEN STRIP_TAC  );;
e( ASSUME_TAC (UNDISCH_ALL lemma0679 ) );;
e( ASM_REAL_ARITH_TAC );;
let thm1 = top_thm () ;;

g `!N. ?n m. &N * (&10 pow n) <= (&m)*(&1+ &m)*(&2+ &m) /\ (&m)*(&1+ &m)*(&2+ &m) < (&N + &1) * (&10 pow n)` ;;
e( GEN_TAC );;
e( DISJ_CASES_TAC  (ARITH_RULE `0<N \/ N=0` )  );;
e( ASM_SIMP_TAC [thm1]  );;
e( EXISTS_TAC `0` THEN EXISTS_TAC `0` THEN ASM_REWRITE_TAC [pow] );;
e( ASM_REAL_ARITH_TAC );;
let thm = top_thm () ;;

val thm : thm =
  |- !N. ?n m.
             &N * &10 pow n <= &m * (&1 + &m) * (&2 + &m) /\
             &m * (&1 + &m) * (&2 + &m) < (&N + &1) * &10 pow n

一般の場合は，次のような構成になります．

# MESON [REAL_ARITH `a<=L /\ L<x /\ x<y /\ y<=a:real ==> F`;]
`    (?M. !m. (&N + &1) * f m - &N * f (SUC m) < &0 ==> m <= M) /\
     (!M. ?L. !m. m <= M ==> f (SUC m) <= L) /\
     (!L. ?n. f 0 < &N * &10 pow n /\ L < &N * &10 pow n) /\
     (!n. ?m. &N * &10 pow n <= f m) /\
     (!n. &N * &10 pow n < (&N + &1) * &10 pow n) /\
     (!x y.
          x < y
          ==> f 0 < x
          ==> (?m. x <= f m)
          ==> (!m. ~(x <= f m /\ f m < y))
          ==> (?m. f m < x /\ y <= f (SUC m))) /\
     (!z m.
          f m < &N * z /\ (&N + &1) * z <= f (SUC m)
          ==> (&N + &1) * f m - &N * f (SUC m) < &0)
     ==> (?n m. &N * &10 pow n <= f m /\ f m < (&N + &1) * &10 pow n)
       `;;
0..0..0..2..4..11..26..41..64..87..110..137..164..191..220..301..382..706..1040.
.1374..1784..2206..2628..3094..3660..4226..5271..6558..7845..10360..12896..15432
..18437..21535..24633..28413..32300..36187..41173..46224..51275..57051..63003..6
8955..76613..solved at 81869
val it : thm =
  |- (?M. !m. (&N + &1) * f m - &N * f (SUC m) < &0 ==> m <= M) /\
     (!M. ?L. !m. m <= M ==> f (SUC m) <= L) /\
     (!L. ?n. f 0 < &N * &10 pow n /\ L < &N * &10 pow n) /\
     (!n. ?m. &N * &10 pow n <= f m) /\
     (!n. &N * &10 pow n < (&N + &1) * &10 pow n) /\
     (!x y.
          x < y
          ==> f 0 < x
          ==> (?m. x <= f m)
          ==> (!m. ~(x <= f m /\ f m < y))
          ==> (?m. f m < x /\ y <= f (SUC m))) /\
     (!z m.
          f m < &N * z /\ (&N + &1) * z <= f (SUC m)
          ==> (&N + &1) * f m - &N * f (SUC m) < &0)
     ==> (?n m. &N * &10 pow n <= f m /\ f m < (&N + &1) * &10 pow n)

従って，この前件の各式を

 `0<N /\ 0<d /\ &0<a d /\ (!m. f m = sum (0..d) (\k. a k * &m pow k))`

から導けば

`!N d a f.
     0 < N /\
     0 < d /\
     &0 < a d /\
     (!m. f m = sum (0..d) (\k. a k * &m pow k))
     ==> (?n m. &N * &10 pow n <= f m /\ f m < (&N + &1) * &10 pow n)`

が定理式になります．