(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* COMPLEMENT LEMMAS FOR EULER TRIANGLE LEMMA *) (* *) (* LEMMA ABOUT RESCALING *) (* *) (* Authour : VU KHAC KY *) (* *) (* ========================================================================= *) flyspeck_needs "trigonometry/delta_x.hl";; (* ========================================================================= *) (* SOME USEFUL TACTICS *) (* ========================================================================= *) module Euler_complement = struct open Sphere;; open Trigonometry1;; open Trigonometry2;; open Prove_by_refinement;; open Delta_x;; let UP_ASM_TAC = FIRST_X_ASSUM MP_TAC;; let DEL_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `a ==> b ==> a`);; let SWITCH_TAC = FIRST_X_ASSUM MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (MESON[] `(a ==> b ==> c) ==> (b ==> a ==> c)`) THEN DISCH_TAC THEN DISCH_TAC;; (* ========================================================================= *) (* THE FIRST LEMMA *) (* ========================================================================= *) let euler_after_rescale_t = `!v0:real^3 v1 v2 v3. norm (v1 - v0) = &1 ==> norm (v2 - v0) = &1 ==> norm (v3 - v0) = &1 ==> &2 * (&1 + (v2 - v0) dot (v3 - v0) + (v3 - v0) dot (v1 - v0) + (v1 - v0) dot (v2 - v0)) = &8 - (v2 - v3) dot (v2 - v3) - (v1 - v3) dot (v1 - v3) - (v1 - v2) dot (v1 - v2)`;; let LEMMA_FOR_EULER_AFTER_RESCALE = prove_by_refinement (euler_after_rescale_t, [(REPEAT GEN_TAC THEN REPEAT DISCH_TAC); (ABBREV_TAC `a = v1:real^3 - v0`); (ABBREV_TAC `b = v2:real^3 - v0`); (ABBREV_TAC `c = v3:real^3 - v0`); (ONCE_REWRITE_TAC[VECTOR_ARITH `x:real^3 - y = (x - v0) - (y - v0)`]); (PURE_ONCE_ASM_REWRITE_TAC[]); (DEL_TAC THEN DEL_TAC THEN DEL_TAC); (REWRITE_TAC[VECTOR_ARITH `(x:real^3 - y) dot (x - y) = x dot x + y dot y - &2 * x dot y`]) ; (PURE_ONCE_REWRITE_TAC[GSYM NORM_POW_2]); (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_ONCE_REWRITE_TAC[REAL_ARITH `&1 pow 2 = &1`]); (PURE_REWRITE_TAC[DOT_SYM]); REAL_ARITH_TAC]);; (*========================================================================= *) (* *) (* THE SECOND LEMMA : DIHV UNCHANGED *) (* *) (* =========================================================================*) let dihv_rescale_unchanged_t = `!v0 v1 v2 v3 w0 w1:real^3 w2 w3 m n p. v1 - v0 = m % (w1 - w0) /\ v2 - v0 = n % (w2 - w0) /\ v3 - v0 = p % (w3 - w0) /\ &0 < m /\ &0 < n /\ &0 < p ==> dihV v0 v1 v2 v3 = dihV w0 w1 w2 w3`;; let DIHV_RESCALE_UNCHANGED = prove_by_refinement (dihv_rescale_unchanged_t , [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC); (REWRITE_TAC[dihV] THEN REPEAT LET_TAC); (REWRITE_TAC[arcV]); (AP_TERM_TAC); (REWRITE_TAC[VECTOR_SUB_RZERO]); (* Begin subgoal 1 *) (SUBGOAL_THEN `vap':real^3 = (m * m * n) % vap` ASSUME_TAC); (EXPAND_TAC "vap'" THEN EXPAND_TAC "vap"); (PURE_ONCE_REWRITE_TAC[ASSUME `(vc':real^3) = m % vc`]); (PURE_ONCE_REWRITE_TAC[ASSUME `(va':real^3) = n % va`]); (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]); (REWRITE_TAC[VECTOR_SUB_LDISTRIB;VECTOR_MUL_ASSOC]); (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b * d) * c`]); (AP_TERM_TAC); (AP_THM_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC); REAL_ARITH_TAC; (* End subgoal 1 *) (* Begin subgoal 2 *) (SUBGOAL_THEN `vbp':real^3 = (m * m * p) % vbp` ASSUME_TAC); (EXPAND_TAC "vbp'" THEN EXPAND_TAC "vbp"); (PURE_ONCE_REWRITE_TAC[ASSUME `(vc':real^3) = m % vc`]); (PURE_ONCE_REWRITE_TAC[ASSUME `(vb':real^3) = p % vb`]); (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]); (REWRITE_TAC[VECTOR_SUB_LDISTRIB;VECTOR_MUL_ASSOC]); (REWRITE_TAC[REAL_ARITH `(a * b * c) * d = (a * b * d) * c`]); (AP_TERM_TAC); (AP_THM_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC); REAL_ARITH_TAC; (* End subgoal 2 *) (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_REWRITE_TAC[DOT_LMUL;DOT_RMUL]); (PURE_REWRITE_TAC[NORM_MUL]); (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c * d = (a * c) * b * d`]); (PURE_REWRITE_TAC[REAL_ABS_MUL]); (SUBGOAL_THEN `&0 <= m /\ &0 <= n /\ &0 <= p` ASSUME_TAC); ASM_REAL_ARITH_TAC; (SUBGOAL_THEN `abs m = m /\ abs n = n /\ abs p = p` ASSUME_TAC); (UP_ASM_TAC THEN MESON_TAC[GSYM REAL_ABS_REFL]); (UP_ASM_TAC THEN STRIP_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_ONCE_REWRITE_TAC[REAL_MUL_ASSOC]); (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(m * m * m * p) * m * n = (m * m * n) * m * m * p`]); (ABBREV_TAC `s = (m * m * n) * m * m * p`); (PURE_ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC]); (PURE_REWRITE_TAC[real_div;REAL_INV_MUL]); (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(a * b * c) = (c * b) * a`]); (REWRITE_TAC[REAL_ARITH `((a * b) * c) * d * e = (((c * d) * b) * a) * e`]); (AP_THM_TAC THEN AP_TERM_TAC); (AP_THM_TAC THEN AP_TERM_TAC); (PURE_ONCE_REWRITE_TAC[GSYM REAL_MUL_LID]); (ONCE_REWRITE_TAC[REAL_ARITH `&1 * x * y = x * y`]); (AP_THM_TAC THEN AP_TERM_TAC); (MATCH_MP_TAC REAL_MUL_LINV); (EXPAND_TAC "s"); (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> ~(a = &0)`)); (ASM_MESON_TAC[REAL_LT_MUL])]);; (*===========================================================================*) (* THE THIRD LEMMA : *) (* The lemmas help to compute p after rescaling *) (* (in general) *) (* *) (*===========================================================================*) let compute_euler_p_after_rescale_t = `!v0:real^3 v1 v2 v3 v0' v1' v2' v3' m n p. v1 - v0 = m % (v1' - v0') /\ v2 - v0 = n % (v2' - v0') /\ v3 - v0 = p % (v3' - v0') /\ &0 < m /\ &0 < n /\ &0 < p ==> euler_p v0 v1 v2 v3 = (m * n * p) * euler_p v0' v1' v2' v3'`;; let COMPUTE_EULER_P_AFTER_RESCALE = prove_by_refinement (compute_euler_p_after_rescale_t, [(REPEAT GEN_TAC THEN STRIP_TAC); (REWRITE_TAC[euler_p]); (PURE_ONCE_REWRITE_TAC[ylist]); (REPEAT LET_TAC); (REPLICATE_TAC 8 UP_ASM_TAC); (PURE_REWRITE_TAC[PAIR_EQ]); (PURE_ONCE_REWRITE_TAC[DIST_SYM]); (PURE_REWRITE_TAC[dist]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "y1'" THEN EXPAND_TAC "y2'" THEN EXPAND_TAC "y3'"); (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3"); (REPLICATE_TAC 3 UP_ASM_TAC); (REPLICATE_TAC 6 DEL_TAC); (REPLICATE_TAC 3 UP_ASM_TAC); (REPLICATE_TAC 6 DEL_TAC); (REPEAT STRIP_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (REPLICATE_TAC 6 DEL_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_ONCE_REWRITE_TAC[NORM_MUL]); (SUBGOAL_THEN `&0 <= m /\ &0 <= n /\ &0 <= p` ASSUME_TAC); (ASM_MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]); (SUBGOAL_THEN `abs m = m /\ abs n = n /\ abs p = p` ASSUME_TAC); (UP_ASM_TAC THEN MESON_TAC[REAL_ABS_REFL]); (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_REWRITE_TAC[DOT_RMUL;DOT_LMUL]); REAL_ARITH_TAC]);; (* ========================================================================= *) (* THE 4-TH LEMMA *) (* This lemma is for computing delta_x *) (* *) (* ========================================================================= *) let VECTOR_EQ_COMPONENT = prove (`!x:real^N y i. x = y ==> x$i = y$i`, REPEAT GEN_TAC THEN SUBGOAL_THEN `?k. 1 <= k /\ k <= dimindex(:N) /\ !z:real^N. z$i = z$k` CHOOSE_TAC THENL [REWRITE_TAC[FINITE_INDEX_INRANGE]; ASM_SIMP_TAC[vector_sub; CART_EQ; LAMBDA_BETA]]);; let compute_delta_x_after_rescale_t = `!v0 v1 v2 v3 v0' v1' v2' v3' m n p x1 x2 x3 x4 x5 x6 x1' x2' x3' x4' x5' x6'. v1:real^3 - v0 = m % (v1' - v0') /\ v2 - v0 = n % (v2' - v0') /\ v3 - v0 = p % (v3' - v0') /\ &0 <= m /\ &0 <= n /\ &0 <= p /\ x1',x2',x3',x4',x5',x6' = xlist v0' v1' v2' v3' /\ x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\ &0 <= delta_x x1' x2' x3' x4' x5' x6' ==> delta_x x1 x2 x3 x4 x5 x6 = (m * n * p) * (m * n * p) * delta_x x1' x2' x3' x4' x5' x6'`;; let COMPUTE_DELTA_X_AFTER_RESCALE = prove_by_refinement (compute_delta_x_after_rescale_t , [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC); (SUBGOAL_THEN `delta_x x1 x2 x3 x4 x5 x6 = (let a = v1:real^3 - v0 in let b = v2 - v0 in let c = v3 - v0 in &4 * (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 - a$2 * b$1 * c$3 + a$2 * b$3 * c$1 + a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2)` ASSUME_TAC); (ASM_MESON_TAC[COMPUTE_DELTA_X]); (SUBGOAL_THEN `delta_x x1' x2' x3' x4' x5' x6' = (let a' = v1':real^3 - v0' in let b' = v2' - v0' in let c' = v3' - v0' in &4 * (a'$1 * b'$2 * c'$3 - a'$1 * b'$3 * c'$2 - a'$2 * b'$1 * c'$3 + a'$2 * b'$3 * c'$1 + a'$3 * b'$1 * c'$2 - a'$3 * b'$2 * c'$1) pow 2)` ASSUME_TAC); (ASM_MESON_TAC[COMPUTE_DELTA_X]); (ASM_REWRITE_TAC[]); (REPEAT LET_TAC); (SUBGOAL_THEN `(a:real^3)$1 = m * (a':real^3)$1 /\ (b:real^3)$1 = n * (b':real^3)$1 /\ (c:real^3)$1 = p * (c':real^3)$1 /\ a$2 = m * a'$2 /\ a$3 = m * a'$3 /\ b$2 = n * b'$2 /\ b$3 = n * b'$3 /\ c$2 = p * c'$2 /\ c$3 = p * c'$3` ASSUME_TAC); (ASM_MESON_TAC[VECTOR_EQ_COMPONENT;VECTOR_MUL_COMPONENT]); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[POW_2]); REAL_ARITH_TAC]);; (* =========================================================================*) (* THE 5-TH LEMMA : *) (* Similar lemma for computing Sqrt(delta_x) *) (*==========================================================================*) let sqrt_delta_x_after_rescale = `!v0 v1 v2 v3 v0' v1' v2' v3' m n p x1 x2 x3 x4 x5 x6 x1' x2' x3' x4' x5' x6'. v1:real^3 - v0 = m % (v1' - v0') /\ v2 - v0 = n % (v2' - v0') /\ v3 - v0 = p % (v3' - v0') /\ &0 <= m /\ &0 <= n /\ &0 <= p /\ x1',x2',x3',x4',x5',x6' = xlist v0' v1' v2' v3' /\ x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 /\ &0 <= delta_x x1' x2' x3' x4' x5' x6' ==> sqrt (delta_x x1 x2 x3 x4 x5 x6) = (m * n * p) * sqrt (delta_x x1' x2' x3' x4' x5' x6')`;; let SQRT_DELTA_X_AFTER_RESCALE = prove_by_refinement (sqrt_delta_x_after_rescale, [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC); (SUBGOAL_THEN `delta_x x1 x2 x3 x4 x5 x6 = (m * n * p) * (m * n * p) * delta_x x1' x2' x3' x4' x5' x6'` ASSUME_TAC); (ASM_MESON_TAC[COMPUTE_DELTA_X_AFTER_RESCALE]); (PURE_ONCE_ASM_REWRITE_TAC[]); (ABBREV_TAC `S = m * n * p`); (PURE_REWRITE_TAC[REAL_MUL_ASSOC]); (SUBGOAL_THEN `sqrt ((S * S) * delta_x x1' x2' x3' x4' x5' x6') = sqrt (S * S) * sqrt (delta_x x1' x2' x3' x4' x5' x6')` ASSUME_TAC); (MATCH_MP_TAC SQRT_MUL); (EXPAND_TAC "S"); (ASM_MESON_TAC[REAL_LE_MUL]); (PURE_ONCE_ASM_REWRITE_TAC[]); (AP_THM_TAC THEN AP_TERM_TAC); (SUBGOAL_THEN `sqrt (S * S) = sqrt S pow 2` ASSUME_TAC); (REWRITE_TAC[REAL_POW_2]); (MATCH_MP_TAC SQRT_MUL); (EXPAND_TAC "S"); (ASM_MESON_TAC[REAL_LE_MUL]); (PURE_ONCE_ASM_REWRITE_TAC[]); (MATCH_MP_TAC SQRT_POW_2); (EXPAND_TAC "S"); (ASM_MESON_TAC[REAL_LE_MUL])]);; (* ===========================================================================*) (* THE SIXTH LEMMA : *) (* *) (* This following sub-lemma is necessary for proving the 6-th Lemma *) (* *) (* ===========================================================================*) let SQRT_OF_POW_2_LE = prove_by_refinement ( `!x. (&0 <= x) ==> sqrt (x pow 2) = x`, [(GEN_TAC THEN DISCH_TAC); (REWRITE_TAC[REAL_POW_2]); (SUBGOAL_THEN `sqrt (x * x) = (sqrt x) pow 2` ASSUME_TAC); (PURE_REWRITE_TAC[REAL_POW_2]); (MATCH_MP_TAC SQRT_MUL); (ASM_REWRITE_TAC[]); (PURE_ASM_REWRITE_TAC[]); (ASM_MESON_TAC[SQRT_POW_2])]);; (* ===========================================================================*) (* THE SIXTH LEMMA : *) (* This lemma says that if the Euler formulation holds *) (* for the case where x1 = x2 = x3 = 1 then it holds for all cases *) (* *) (* ===========================================================================*) let EULER_FORMULA_RESCALE = prove_by_refinement ( `(!v0 v1:real^3 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)) ==> (!v0 v1:real^3 v2 v3. let p = euler_p v0 v1 v2 v3 in let x1,x2,x3,x4,x5,x6 = xlist v0 v1 v2 v3 in let alpha1 = dihV v0 v1 v2 v3 in let alpha2 = dihV v0 v2 v3 v1 in let alpha3 = dihV v0 v3 v1 v2 in let d = delta_x x1 x2 x3 x4 x5 x6 in &0 < d ==> alpha1 + alpha2 + alpha3 - pi = pi - &2 * atn2 (sqrt d,&2 * p))`, (* -------------------------------------------------------------------------*) (* Rescale by considering new points v1',v2',v3' *) (* -------------------------------------------------------------------------*) [(DISCH_TAC THEN REPEAT GEN_TAC THEN REPEAT LET_TAC THEN DISCH_TAC); (ABBREV_TAC `v1' = v0 + inv (norm(v1:real^3 - v0)) % (v1 - v0)`); (ABBREV_TAC `v2' = v0 + inv (norm(v2:real^3 - v0)) % (v2 - v0)`); (ABBREV_TAC `v3' = v0 + inv (norm(v3:real^3 - v0)) % (v3 - v0)`); (ABBREV_TAC `w1' = (v1':real^3) - v0`); (ABBREV_TAC `w2' = (v2':real^3) - v0`); (ABBREV_TAC `w3' = (v3':real^3)- v0`); (* -------------------------------------------------------------------------*) (* Subgoal 1: &0 < norm (v1 - v0) *) (* &0 < norm (v2 - v0) *) (* &0 < norm (v3 - v0) *) (* -------------------------------------------------------------------------*) (SUBGOAL_THEN `&0 < norm (v1:real^3 - v0) /\ &0 < norm (v2:real^3 - v0) /\ &0 < norm (v3:real^3 - v0)` ASSUME_TAC); (PURE_ONCE_REWRITE_TAC[NORM_POS_LT]); (PURE_REWRITE_TAC[VECTOR_ARITH `(a - b = vec 0) <=> (a = b)`; MESON[] `(a <=> b) <=> ~ a <=> ~ b`]); (REPEAT CONJ_TAC); (* Break into 3 subgoal *) STRIP_TAC; (SUBGOAL_THEN `collinear {v0:real^3 , v1, v2}` ASSUME_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_REWRITE_TAC[collinear; SET_RULE `{a, a, b} = {a , b}`]); (EXISTS_TAC `v2:real^3 - v0`); (REPEAT GEN_TAC); (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]); STRIP_TAC; (* Break into 4 subgoals *) (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC); (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]); STRIP_TAC; (SUBGOAL_THEN `collinear {v0:real^3 , v1, v2}` ASSUME_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_REWRITE_TAC[collinear; SET_RULE `{a, b, a} = {a , b}`]); (EXISTS_TAC `v1:real^3 - v0`); (REPEAT GEN_TAC); (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]); STRIP_TAC; (* Break into 4 subgoals *) (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC); (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]); STRIP_TAC; (SUBGOAL_THEN `collinear {v0:real^3 , v1, v3}` ASSUME_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (PURE_REWRITE_TAC[collinear; SET_RULE `{a, b, a} = {a , b}`]); (EXISTS_TAC `v1:real^3 - v0`); (REPEAT GEN_TAC); (REWRITE_TAC[SET_RULE ` x IN {a, b} <=> (x = a \/ x = b)`]); STRIP_TAC; (* Break into 4 subgoals *) (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `-- &1` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&1` THEN VECTOR_ARITH_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (EXISTS_TAC `&0` THEN VECTOR_ARITH_TAC); (ASM_MESON_TAC[DELTA_X_LT_0_COLLINEAR]); (* -------------------------------------------------------------------------*) (* Subgoal 2: w1', w2', w3' havnorms equal 1 *) (* -------------------------------------------------------------------------*) (SUBGOAL_THEN `norm (w1':real^3) = &1 /\ norm (w2':real^3) = &1 /\ norm (w3':real^3) = &1` ASSUME_TAC); (EXPAND_TAC "w1'" THEN EXPAND_TAC "w2'" THEN EXPAND_TAC "w3'"); (UP_ASM_TAC THEN REPLICATE_TAC 3 DEL_TAC THEN DISCH_TAC); (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'"); (ONCE_REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]); (REWRITE_TAC[NORM_MUL;REAL_ABS_INV]); (SUBGOAL_THEN `abs (norm (v1 - v0)) = norm (v1:real^3 - v0) /\ abs (norm (v2 - v0)) = norm (v2:real^3 - v0) /\ abs (norm (v3 - v0)) = norm (v3:real^3 - v0)` ASSUME_TAC); (SIMP_TAC[NORM_POS_LE;REAL_ABS_REFL]); (ONCE_ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~(a = &0)`;REAL_MUL_LINV]); (* ------------------------------------------------------------------------- *) (* SUBGOAL 3 : *) (* alpha1, alpha2, alpha3 arunchanged *) (* ------------------------------------------------------------------------- *) (ABBREV_TAC `alpha1' = dihV (v0:real^3) v1' v2' v3'`); (ABBREV_TAC `alpha2' = dihV (v0:real^3) v2' v3' v1'`); (ABBREV_TAC `alpha3' = dihV (v0:real^3) v3' v1' v2'`); (SUBGOAL_THEN `alpha1:real = alpha1' /\ alpha2:real = alpha2' /\ alpha3:real = alpha3'` ASSUME_TAC); (EXPAND_TAC "alpha1" THEN EXPAND_TAC "alpha2" THEN EXPAND_TAC "alpha3"); (EXPAND_TAC "alpha1'" THEN EXPAND_TAC "alpha2'" THEN EXPAND_TAC "alpha3'"); (ABBREV_TAC `m = inv (norm (v1:real^3 - v0))`); (ABBREV_TAC `n = inv (norm (v2:real^3 - v0))`); (ABBREV_TAC `q = inv (norm (v3:real^3 - v0))`); (SUBGOAL_THEN ` v1' - v0 = m % (v1:real^3 - v0) /\ v2' - v0 = n % (v2:real^3 - v0) /\ v3' - v0 = q % (v3:real^3 - v0)` ASSUME_TAC); (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'"); (VECTOR_ARITH_TAC); (SUBGOAL_THEN `&0 < m /\ &0 < n /\ &0 < q ` ASSUME_TAC); (EXPAND_TAC "m" THEN EXPAND_TAC "n" THEN EXPAND_TAC "q"); (REPLICATE_TAC 8 DEL_TAC THEN UP_ASM_TAC THEN STRIP_TAC); (ASM_MESON_TAC[REAL_LT_INV]); (ASM_MESON_TAC[DIHV_RESCALE_UNCHANGED]); (* ========================================================================== *) (* Subgoal 4: *) (* (x1',x2',x3,'x4',x5',x6') = xlist (v0:real^3) v1' v2' v3' *) (* ========================================================================== *) (ABBREV_TAC `p' = euler_p (v0:real^3) v1' v2' v3'`); (ABBREV_TAC `x1' = dist (v0:real^3,v1') pow 2`); (ABBREV_TAC `x2' = dist (v0:real^3,v2') pow 2`); (ABBREV_TAC `x3' = dist (v0:real^3,v3') pow 2`); (ABBREV_TAC `x4' = dist (v2':real^3,v3') pow 2`); (ABBREV_TAC `x5' = dist (v1':real^3,v3') pow 2`); (ABBREV_TAC `x6' = dist (v1':real^3,v2') pow 2`); (ABBREV_TAC `d' = delta_x (x1':real) x2' x3' x4' x5' x6' `); (SUBGOAL_THEN `x1':real,x2',x3',x4',x5',x6' = xlist (v0:real^3) v1' v2' v3'` ASSUME_TAC); (REWRITE_TAC[xlist;ylist]); (REPEAT LET_TAC); (UP_ASM_TAC THEN PURE_REWRITE_TAC[PAIR_EQ] THEN STRIP_TAC); (ASM_MESON_TAC[PAIR_EQ]); (* --------------------------------------------------------------------------*) (* Subgoal 5: *) (* p' = k * p with somk *) (*---------------------------------------------------------------------------*) (ABBREV_TAC `t1 = inv (norm ((v1:real^3) - v0)) `); (ABBREV_TAC `t2 = inv (norm ((v2:real^3) - v0)) `); (ABBREV_TAC `t3 = inv (norm ((v3:real^3) - v0)) `); (SUBGOAL_THEN `p' = (t1 * t2 * t3) * p` ASSUME_TAC); (EXPAND_TAC "p" THEN EXPAND_TAC "p'"); (MATCH_MP_TAC COMPUTE_EULER_P_AFTER_RESCALE); (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'"); (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]); (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3"); (ASM_MESON_TAC[REAL_LT_INV]); (* --------------------------------------------------------------------------*) (* Subgoal 6: *) (* d' = k * d with somk *) (*---------------------------------------------------------------------------*) (SUBGOAL_THEN `d' = (t1 * t2 * t3) * (t1 * t2 * t3) * d` ASSUME_TAC); (EXPAND_TAC "d" THEN EXPAND_TAC "d'"); (MATCH_MP_TAC COMPUTE_DELTA_X_AFTER_RESCALE); (EXISTS_TAC `v0:real^3`); (EXISTS_TAC `v1':real^3`); (EXISTS_TAC `v2':real^3`); (EXISTS_TAC `v3':real^3`); (EXISTS_TAC `v0:real^3`); (EXISTS_TAC `v1:real^3`); (EXISTS_TAC `v2:real^3`); (EXISTS_TAC `v3:real^3`); (EXPAND_TAC "v1'" THEN EXPAND_TAC "v2'" THEN EXPAND_TAC "v3'"); (REWRITE_TAC[VECTOR_ARITH `((a:real^3) + b) - a = b`]); (ASM_REWRITE_TAC[]); (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 < d` ASSUME_TAC); (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3"); (REPLICATE_TAC 18 DEL_TAC); (UP_ASM_TAC THEN REPLICATE_TAC 6 DEL_TAC THEN UP_ASM_TAC); (MESON_TAC[REAL_LT_INV]); (UP_ASM_TAC THEN MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]); (* -------------------------------------------------------------------------- *) (* Subgoal 7: *) (* This part is thproof of d' > 0 *) (* -------------------------------------------------------------------------- *) (SUBGOAL_THEN `&0 < d'` ASSUME_TAC); (PURE_ONCE_ASM_REWRITE_TAC[]); (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 < d` ASSUME_TAC); (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3"); (REPLICATE_TAC 19 DEL_TAC); (UP_ASM_TAC THEN REPLICATE_TAC 6 DEL_TAC THEN UP_ASM_TAC); (MESON_TAC[REAL_LT_INV]); (UP_ASM_TAC THEN MESON_TAC[REAL_LT_MUL]); (*---------------------------------------------------------------------------*) (* Subgoal 8: *) (* atn2 (sqrt d,&2 * p) is unchanged *) (*---------------------------------------------------------------------------*) (SUBGOAL_THEN `&2 * atn2 (sqrt (d':real), &2 * (p':real)) = &2 * atn2 (sqrt (d:real), &2 * (p:real))` ASSUME_TAC); AP_TERM_TAC; (* Sugoal 8.1 *) (SUBGOAL_THEN `&0 < sqrt d /\ &0 < sqrt d'` ASSUME_TAC); (MESON_TAC[ASSUME `&0 < d`; ASSUME `&0 < d'`; SQRT_POS_LT]); (* Sugoal 8.2 *) (SUBGOAL_THEN `atn2 (sqrt d,&2 * p) = atn ((&2 * p) / sqrt d)` ASSUME_TAC); (FIRST_ASSUM MP_TAC THEN MESON_TAC[ATN2_BREAKDOWN]); (* Sugoal 8.3 *) (SUBGOAL_THEN `atn2 (sqrt d',&2 * p') = atn ((&2 * p') / sqrt d')` ASSUME_TAC); (MESON_TAC[ASSUME `&0 < sqrt d /\ &0 < sqrt d'`; ATN2_BREAKDOWN]); (ONCE_ASM_REWRITE_TAC[]); AP_TERM_TAC; (DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN STRIP_TAC); (* Sugoal 8.4 *) (SUBGOAL_THEN `((&2 * p') / sqrt d' = (&2 * p) / sqrt d) <=> &2 * p' = ((&2 * p) / sqrt d) * sqrt d'` ASSUME_TAC); (UP_ASM_TAC THEN MESON_TAC[REAL_EQ_LDIV_EQ]); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `((x * y) / b) * c = x * (c * y) / b`]); AP_TERM_TAC; DEL_TAC; (PURE_ASM_REWRITE_TAC[REAL_EQ_LDIV_EQ]); (PURE_ONCE_REWRITE_TAC[REAL_ARITH `(x * y) / b = (x / b) * y`]); (AP_THM_TAC THEN AP_TERM_TAC); (ABBREV_TAC `S = t1 * t2 * t3`); (REWRITE_TAC[REAL_MUL_ASSOC;GSYM REAL_POW_2]); (* Subgoal 8.5 *) (SUBGOAL_THEN `sqrt (S pow 2 * d) = sqrt (S pow 2) * sqrt d` ASSUME_TAC); (MATCH_MP_TAC SQRT_MUL); (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> &0 <= a`]); (MESON_TAC[REAL_LE_POW_2]); (ONCE_ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[REAL_ARITH `(a * b) / c = a * (b / c)`]); (* Subgoal 8.6 *) (SUBGOAL_THEN `sqrt d / sqrt d = &1` ASSUME_TAC); (MATCH_MP_TAC REAL_DIV_REFL); (ASM_SIMP_TAC[REAL_ARITH `&0 < a ==> ~ (a = &0)`]); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_MUL_RID]); (MATCH_MP_TAC (GSYM SQRT_OF_POW_2_LE)); (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`)); (EXPAND_TAC "S"); (* Subgoal 8.7 *) (SUBGOAL_THEN `&0 < t1 /\ &0 < t2 /\ &0 < t3 /\ &0 < d` ASSUME_TAC); (EXPAND_TAC "t1" THEN EXPAND_TAC "t2" THEN EXPAND_TAC "t3"); (REPLICATE_TAC 19 DEL_TAC); (ASM_MESON_TAC[REAL_LT_INV]); (UP_ASM_TAC THEN MESON_TAC[REAL_LT_MUL]); (*---------------------------------------------------------------------------*) (* SUBGOAL 9 : *) (* Finish the lemma about rescaling *) (*---------------------------------------------------------------------------*) (SUBGOAL_THEN `alpha1' + alpha2' + alpha3' - pi = pi - &2 * atn2 (sqrt d',&2 * p')` ASSUME_TAC); (ASM_MESON_TAC[]); (ASM_MESON_TAC[])]);; (* ==========================================================================*) (* LEMMA 7 : *) (* ~ collinear {a, b, c} ==> norm(a - b) > &0 *) (* ==========================================================================*) let COLLINEAR_NORM_LT_0 = prove_by_refinement ( `!(a:real^3) b c. ~collinear {a, b, c} ==> &0 < norm (a - b)`, [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC); (REWRITE_TAC[NORM_POS_LT]); STRIP_TAC; (UP_ASM_TAC THEN PURE_ONCE_REWRITE_TAC[ VECTOR_ARITH `(a:real^3) - b = vec 0 <=> b - a = vec 0`]); STRIP_TAC; (SUBGOAL_THEN `collinear {(a:real^3), b, c}` ASSUME_TAC); (MATCH_MP_TAC (GEN_ALL ALLEMI_COLLINEAR)); (ASM_REWRITE_TAC[]); (MESON_TAC [VECTOR_ARITH `a dot vec 0 = &0`; VECTOR_ARITH `a % vec 0 = vec 0`; VECTOR_ARITH `(&0) % c = vec 0`]); (ASM_MESON_TAC[])]);; (* ========================================================================= *) (* LEMMA 8: *) (* ========================================================================= *) let REAL_LT_RSQRT2 = prove (`!x y. x pow 2 < y ==> -- sqrt y < x`, REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH `abs x < a ==> -- a < x`) THEN REWRITE_TAC[GSYM POW_2_SQRT_ABS] THEN MATCH_MP_TAC SQRT_MONO_LT THEN ASM_REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);; let EULER_TRIANGLE_REAL_INTERVAL = prove_by_refinement ( `!s a b c. s = {x | &0 < ups_x x b c - x * b * c} /\ &0 < ups_x a b c - a * b * c ==> is_realinterval s`, [(REPEAT GEN_TAC THEN STRIP_TAC); (ABBREV_TAC `d = b * c * b * c / &4 - b * c * (b + c) + &4 * b * c `); (ABBREV_TAC `f = (\a. a - b - c + b * c / &2)`); (* ------------------------------------------------------------------------- *) (* SUBGOAL 1 *) (* ------------------------------------------------------------------------- *) (SUBGOAL_THEN `&0 < d` ASSUME_TAC); (EXPAND_TAC "d" THEN DEL_TAC THEN DEL_TAC); (UP_ASM_TAC THEN REWRITE_TAC[ups_x] THEN DISCH_TAC); (MATCH_MP_TAC (REAL_ARITH `&0 <= (a - b - c + b * c / &2) pow 2 /\ &0 < S - (a - b - c + b * c / &2) pow 2 ==> &0 < S`)); (REWRITE_TAC[REAL_LE_POW_2]); ASM_REAL_ARITH_TAC; (* ------------------------------------------------------------------------- *) (* SUBGOAL 2 *) (* ------------------------------------------------------------------------- *) (SUBGOAL_THEN `!(z:real). z IN s <=> f z < sqrt d /\ --sqrt d < f z` ASSUME_TAC); GEN_TAC; (ONCE_ASM_REWRITE_TAC[] THEN ONCE_ASM_REWRITE_TAC[IN_ELIM_THM]); (EQ_TAC); (* Break into 2 subgoal 2.1 and 2.2 *) (REWRITE_TAC[ups_x] THEN DISCH_TAC); (SUBGOAL_THEN `(f (z:real)) pow 2 < d /\ (f z) pow 2 < d` ASSUME_TAC); (EXPAND_TAC "d" THEN EXPAND_TAC "f"); (PURE_REWRITE_TAC[REAL_POW_2]); (ASM_REAL_ARITH_TAC); (ASM_MESON_TAC[REAL_LT_RSQRT;REAL_LT_RSQRT2]); (REWRITE_TAC[ups_x] THEN EXPAND_TAC "f"); STRIP_TAC; (REWRITE_TAC[REAL_ARITH `(--z * z - b * b - c * c + &2 * z * c + &2 * z * b + &2 * b * c) - z * b * c = (b * c * b * c / &4 - b * c * (b + c) + &4 * b * c) - (z - b - c + b * c / &2) pow 2`]); (REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`]); (PURE_ONCE_ASM_REWRITE_TAC[]); (REPLICATE_TAC 2 UP_ASM_TAC THEN PURE_REWRITE_TAC[MESON[REAL_BOUNDS_LT] `(a < x ==> -- x < a ==> y) <=> abs a < x ==> y` ]); DISCH_TAC; (SUBGOAL_THEN `d = sqrt d pow 2` ASSUME_TAC); (ASM_MESON_TAC[REAL_ARITH `&0 < a ==> &0 <= a`; SQRT_POW_2]); (PURE_ONCE_ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS]); (MATCH_MP_TAC (REAL_ARITH `x = sqrt d /\ y < sqrt d ==> y < x`)); (ASM_REWRITE_TAC[]); (PURE_REWRITE_TAC[REAL_ABS_REFL]); (MATCH_MP_TAC (REAL_ARITH `&0 < x ==> &0 <= x`)); (ASM_MESON_TAC[SQRT_POS_LT]); (* ------------------------------------------------------------------------- *) (* LAST SUBGOALS *) (* ------------------------------------------------------------------------- *) (REWRITE_TAC[is_realinterval]); (REPEAT GEN_TAC THEN STRIP_TAC); (ONCE_ASM_REWRITE_TAC[]); CONJ_TAC; (SUBGOAL_THEN `f (c':real) <= f b'` ASSUME_TAC); (EXPAND_TAC "f" THEN ASM_REAL_ARITH_TAC); (SUBGOAL_THEN `f (b':real) < sqrt d` ASSUME_TAC); (EXPAND_TAC "f" THEN ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (SUBGOAL_THEN `f (a':real) <= f c'` ASSUME_TAC); (EXPAND_TAC "f" THEN ASM_REAL_ARITH_TAC); (SUBGOAL_THEN `-- sqrt d < f (a':real)` ASSUME_TAC); (EXPAND_TAC "f" THEN ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC)]);; (* ==========================================================================*) (* LEMMA 10: *) (* *) (* ==========================================================================*) let OJEKOJF2 = prove (`!v0:real^3 v1 v2 v3. let ga = dihV v0 v1 v2 v3 in let v01 = dist (v0,v1) pow 2 in let v02 = dist (v0,v2) pow 2 in let v03 = dist (v0,v3) pow 2 in let v12 = dist (v1,v2) pow 2 in let v13 = dist (v1,v3) pow 2 in let v23 = dist (v2,v3) pow 2 in ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3} ==> ga = pi / &2 - atn2 (sqrt (&4 * v01 * delta_x v01 v02 v03 v23 v13 v12), delta_x4 v01 v02 v03 v23 v13 v12)`, MP_TAC OJEKOJF THEN REPEAT LET_TAC THEN MESON_TAC[]);; let COMPUTE_DIHV_ATN2 = prove (`!(v0:real^3) v1 v2 v3 gamma x1 x2 x3 x4 x5 x6. gamma = dihV v0 v1 v2 v3 /\ x1 = dist (v0,v1) pow 2 /\ x2 = dist (v0,v2) pow 2 /\ x3 = dist (v0,v3) pow 2 /\ x6 = dist (v1,v2) pow 2 /\ x5 = dist (v1,v3) pow 2 /\ x4 = dist (v2,v3) pow 2 /\ ~collinear {v0, v1, v2} /\ ~collinear {v0, v1, v3} ==> gamma = pi / &2 - atn2( sqrt ( &4 * x1 * delta_x x1 x2 x3 x4 x5 x6), delta_x4 x1 x2 x3 x4 x5 x6)`, REPEAT STRIP_TAC THEN MP_TAC OJEKOJF2 THEN REPEAT LET_TAC THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "ga" THEN EXPAND_TAC "v01" THEN EXPAND_TAC "v02" THEN EXPAND_TAC "v03" THEN EXPAND_TAC "v13" THEN EXPAND_TAC "v23" THEN EXPAND_TAC "v12" THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);; end;;