Example (17.1)

前回の実行結果です．

# 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`

# e(ONCE_REWRITE_TAC[ARITH_RULE`x<y<=>x-y< &0`; ]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 < a`]
  1 [`&0 < b`]

`a * c - b * d < &0 <=> c / b - d / a < &0`

# e(ASM_SIMP_TAC[RAT_LEMMA3]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 < a`]
  1 [`&0 < b`]

`a * c - b * d < &0 <=> (c * a - d * b) * inv b * inv a < &0`

# e(ASM_SIMP_TAC[REAL_SOSFIELD`&0<x ==>(a*b* inv(x)< &0 <=> a*b< &0)`]);;
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Translating proof certificate to HOL
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Searching with depth limit 5
Translating proof certificate to HOL
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 < a`]
  1 [`&0 < b`]

`a * c - b * d < &0 <=> (c * a - d * b) * inv b < &0`

# e(ASM_SIMP_TAC[REAL_SOSFIELD`&0<x ==>(a* inv(x)< &0 <=> a< &0)`] THEN REAL_ARI
TH_TAC);;
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Translating proof certificate to HOL
val it : goalstack = No subgoals

# let lemma1=top_thm();;
val lemma1 : thm =
  |- !a b c d. &0 < a /\ &0 < b ==> (a * c < b * d <=> c / b < d / a)
#
  let lemma2=MESON[
  REAL_FIELD`&0< &n ==> (!x. &n <= x /\ x <= &n + &1 ==> &0<x /\ ~(x= &0))`;
  DIFF_CONV`(\x. ln x / x)`;
  ]`&0< &n ==> (!x. &n <= x /\ x <= &n + &1
       ==> ((\x. ln x / x) diffl ((inv x * &1) * x - &1 * ln x) / x pow 2) x)`;;

2 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
0..0..1..2..4..10..21..38..60..86..solved at 143
val lemma2 : thm =
  |- &0 < &n
     ==> (!x. &n <= x /\ x <= &n + &1
              ==> ((\x. ln x / x) diffl
                   ((inv x * &1) * x - &1 * ln x) / x pow 2)
                  x)
#
  let lemma3=REAL_SOSFIELD`&0<z ==>(((&n + &1) - &n) * ((inv z * &1) * z - &1 *
ln z) / z pow 2 < &0<=> &1 < ln z)`;;
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Searching with depth limit 5
Translating proof certificate to HOL
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Searching with depth limit 5
Searching with depth limit 6
csdp warning: Reduced accuracy
Searching with depth limit 7
Translating proof certificate to HOL
val lemma3 : thm =
  |- &0 < z
     ==> (((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2 < &0 <=>
          &1 < ln z)
#
  let lemma4=MESON
  [
  REAL_FIELD`inv (&2) <= ln (&2)<=> &1<= &2*ln(&2)`;
  MP (GSYM(SPECL[`2`;`&2`]LN_POW)) (REAL_FIELD`&0< &2`);
  REAL_FIELD`&2 pow 2 = &4`;
  ]`inv (&2) <= ln (&2)<=> &1<=ln(&4)`;;
1 basis elements and 0 critical pairs
1 basis elements and 0 critical pairs
0..0..1..2..3..7..13..21..39..solved at 49
0..0..solved at 2
0..0..solved at 4
0..0..3..6..9..21..37..55..89..125..solved at 148
val lemma4 : thm = |- inv (&2) <= ln (&2) <=> &1 <= ln (&4)
#
  g`!n. 3<=n ==> (&n + &1) pow n < &n pow (n + 1)`;;
val it : goalstack = 1 subgoal (1 total)

`!n. 3 <= n ==> (&n + &1) pow n < &n pow (n + 1)`

# e(REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]

`(&n + &1) pow n < &n pow (n + 1)`

# e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`3<=n==>(n=3 \/ 4<=n)`)));;
val it : goalstack = 2 subgoals (2 total)

  0 [`3 <= n`]
  1 [`4 <= n`]

`(&n + &1) pow n < &n pow (n + 1)`

  0 [`3 <= n`]
  1 [`n = 3`]

`(&n + &1) pow n < &n pow (n + 1)`

# e(ASM_SIMP_TAC[ARITH] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]

`(&n + &1) pow n < &n pow (n + 1)`

# e(DISJ_CASES_TAC(UNDISCH(ARITH_RULE`4<=n==>(n=4 \/ 5<=n)`)));;
val it : goalstack = 2 subgoals (2 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]

`(&n + &1) pow n < &n pow (n + 1)`

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`n = 4`]

`(&n + &1) pow n < &n pow (n + 1)`

# e(ASM_SIMP_TAC[ARITH] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]

`(&n + &1) pow n < &n pow (n + 1)`

#

  e(MP_TAC (ARITH_RULE`&3<= &n==> &3<= &n /\ &0< &n + &1 /\ &0< &n /\ &n < &n +
