text_formalization/trigonometry/delta_x.hl

   1
   2
   3 (* ========================================================================= *)
   4 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   5 (*          COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA                       *)
   6 (*                                                                           *)
   7 (*                  LEMMA ABOUT DELTA_X                                      *)
   8 (*                                                                           *)
   9 (*      Authour : VU KHAC KY                                                 *)
  10 (*                                                                           *)
  11 (*      Date: 2010-04-02                                                     *)
  12 (* ========================================================================= *)
  13
  14
  15 (* ========================================================================= *)
  16 (*                     SOME USEFUL TACTICS                                   *)
  17 (* ========================================================================= *)
  18
  19 module Delta_x = struct
  20
  21 open Sphere;;
  22 open Trigonometry1;;
  23 open Trigonometry2;;
  24 open Prove_by_refinement;;
  25
  26 let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;;
  27
  28 let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);;
  29
  30 let SWITCH_TAC =
  31    FIRST_X_ASSUM MP_TAC THEN
  32    FIRST_X_ASSUM MP_TAC THEN
  33    MATCH_MP_TAC (MESON[] `(a ==> b ==> c) ==> (b ==> a ==> c)`) THEN
  34    DISCH_TAC THEN
  35    DISCH_TAC;;
  36
  37 (* ========================================================================= *)
  38 (*                  THE FIRST LEMMA                                          *)
  39 (* ========================================================================= *)
  40
  41 let compute_delta_x_t =
  42  `!v0:real^3 v1 v2 v3 x1 x2 x3 x4 x5 x6.
  43    x1, x2, x3, x4, x5, x6  = xlist v0 v1 v2 v3
  44    ==> delta_x x1 x2 x3 x4 x5 x6 =
  45    (let a = v1 - v0 in
  46     let b = v2 - v0 in
  47     let c = v3 - v0 in
  48       &4 *
  49      (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 -
  50       a$2 * b$1 * c$3 + a$2 * b$3 * c$1 +
  51       a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2 )`;;
  52
  53 let COMPUTE_DELTA_X = prove_by_refinement (compute_delta_x_t,
  54 [(REPEAT GEN_TAC);
  55  (REWRITE_TAC[delta_x;xlist;ylist]);
  56  (REPEAT LET_TAC THEN DISCH_TAC);
  57
  58   (UP_ASM_TAC THEN UP_ASM_TAC THEN PURE_REWRITE_TAC[PAIR_EQ]);
  59   (PURE_ONCE_REWRITE_TAC[DIST_SYM]);
  60   (REPEAT DISCH_TAC);
  61
  62   (SUBGOAL_THEN
  63     `(a:real^3) dot a  = x1 /\ (b:real ^3) dot b = x2 /\ (c:real^3) dot c = x3`
  64     ASSUME_TAC);
  65   (*  Begin subgoal 1 *)
  66
  67   (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
  68   (UP_ASM_TAC THEN UP_ASM_TAC);
  69   (PURE_REWRITE_TAC[dist]);
  70   (MESON_TAC[NORM_POW_2]);
  71   (* End subgoal 1 *)
  72
  73   (SUBGOAL_THEN
  74     `(b:real^3) dot b + (c:real^3) dot c - &2 * (b dot c)  = x4 /\
  75      (a:real^3) dot a + (c:real^3) dot c - &2 * (a dot c)  = x5 /\
  76      (a:real^3) dot a + (b:real^3) dot b - &2 * (a dot b)  = x6`
  77     ASSUME_TAC);
  78   (* Begin subgoal 2 *)
  79
  80   DEL_TAC;
  81   (PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ]);
  82   (PURE_ONCE_ASM_REWRITE_TAC[]);
  83   DEL_TAC;
  84   (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[dist]);
  85   STRIP_TAC;
  86   (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
  87   (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
  88   (PURE_ONCE_REWRITE_TAC[NORM_POW_2]);
  89   VECTOR_ARITH_TAC;
  90   (* End subgoal 2 *)
  91
  92   ( SUBGOAL_THEN `(x1:real) * x4 * (--x1 + x2 + x3 - x4 + x5 + x6) +
  93                     x2 * x5 * (x1 - x2 + x3 + x4 - x5 + x6) +
  94                     x3 * x6 * (x1 + x2 - x3 + x4 + x5 - x6) -
  95                     x2 * x3 * x4 - x1 * x3 * x5 - x1 * x2 * x6 -
  96                     x4 * x5 * x6 =
  97                     &4 * (a dot a) * (b dot b) * ((c:real^3) dot c)
  98                  -  (&4) * (a dot a) * (b dot c) * (b dot c)
  99                  -  (&4) * (a dot c) * (a dot c) * (b dot b)
 100                  -  (&4) * (a dot b) * (a dot b) * (c dot c)
 101                  +  (&8) * (a dot b) * (a dot c) * (b dot c)` ASSUME_TAC);
 102    (* Begin subgoal 3 *)
 103
 104   (UP_ASM_TAC THEN UP_ASM_TAC THEN REPEAT STRIP_TAC);
 105   (EXPAND_TAC "x1" THEN EXPAND_TAC "x2" THEN EXPAND_TAC "x3");
 106   (EXPAND_TAC "x4" THEN EXPAND_TAC "x5" THEN EXPAND_TAC "x6" );
 107   (REAL_ARITH_TAC);
 108   (* End subgoal 3 *)
 109
 110  (PURE_ONCE_ASM_REWRITE_TAC[]);
 111  (REWRITE_TAC[DOT_3;POW_2] THEN REAL_ARITH_TAC)]);;
 112
 113 (* ========================================================================= *)
 114 (*    THE SECOND LEMMA:   delta_x = &4 * (det A) pow 2                       *)
 115 (* ========================================================================= *)
 116
 117 let  delta_x_det_x_t =
 118  `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6 A:real^3^3.
 119    x1, x2, x3, x4, x5, x6 = xlist v0 v1 v2 v3 /\
 120    A$1 = v1 - v0 /\
 121    A$2 = v2 - v0 /\
 122    A$3 = v3 - v0
 123    ==> (delta_x x1 x2 x3 x4 x5 x6 = &4 * det A pow 2)`;;
 124
 125 let DELTA_X_DET_3 = prove_by_refinement (delta_x_det_x_t ,
 126 [(REPEAT STRIP_TAC);
 127  (MP_TAC (SPEC_ALL DET_3) THEN DISCH_TAC);
 128  (ASM_REWRITE_TAC[]);
 129  (MP_TAC COMPUTE_DELTA_X);
 130  (REPEAT LET_TAC THEN STRIP_TAC);
 131  (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
 132  (ASM_SIMP_TAC[] THEN REAL_ARITH_TAC)]);;
 133
 134 (* ========================================================================= *)
 135 (*       THE THIRD LEMMA:                                                    *)
 136 (*                  delta > &0 ==> v0 v1 v2 are not collinear                *)
 137 (*                                 v0 v1 v3 are not collinear                *)
 138 (*                                 v0 v2 v3 are not collinear                *)
 139 (* ========================================================================= *)
 140
 141 let delta_x_collinear_t =
 142  `!(v0:real^3) v1 v2 v3 (x1:real) x2 x3 x4 x5 x6.
 143    ( x1, x2, x3, x4, x5, x6 = xlist v0 v1 v2 v3)
 144     ==> (&0 < (delta_x x1 x2 x3 x4 x5 x6))
 145     ==> ~collinear {v0, v1, v2} /\
 146         ~collinear {v0, v1, v3} /\
 147         ~collinear {v0, v3, v2}`;;
 148
 149 let DELTA_X_LT_0_COLLINEAR = prove_by_refinement (delta_x_collinear_t,
 150 [(REPEAT GEN_TAC THEN DISCH_TAC);
 151  (ASM_SIMP_TAC[COMPUTE_DELTA_X]);
 152  (REPEAT LET_TAC);
 153  (PURE_REWRITE_TAC[PAIR_EQ]);
 154  STRIP_TAC;
 155  (PURE_ONCE_REWRITE_TAC[collinear]);
 156  (REPEAT STRIP_TAC);   (* Break the proof into 3 subgoals *)
 157
 158  (* -------------- Begin subgoal 1----------------------------------------- *)
 159
 160    SWITCH_TAC;
 161    UP_ASM_TAC;
 162    (MATCH_MP_TAC (REAL_ARITH `&0 = a ==> &0 < a ==> F`));
 163
 164      (SUBGOAL_THEN `?m n. a = m % (u:real^3) /\ b = n % u` CHOOSE_TAC);
 165      (EXPAND_TAC "a" THEN EXPAND_TAC "b");
 166      (ASM_MESON_TAC[SET_RULE `v0 IN {v0, v1, v2} /\
 167                                v1 IN {v0, v1, v2} /\
 168                                v2 IN {v0, v1, v2} `]);
 169
 170    (FIRST_X_ASSUM CHOOSE_TAC);
 171
 172       (SUBGOAL_THEN
 173         `!i. (a:real^3)$i = m * (u:real^3)$i /\ (b:real^3)$i = n * u$i`
 174         ASSUME_TAC);
 175       (ASM_MESON_TAC[VECTOR_MUL_COMPONENT]);
 176
 177    (ASM_REWRITE_TAC[]);
 178    (REAL_ARITH_TAC);
 179
 180  (* -------------- End subgoal 1----------------------------------------- ---*)
 181
 182  (* -------------- Begin subgoal 2 ----------------------------------------- *)
 183
 184    SWITCH_TAC;
 185    UP_ASM_TAC;
 186    (MATCH_MP_TAC (REAL_ARITH `&0 = a ==> &0 < a ==> F`));
 187
 188      (SUBGOAL_THEN `?m n. a = m % (u:real^3) /\ c = n % u` CHOOSE_TAC);
 189      (EXPAND_TAC "a" THEN EXPAND_TAC "c");
 190      (ASM_MESON_TAC[SET_RULE `v0 IN {v0, v1, v2} /\
 191                                v1 IN {v0, v1, v2} /\
 192                                v2 IN {v0, v1, v2} `]);
 193
 194    (FIRST_X_ASSUM CHOOSE_TAC);
 195
 196       (SUBGOAL_THEN
 197         `!i. (a:real^3)$i = m * (u:real^3)$i /\ (c:real^3)$i = n * u$i`
 198         ASSUME_TAC);
 199       (ASM_MESON_TAC[VECTOR_MUL_COMPONENT]);
 200
 201    (ASM_REWRITE_TAC[]);
 202    (REAL_ARITH_TAC);
 203
 204 (* -------------- End subgoal 2----------------------------------------- ---*)
 205
 206 (* -------------- Begin subgoal 3 ----------------------------------------- *)
 207
 208    SWITCH_TAC;
 209    UP_ASM_TAC;
 210    (MATCH_MP_TAC (REAL_ARITH `&0 = a ==> &0 < a ==> F`));
 211
 212      (SUBGOAL_THEN `?m n. c = m % (u:real^3) /\ b = n % u` CHOOSE_TAC);
 213      (EXPAND_TAC "b" THEN EXPAND_TAC "c");
 214      (ASM_MESON_TAC[SET_RULE `v0 IN {v0, v1, v2} /\
 215                                v1 IN {v0, v1, v2} /\
 216                                v2 IN {v0, v1, v2} `]);
 217
 218    (FIRST_X_ASSUM CHOOSE_TAC);
 219
 220       (SUBGOAL_THEN
 221         `!i. (c:real^3)$i = m * (u:real^3)$i /\ (b:real^3)$i = n * u$i`
 222         ASSUME_TAC);
 223       (ASM_MESON_TAC[VECTOR_MUL_COMPONENT]);
 224
 225    (ASM_REWRITE_TAC[]);
 226    (REAL_ARITH_TAC)]);;
 227
 228  (* -------------- End subgoal 3 and also end main goal -------------------- *)
 229
 230 end;;