(* ========================================================================= *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA *)
(* *)
(* EULER TRIANGLE LEMMA *)
(* *)
(* Authour : VU KHAC KY *)
(* Date : 2010-04-02 *)
(* Books name: JLPSDHF *)
(* ========================================================================= *)
(* =========================================================================*)
(* *)
(* BEGIN THE MAIN THEORM ABOUT EULER ANGLE SUM *)
(* *)
(*==========================================================================*)
flyspeck_needs "general/sphere.hl";;
flyspeck_needs "general/prove_by_refinement.hl";;
flyspeck_needs "trigonometry/trig1.hl";;
flyspeck_needs "trigonometry/trig2.hl";;
flyspeck_needs "trigonometry/delta_x.hl";;
flyspeck_needs "trigonometry/euler_complement.hl";;
flyspeck_needs "trigonometry/euler_multivariate.hl";;
module Euler_main_theorem = struct
open Sphere;;
open Trigonometry1;;
open Trigonometry2;;
open Prove_by_refinement;;
open Delta_x;;
open Euler_complement;;
open Euler_multivariate;;
let euler_angle_sum_rescale =
` !v0:real^3 v1 v2 v3 p x1 x2 x3 x4 x5 x6 alpha1 alpha2 alpha3 d w1 w2 w3.
p = euler_p v0 v1 v2 v3 /\
x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\
alpha1 = dihV v0 v1 v2 v3 /\
alpha2 = dihV v0 v2 v3 v1 /\
alpha3 = dihV v0 v3 v1 v2 /\
d = delta_x x1 x2 x3 x4 x5 x6 /\
w1 = v1 - v0 /\
w2 = v2 - v0 /\
w3 = v3 - v0 /\
&0 < d /\
norm w1 = &1 /\
norm w2 = &1 /\
norm w3 = &1
==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p)`;;
let EULER_ANGLE_SUM_rescal = prove_by_refinement (euler_angle_sum_rescale ,
[ (REPEAT GEN_TAC) ;
(REPEAT STRIP_TAC);
(REPLICATE_TAC 11 UP_ASM_TAC);
(FIRST_ASSUM MP_TAC THEN SWITCH_TAC THEN FIRST_ASSUM MP_TAC);
(REWRITE_TAC[euler_p;xlist;ylist]);
(REPEAT LET_TAC);
(REPEAT UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC);
(* ==========================================================================*)
(* 3 FIRST SUBGOALS: *)
(* ==========================================================================*)
(SUBGOAL_THEN
` ~collinear {(v0:real^3), v1, v2} /\
~collinear {v0, v1, v3} /\
~collinear {v0, v3, v2}`
ASSUME_TAC);
(ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]);
(SUBGOAL_THEN `y1 = &1 /\ y2 = &1 /\ y3 = &1` ASSUME_TAC);
(EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
(PURE_ONCE_REWRITE_TAC[DIST_SYM]);
(PURE_ONCE_REWRITE_TAC[dist]);
(ASM_MESON_TAC[]);
(UP_ASM_TAC THEN STRIP_TAC);
(SUBGOAL_THEN `x1 = &1 /\ x2 = &1 /\ x3 = &1` ASSUME_TAC);
(ASM_REWRITE_TAC[]);
(ONCE_ASM_REWRITE_TAC[REAL_POW_2]);
REAL_ARITH_TAC;
(UP_ASM_TAC THEN STRIP_TAC);
(* ==========================================================================*)
(* Subgoal 4: Comput p and delta *)
(* ==========================================================================*)
(SUBGOAL_THEN
`&2 * p = &8 - x4 - x5 - x6 /\ d = ups_x x4 x5 x6 - x4 * x5 * x6`
ASSUME_TAC);
(SUBGOAL_THEN
`x4 = (v2 - v3) dot (v2 - v3:real^3) /\
x5 = (v1 - v3) dot (v1 - v3) /\
x6 = (v1 - v2) dot (v1 - v2)`
ASSUME_TAC);
(ASM_REWRITE_TAC[]);
(EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
(ONCE_REWRITE_TAC[dist]);
(REWRITE_TAC[NORM_POW_2]);
CONJ_TAC; (* Break into 2 subgoals *)
(REPEAT UP_ASM_TAC THEN DISCH_TAC THEN DISCH_TAC);
(DEL_TAC THEN REPEAT DISCH_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC [REAL_MUL_LID]);
(EXPAND_TAC "w1'" THEN EXPAND_TAC "w2'" THEN EXPAND_TAC "w3'");
(EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
(REWRITE_TAC[dist]);
(REWRITE_TAC[NORM_POW_2]);
(ASM_MESON_TAC[LEMMA_FOR_EULER_AFTER_RESCALE]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[ups_x;delta_x]);
(ONCE_ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
(* ========================================================================= *)
(* Re-comput alpha1, alpha2, alpha3 . *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* Subgoal 5: alpha1 *)
(* ------------------------------------------------------------------------- *)
(SUBGOAL_THEN
`alpha1 =
pi / &2 -
atn2 (sqrt (&4 * x1 * delta_x x1 x2 x3 x4 x5 x6),delta_x4 x1 x2 x3 x4 x5 x6)`
ASSUME_TAC);
(REPLICATE_TAC 7 DEL_TAC THEN UP_ASM_TAC THEN DISCH_TAC);
(MP_TAC COMPUTE_DIHV_ATN2);
(ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
(* ------------------------------------------------------------------------- *)
(* Subgoal 6: alpha2 *)
(* ------------------------------------------------------------------------- *)
(SUBGOAL_THEN
`alpha2 =
pi / &2 -
atn2 (sqrt (&4 * x2 * delta_x x2 x3 x1 x5 x6 x4),delta_x4 x2 x3 x1 x5 x6 x4)`
ASSUME_TAC);
(REPLICATE_TAC 8 DEL_TAC);
(SUBGOAL_THEN
`x4 = dist (v2:real^3,v3) pow 2 /\
x5 = dist (v3,v1) pow 2 /\
x6 = dist (v2,v1) pow 2 /\
~collinear {v0, v2, v3} /\
~collinear {v0, v2, v1}`
ASSUME_TAC);
(ASM_MESON_TAC[DIST_SYM;SET_RULE `{v0,v1, v2} = {v0,v2,v1}`]);
(REPLICATE_TAC 13 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
(REPEAT DISCH_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
(ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
(* ------------------------------------------------------------------------- *)
(* Subgoal 7: alpha3 *)
(* ------------------------------------------------------------------------- *)
(SUBGOAL_THEN
`alpha3 =
pi / &2 -
atn2 (sqrt (&4 * x3 * delta_x x3 x1 x2 x6 x4 x5),delta_x4 x3 x1 x2 x6 x4 x5)`
ASSUME_TAC);
(REPLICATE_TAC 9 DEL_TAC);
(SUBGOAL_THEN
`x5 = dist (v3:real^3,v1) pow 2 /\
x4 = dist (v3,v2) pow 2 /\
x6 = dist (v1,v2) pow 2 /\
~collinear {v0, v3, v1} /\
~collinear {v0, v3, v2}`
ASSUME_TAC);
(ASM_MESON_TAC[DIST_SYM;SET_RULE `{v0,v1, v2} = {v0,v2,v1}`]);
(REPLICATE_TAC 13 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
(REPEAT DISCH_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
(ASM_MESON_TAC[COMPUTE_DIHV_ATN2]);
(* ------------------------------------------------------------------------- *)
(* Subgoal 8: delta_x is symmetry *)
(* ------------------------------------------------------------------------- *)
(SUBGOAL_THEN
`delta_x x2 x3 x1 x5 x6 x4 = d /\ delta_x x3 x1 x2 x6 x4 x5 = d`
ASSUME_TAC);
(SUBGOAL_THEN
`x2, x3, x1, x5, x6, x4 = xlist (v0:real^3) v2 v3 v1`
ASSUME_TAC);
(REWRITE_TAC[xlist;ylist]);
(REPEAT LET_TAC);
(UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
(ASM_MESON_TAC[DIST_SYM]);
(SUBGOAL_THEN
`x3, x1, x2, x6, x4, x5 = xlist (v0:real^3) v3 v1 v2`
ASSUME_TAC);
(REWRITE_TAC[xlist;ylist]);
(REPEAT LET_TAC);
(UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC);
(ASM_MESON_TAC[DIST_SYM]);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[delta_x]);
REAL_ARITH_TAC;
(* ------------------------------------------------------------------------- *)
(* Subgoal 9: Th simplest form of alpha1,2,3 *)
(* ------------------------------------------------------------------------- *)
(SUBGOAL_THEN
`alpha1 =
pi / &2 - atn ((-- &2 * x4 + &2 * x5 + &2 * x6 - x5 * x6) / sqrt (&4 * d)) /\
alpha2 =
pi / &2 - atn ((-- &2 * x5 + &2 * x6 + &2 * x4 - x6 * x4) / sqrt (&4 * d)) /\
alpha3 =
pi / &2 - atn ((-- &2 * x6 + &2 * x4 + &2 * x5 - x4 * x5) / sqrt (&4 * d))`
ASSUME_TAC);
(ABBREV_TAC `4D = &4 * d`);
(REPLICATE_TAC 21 UP_ASM_TAC THEN REPLICATE_TAC 9 DEL_TAC);
(REPEAT DISCH_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[REAL_ARITH `a - x = a - y <=> x = y`]);
(REWRITE_TAC[GSYM (ASSUME `d = delta_x x1 x2 x3 x4 x5 x6`)]);
(REWRITE_TAC[ASSUME `delta_x x2 x3 x1 x5 x6 x4 = d /\
delta_x x3 x1 x2 x6 x4 x5 = d`]);
(REWRITE_TAC[delta_x4]);
(REWRITE_TAC[ASSUME `x1 = &1`]);
(REWRITE_TAC[ASSUME `x2 = &1`]);
(REWRITE_TAC[ASSUME `x3 = &1`]);
(REWRITE_TAC[REAL_MUL_LID;REAL_MUL_RID]);
(REWRITE_TAC[REAL_ARITH
`-- &1 - x4 + x5 + x6 - x5 * x6 + -- &1 + &1 + &1 - x4 + x5 + x6
= (-- &2 * x4 + &2 * x5 + &2 * x6 - x5 * x6) /\
-- &1 - x5 + x6 + x4 - x6 * x4 + -- &1 + &1 + &1 - x5 + x6 + x4
= (-- &2 * x5 + &2 * x6 + &2 * x4 - x6 * x4) /\
-- &1 - x6 + x4 + x5 - x4 * x5 + -- &1 + &1 + &1 - x6 + x4 + x5
= (-- &2 * x6 + &2 * x4 + &2 * x5 - x4 * x5)`]);
(EXPAND_TAC "4D");
(SUBGOAL_THEN `&0 < sqrt (&4 * d)` ASSUME_TAC);
(MATCH_MP_TAC SQRT_POS_LT);
(ASM_MESON_TAC[REAL_ARITH `&0 < &4`;REAL_LT_MUL]);
(ASM_MESON_TAC[ATN2_BREAKDOWN]);
(* ------------------------------------------------------------------------- *)
(* Subgoal 10, 11: Something remains *)
(* ------------------------------------------------------------------------- *)
(ABBREV_TAC `a = (x4:real)`);
(ABBREV_TAC `b = (x5:real)`);
(ABBREV_TAC `c = (x6:real)`);
(SUBGOAL_THEN
`atn2 (sqrt d,&2 * p) = atn ((&8 - a - b - c) / sqrt d)`
ASSUME_TAC);
(SUBGOAL_THEN `&0 < sqrt d ` ASSUME_TAC);
(MATCH_MP_TAC SQRT_POS_LT THEN ASM_MESON_TAC[]);
(ASM_MESON_TAC[ATN2_BREAKDOWN]);
(SUBGOAL_THEN `sqrt (&4 * d) = &2 * sqrt d` ASSUME_TAC);
(SUBGOAL_THEN `sqrt (&4 * d) = sqrt (&4) * sqrt d` ASSUME_TAC);
(MATCH_MP_TAC SQRT_MUL);
ASM_REAL_ARITH_TAC;
(ASM_REWRITE_TAC[]);
(AP_THM_TAC THEN AP_TERM_TAC);
(REWRITE_TAC[REAL_ARITH `&4 = &2 * &2 `]);
(REWRITE_TAC[MESON[SQRT_MUL;REAL_ARITH `&0 <= &2`]
`sqrt (&2 * &2) = sqrt (&2) * sqrt (&2)`]);
(REWRITE_TAC[GSYM POW_2]);
(MATCH_MP_TAC SQRT_POW_2);
REAL_ARITH_TAC;
(REPLICATE_TAC 7 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
(REPLICATE_TAC 16 UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC);
(REPEAT STRIP_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(* ------------------------------------------------------------------------- *)
(* Subgoal 12: &0 < a, b , c < &4 *)
(* ------------------------------------------------------------------------- *)
(SUBGOAL_THEN `a < &4 /\ b < &4 /\ c < &4` ASSUME_TAC);
(EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
(ASM_REWRITE_TAC[REAL_ARITH `&4 = &2 pow 2`]);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC REAL_POW_LT2);
(EXPAND_TAC "y4");
(REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
(MATCH_MP_TAC (REAL_ARITH
`dist (v0:real^3,v2) = &1 /\ dist (v0,v3) = &1 /\
dist (v2,v3) < dist (v0:real^3,v2) + dist (v0,v3)
==> dist (v2,v3) < &2`));
STRIP_TAC;
(ASM_REWRITE_TAC[]);
STRIP_TAC;
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
(REWRITE_TAC[DIST_TRIANGLE_ALT]);
(REWRITE_TAC[dist]);
(MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
(REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
(REWRITE_TAC[NORM_POW_2]);
(ABBREV_TAC `m = v0:real^3 - v2`);
(ABBREV_TAC `n = v0:real^3 - v3`);
(SUBGOAL_THEN `v2:real^3 - v3 = n - m` ASSUME_TAC);
(EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[NORM_POW_2]);
(REWRITE_TAC[VECTOR_ARITH
`(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
(REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
(MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
(REWRITE_TAC [NORM_POW_2]);
(ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
(REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
(EXPAND_TAC "n" THEN EXPAND_TAC "m");
(ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
(ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
(PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, a, c}`]);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC REAL_POW_LT2);
(EXPAND_TAC "y5");
(REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
(MATCH_MP_TAC (REAL_ARITH
`dist (v0:real^3,v1) = &1 /\ dist (v0,v3) = &1 /\
dist (v1,v3) < dist (v0:real^3,v1) + dist (v0,v3)
==> dist (v1,v3) < &2`));
STRIP_TAC;
(ASM_REWRITE_TAC[]);
STRIP_TAC;
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
(REWRITE_TAC[DIST_TRIANGLE_ALT]);
(REWRITE_TAC[dist]);
(MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
(REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
(REWRITE_TAC[NORM_POW_2]);
(ABBREV_TAC `m = v0:real^3 - v1`);
(ABBREV_TAC `n = v0:real^3 - v3`);
(SUBGOAL_THEN `v1:real^3 - v3 = n - m` ASSUME_TAC);
(EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[NORM_POW_2]);
(REWRITE_TAC[VECTOR_ARITH
`(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
(REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
(MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
(REWRITE_TAC [NORM_POW_2]);
(ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
(REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
(EXPAND_TAC "n" THEN EXPAND_TAC "m");
(ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
(ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
(PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, c, a}`]);
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC REAL_POW_LT2);
(EXPAND_TAC "y6");
(REWRITE_TAC[ARITH_RULE `~(2 = 0)`; DIST_POS_LE]);
(MATCH_MP_TAC (REAL_ARITH
`dist (v0:real^3,v1) = &1 /\ dist (v0,v3) = &1 /\
dist (v1,v3) < dist (v0:real^3,v1) + dist (v0,v3)
==> dist (v1,v3) < &2`));
STRIP_TAC;
(ASM_REWRITE_TAC[]);
STRIP_TAC;
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC (REAL_ARITH `a <= b /\ ~(a = b) ==> a < b`));
(REWRITE_TAC[DIST_TRIANGLE_ALT]);
(REWRITE_TAC[dist]);
(MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
(REWRITE_TAC[REAL_ARITH `(a + b) pow 2 = a pow 2 + b pow 2 + &2 * a * b`]);
(REWRITE_TAC[NORM_POW_2]);
(ABBREV_TAC `m = v0:real^3 - v1`);
(ABBREV_TAC `n = v0:real^3 - v2`);
(SUBGOAL_THEN `v1:real^3 - v2 = n - m` ASSUME_TAC);
(EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN VECTOR_ARITH_TAC);
(ONCE_ASM_REWRITE_TAC[]);
(REWRITE_TAC[NORM_POW_2]);
(REWRITE_TAC[VECTOR_ARITH
`(m - n) dot (m - n) = m dot m + n dot n - &2 * m dot n`]);
(REWRITE_TAC[REAL_ARITH `a + b - &2 * c = b + a + &2 * d <=> --c = d`]);
(MATCH_MP_TAC (MESON[] `~(a pow 2 = b pow 2) ==> ~(a = b)`));
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(--x) pow 2 = x pow 2`]);
(PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) pow 2 = (y pow 2) * (x pow 2)`]);
(REWRITE_TAC [NORM_POW_2]);
(ONCE_REWRITE_TAC[VECTOR_ARITH `(n dot m) = (--n) dot (--m)`]);
(REWRITE_TAC[MESON[] `(a <=> b) <=> (~b <=> ~a)`; DOT_CAUCHY_SCHWARZ_EQUAL]);
(EXPAND_TAC "n" THEN EXPAND_TAC "m");
(ONCE_REWRITE_TAC[VECTOR_ARITH `--(x - y) = y - x:real^3`]);
(ONCE_REWRITE_TAC[GSYM COLLINEAR_3]);
(PURE_ONCE_REWRITE_TAC[SET_RULE `{a, b , c} = {b, c, a}`]);
(ASM_REWRITE_TAC[]);
(SUBGOAL_THEN `&0 < a /\ &0 < b /\ &0 < c` ASSUME_TAC);
(EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c");
(ASM_REWRITE_TAC[]);
STRIP_TAC;
(MATCH_MP_TAC REAL_POW_LT);
(EXPAND_TAC "y4");
(REWRITE_TAC[dist]);
(MATCH_MP_TAC (NORM_ARITH `~(v2 = v3) ==> &0 < norm (v2 - v3)`));
STRIP_TAC;
(MATCH_MP_TAC (MESON[]
` collinear {v0:real^3, v2, v3} /\ ~ collinear {v0, v2, v3} ==> F`));
(CONJ_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
(ASM_MESON_TAC[COLLINEAR_2]);
(ASM_MESON_TAC[]);
STRIP_TAC;
(MATCH_MP_TAC REAL_POW_LT);
(EXPAND_TAC "y5");
(REWRITE_TAC[dist]);
(MATCH_MP_TAC (NORM_ARITH `~(v1 = v3) ==> &0 < norm (v1 - v3)`));
STRIP_TAC;
(MATCH_MP_TAC (MESON[]
` collinear {v0:real^3, v3, v1} /\ ~ collinear {v0, v3, v1} ==> F`));
(CONJ_TAC);
(ASM_REWRITE_TAC[]);
(REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
(ASM_MESON_TAC[COLLINEAR_2]);
(ASM_MESON_TAC[]);
(MATCH_MP_TAC REAL_POW_LT);
(EXPAND_TAC "y6");
(REWRITE_TAC[dist]);
(MATCH_MP_TAC (NORM_ARITH `~(v1 = v2) ==> &0 < norm (v1 - v2)`));
STRIP_TAC;
(MATCH_MP_TAC (MESON[]
` collinear {v0:real^3, v1, v2} /\ ~ collinear {v0, v1, v2} ==> F`));
(CONJ_TAC);
(REWRITE_TAC[ASSUME `v1 :real^3 = v2`]);
(REWRITE_TAC[SET_RULE `{a, b , b} = {a, b}`]);
(ASM_MESON_TAC[COLLINEAR_2]);
(ASM_MESON_TAC[]);
(* ------------------------------------------------------------------------- *)
(* FINISH the EULER LEMMA *)
(* ------------------------------------------------------------------------- *)
(REPLICATE_TAC 3 UP_ASM_TAC);
(REPLICATE_TAC 9 DEL_TAC);
(UP_ASM_TAC THEN REPLICATE_TAC 13 DEL_TAC THEN UP_ASM_TAC);
(REPEAT DEL_TAC THEN REPEAT DISCH_TAC);
(ASM_REWRITE_TAC[]);
(MP_TAC DERIVATIVE_WRT_A_Euler_lemma THEN LET_TAC);
(ASM_MESON_TAC[])]);;