formal_lp/ineqs/delta_ineq.hl

   1 needs "tame/Inequalities.hl";;
   2
   3 module Delta_ineq = struct
   4
   5 open Tame_inequalities;;
   6
   7 let lemma1 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x1 /\ x1 <= #6.3504 /\ #4.0 <= x4
   8                    ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x #4.0 x2 x3 x4 x5 x6
   9                    \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x #6.3504 x2 x3 x4 x5 x6`,
  10    REPEAT STRIP_TAC THEN
  11      SUBGOAL_THEN `!x1. delta_x x1 x2 x3 x4 x5 x6 = (\x. delta_x x x2 x3 x4 x5 x6) x1` (fun th -> ONCE_REWRITE_TAC[th]) THENL
  12      [
  13        REWRITE_TAC[];
  14        ALL_TAC
  15      ] THEN
  16
  17      MATCH_MP_TAC lemma' THEN
  18      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
  19      MAP_EVERY EXISTS_TAC [`--x4`; `x4*(x2+x3-x4+x5+x6)+x2*x5+x3*x6-x3*x5-x2*x6`; `x2*x5*(x3-x2+x4-x5+x6) + x3*x6*(x2-x3+x4+x5-x6)-x2*x3*x4-x4*x5*x6`] THEN
  20      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  21
  22
  23 let lemma2 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x2 /\ x2 <= #6.3504 /\ #4.0 <= x5
  24                    ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 #4.0 x3 x4 x5 x6
  25                    \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 #6.3504 x3 x4 x5 x6`,
  26    REPEAT STRIP_TAC THEN
  27      SUBGOAL_THEN `!x2. delta_x x1 x2 x3 x4 x5 x6 = (\x. delta_x x1 x x3 x4 x5 x6) x2` (fun th -> ONCE_REWRITE_TAC[th]) THENL
  28      [
  29        REWRITE_TAC[];
  30        ALL_TAC
  31      ] THEN
  32
  33      MATCH_MP_TAC lemma' THEN
  34      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
  35      MAP_EVERY EXISTS_TAC [`--x5`; `x5*(x1+x3+x4-x5+x6)+x1*x4+x3*x6-x3*x4-x1*x6`; `x1*x4*(--x1+x3-x4+x5+x6) + x3*x6*(x1-x3+x4+x5-x6)-x1*x3*x5-x4*x5*x6`] THEN
  36      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  37
  38
  39 let lemma3 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x3 /\ x3 <= #6.3504 /\ #4.0 <= x6
  40                    ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #4.0 x4 x5 x6
  41                    \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 #6.3504 x4 x5 x6`,
  42    REPEAT STRIP_TAC THEN
  43      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
  44      MATCH_MP_TAC lemma' THEN
  45      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
  46      MAP_EVERY EXISTS_TAC [`--x6`; `x6*(x1+x2-x6+x4+x5)+x1*x4+x2*x5-x2*x4-x1*x5`; `x2*x5*(x1-x2+x4-x5+x6) + x1*x4*(--x1+x2-x4+x5+x6)-x1*x2*x6-x4*x5*x6`] THEN
  47      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  48
  49
  50 let lemma4 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x4 /\ x4 <= &9 /\ #4.0 <= x1
  51                    ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 #4.0 x5 x6
  52                    \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 (&9) x5 x6`,
  53    REPEAT STRIP_TAC THEN
  54      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN
  55      MATCH_MP_TAC lemma' THEN
  56      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
  57      MAP_EVERY EXISTS_TAC [`--x1`; `x1*(--x1+x2+x3+x5+x6)+x2*x5+x3*x6-x2*x3-x5*x6`; `x2*x5*(x1-x2+x3-x5+x6) + x3*x6*(x1+x2-x3+x5-x6)-x1*x3*x5-x1*x2*x6`] THEN
  58      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  59
  60
  61 let lemma5 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x5 /\ x5 <= &9 /\ #4.0 <= x2
  62                    ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 #4.0 x6
  63                    \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 (&9) x6`,
  64    REPEAT STRIP_TAC THEN
  65      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN
  66      MATCH_MP_TAC lemma' THEN
  67      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
  68      MAP_EVERY EXISTS_TAC [`--x2`; `x2*(x1+x3-x2+x4+x6)+x1*x4+x3*x6-x1*x3-x4*x6`; `x1*x4*(--x1+x2+x3-x4+x6) + x3*x6*(x1+x2-x3+x4-x6)-x2*x3*x4-x1*x2*x6`] THEN
  69      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  70
  71
  72 let lemma6 = prove(`!x1 x2 x3 x4 x5 x6. #4.0 <= x6 /\ x6 <= &9 /\ #4.0 <= x3
  73                    ==> delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 #4.0
  74                    \/ delta_x x1 x2 x3 x4 x5 x6 >= delta_x x1 x2 x3 x4 x5 (&9)`,
  75    REPEAT STRIP_TAC THEN
  76      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
  77      MATCH_MP_TAC lemma' THEN
  78      ASM_REWRITE_TAC[Sphere.delta_x; FUN_EQ_THM] THEN
  79      MAP_EVERY EXISTS_TAC [`--x3`; `x3*(x1+x2-x3+x4+x5)+x1*x4+x2*x5-x1*x2-x4*x5`; `x2*x5*(x1-x2+x3+x4-x5) + x1*x4*(--x1+x2+x3-x4+x5)-x2*x3*x4-x1*x3*x5`] THEN
  80      POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
  81
  82
  83 (* delta_x > 0 for apex darts *)
  84 let delta_x_pos_apex = prove(`!x1 x2 x3 x4 x5 x6. ineq [#4.0,x1,#6.3504;
  85                                                         #4.0,x2,#6.3504;
  86                                                         #4.0,x3,#6.3504;
  87                                                         #4.0,x4,&9;
  88                                                         #4.0,x5,&9;
  89                                                         #4.0,x6,&9] (delta_x x1 x2 x3 x4 x5 x6 >= &1)`,
  90    REPEAT STRIP_TAC THEN
  91      REWRITE_TAC[INEQ_ALT; ALL] THEN
  92      REPEAT STRIP_TAC THEN
  93      ASSUME_TAC (REAL_ARITH `#4.0 <= #4.0 /\ #4.0 <= #6.3504`) THEN
  94
  95      (* x1 *)
  96      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x x2 x3 x4 x5 x6) x1`)] THEN
  97      MATCH_MP_TAC main_lemma THEN
  98      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
  99      ASM_SIMP_TAC[lemma1] THEN
 100      CONJ_TAC THEN
 101
 102      (* x2 *)
 103      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x x3 x4 x5 x6) x2`)] THEN
 104      MATCH_MP_TAC main_lemma THEN
 105      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 106      ASM_SIMP_TAC[lemma2] THEN
 107      CONJ_TAC THEN
 108
 109      (* x3 *)
 110      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x x4 x5 x6) x3`)] THEN
 111      MATCH_MP_TAC main_lemma THEN
 112      MAP_EVERY EXISTS_TAC [`#4.0`; `#6.3504`] THEN
 113      ASM_SIMP_TAC[lemma3] THEN
 114      CONJ_TAC THEN
 115
 116      (* x4 *)
 117      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x x5 x6) x4`)] THEN
 118      MATCH_MP_TAC main_lemma THEN
 119      MAP_EVERY EXISTS_TAC [`#4.0`; `&9`] THEN
 120      ASM_SIMP_TAC[lemma4] THEN
 121      CONJ_TAC THEN
 122
 123      (* x5 *)
 124      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x x6) x5`)] THEN
 125      MATCH_MP_TAC main_lemma THEN
 126      MAP_EVERY EXISTS_TAC [`#4.0`; `&9`] THEN
 127      ASM_SIMP_TAC[lemma5] THEN
 128      CONJ_TAC THEN
 129
 130      (* x6 *)
 131      ONCE_REWRITE_TAC[SYM (BETA_CONV `(\x. delta_x x1 x2 x3 x4 x5 x) x6`)] THEN
 132      MATCH_MP_TAC main_lemma THEN
 133      MAP_EVERY EXISTS_TAC [`#4.0`; `&9`] THEN
 134      ASM_SIMP_TAC[lemma6] THEN
 135      CONJ_TAC THEN
 136
 137      (* Final stage *)
 138      REWRITE_TAC[Sphere.delta_x] THEN
 139      CONV_TAC REAL_RAT_REDUCE_CONV);;
 140
 141
 142 let aux_lemma1 = prove(`!a. &2 <= a /\ a <= #2.52 ==> #4.0 <= a * a /\ a * a <= #6.3504`,
 143                        REWRITE_TAC[ARITH_RULE `#4.0 = &2 * &2 /\ #6.3504 = #2.52 * #2.52`] THEN
 144                          REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN ARITH_TAC);;
 145
 146 let aux_lemma2 = prove(`!a. &2 <= a /\ a <= &3 ==> #4.0 <= a * a /\ a * a <= &9`,
 147                        REWRITE_TAC[ARITH_RULE `#4.0 = &2 * &2 /\ &9 = &3 * &3`] THEN
 148                          REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN ARITH_TAC);;
 149
 150
 151 let delta_y_pos_apex = prove(`!y1 y2 y3 y4 y5 y6.
 152                              &2 <= y1 /\ y1 <= #2.52
 153                              /\ &2 <= y2 /\ y2 <= #2.52
 154                              /\ &2 <= y3 /\ y3 <= #2.52
 155                              /\ &2 <= y4 /\ y4 <= &3
 156                              /\ &2 <= y5 /\ y5 <= &3
 157                              /\ &2 <= y6 /\ y6 <= &3
 158                              ==> &0 <= delta_y y1 y2 y3 y4 y5 y6`,
 159                              REPEAT STRIP_TAC THEN REWRITE_TAC[Sphere.delta_y] THEN
 160                                MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1` THEN
 161                                REWRITE_TAC[ARITH_RULE `&0 <= &1`; GSYM real_ge] THEN
 162                                MP_TAC delta_x_pos_apex THEN REWRITE_TAC[INEQ_ALT; ALL] THEN
 163                                DISCH_THEN MATCH_MP_TAC THEN
 164                                ASM_SIMP_TAC[aux_lemma1; aux_lemma2]);;
 165
 166 end;;