&1`) THEN ASM_SIMP_TAC[REAL_LE] THEN REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]

`(&n + &1) pow n < &n pow (n + 1)`

# e(MP_TAC (MESON[REAL_POW_LT]`&0< &n + &1 /\ &0< &n ==> &0 < (&n + &1) pow n /\
 &0 < &n pow (n + 1)`) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ASM_SIMP_T
AC[GSYM LN_MONO_LT; LN_POW; GSYM REAL_ADD; lemma1]);;
0..0..1..solved at 4
0..0..1..solved at 4
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]

`ln (&n + &1) / (&n + &1) < ln (&n) / &n`

# e(ASM_SIMP_TAC[lemma1]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]

`ln (&n + &1) / (&n + &1) < ln (&n) / &n`

# e(MP_TAC (SPECL[`\x. ln x /x`;`\x. ((inv x * &1) * x - &1 * ln x) / x pow 2`;`
&n:real`;`&n+ &1`]MVT_ALT) THEN BETA_TAC THEN ASM_SIMP_TAC[]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]

`((!x. &n <= x /\ x <= &n + &1
       ==> ((\x. ln x / x) diffl ((inv x * &1) * x - &1 * ln x) / x pow 2) x)
  ==> (?z. &n < z /\
           z < &n + &1 /\
           ln (&n + &1) / (&n + &1) - ln (&n) / &n =
           ((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2))
 ==> ln (&n + &1) / (&n + &1) < ln (&n) / &n`

# e(ASSUME_TAC(UNDISCH lemma2) THEN ASM_SIMP_TAC[] THEN FIRST_X_ASSUM(fun t->ALL
_TAC) THEN REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[ARITH_RULE`x<y<=>x-y< &0`] THE
N ASM_SIMP_TAC[]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]
  8 [`&n < z`]
  9 [`z < &n + &1`]
 10 [`ln (&n + &1) / (&n + &1) - ln (&n) / &n =
      ((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2`]

`((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2 < &0`

# e(MP_TAC (REAL_ARITH`&0< &n /\ &n<z ==> &0<z`) THEN ASM_SIMP_TAC[] THEN STRIP_
TAC THEN ASM_REWRITE_TAC[UNDISCH lemma3]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]
  8 [`&n < z`]
  9 [`z < &n + &1`]
 10 [`ln (&n + &1) / (&n + &1) - ln (&n) / &n =
      ((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2`]
 11 [`&0 < z`]

`&1 < ln z`

# e(MP_TAC (SPEC`inv(&2)`REAL_EXP_BOUND_LEMMA) THEN SIMP_TAC[REAL_ARITH`&0 <= in
v (&2) /\ inv (&2) <= inv (&2) /\ &1 + &2 * inv (&2) = &2`] );;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]
  8 [`&n < z`]
  9 [`z < &n + &1`]
 10 [`ln (&n + &1) / (&n + &1) - ln (&n) / &n =
      ((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2`]
 11 [`&0 < z`]

`exp (inv (&2)) <= &2 ==> &1 < ln z`

#
  e(REWRITE_TAC[MESON[REAL_ARITH`&0< &2`; EXP_LN; ]`x<= &2<=>x<=exp(ln(&2))`; RE
AL_EXP_MONO_LE; lemma4]);;
0..0..1..2..3..7..13..21..solved at 34
0..0..1..2..3..7..solved at 14
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]
  8 [`&n < z`]
  9 [`z < &n + &1`]
 10 [`ln (&n + &1) / (&n + &1) - ln (&n) / &n =
      ((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2`]
 11 [`&0 < z`]

`&1 <= ln (&4) ==> &1 < ln z`

#
  let lemma5=MESON[REAL_ARITH`&0< &4 /\ &0< &5 /\ &4< &5`; LN_MONO_LT]`ln(&4)<ln
(&5)`;;
0..0..1..2..3..solved at 9
val lemma5 : thm = |- ln (&4) < ln (&5)
#
  e(ASSUME_TAC lemma5);;
val it : goalstack = 1 subgoal (1 total)

  0 [`3 <= n`]
  1 [`4 <= n`]
  2 [`5 <= n`]
  3 [`&0 < &n + &1`]
  4 [`&0 < &n`]
  5 [`&n < &n + &1`]
  6 [`&0 < (&n + &1) pow n`]
  7 [`&0 < &n pow (n + 1)`]
  8 [`&n < z`]
  9 [`z < &n + &1`]
 10 [`ln (&n + &1) / (&n + &1) - ln (&n) / &n =
      ((&n + &1) - &n) * ((inv z * &1) * z - &1 * ln z) / z pow 2`]
 11 [`&0 < z`]
 12 [`ln (&4) < ln (&5)`]

`&1 <= ln (&4) ==> &1 < ln z`

#
  e(ASSUME_TAC (REAL_ARITH`&0< &5`) THEN MP_TAC (MESON[
  GSYM REAL_LE;
  REAL_LET_TRANS;
  LN_MONO_LT]
  `5 <= n /\ &n<z /\ &0< &5 /\ &0<z ==> ln(&5)<ln(z)`) THEN ASM_SIMP_TAC[] THEN
ASM_REAL_ARITH_TAC);;
0..0..1..2..4..10..17..25..solved at 37
val it : goalstack = No subgoals