不等式の性質 by HOL4.

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. Incomplete goalstack:
         Initial goal:

         !s t a b.
           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


     : proofs
- e( REPEAT STRIP_TAC THEN Induct_on `n` );
OK..
2 subgoals:
> val it =

    (s * a + t * b) pow SUC n <= s * a pow SUC n + t * b pow SUC n
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n


    (s * a + t * b) pow 0 <= s * a pow 0 + t * b pow 0
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
     : proof
- e( METIS_TAC [pow, REAL_MUL_RID, REAL_LE_REFL] );
OK..
metis: r[+0+11]+0+0+0+0+0+0+1+0+1+1+1+0+0#

Goal proved.
 [s + t = 1, 0 <= a, 0 <= b, 0 <= s, 0 <= t]
|- (s * a + t * b) pow 0 <= s * a pow 0 + t * b pow 0

Remaining subgoals:
> val it =

    (s * a + t * b) pow SUC n <= s * a pow SUC n + t * b pow SUC n
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n
     : proof
- e( REWRITE_TAC [pow] );
OK..
1 subgoal:
> val it =

    (s * a + t * b) * (s * a + t * b) pow n <=
    s * (a * a pow n) + t * (b * b pow n)
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n
     : proof
- val lem1 = PROVE [REAL_LE_MUL, REAL_LE_ADD]``!s t a b:real. 0 <= s ==> 0 <= t ==> 0 <= a ==> 0 <= b ==> 0 <= s*a + t*b``;
Meson search level: ..........
> val lem1 =
     []
    |- !s t a b.
         0 <= s ==> 0 <= t ==> 0 <= a ==> 0 <= b ==> 0 <= s * a + t * b : thm
- val lem2 = SPECL [``s*a + t*b:real``,``(s*a + t*b) pow n``,``s*a pow n + t*b pow n``] REAL_LE_LMUL_IMP;
> val lem2 =
     []
    |- 0 <= s * a + t * b /\
       (s * a + t * b) pow n <= s * a pow n + t * b pow n ==>
       (s * a + t * b) * (s * a + t * b) pow n <=
       (s * a + t * b) * (s * a pow n + t * b pow n) : thm
- e( SUBGOAL_THEN ``(s*a + t*b) * (s*a pow n + t*b pow n) <= s * (a * a pow n) + t * (b * b pow n)``  (fn t => MAP_EVERY MP_TAC [t,SPEC_ALL lem1,lem2]
 THEN PROVE_TAC [REAL_LE_TRANS] )  );
OK..
Meson search level: ................................
1 subgoal:
> val it =

    (s * a + t * b) * (s * a pow n + t * b pow n) <=
    s * (a * a pow n) + t * (b * b pow n)
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n
     : proof
- val lem3 = EQT_ELIM (SIMP_CONV (real_ss ++ REAL_ARITH_ss) [GSYM REAL_EQ_SUB_LADD] ``!s t a b x y:real. (s+t=1) ==> (s * (a * x) + t * (b * y) - (s *
 a + t * b) * (s * x + t * y)=(b-a)*(y-x)*s*t)``);
> val lem3 =
     []
    |- !s t a b x y.
         (s + t = 1) ==>
         (s * (a * x) + t * (b * y) - (s * a + t * b) * (s * x + t * y) =
          (b - a) * (y - x) * s * t) : thm
- e( ONCE_REWRITE_TAC [GSYM REAL_SUB_LE]  );
OK..
1 subgoal:
> val it =

    0 <=
    s * (a * a pow n) + t * (b * b pow n) -
    (s * a + t * b) * (s * a pow n + t * b pow n)
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n
     : proof
- e( REWRITE_TAC [UNDISCH(SPEC_ALL lem3)]  );
OK..
1 subgoal:
> val it =

    0 <= (b - a) * (b pow n - a pow n) * s * t
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n
     : proof
- e( METIS_TAC [POW_LE, REAL_SUB_LE, REAL_LE_MUL, REAL_LE_TOTAL,  REAL_NEG_MUL2, REAL_NEG_SUB]  );
OK..
metis: r[+0+16]+0+0+0+0+0+0+0+0+2+0+0+0+0+0+2+0+1+0+0+5+1+1+7+1+1+1+0+2+1+2+1+1#

Goal proved.

[s + t = 1, 0 <= a, 0 <= b, 0 <= s, 0 <= t,
 (s * a + t * b) pow n <= s * a pow n + t * b pow n]
|- 0 <= (b - a) * (b pow n - a pow n) * s * t

Goal proved.

[s + t = 1, 0 <= a, 0 <= b, 0 <= s, 0 <= t,
 (s * a + t * b) pow n <= s * a pow n + t * b pow n]
|- 0 <=
   s * (a * a pow n) + t * (b * b pow n) -
   (s * a + t * b) * (s * a pow n + t * b pow n)

Goal proved.

[s + t = 1, 0 <= a, 0 <= b, 0 <= s, 0 <= t,
 (s * a + t * b) pow n <= s * a pow n + t * b pow n]
|- (s * a + t * b) * (s * a pow n + t * b pow n) <=
   s * (a * a pow n) + t * (b * b pow n)

Goal proved.

[s + t = 1, 0 <= a, 0 <= b, 0 <= s, 0 <= t,
 (s * a + t * b) pow n <= s * a pow n + t * b pow n]
|- (s * a + t * b) * (s * a + t * b) pow n <=
   s * (a * a pow n) + t * (b * b pow n)

Goal proved.

[s + t = 1, 0 <= a, 0 <= b, 0 <= s, 0 <= t,
 (s * a + t * b) pow n <= s * a pow n + t * b pow n]
|- (s * a + t * b) pow SUC n <= s * a pow SUC n + t * b pow SUC n
> val it =
    Initial goal proved.
     []
    |- !s t a b.
         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 : proof
-