miz3/Samples/icms.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* From Multivariate/misc.ml                                                 *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 prioritize_real();;
   6
   7 let REAL_POW_LBOUND = prove
   8  (`!x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n`,
   9   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  10   INDUCT_TAC THEN
  11   REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_ADD_RID; REAL_LE_REFL] THEN
  12   REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN
  13   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(&1 + x) * (&1 + &n * x)` THEN
  14   ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ARITH `&0 <= x ==> &0 <= &1 + x`] THEN
  15   ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_ARITH
  16    `&1 + (n + &1) * x <= (&1 + x) * (&1 + n * x) <=> &0 <= n * x * x`]);;
  17
  18 let REAL_ARCH_POW = prove
  19  (`!x y. &1 < x ==> ?n. y < x pow n`,
  20   REPEAT STRIP_TAC THEN
  21   MP_TAC(SPEC `x - &1` REAL_ARCH) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
  22   DISCH_THEN(MP_TAC o SPEC `y:real`) THEN MATCH_MP_TAC MONO_EXISTS THEN
  23   X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
  24   EXISTS_TAC `&1 + &n * (x - &1)` THEN
  25   ASM_SIMP_TAC[REAL_ARITH `x < y ==> x < &1 + y`] THEN
  26   ASM_MESON_TAC[REAL_POW_LBOUND; REAL_SUB_ADD2; REAL_ARITH
  27     `&1 < x ==> &0 <= x - &1`]);;
  28
  29 let ABS_CASES = thm `;
  30   !x. x = &0 \/ &0 < abs(x)`;;
  31
  32 let LL =  REAL_ARITH `&1 < k ==> &0 < k`;;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* Miz3 solutions to IMO problem from ICMS 2006.                             *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 horizon := 0;;
  39
  40 let IMO_1 = thm `;
  41   !k. &1 < k ==> &0 < k [LL] by REAL_ARITH;
  42   now
  43     let f g be real->real;
  44     let x be real;
  45     assume !x y. f (x + y) + f (x - y) = &2 * f x * g y [1];
  46     assume ~(!x. f x = &0) [2];
  47     assume !x. abs (f x) <= &1 [3];
  48     now
  49       let k be real;
  50       assume sup (IMAGE (\x. abs (f x)) (:real)) = k [4];
  51       ~(IMAGE (\x. abs (f x)) (:real) = {}) /\ (?b. !x. abs (f x) <= b) [5]
  52         by ASM SET_TAC[],-,3;
  53       now
  54         assume !x. abs (f x) <= k [6];
  55         assume !b. (!x. abs (f x) <= b) ==> k <= b [7];
  56         now
  57           let y be real;
  58           assume &1 < abs (g y) [8];
  59           !x. abs (f x) <= k / abs (g y) [9]
  60             by ASM_MESON_TAC[REAL_LE_RDIV_EQ; REAL_ABS_MUL; LL;
  61               REAL_ARITH (parse_term
  62                 "u + v = &2 * z /\\ abs u <= k /\\ abs v <= k ==> abs z <= k")
  63              ],-,1,6;
  64           ~(k <= k / abs (g y))
  65             by TIMED_TAC 2
  66               (ASM_MESON_TAC[REAL_NOT_LE; REAL_LT_LDIV_EQ; REAL_LT_LMUL;
  67                  REAL_MUL_RID; LL; REAL_ARITH (parse_term
  68                   "~(z = &0) /\\ abs z <= k ==> &0 < k")
  69                 ]),LL,2,6,8;
  70           (!x. abs (f x) <= k / abs (g y)) /\ ~(k <= k / abs (g y))
  71             by CONJ_TAC,-,9;
  72           ((!x. abs (f x) <= k / abs (g y)) ==> k <= k / abs (g y)) ==> F
  73             by SIMP_TAC[NOT_IMP; NOT_FORALL_THM],-;
  74           thus F by FIRST_X_ASSUM(MP_TAC o
  75             SPEC (parse_term "k / abs(g(y:real))")),-,7;
  76         end;
  77         ~(?y. &1 < abs (g y)) by STRIP_TAC,-;
  78         thus !y. abs (g y) <= &1
  79           by SIMP_TAC[GSYM REAL_NOT_LT; GSYM NOT_EXISTS_THM],-;
  80       end;
  81       (!x. abs (f x) <= k) /\ (!b. (!x. abs (f x) <= b) ==> k <= b)
  82       ==> (!y. abs (g y) <= &1) by STRIP_TAC,-;
  83       (~(IMAGE (\x. abs (f x)) (:real) = {}) /\ (?b. !x. abs (f x) <= b)
  84        ==> (!x. abs (f x) <= k) /\ (!b. (!x. abs (f x) <= b) ==> k <= b))
  85       ==> (!y. abs (g y) <= &1) by ANTS_TAC,-,5;
  86       (~(IMAGE (\x. abs (f x)) (:real) = {}) /\
  87        (?b. !x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
  88        ==> (!x. x IN IMAGE (\x. abs (f x)) (:real)
  89                 ==> x <= sup (IMAGE (\x. abs (f x)) (:real))) /\
  90            (!b. (!x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
  91                 ==> sup (IMAGE (\x. abs (f x)) (:real)) <= b))
  92       ==> (!y. abs (g y) <= &1)
  93         by ASM_SIMP_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_UNIV],-,4;
  94       thus !y. abs (g y) <= &1
  95         by MP_TAC(SPEC (parse_term "IMAGE (\\x. abs(f(x))) (:real)") SUP),-;
  96     end;
  97     !y. abs (g y) <= &1
  98       by ABBREV_TAC (parse_term "k = sup (IMAGE (\\x. abs(f(x))) (:real))"),-;
  99     thus abs (g x) <= &1
 100       by SPEC_TAC ((parse_term "x:real"),(parse_term "y:real")),-;
 101   end;
 102   thus !f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\
 103              ~(!x. f(x) = &0) /\ (!x. abs(f(x)) <= &1)
 104              ==> !x. abs(g(x)) <= &1 by REPEAT STRIP_TAC,-`;;
 105
 106 horizon := 1;;
 107
 108 let IMO_2 = thm `;
 109   let f g be real->real;
 110   assume !x y. f (x + y) + f (x - y) = &2 * f x * g y [1];
 111   assume ~(!x. f x = &0) [2];
 112   assume !x. abs (f x) <= &1 [3];
 113   thus !x. abs (g x) <= &1
 114   proof set s = IMAGE (\x. abs (f x)) (:real);
 115     ~(s = {}) [4] by SET_TAC;
 116     !b. (!y. y IN s ==> y <= b) <=> (!x. abs (f x) <= b) by IN_IMAGE,IN_UNIV;
 117     set k = sup s;
 118     (!x. abs (f x) <= k) /\ !b. (!x. abs (f x) <= b) ==> k <= b [5] by 3,4,SUP;
 119     assume ~thesis;
 120     consider y such that &1 < abs (g y) [6] by REAL_NOT_LT;
 121     &0 < abs (g y) [7] by REAL_ARITH;
 122     !x. abs (f x) <= k / abs (g y) [8]
 123     proof let x be real;
 124       abs (f (x + y)) <= k /\ abs (f (x - y)) <= k /\
 125       f (x + y) + f (x - y) = &2 * f x * g y by 1,5;
 126       abs (f x * g y) <= k by REAL_ARITH;
 127     qed by 7,REAL_ABS_MUL,REAL_LE_RDIV_EQ;
 128     consider x such that &0 < abs (f x) /\ abs (f x) <= k by 2,5,ABS_CASES;
 129     &0 < k by REAL_ARITH;
 130     k / abs (g y) < k by 6,7,REAL_LT_LMUL,REAL_MUL_RID,REAL_LT_LDIV_EQ;
 131   qed by 5,8,REAL_NOT_LE`;;
 132
 133 let IMO_3 = thm `;
 134   let f g be real->real;
 135   assume !x y. f (x + y) + f (x - y) = &2 * f x * g y [1];
 136   assume ~(!x. f x = &0) [2];
 137   assume !x. abs (f x) <= &1 [3];
 138   thus !x. abs (g x) <= &1
 139   proof
 140     now [4] let y be real;
 141       !x. abs (f x * g y pow 0) <= &1 [5] by 3,real_pow,REAL_MUL_RID;
 142       now let l be num;
 143         assume !x. abs (f x * g y pow l) <= &1;
 144         let x be real;
 145         abs (f (x + y) * g y pow l) <= &1 /\
 146         abs (f (x - y) * g y pow l) <= &1;
 147         abs ((f (x + y) + f (x - y)) * g y pow l) <= &2 by REAL_ARITH;
 148         abs ((&2 * f x * g y) * g y pow l) <= &2 by 1;
 149         abs (f x * g y * g y pow l) <= &1 by REAL_ARITH;
 150         thus abs (f x * g y pow SUC l) <= &1 by real_pow,REAL_MUL_RID;
 151       end;
 152       thus !l x. abs (f x * g y pow l) <= &1 by INDUCT_TAC,5;
 153     end;
 154     !x y. ~(x = &0) /\ &1 < abs(y) ==> ?n. &1 < abs(y pow n * x)
 155       by SIMP_TAC,REAL_ABS_MUL,REAL_ABS_POW,GSYM REAL_LT_LDIV_EQ,
 156         GSYM REAL_ABS_NZ,REAL_ARCH_POW;
 157   qed by 2,4,REAL_NOT_LE,REAL_MUL_SYM`;;