3 (* ========================================================================= *)
4 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA *)
7 (* LEMMA ABOUT DELTA_X *)
9 (* Authour : VU KHAC KY *)
11 (* Date: 2010-04-02 *)
12 (* ========================================================================= *)
15 (* ========================================================================= *)
16 (* SOME USEFUL TACTICS *)
17 (* ========================================================================= *)
19 module Delta_x = struct
24 open Prove_by_refinement;;
26 let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;;
28 let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);;
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
37 (* ========================================================================= *)
39 (* ========================================================================= *)
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 =
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 )`;;
53 let COMPUTE_DELTA_X = prove_by_refinement (compute_delta_x_t,
55 (REWRITE_TAC[delta_x;xlist;ylist]);
56 (REPEAT LET_TAC THEN DISCH_TAC);
58 (UP_ASM_TAC THEN UP_ASM_TAC THEN PURE_REWRITE_TAC[PAIR_EQ]);
59 (PURE_ONCE_REWRITE_TAC[DIST_SYM]);
63 `(a:real^3) dot a = x1 /\ (b:real ^3) dot b = x2 /\ (c:real^3) dot c = x3`
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]);
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`
81 (PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ]);
82 (PURE_ONCE_ASM_REWRITE_TAC[]);
84 (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[dist]);
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]);
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 -
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 *)
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" );
110 (PURE_ONCE_ASM_REWRITE_TAC[]);
111 (REWRITE_TAC[DOT_3;POW_2] THEN REAL_ARITH_TAC)]);;
113 (* ========================================================================= *)
114 (* THE SECOND LEMMA: delta_x = &4 * (det A) pow 2 *)
115 (* ========================================================================= *)
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 /\
123 ==> (delta_x x1 x2 x3 x4 x5 x6 = &4 * det A pow 2)`;;
125 let DELTA_X_DET_3 = prove_by_refinement (delta_x_det_x_t ,
127 (MP_TAC (SPEC_ALL DET_3) THEN DISCH_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)]);;
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 (* ========================================================================= *)
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}`;;
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]);
153 (PURE_REWRITE_TAC[PAIR_EQ]);
155 (PURE_ONCE_REWRITE_TAC[collinear]);
156 (REPEAT STRIP_TAC); (* Break the proof into 3 subgoals *)
158 (* -------------- Begin subgoal 1----------------------------------------- *)
162 (MATCH_MP_TAC (REAL_ARITH `&0 = a ==> &0 < a ==> F`));
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} `]);
170 (FIRST_X_ASSUM CHOOSE_TAC);
173 `!i. (a:real^3)$i = m * (u:real^3)$i /\ (b:real^3)$i = n * u$i`
175 (ASM_MESON_TAC[VECTOR_MUL_COMPONENT]);
180 (* -------------- End subgoal 1----------------------------------------- ---*)
182 (* -------------- Begin subgoal 2 ----------------------------------------- *)
186 (MATCH_MP_TAC (REAL_ARITH `&0 = a ==> &0 < a ==> F`));
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} `]);
194 (FIRST_X_ASSUM CHOOSE_TAC);
197 `!i. (a:real^3)$i = m * (u:real^3)$i /\ (c:real^3)$i = n * u$i`
199 (ASM_MESON_TAC[VECTOR_MUL_COMPONENT]);
204 (* -------------- End subgoal 2----------------------------------------- ---*)
206 (* -------------- Begin subgoal 3 ----------------------------------------- *)
210 (MATCH_MP_TAC (REAL_ARITH `&0 = a ==> &0 < a ==> F`));
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} `]);
218 (FIRST_X_ASSUM CHOOSE_TAC);
221 `!i. (c:real^3)$i = m * (u:real^3)$i /\ (b:real^3)$i = n * u$i`
223 (ASM_MESON_TAC[VECTOR_MUL_COMPONENT]);
228 (* -------------- End subgoal 3 and also end main goal -------------------- *)