(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Local Fan *)
(* Author: Nguyen Quang Truong *)
(* Date: 2010-05-09 *)
(* ========================================================================== *)
(* rho_fan interior_angle *)
flyspeck_needs "local/LDURDPN.hl";;
module type Local_lemmas_type = sig
end;;
(* ================================================================ *)
(* lemma 6.13 - KOMWBWC *)
module Local_lemmas = struct
parse_as_infix("has_orders",(12,"right"));;
parse_as_infix("cyclic_on",(13,"right"));;
open Ldurdpn;;
open Lvducxu;;
open Sphere;;
open Trigonometry1;;
open Trigonometry2;;
open Hypermap;;
open Fan;;
open Prove_by_refinement;;
open Wrgcvdr_cizmrrh;;
open Aff_sgn_tac;;
let SWITCH_TAC t = UNDISCH_TAC t THEN DISCH_THEN (ASSUME_TAC o GSYM);;
let LOCAL_FAN_RHO_NODE_PROS = prove_by_refinement
(`
local_fan (V,E,
FF)
==> (!x. x
IN V ==> x, (
rho_node1 FF x)
IN FF) /\
(!x. x
IN FF ==> x =
FST x,
rho_node1 FF (
FST x))`,
[ABBREV_TAC `k = (\x.
FST (x:real^3 # real^3)) `;
SWITCH_TAC `(\x.
FST (x:real^3 # real^3)) = k`;
STRIP_TAC;
MP_TAC2 Wrgcvdr_cizmrrh.BIJ_BETWEEN_FF_AND_V;
REWRITE_TAC[
BIJ];
STRIP_TAC;
SUBGOAL_THEN ` (!x. x
IN V ==> x,
rho_node1 FF x
IN (FF:real^3 # real^3 -> bool))` ASSUME_TAC;
REPEAT STRIP_TAC;
REWRITE_TAC[
rho_node1];
CONV_TAC SELECT_CONV;
DOWN THEN DOWN;
REWRITE_TAC[
SURJ];
STRIP_TAC;
FIRST_ASSUM NHANH;
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC `
SND (y:real^3 # real^3) `;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[];
DOWN THEN SIMP_TAC[];
DOWN;
REWRITE_TAC[
SURJ];
STRIP_TAC THEN STRIP_TAC;
UNDISCH_TAC ` !x. x
IN (FF:real^3 # real^3 -> bool) ==> k x
IN (V:real^3 -> bool) ` ;
DISCH_THEN NHANH;
FIRST_X_ASSUM NHANH;
DOWN THEN DOWN;
ASM_REWRITE_TAC[
INJ];
MESON_TAC[
FST]]);;
let SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ = prove_by_refinement
(` {a:real^3,b,c}
SUBSET affine hull {x,y,z} /\ ~(
collinear {a,b,c})
==>
affine hull {x,y,z} =
affine hull {a,b,c} `,
ASM_SIMP_TAC[];
MESON_TAC[FACE_NOT_EMPTY; ARITH_RULE` 1 <= a ==> ~( 1 = 2 * a ) `]]);;
let GRAPH_WITH_SET2 = prove(
`
graph E ==> (! a b. {a,b}
IN E ==> ~( a = b )) `,
REWRITE_TAC[graph2] THEN DISCH_THEN NHANH THEN
SIMP_TAC[Geomdetail.CARD2]);;
let LOCAL_FAN_RHO_NODE_PROS2 = ONCE_REWRITE_RULE[TAUT` a /\ b <=> b /\ a `] LOCAL_FAN_RHO_NODE_PROS;;
REWRITE_TAC[ARITH_RULE` a <= b <=> a < b + 1 `];
REWRITE_TAC[FINTE_OF_N_FIRST_ELMS2];
STRIP_TAC;
ASM_CASES_TAC ` l = 0 `;
ASM_REWRITE_TAC[ARITH_RULE ` x < 0 + 1 <=> x = 0`; IN_ELIM_THM];
CONJ_TAC;
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[VECTOR_SUB_REFL; DOT_LZERO];
REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER; IN_ELIM_THM];
STRIP_TAC;
STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[ITER; AFFINE_HULL_2; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
SUBGOAL_THEN ` v dot (e:real^3) = &0` ASSUME_TAC;
EXPAND_TAC "e";
REWRITE_TAC[DOT_CROSS_SELF];
DOWN;
ASM_REWRITE_TAC[DOT_LMUL; REAL_ENTIRE; DOT_EQ_0];
STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN;
REWRITE_TAC[VECTOR_MUL_LZERO];
MP_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
REWRITE_TAC[FAN; fan2];
UNDISCH_TAC ` v:real^3 IN V `;
MESON_TAC[];
SUBGOAL_THEN ` {vec 0, v, rho_node1 (FF:real^3 # real^3 -> bool) v} SUBSET P ` ASSUME_TAC;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
UNDISCH_TAC ` U SUBSET (P:real^3 -> bool) `;
MATCH_MP_TAC (SET_RULE` a IN S /\ b IN S ==> S SUBSET A ==> a IN A /\ b IN A `);
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC ` 0`;
DOWN;
REWRITE_TAC[ITER];
ARITH_TAC;
EXISTS_TAC ` 1 `;
DOWN;
REWRITE_TAC[ITER1];
ARITH_TAC;
DOWN;
UNDISCH_TAC ` plane (P:real^3 -> bool) `;
PHA;
NHANH PLANE_AFFINE_HUL_INTER_P;
ASM_REWRITE_TAC[VECTOR_SUB_RZERO; VECTOR_ADD_LID];
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_V;
UNDISCH_TAC ` v:real^3 IN V `;
FIRST_ASSUM NHANH;
ASM_REWRITE_TAC[ARITH_RULE` a < b + 1 <=> a <= b `];
REPEAT STRIP_TAC;
SUBGOAL_THEN ` ! u. u IN U ==> (u:real^3) dot --e = &0 ` ASSUME_TAC;
REPEAT STRIP_TAC;
SUBGOAL_THEN ` {vec 0, v, rho_node1 FF v, u:real^3} SUBSET P` MP_TAC;
DOWN_TAC;
SIMP_TAC[INSERT_SUBSET];
STRIP_TAC;
DOWN;
UNDISCH_TAC ` U SUBSET (P:real^3 -> bool) `;
SET_TAC[];
UNDISCH_TAC `plane (P:real^3 -> bool) `;
REWRITE_TAC[plane];
STRIP_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN ` coplanar {vec 0, v, rho_node1 FF v, u:real^3} ` MP_TAC;
REWRITE_TAC[coplanar];
DOWN THEN MESON_TAC[];
ASM_REWRITE_TAC[COPLANAR_IFF_CROSS_DOT; VECTOR_SUB_RZERO; DOT_RNEG];
SIMP_TAC[DOT_SYM];
REAL_ARITH_TAC;
ASM_SIMP_TAC[DOT_LSUB; VECTOR_SUB_LZERO];
REAL_ARITH_TAC;
REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER];
REPEAT STRIP_TAC;
SUBGOAL_THEN ` x IN affine hull {vec 0, e:real^3} INTER P` MP_TAC;
ASM_REWRITE_TAC[IN_INTER];
UNDISCH_TAC ` x IN U:real ^3 -> bool `;
UNDISCH_TAC ` U SUBSET P:real^3 -> bool `;
SET_TAC[];
ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
SUBGOAL_THEN ` U SUBSET (V:real^3 -> bool) ` MP_TAC;
EXPAND_TAC "U";
EXPAND_TAC "V";
REWRITE_TAC[GSYM POWER_TO_ITER; lemma_subset_orbit];
REWRITE_TAC[SUBSET];
STRIP_TAC;
UNDISCH_TAC ` x:real^3 IN U `;
FIRST_X_ASSUM NHANH;
MP_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
REWRITE_TAC[FAN; fan2];
MESON_TAC[]]);;
open Fan_misc;;
open Fan_defs;;
open Planarity;;
open Topology;;
REWRITE_TAC[IN_ELIM_THM];
EXPAND_TAC "px";
EXPAND_TAC "py";
EXPAND_TAC "pz";
MP_TAC2 (ARITH_RULE` SUC i < l ==> SUC i + 1 <= l /\ i <= l /\ i + 1 <= l`);
MESON_TAC[];
STRIP_TAC;
SUBGOAL_THEN ` {px, py, pz} SUBSET (P:real^3 -> bool) ` ASSUME_TAC;
UNDISCH_TAC ` U SUBSET (P:real^3 -> bool) `;
DOWN;
PHA;
REWRITE_TAC[SUBSET_TRANS];
SUBGOAL_THEN ` rho_node1 (FF:real^3 # real^3 -> bool) px = py /\
rho_node1 (FF:real^3 # real^3 -> bool) py = pz` MP_TAC;
EXPAND_TAC "px";
EXPAND_TAC "py";
EXPAND_TAC "pz";
REWRITE_TAC[GSYM ITER; ADD1];
STRIP_TAC;
SUBGOAL_THEN ` {vec 0, px, rho_node1 FF px} SUBSET (P:real^3 -> bool) ` MP_TAC;
UNDISCH_TAC ` {px,py,pz:real^3} SUBSET P `;
ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET];
STRIP_TAC;
SUBGOAL_THEN ` affine hull {vec 0, px, py:real^3} = P ` MP_TAC;
MATCH_MP_TAC THREE_NOT_COLL_DETER_PLANE;
ASM_REWRITE_TAC[];
UNDISCH_TAC ` ~collinear {vec 0, px, rho_node1 FF (px:real^3)}`;
UNDISCH_TAC ` {vec 0, px, rho_node1 FF px} SUBSET (P:real^3 -> bool) `;
PHA;
ASM_SIMP_TAC[];
REWRITE_TAC[AFFINE_HULL_3];
STRIP_TAC;
UNDISCH_TAC ` {px, py, pz} SUBSET (P:real^3 -> bool) `;
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
STRIP_TAC;
DOWN;
EXPAND_TAC "P";
REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
ASM_CASES_TAC` v' < &0 `;
ASM_REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID];
ONCE_REWRITE_TAC[CROSS_SKEW];
REWRITE_TAC[ DOT_LMUL; DOT_LNEG; REAL_ARITH` a * -- b = (-- a ) * b `];
MATCH_MP_TAC REAL_LT_MUL;
ASM_SIMP_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `];
DOWN;
REWRITE_TAC[REAL_ARITH` ~( a < &0 ) <=> &0 <= a `];
STRIP_TAC;
ASM_CASES_TAC ` &0 <= w `;
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_V;
UNDISCH_TAC `v:real^3 IN V `;
FIRST_ASSUM NHANH;
STRIP_TAC;
SUBGOAL_THEN ` px:real^3 IN V ` MP_TAC;
EXPAND_TAC "V";
EXPAND_TAC "px";
REWRITE_TAC[lemma_in_orbit; GSYM POWER_TO_ITER];
MP_TAC2 LOCAL_FAN_IMP_NOT_SEMI_IDE;
DISCH_THEN NHANH;
SWITCH_TAC ` pz = v' % px + w % (py:real^3) `;
ASM_REWRITE_TAC[];
STRIP_TAC;
MP_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
REWRITE_TAC[FAN; fan7];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC2 o (SPECL [` {px, py:real^3}`;` {pz:real^3 }`]));
UNDISCH_TAC ` (px:real^3),rho_node1 FF px IN ord_pairs E`;
ASM_SIMP_TAC[Wrgcvdr_cizmrrh.IN_ORD_E_EQ_IN_E; IN_UNION];
STRIP_TAC;
DISJ2_TAC;
REWRITE_TAC[IN_ELIM_THM; EXTENSION; IN_INSERT; NOT_IN_EMPTY];
EXISTS_TAC ` pz:real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC ` ITER (SUC i + 1) (rho_node1 FF) v:real^3 = pz:real^3`;
STRIP_TAC;
EXPAND_TAC "pz";
EXPAND_TAC "V";
REWRITE_TAC[GSYM POWER_TO_ITER; lemma_in_orbit];
SUBGOAL_THEN ` {px,py} INTER {pz:real^3} = {} ` SUBST1_TAC;
ASM_REWRITE_TAC[SET_RULE ` {a,b} INTER {x} = {} <=> ~( x = a ) /\ ~( x = b )`];
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
SUBGOAL_THEN ` py:real^3 IN V ` MP_TAC;
EXPAND_TAC "py";
EXPAND_TAC "V";
EXPAND_TAC "px";
REWRITE_TAC[GSYM ITER];
REWRITE_TAC[GSYM POWER_TO_ITER; lemma_in_orbit];
FIRST_X_ASSUM NHANH;
ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING];
SUBGOAL_THEN ` pz:real^3 IN V /\ py IN V` MP_TAC;
SWITCH_TAC ` ITER (SUC i + 1) (rho_node1 FF) v = pz:real^3 `;
ASM_REWRITE_TAC[GSYM ITER];
EXPAND_TAC "V";
EXPAND_TAC "py";
EXPAND_TAC "px";
REWRITE_TAC[GSYM ITER];
REWRITE_TAC[GSYM POWER_TO_ITER; lemma_in_orbit];
STRIP_TAC;
SUBGOAL_THEN ` DISJOINT {vec 0} {px, py:real^3} /\ ~( vec 0 = pz:real^3)` MP_TAC;
UNDISCH_TAC ` fan2 (vec 0:real^3, V:real^3 -> bool, E: (real^3 -> bool) -> bool) `;
REWRITE_TAC[fan2; SET_RULE `DISJOINT {x} {a,b} <=> ~( x = a ) /\ ~( x = b ) `];
ASM_MESON_TAC[];
REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING];
STRIP_TAC;
SUBGOAL_THEN ` pz:real^3 IN aff_ge {vec 0} {px, py} INTER aff_ge {vec 0} {pz} ` ASSUME_TAC;
ASM_SIMP_TAC[IN_INTER; Fan.AFF_GE_1_2; Fan.AFF_GE_1_1];
CONJ_TAC;
REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
EXPAND_TAC "pz";
UNDISCH_TAC ` &0 <= v' `;
UNDISCH_TAC ` &0 <= w `;
MESON_TAC[REAL_ARITH` (&1 - a - b ) + a + b = &1 `];
REWRITE_TAC[IN_ELIM_THM];
REWRITE_TAC[ENDS_IN_HALFLINE];
DISCH_THEN SUBST_ALL_TAC;
DOWN;
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
DOWN;
MESON_TAC[];
ASM_CASES_TAC ` v' = &0 `;
UNDISCH_TAC` pz = v' % px + w % (py:real^3) `;
ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID];
NHANH (MESON[COLLINEAR_LEMMA]` x = a % y ==> collinear {vec 0,y,x}`);
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
ASSUME_TAC2 LOCAL_FAN_ITER_RHO_NODE_IN_V;
FIRST_ASSUM (MP_TAC o (SPEC ` i + 1 `));
FIRST_ASSUM NHANH;
ASM_REWRITE_TAC[];
SIMP_TAC[];
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
ASSUME_TAC2 LOCAL_FAN_IMP_NOT_SEMI_IDE;
ASSUME_TAC2 LOCAL_FAN_ITER_RHO_NODE_IN_V;
FIRST_ASSUM (MP_TAC o (SPEC ` i: num`));
FIRST_X_ASSUM NHANH;
FIRST_ASSUM (MP_TAC o (SPEC ` i + 1`));
FIRST_ASSUM NHANH;
SWITCH_TAC ` pz = v' % px + w % (py:real^3) `;
ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.IN_ORD_E_EQ_IN_E];
STRIP_TAC THEN STRIP_TAC;
MP_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
REWRITE_TAC[FAN; fan7];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC2 o (SPECL [` {py, pz:real^3}`;` {px:real^3}`]));
ASM_REWRITE_TAC[IN_UNION; IN_ELIM_THM; EXTENSION; IN_INSERT; NOT_IN_EMPTY];
DISJ2_TAC;
EXISTS_TAC ` px:real^3`;
UNDISCH_TAC ` ITER (i) (rho_node1 FF) v = (px:real^3)`;
DISCH_THEN (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[];
SUBGOAL_THEN ` {py, pz} INTER {px:real^3} = {} ` SUBST1_TAC;
ASM_REWRITE_TAC[SET_RULE` {a,b} INTER {x} = {} <=> ~( a = x ) /\ ~( b = x )`; AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING];
SUBGOAL_THEN ` DISJOINT {vec 0} {py, pz:real^3} /\ ~( vec 0 = px:real^3)` MP_TAC;
REWRITE_TAC[SET_RULE` DISJOINT {x} {a,b} <=> ~( x = a ) /\ ~( x = b )`];
DOWN_TAC;
NHANH Collect_geom.NOT_COL3_IMP_DIFF;
SIMP_TAC[DE_MORGAN_THM];
STRIP_TAC;
SUBGOAL_THEN ` v' % (px:real^3) IN aff_ge {vec 0} {py, pz} INTER aff_ge {vec 0} {px} ` MP_TAC;
ASM_SIMP_TAC[Fan.AFF_GE_1_2; Fan.AFF_GE_1_1; IN_INTER; IN_ELIM_THM];
CONJ_TAC;
UNDISCH_TAC ` v' % px + w % py = (pz:real^3 )`;
UNDISCH_TAC` ~( &0 <= w ) `;
NHANH (REAL_ARITH` ~( &0 <= x ) ==> &0 <= -- x `);
PHA;
SIMP_TAC[VECTOR_ARITH` a + b % y = z <=> a = ( -- b ) % y + z `; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
MESON_TAC[REAL_ARITH` &0 <= &1 /\ a + -- a + &1 = &1 `; VECTOR_MUL_LID];
REWRITE_TAC[HALFLINE; IN_ELIM_THM];
EXISTS_TAC ` v':real` ;
ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];
DISCH_TAC;
DISCH_THEN SUBST_ALL_TAC;
DOWN;
ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; VECTOR_MUL_EQ_0;
AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]]);;
let MIXED_PROD_POS_IMP_RANGE_AZIM = prove_by_refinement
(`~collinear {
vec 0, u, v} /\ ~collinear {
vec 0, u, w} /\
&0 < (u
cross v)
dot w ==> &0 <
azim (
vec 0) u v w /\
azim (
vec 0) u v w <
pi `,
[STRIP_TAC;
MP_TAC2 (SPEC_ALL Planarity.JBDNJJB);
STRIP_TAC;
SUBGOAL_THEN` &0 <
sin (
azim (
vec 0) u v w) ` ASSUME_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC
REAL_LT_MUL;
ASM_REWRITE_TAC[];
MP_TAC (SPECL [`
vec 0:real^3 `;` u:real^3`;` v:real^3 `;` w:real^3 `]
AZIM_RANGE);
ASM_CASES_TAC `
azim (
vec 0) u v w <=
pi `;
MP_TAC
PI_POS;
REWRITE_TAC[REAL_ARITH` &0 < x <=> -- x < &0 `];
PHA;
NGOAC;
NHANH (REAL_ARITH` a < b /\ b <= c ==> a < c `);
STRIP_TAC;
MP_TAC2 (SPEC `
azim (
vec 0) u v w ` Trigonometry1.SIN_NEGPOS_PI);
STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
ASM_REWRITE_TAC[REAL_ARITH` -- x < &0 <=> &0 < x `];
STRIP_TAC;
UNDISCH_TAC` &0 <
sin (
azim (
vec 0) u v w) `;
MP_TAC2 (SPEC `
azim (
vec 0) u v w `
PI_TO_TWO_PI_NEG_SIN);
ASM_REWRITE_TAC[REAL_ARITH` a < b <=> ~( b <= a ) `];
PHA;
REWRITE_TAC[REAL_ARITH` ~( a < b /\ b < a ) `]]);;
let AFF_SGN_TRULE tm = prove (tm, AFF_SGN_TAC);;
let AFF_GE11 = AFF_SGN_TRULE`!x v:real^N.
~(x = v)
==> aff_ge {x} {v} =
{y | ?t1 t2. &0 <= t2 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v} `;;
let X_IN_AFF_GE11 = prove(`! x:real^N. ~( c = x ) ==> x
IN aff_ge {c} {x}`,
SIMP_TAC[AFF_GE11;
IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
EXISTS_TAC `&0 ` THEN EXISTS_TAC ` &1 ` THEN
REWRITE_TAC[REAL_ARITH` &0 <= &1 /\ &0 + &1 = &1 `] THEN VECTOR_ARITH_TAC);;
let AFF_GE22 =
AFF_SGN_TRULE`! a b x (y:real^N). DISJOINT {a,b} {x,y} ==> aff_ge {a,b} {x,y} =
{z | ? aa bb xx yy. &0 <= xx /\ &0 <= yy
/\ aa + bb + xx + yy = &1 /\ z = aa % a + bb % b + xx % x + yy % y }`;;
REWRITE_TAC[GSYM ITER; ADD1];
ASM_REWRITE_TAC[];
ASM_CASES_TAC ` y IN aff_ge {vec 0} {x , sx:real^3}`;
SUBGOAL_THEN ` {x,sx:real^3} IN E ` ASSUME_TAC;
REWRITE_TAC[Wrgcvdr_cizmrrh.IN_E_IFF_IN_ORD_E];
MATCH_MP_TAC LOCAL_FAN_IN_FF_IN_ORD_PAIRS;
ASM_REWRITE_TAC[];
SUBGOAL_THEN ` x IN (V:real^3 -> bool) ` MP_TAC;
EXPAND_TAC "x";
ASM_REWRITE_TAC[];
MP_TAC2 LOCAL_FAN_RHO_NODE_PROS2;
STRIP_TAC;
FIRST_ASSUM NHANH;
EXPAND_TAC "x";
REWRITE_TAC[GSYM ITER; ADD1];
ASM_SIMP_TAC[];
SUBGOAL_THEN ` y:real^3 IN V ` ASSUME_TAC;
UNDISCH_TAC ` y IN U:real^3 -> bool ` ;
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
ASM_REWRITE_TAC[];
MP_TAC2 (ISPECL [`V:real^3 -> bool`;` E: (real^3 -> bool) -> bool`;
` vec 0:real^3 `;` x:real^3 `;` y:real^3 `;` sx: real^3 `] (GEN_ALL
FAN_IN_AFF_GE_IMP_EQ));
ASSUME_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
FIRST_X_ASSUM ACCEPT_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC ` ~(y:real^3 = rho_node1 FF (x:real^3)) `;
EXPAND_TAC "x";
REWRITE_TAC[ADD1; GSYM ITER];
ASM_SIMP_TAC[];
SUBGOAL_THEN ` rho_node1 (FF:real^3 # real^3 -> bool) x = sx ` ASSUME_TAC;
EXPAND_TAC "x";
REWRITE_TAC[ADD1; GSYM ITER];
FIRST_ASSUM ACCEPT_TAC;
SUBGOAL_THEN ` wedge (vec 0) e x sx = aff_gt {vec 0, e} {x,sx} ` ASSUME_TAC;
MATCH_MP_TAC WEDGE_LUNE;
ASM_REWRITE_TAC[GSYM CROSS_DOT_COPLANAR];
ASM_SIMP_TAC[REAL_ARITH` &0 < x ==> ~( x = &0) `];
UNDISCH_TAC` &0 < (e cross x) dot sx `;
NHANH_PAT `\x. x ==> y ` REAL_LT_IMP_NE;
SIMP_TAC[EQ_SYM_EQ; CROSS_DOT_COPLANAR];
NHANH (SMOOTH_GEN_ALL Trigonometry2.NONCOPLANAR_3_BASIS);
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPEC ` y: real^3 `));
REWRITE_TAC[VECTOR_SUB_RZERO];
STRIP_TAC;
UNDISCH_TAC ` ~(y IN aff_ge {vec 0} {x, sx:real^3}) `;
UNDISCH_TAC ` ~coplanar {vec 0, e, x, sx:real^3} `;
ONCE_REWRITE_TAC[SET_RULE` {a,b,c} = {b,c,a}`];
NHANH NOT_COPLANAR_NOT_COLLINEAR;
NHANH th3;
SIMP_TAC[Fan.AFF_GE_1_2];
STRIP_TAC;
REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
REWRITE_TAC[MESON[REAL_ARITH` (&1 - a - b) + a + b = &1`]` (?t1 t2 t3.
&0 <= t2 /\ &0 <= t3 /\ t1 + t2 + t3 = &1 /\ y = t2 % x + t3 % sx)
<=> (? t2 t3. &0 <= t2 /\ &0 <= t3 /\ y = t2 % x + t3 % sx) `];
STRIP_TAC;
SUBGOAL_THEN ` ~( y:real^3 IN aff_ge {vec 0, e} {x, sx} )` ASSUME_TAC;
SUBGOAL_THEN ` DISJOINT {vec 0, e} {x, sx:real^3} ` MP_TAC;
REWRITE_TAC[DISJOINT; SET_RULE` (a INSERT A ) INTER ( b INSERT B) = {} <=>
~( a = b ) /\ ~ ( a IN B ) /\ ~( b IN A ) /\ A INTER B = {} `; NOT_IN_EMPTY;
IN_INSERT; INTER_EMPTY];
ASM_REWRITE_TAC[];
UNDISCH_TAC ` ~coplanar {vec 0, x, sx, e:real^3}`;
SIMP_TAC[INSERT_COMM];
NHANH NOT_COPLANAR_NOT_COLLINEAR;
NHANH th3;
SIMP_TAC[EQ_SYM_EQ];
SIMP_TAC[AFF_GE22; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
UNDISCH_TAC ` ~(?t2 t3. &0 <= t2 /\ &0 <= t3 /\ y = t2 % x + t3 % sx:real^3)`;
UNDISCH_TAC` !ta tb tc.
(y:real^3) = ta % e + tb % x + tc % sx ==> ta = t1 /\ tb = t2 /\ tc = t3 `;
REWRITE_TAC[TAUT` ~ a ==> ~ b <=> b ==> a `];
SUBGOAL_THEN ` {vec 0,x,sx:real^3} SUBSET P ` ASSUME_TAC;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
UNDISCH_TAC ` U SUBSET (P:real^3 -> bool) `;
MATCH_MP_TAC (SET_RULE` x IN U /\ y IN U ==> U SUBSET P ==> x IN P /\ y IN P `);
EXPAND_TAC "U";
EXPAND_TAC "sx";
EXPAND_TAC "x";
REWRITE_TAC[IN_ELIM_THM; GSYM ITER; ADD1];
UNDISCH_TAC ` n < l:num `;
MESON_TAC[ARITH_RULE ` a < b:num ==> a <= b /\ a + 1 <= b `];
SUBGOAL_THEN ` affine hull {vec 0,x, sx:real^3} = P ` ASSUME_TAC;
MATCH_MP_TAC THREE_NOT_COLL_DETER_PLANE;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (SET_RULE` y:real^3 IN U /\ U SUBSET P ==> y IN P `);
DOWN;
EXPAND_TAC "P";
REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
REPEAT STRIP_TAC;
EXISTS_TAC ` xx:real ` ;
EXISTS_TAC `yy:real `;
ASM_REWRITE_TAC[];
FIRST_ASSUM (MP_TAC o (SPECL [`&0 `;` v': real`;` w:real `]));
ANTS_TAC;
DOWN THEN REMOVE_TAC;
UNDISCH_TAC ` y = t1 % e + t2 % x + t3 % (sx:real^3) `;
REMOVE_TAC;
ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID];
DOWN;
FIRST_ASSUM NHANH;
SIMP_TAC[];
STRIP_TAC;
STRIP_TAC;
UNDISCH_TAC ` &0 = t1 `;
DISCH_THEN (SUBST1_TAC o SYM);
VECTOR_ARITH_TAC;
ASSUME_TAC2 (SIMP_RULE[INSERT_COMM] (SPECL [`vec 0:real^3 `;` e:real^3 `;
` x:real^3 `;` sx: real^3 `] WEDGE_LUNE_GE));
UNDISCH_TAC ` ~(y IN aff_ge {vec 0, e} {x, sx:real^3})`;
SIMP_TAC[INSERT_COMM];
FIRST_X_ASSUM (SUBST1_TAC o SYM);
REWRITE_TAC[IN_ELIM_THM];
MP_TAC (SPECL [`vec 0:real^3 `;` e:real^3 `;` x:real^3 `;` y:real^3 `]
AZIM_RANGE);
REAL_ARITH_TAC]);;
REWRITE_TAC[IN_ELIM_THM];
UNDISCH_TAC ` n < l:num `;
MESON_TAC[ARITH_RULE` a < l:num ==> a + 1 <= l `];
UNDISCH_TAC ` cyclic_set U (vec 0) (e:real^3) `;
PHA;
SIMP_TAC[IN];
REPEAT STRIP_TAC;
DOWN THEN DOWN;
UNDISCH_TAC ` ~(rho_node1 FF x = (x:real^3)) `;
SET_TAC[];
ASSUME_TAC2 RHO_NODE_SET_IN_A_PLANE_IMP_POS_DIRECT;
UNDISCH_TAC ` n < l:num `;
PHA;
FIRST_X_ASSUM NHANH;
NHANH REAL_LT_IMP_NE;
DOWN;
ASM_SIMP_TAC[CROSS_DOT_COPLANAR; EQ_SYM_EQ; INSERT_COMM];
ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
NHANH NOT_COPLANAR_NOT_COLLINEAR;
SIMP_TAC[INSERT_COMM];
UNDISCH_TAC ` !(x:real^3) n.
x = ITER n (rho_node1 FF) v /\ n < l
==> (!y. y IN U /\ ~(y = x) /\ ~(y = rho_node1 FF x)
==> azim (vec 0) e x (rho_node1 FF x) < azim (vec 0) e x y)`;
DISCH_THEN ASSUME_TAC2;
ASM_CASES_TAC ` q:real^3 = rho_node1 FF (x:real^3) `;
DISJ2_TAC;
FIRST_X_ASSUM SUBST1_TAC;
REWRITE_TAC[REAL_LE_REFL];
DISJ1_TAC;
REPLICATE_TAC 4 DOWN THEN PHA;
REWRITE_TAC[IN];
MESON_TAC[]]);;
REWRITE_TAC[IN_ELIM_THM];
UNDISCH_TAC ` n < l:num `;
MESON_TAC[ARITH_RULE` n < l:num ==> n <= l /\ n + 1 <= l `];
PHA;
NHANH_PAT `\x. x ==> y ` REAL_LT_IMP_LE;
ONCE_REWRITE_TAC[TAUT` a /\ b /\ c <=> (a /\c) /\ b`];
NHANH Fan.sum2_azim_fan;
STRIP_TAC;
ASM_CASES_TAC ` azim (vec 0) e x (rho_node1 FF x) = &0 `;
DOWN;
NHANH (MESON[AZIM_EQ_0_PI_IMP_COPLANAR]` azim v0 v1 w1 w2 = &0
==> coplanar {v0, v1, w1, w2} `);
REWRITE_TAC[GSYM CROSS_DOT_COPLANAR];
STRIP_TAC;
ASSUME_TAC2 RHO_NODE_SET_IN_A_PLANE_IMP_POS_DIRECT;
UNDISCH_TAC ` n < l:num `;
FIRST_X_ASSUM NHANH;
DOWN;
ASM_REWRITE_TAC[GSYM ITER; ADD1];
PAT_ONCE_REWRITE_TAC `\x. x ==> ll ` [CROSS_TRIPLE];
SIMP_TAC[REAL_ARITH` a = &0 ==> ~( &0 < a ) `];
SUBGOAL_THEN ` azim (vec 0) e (rho_node1 FF x) y < azim (vec 0) e x y ` MP_TAC;
DOWN;
ASM_REWRITE_TAC[REAL_ARITH ` a < b + a <=> &0 < b `];
MESON_TAC[REWRITE_RULE[REAL_ARITH` a <= b <=> b = a \/ a < b `] AZIM_RANGE];
UNDISCH_TAC ` cyclic_set U (vec 0) (e:real^3) `;
NHANH Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR;
STRIP_TAC;
SUBGOAL_THEN` x IN (U:real^3 -> bool) /\ rho_node1 FF x IN U /\ y IN U ` MP_TAC;
ASM_REWRITE_TAC[GSYM ITER; ADD1];
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
UNDISCH_TAC ` n < l:num `;
MESON_TAC[ARITH_RULE` a < n:num ==> a <= n /\ a + 1 <= n `];
FIRST_ASSUM NHANH;
STRIP_TAC;
ASM_CASES_TAC` azim (vec 0) e (rho_node1 (FF:real^3 # real^3 -> bool) x:real^3) y = &0 `;
REPLICATE_TAC 3 DOWN;
ONCE_REWRITE_TAC[SET_RULE` {a,b,c} = {b,c,a}`];
ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> a /\ b ==> c `];
NHANH AZIM_EQ_0_ALT;
SIMP_TAC[];
STRIP_TAC;
UNDISCH_TAC ` ~collinear {vec 0, (e:real^3), rho_node1 (FF:real^3 # real^3 -> bool) x}`;
NHANH th3a;
SIMP_TAC[AFF_GT_2_1; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
REPEAT STRIP_TAC;
SUBGOAL_THEN ` {vec 0, x, rho_node1 FF (x:real^3)} SUBSET P ` ASSUME_TAC;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
UNDISCH_TAC ` U SUBSET (P:real^3 -> bool) `;
MATCH_MP_TAC (SET_RULE` a IN U /\ b IN U ==> U SUBSET P ==> a IN P /\ b IN P `);
UNDISCH_TAC ` x:real^3 IN U `;
UNDISCH_TAC ` rho_node1 (FF: real^3 # real^3 -> bool) x IN U `;
ASM_REWRITE_TAC[];
SIMP_TAC[];
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
SUBGOAL_THEN ` x IN (V:real^3 -> bool) ` ASSUME_TAC;
ASM_SIMP_TAC[];
MP_TAC2 LOCAL_FAN_ITER_RHO_NODE_IN_V;
DOWN;
FIRST_X_ASSUM NHANH;
STRIP_TAC;
SUBGOAL_THEN ` affine hull {vec 0, x, rho_node1 (FF:real^3 # real^3 -> bool) x} = P` MP_TAC;
MATCH_MP_TAC THREE_NOT_COLL_DETER_PLANE;
ASM_REWRITE_TAC[];
STRIP_TAC;
MP_TAC2 (SET_RULE` y IN U /\ U SUBSET (P:real^3 -> bool) ==> y IN P`);
EXPAND_TAC "P";
REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
ASSUME_TAC2 RHO_NODE_SET_IN_A_PLANE_IMP_POS_DIRECT;
UNDISCH_TAC ` n < l:num`;
FIRST_X_ASSUM NHANH;
SWITCH_TAC ` x = ITER n (rho_node1 FF) (v:real^3) `;
ASM_REWRITE_TAC[GSYM ADD1; ITER];
NHANH_PAT `\x. x ==> y ` REAL_LT_IMP_NE;
SIMP_TAC[EQ_SYM_EQ; CROSS_DOT_COPLANAR];
NHANH (SMOOTH_GEN_ALL Trigonometry2.NONCOPLANAR_3_BASIS);
REWRITE_TAC[VECTOR_SUB_RZERO];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC ` y:real^3 `));
STRIP_TAC;
UNDISCH_TAC ` y = v' % x + w % rho_node1 (FF:real^3 # real^3 -> bool) x`;
PAT_ONCE_REWRITE_TAC`\x. x ==> y ` [VECTOR_ARITH` a + b % x = a + b % x + &0 % e `];
FIRST_ASSUM NHANH;
STRIP_TAC;
UNDISCH_TAC ` y = t2 % e + t3 % rho_node1 (FF:real^3 # real^3 -> bool) x`;
PAT_ONCE_REWRITE_TAC`\x. x ==> y ` [VECTOR_ARITH` a + b % xx = &0 % x + b % xx + a `];
FIRST_ASSUM NHANH;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
STRIP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC ` y = &0 % x + t3 % rho_node1 FF x + &0 % (e:real^3)`;
REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_ADD_RID];
MP_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
REWRITE_TAC[FAN; fan7];
REPEAT STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPECL [`{y:real^3}`;` {rho_node1 (FF:real^3 # real^3 -> bool) x }`]));
ANTS_TAC;
ASSUME_TAC2 LOCAL_FAN_ITER_RHO_NODE_IN_V;
REWRITE_TAC[IN_UNION; IN_ELIM_THM];
CONJ_TAC;
DISJ2_TAC;
EXISTS_TAC `y:real^3 `;
UNDISCH_TAC ` y IN U:real^3 -> bool`;
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
REPLICATE_TAC 3 DOWN THEN PHA;
SIMP_TAC[];
DISJ2_TAC;
EXISTS_TAC ` rho_node1 (FF:real^3 # real^3 -> bool) x `;
EXPAND_TAC "x";
REWRITE_TAC[GSYM ITER];
DOWN THEN SIMP_TAC[];
UNDISCH_TAC ` ~( y:real^3 = rho_node1 FF (x:real^3) ) `;
SIMP_TAC[SET_RULE` ~( a = b ) ==> {a} INTER {b} = {} `; AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING];
SUBGOAL_THEN `! y. y:real^3 IN U ==> ~( vec 0 = y:real^3) ` MP_TAC;
UNDISCH_TAC ` !v. v IN U ==> ~collinear {v, vec 0, e:real^3} `;
DISCH_THEN NHANH;
NHANH th3b;
SIMP_TAC[EQ_SYM_EQ];
STRIP_TAC;
UNDISCH_TAC `y:real^3 IN U `;
UNDISCH_TAC ` rho_node1 FF (x:real^3) IN (U:real^3 -> bool) `;
FIRST_X_ASSUM NHANH;
STRIP_TAC THEN STRIP_TAC;
SUBGOAL_THEN ` y:real^3 IN aff_ge {vec 0} {y} INTER aff_ge {vec 0} {rho_node1 FF (x:real^3)} ` ASSUME_TAC;
DOWN THEN DOWN THEN DOWN;
PHA;
SIMP_TAC[IN_INTER; X_IN_AFF_GE11];
SIMP_TAC[AFF_GE11; IN_ELIM_THM; VECTOR_ARITH` t % vec 0 + x = x `];
STRIP_TAC;
EXISTS_TAC ` &1 - t3 `;
EXISTS_TAC ` t3:real `;
UNDISCH_TAC ` y = t3 % rho_node1 (FF:real^3 # real^3 -> bool) x`;
SIMP_TAC[];
REMOVE_TAC;
UNDISCH_TAC` &0 < t3`;
REAL_ARITH_TAC;
REMOVE_TAC;
DISCH_THEN SUBST_ALL_TAC;
DOWN THEN DOWN;
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
MESON_TAC[];
MP_TAC (MESON[AZIM_RANGE]` &0 <= azim (vec 0) e (rho_node1 FF (x:real^3)) y`);
PHA;
NHANH (REAL_ARITH` &0 <= a /\ a < b ==> ~( b = &0 ) `);
STRIP_TAC;
SWITCH_TAC ` x = ITER n (rho_node1 FF) (v:real^3) `;
ASM_REWRITE_TAC[];
DOWN_TAC;
ONCE_REWRITE_TAC[SET_RULE` {a,b,c} = {b,c,a}`];
STRIP_TAC;
UNDISCH_TAC ` ~collinear {vec 0, e, (y:real^3) }`;
UNDISCH_TAC ` ~collinear {vec 0, e, x:real^3}`;
PHA;
NHANH AZIM_COMPL;
ASM_REWRITE_TAC[];
STRIP_TAC;
UNDISCH_TAC ` ~collinear {vec 0, e, y:real^3}`;
UNDISCH_TAC ` ~collinear {vec 0, e, rho_node1 (FF:real^3 # real^3 -> bool) x}`;
PHA;
NHANH AZIM_COMPL;
SWITCH_TAC ` azim (vec 0) e x y =
azim (vec 0) e x (rho_node1 (FF:real^3 # real^3 -> bool) x) + azim (vec 0) e (rho_node1 FF x) y `;
ASM_SIMP_TAC[REAL_ARITH` a - b < a - c <=> c < b `]]);;
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
UNDISCH_TAC ` n <= l:num `;
SWITCH_TAC ` y = ITER n (rho_node1 FF) v:real^3 `;
ASM_REWRITE_TAC[];
EXPAND_TAC "y";
ASM_CASES_TAC ` n = 0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN;
ASM_REWRITE_TAC[ITER];
ASM_CASES_TAC` n = l:num `;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC ` ITER l (rho_node1 FF) v = ls:real^3 `;
ASM_REWRITE_TAC[];
DOWN THEN DOWN;
SPEC_TAC (`n:num`,` n:num`);
INDUCT_TAC;
REWRITE_TAC[];
REPEAT STRIP_TAC;
ASM_CASES_TAC ` n' = 0 `;
ASM_REWRITE_TAC[ADD; ITER1];
UNDISCH_TAC ` !x n.
x = ITER n (rho_node1 FF) (v:real^3) /\ n < l
==> (!y. y IN U /\ ~(y = x) /\ ~(y = rho_node1 FF x)
==> azim (vec 0) e y x < azim (vec 0) e y (rho_node1 FF x))`;
DISCH_THEN (MP_TAC o (SPECL [`v:real^3 `;`0`]));
SIMP_TAC[ITER];
ANTS_TAC;
DOWN THEN DOWN THEN ARITH_TAC;
DISCH_THEN MATCH_MP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
SUBST_ALL_TAC (SYM ONE);
DOWN THEN DOWN;
PHA;
REWRITE_TAC[ARITH_RULE` ~( 1 = z ) /\ 1 <= z <=> 0 < z /\ 1 < z `];
UNDISCH_TAC ` !i. i < l ==> ~(ls = ITER i (rho_node1 FF) (v:real^3)) `;
DISCH_THEN NHANH;
SIMP_TAC[ITER1; ITER];
EXPAND_TAC "ls";
EXPAND_TAC "U";
STRIP_TAC;
REWRITE_TAC[IN_ELIM_THM];
MESON_TAC[LE_REFL];
UNDISCH_TAC ` ~(n' = 0)
==> ~(n' = l)
==> n' <= l
==> azim (vec 0) e ls v < azim (vec 0) e ls (ITER n' (rho_node1 FF) v)`;
PHA;
ANTS_TAC;
REPLICATE_TAC 3 DOWN THEN PHA;
ARITH_TAC;
STRIP_TAC;
UNDISCH_TAC ` !x n.
x = ITER n (rho_node1 FF) v /\ n < l
==> (!y. y IN U /\ ~(y = x) /\ ~(y = rho_node1 FF x)
==> azim (vec 0) e y x < azim (vec 0) e y (rho_node1 FF x))`;
DISCH_THEN (MP_TAC o (SPECL [`ITER n' (rho_node1 FF) v:real^3 `;` n':num`]));
ANTS_TAC;
UNDISCH_TAC` SUC n' <= l `;
REWRITE_TAC[ARITH_RULE` SUC n <= m <=> n < m `];
DISCH_THEN (MP_TAC o (SPEC ` ls:real^3 `));
ANTS_TAC;
UNDISCH_TAC ` SUC n' <= l `;
UNDISCH_TAC ` ~( SUC n' = l ) `;
PHA;
REWRITE_TAC[ARITH_RULE` ~(SUC n' = l) /\ SUC n' <= l <=> n' < l /\ SUC n' < l`];
FIRST_ASSUM NHANH;
SIMP_TAC[ITER];
STRIP_TAC;
EXPAND_TAC "ls";
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
MESON_TAC[LE_REFL];
DOWN THEN PHA;
REWRITE_TAC[ITER];
REAL_ARITH_TAC]);;
FIRST_X_ASSUM SUBST1_TAC;
REWRITE_TAC[ITER];
MESON_TAC[Lvducxu.W_SUBSET_SINGLETON_IMP_IDE; SUBSET_REFL];
MATCH_MP_TAC Wrgcvdr_cizmrrh.IDENTIFY_AZIM_CYCLE;
ASSUME_TAC2 LOCAL_FAN_IMP_CYCLIC_SET;
UNDISCH_TAC ` ~( l = 0 ) `;
REWRITE_TAC[ARITH_RULE` ~( l = 0) <=> 0 < l `];
USE_FIRST ` !i. i < l ==> ~(ls = ITER i (rho_node1 FF) v:real^3) ` NHANH;
SUBGOAL_THEN ` ls:real^3 IN U /\ v IN U` ASSUME_TAC;
EXPAND_TAC "ls";
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
MESON_TAC[LE_REFL; LE_0; ITER];
ASM_SIMP_TAC[ITER; LE_0];
STRIP_TAC;
CONJ_TAC;
DOWN THEN DOWN THEN DOWN THEN PHA;
SET_TAC[];
CONJ_TAC;
UNDISCH_TAC ` cyclic_set U (vec 0) (e:real^3) `;
NHANH Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR;
ASM_MESON_TAC[];
CONJ_TAC;
ONCE_REWRITE_TAC[GSYM IN];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
ASM_CASES_TAC ` q = v:real^3 `;
ASM_SIMP_TAC[REAL_LE_REFL];
DISJ1_TAC;
ASM_MESON_TAC[IN]]);;
REWRITE_TAC[orbit_map; IN_ELIM_THM; POWER_TO_ITER];
EXISTS_TAC `l:num`;
REWRITE_TAC[ARITH_RULE` x >= 0 `];
DOWN;
PHA;
FIRST_ASSUM NHANH;
SUBGOAL_THEN ` ITER ( k - l ) f ( ITER l f v ) = ITER l f (v:A) ` ASSUME_TAC;
ASM_SIMP_TAC[ITER_ADD; ARITH_RULE`l < k ==> ( k - l ) + l:num = k `];
DOWN;
UNDISCH_TAC ` l < k:num`;
PHA;
ONCE_REWRITE_TAC[ARITH_RULE` a < b <=> 0 < b - a `];
NHANH Lvducxu.ITER_CYCLIC_ORBIT;
SIMP_TAC[];
ASM_MESON_TAC[
ARITH_RULE` a < b:num /\ aa <= a - i ==> ~( aa = b ) `;
ISPECL [`f:A -> A `;` ITER l f (v:A) `; ` k - l:num` ] (GEN_ALL Wrgcvdr_cizmrrh.CARD_LE_K_OF_SET_K_FIRST_ELMS)]]);;
(* -------------------------------- *)
(* ================================ *)
(* -------------------------------- *)
(* lemma OZQVSFF *)
(* ================================ *)
let IN_WEDGE_IMP_AZIM_LE = prove(`! x y. y
IN wedge_ge v0 v1 w1 w2 /\
azim v0 v1 w1 x <=
azim v0 v1 w1 y /\
~collinear {v0, v1, x} /\
~collinear {v0, v1, y} /\
~collinear {v0, v1, w1}
==>
azim v0 v1 x y <=
azim v0 v1 w1 w2`,
NHANH Fan.sum4_azim_fan THEN
REWRITE_TAC[
WEDGE_GE_AZIM_LE] THEN
REPEAT GEN_TAC THEN
MP_TAC (SPECL [`v0:real^3`;` v1:real^3`;`w1:real^3`;` x:real^3`]
AZIM_RANGE) THEN
REAL_ARITH_TAC);;
let HYP_MAPS_INVERSABLE =
MESON[hypermap_lemma; PERMUTES_INVERSES_o]`! H:(A) hypermap.
inverse (face_map H) o (face_map H ) = I /\
inverse (node_map H) o (node_map H ) = I /\
inverse (edge_map H) o (edge_map H ) = I /\
(face_map H ) o inverse (face_map H) = I /\
(node_map H ) o inverse (node_map H) = I/\
(edge_map H ) o inverse (edge_map H) = I`;;
let LOFA_DARTS_FF_UNION_SWITCH_FF = prove_by_refinement
(`
local_fan (V,E,
FF) ==>
darts_of_hyp E V =
FF UNION {v,w | w,v
IN FF }`,
[REWRITE_TAC[
local_fan];
LET_TAC;
REWRITE_TAC[dih2k; Lvducxu.HAS_ORD2_INTERPRET; Lvducxu.EDGE_MAP_RESO_INVERSE];
LET_TAC;
STRIP_TAC;
UNDISCH_TAC ` x':real^3 # real^3
IN dart H `;
FIRST_X_ASSUM NHANH;
ONCE_REWRITE_TAC[
inverse2_hypermap_maps];
REWRITE_TAC[
IMAGE_o];
ONCE_REWRITE_TAC[Lvducxu.ENF_IMAGE_ITSELF];
ASM_REWRITE_TAC[GSYM
IMAGE_o; GSYM
o_ASSOC; HYP_MAPS_INVERSABLE;
I_O_ID;
GSYM Lvducxu.ENF_IMAGE_ITSELF];
UNDISCH_TAC `
FAN (
vec 0:real^3, V, E) `;
NHANH
ELMS_OF_HYPERMAP_HYP;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASM_REWRITE_TAC[];
MATCH_MP_TAC (MESON[]` x = y ==> f x = f y`);
REWRITE_TAC[
IMAGE;
EXTENSION;
IN_ELIM_THM;
ee_of_hyp2];
SUBGOAL_THEN ` x'
IN dart (H:(real^3 # real^3) hypermap) ` MP_TAC;
FIRST_X_ASSUM MP_TAC;
ASM_REWRITE_TAC[];
NHANH
lemma_face_subset;
REWRITE_TAC[
SUBSET];
STRIP_TAC;
GEN_TAC THEN EQ_TAC;
STRIP_TAC;
DOWN THEN DOWN;
FIRST_X_ASSUM NHANH;
ASM_SIMP_TAC[];
REPEAT STRIP_TAC;
EXISTS_TAC `
SND (x''':real^3 #real^3 ) `;
EXISTS_TAC `
FST (x''':real^3 #real^3 ) `;
ASM_REWRITE_TAC[];
STRIP_TAC;
EXISTS_TAC `w:real^3, v:real^3 `;
DOWN THEN DOWN THEN PHA;
FIRST_X_ASSUM NHANH;
ASM_SIMP_TAC[]]);;
let SELF_CYCLIC_IMP_FINITE = prove_by_refinement
(`(! x:A. x
IN V ==> V =
orbit_map f x ) ==> FINITE V `,
[ASM_CASES_TAC `V:A -> bool = {} `;
ASM_REWRITE_TAC[
FINITE_EMPTY];
DOWN;
REWRITE_TAC[SET_RULE` ~( x = {}) <=> ? a. a
IN x `];
REPEAT STRIP_TAC;
UNDISCH_TAC` a:A
IN V `;
FIRST_ASSUM NHANH;
STRIP_TAC;
MP_TAC (ISPECL [`f:A -> A `;` a:A `]
in_orbit_map1);
FIRST_X_ASSUM (SUBST1_TAC o SYM);
FIRST_ASSUM NHANH;
STRIP_TAC;
SUBGOAL_THEN ` a:A
IN V ` MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
FIRST_ASSUM SUBST1_TAC;
REWRITE_TAC[
orbit_map;
IN_ELIM_THM;
POWER_TO_ITER; GSYM
ITER_ALT];
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o SYM);
MP_TAC (ARITH_RULE` 0 < SUC n `);
PHA;
NHANH Lvducxu.ITER_CYCLIC_ORBIT;
UNDISCH_TAC ` a:A
IN V `;
FIRST_X_ASSUM NHANH;
ASM_SIMP_TAC[
orbit_map;
POWER_TO_ITER; GSYM
ITER_ALT];
REPEAT STRIP_TAC;
REWRITE_TAC[
SET_RULE` {
ITER n' f a | n' < n} = {y | ? n' . n' < n /\ y =
ITER n' f a }`;
Wrgcvdr_cizmrrh.FINITE_OF_N_FIRST_ELMS]]);;
STRIP_TAC;
DOWN;
UNDISCH_TAC ` x:real^3 IN V `;
UNDISCH_TAC ` vv:real^3 IN V `;
PHA;
FIRST_X_ASSUM NHANH;
SIMP_TAC[IN_INSERT];
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
STRIP_TAC;
UNDISCH_TAC `v, rho_node1 FF v IN FF `;
UNDISCH_TAC ` local_fan (V,E,FF) `;
PHA;
NHANH LOCAL_FAN_IN_FF_IN_ORD_PAIRS;
ASM_SIMP_TAC[Wrgcvdr_cizmrrh.IN_E_IFF_IN_ORD_E];
UNDISCH_TAC ` vv,rho_node1 FF vv IN FF `;
FIRST_X_ASSUM NHANH;
ASM_REWRITE_TAC[];
UNDISCH_TAC `local_fan (V,E,FF) `;
PHA;
NHANH LOCAL_FAN_IN_FF_IN_ORD_PAIRS;
SIMP_TAC[Wrgcvdr_cizmrrh.IN_ORD_E_EQ_IN_E; INSERT_COMM]]);;
let RHO_NODE_INVERSE_POINT = MESON[]`
w,v IN FF /\ (! ww. ww,v IN FF ==> ww = w )
==> (@a. a,v IN FF ) = w `;;
let AZIM_CYCLE_TWO_POINT_SET = prove_by_refinement
(`
azim_cycle {a,b} v w a = b `,
[ASM_CASES_TAC ` a = b:real^3`;
ASM_REWRITE_TAC[
INSERT_INSERT];
REWRITE_TAC[ MATCH_MP Lvducxu.W_SUBSET_SINGLETON_IMP_IDE (SET_RULE` {p:real^3}
SUBSET {p}`)];
ABBREV_TAC ` W = {a,b:real^3} `;
ABBREV_TAC ` u =
azim_cycle W v w a `;
ABBREV_TAC ` p = a:real^3`;
SUBGOAL_THEN ` ~(u = p) /\
W u /\
(!q. ~(q = p) /\ W q
==>
azim v w p u <
azim v w p q \/
azim v w p u =
azim v w p q /\
norm (projection (w - v) (u - v)) <=
norm (projection (w - v) (q - v))) ` ASSUME_TAC;
EXPAND_TAC "u";
SUBGOAL_THEN ` ~(W SUBSET {p:real^3}) ` MP_TAC;
ASM SET_TAC[];
REWRITE_TAC[azim_cycle];
SIMP_TAC[];
DISCH_TAC;
CONV_TAC SELECT_CONV;
EXISTS_TAC `b:real^3 `;
ASM_REWRITE_TAC[];
EXPAND_TAC "W";
CONJ_TAC;
SET_TAC[];
REWRITE_TAC[SET_RULE` ~(q = p) /\ {p, b} q <=> q = b /\ ~( q = p)`];
SIMP_TAC[REAL_LE_REFL];
ASM SET_TAC[]]);;
let MOST_EXPAND_IN_WEDGE_GE = prove_by_refinement
(` ~collinear {v0,v1, w1} /\
~collinear {v0,v1, w2} /\
~collinear {v0,v1, x} /\ ~
collinear {v0, v1, y} /\
y
IN wedge_ge v0 v1 w1 w2 /\
azim v0 v1 w1 x <=
azim v0 v1 w1 y /\
azim v0 v1 x y =
azim v0 v1 w1 w2 ==>
azim v0 v1 w1 x = &0 /\
azim v0 v1 y w2 = &0 `,
[REWRITE_TAC[
wedge_ge;
IN_ELIM_THM];
STRIP_TAC;
SUBGOAL_THEN `
azim v0 v1 w1 w2 =
azim v0 v1 w1 y +
azim v0 v1 y w2` ASSUME_TAC;
MATCH_MP_TAC Fan.sum4_azim_fan;
ASM_REWRITE_TAC[];
SUBGOAL_THEN `
azim v0 v1 w1 y =
azim v0 v1 w1 x +
azim v0 v1 x y` ASSUME_TAC;
MATCH_MP_TAC Fan.sum4_azim_fan;
ASM_REWRITE_TAC[];
UNDISCH_TAC`
azim v0 v1 w1 w2 =
azim v0 v1 w1 y +
azim v0 v1 y w2 `;
ASM_REWRITE_TAC[];
MP_TAC (
SPECL [`v0:real^3`; ` v1:real^3 `;`w1:real^3 `;` x:real^3 `]
AZIM_RANGE);
MP_TAC (
SPECL [`v0:real^3`; ` v1:real^3 `;`y:real^3 `;` w2:real^3 `]
AZIM_RANGE);
REAL_ARITH_TAC]);;
let OZQVSFF = prove_by_refinement
(`! u w.
convex_local_fan (V,E,
FF) /\
{u,v,w}
SUBSET V /\
plane P /\
{
vec 0, u, v, w}
SUBSET P /\
{u,w}
INTER aff {
vec 0, v} = {} /\
~( aff {v,
vec 0}
INTER conv0 {w,u} = {} ) ==>
interior_angle1 (
vec 0)
FF v =
pi /\
rho_node1 FF v
IN P /\
ivs_rho_node1 FF v
IN P`,
[MATCH_MP_TAC (MESON[REAL_ARITH` a <= b \/ b <= a `]`
(! x y. P x y ==> P y x ) /\ (! x y.
azim (
vec 0) v (
rho_node1 FF v) y <=
azim (
vec 0) v (
rho_node1 FF v) x ==> P x y ) ==>
(! x y. P x y ) `);
CONJ_TAC;
SIMP_TAC[
INSERT_COMM];
REWRITE_TAC[
convex_local_fan;
INSERT_SUBSET;
EMPTY_SUBSET; Trigonometry2.INSERT_INTER_EMPTY];
NHANH Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
NHANH
FAN_IMP_V_DIFF;
REPLICATE_TAC 4 STRIP_TAC;
UNDISCH_TAC ` !v:real^3. v
IN V ==> ~(v =
vec 0)`;
DISCH_TAC;
UNDISCH_TAC` v:real^3
IN V `;
FIRST_ASSUM NHANH;
STRIP_TAC;
UNDISCH_TAC ` ~( u
IN aff {
vec 0, v:real^3})`;
UNDISCH_TAC ` ~( w:real^3
IN aff {
vec 0, v})`;
ASM_SIMP_TAC[
INSERT_COMM; Trigonometry2.NOT_EQ_IMP_AFF_AND_COLL3];
REPEAT DISCH_TAC;
SUBGOAL_THEN `
azim (
vec 0) v w u =
pi ` ASSUME_TAC;
DOWN THEN DOWN THEN PHA;
PAT_ONCE_REWRITE_TAC `\x. y /\ x ==> k ` [
INSERT_COMM];
NHANH (SIMP_RULE[
INSERT_COMM] Ldurdpn.LDURDPN);
STRIP_TAC;
FIRST_X_ASSUM SUBST1_TAC;
CONJ_TAC;
EXISTS_TAC `P:real^3 -> bool`;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET];
FIRST_ASSUM ACCEPT_TAC;
UNDISCH_TAC ` v:real^3
IN V `;
ASSUME_TAC2
LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN IMP_TAC;
REMOVE_TAC;
DISCH_THEN NHANH;
UNDISCH_TAC ` !x:real^3 #real^3. x
IN FF ==>
azim_in_fan x E <=
pi /\ V
SUBSET wedge_in_fan_ge x E`;
DISCH_TAC;
FIRST_ASSUM NHANH;
REWRITE_TAC[
SUBSET];
STRIP_TAC;
UNDISCH_TAC` w:real^3
IN V `;
UNDISCH_TAC ` u:real^3
IN V `;
FIRST_ASSUM NHANH;
REWRITE_TAC[
wedge_in_fan_ge];
SUBGOAL_THEN `
CARD (
EE (v:real^3) E ) = 2 ` MP_TAC;
MATCH_MP_TAC
LOFA_CARD_EE_V_1;
ASM_REWRITE_TAC[];
NHANH (ARITH_RULE ` a = 2 ==> a > 1 `);
SIMP_TAC[];
REPLICATE_TAC 3 STRIP_TAC;
UNDISCH_TAC ` v:real^3
IN V `;
UNDISCH_TAC `
local_fan (V,E,
FF) `;
PHA;
NHANH
EXISTS_INVERSE_OF_V;
STRIP_TAC;
ASSUME_TAC2
LOFA_IMP_EE_TWO_ELMS;
UNDISCH_TAC `
azim_in_fan (v,
rho_node1 FF v) E <=
pi `;
REWRITE_TAC[
azim_in_fan];
LET_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN`
azim (
vec 0) v w u <=
azim (
vec 0) v (
rho_node1 FF v) d ` ASSUME_TAC;
MATCH_MP_TAC
IN_WEDGE_IMP_AZIM_LE;
ASM_SIMP_TAC[
INSERT_COMM];
UNDISCH_TAC ` v,
rho_node1 FF v
IN FF `;
UNDISCH_TAC `
local_fan (V,E,
FF) `;
PHA;
NHANH
LOCAL_FAN_IN_FF_NOT_COLLINEAR;
SIMP_TAC[
INSERT_COMM];
DOWN;
UNDISCH_TAC `
azim (
vec 0) v w u =
pi `;
PHA;
DISCH_TAC;
REWRITE_TAC[
interior_angle1];
SUBGOAL_THEN `(@a. a,v
IN (FF:real^3 # real^3 -> bool)) = vv ` ASSUME_TAC;
MATCH_MP_TAC RHO_NODE_INVERSE_POINT;
MP_TAC2
LOCAL_FAN_RHO_NODE_PROS2;
STRIP_TAC;
UNDISCH_TAC ` vv:real^3
IN V `;
FIRST_X_ASSUM NHANH;
ASM_SIMP_TAC[];
REPEAT STRIP_TAC;
DOWN;
FIRST_ASSUM NHANH;
REWRITE_TAC[
PAIR_EQ];
UNDISCH_TAC `
local_fan (V,E,
FF) `;
PHA;
NGOAC;
NHANH
LOCAL_FAN_IMP_IN_V;
UNDISCH_TAC ` vv:real^3
IN V `;
NHANH
LOFA_IMP_BIJ_VV;
REWRITE_TAC[
BIJ;
INJ];
EXPAND_TAC "v";
MESON_TAC[];
SUBGOAL_THEN ` azim_cycle (EE v E) (vec 0) v (rho_node1 FF v) = vv ` ASSUME_TAC;
UNDISCH_TAC ` EE v E = {rho_node1 FF v, vv} `;
EXPAND_TAC "d";
SIMP_TAC[AZIM_CYCLE_TWO_POINT_SET];
FIRST_X_ASSUM SUBST_ALL_TAC;
ONCE_REWRITE_TAC[TAUT` a/\ b <=> a /\ (a ==> b ) `];
CONJ_TAC;
FIRST_X_ASSUM SUBST1_TAC;
DOWN;
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
FIRST_ASSUM SUBST1_TAC;
STRIP_TAC;
SUBGOAL_THEN ` ~collinear {v, rho_node1 FF v, vec 0} /\ ~collinear {d, v, vec 0} ` ASSUME_TAC;
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
UNDISCH_TAC ` v:real^3 IN V `;
UNDISCH_TAC ` vv:real^3 IN V `;
FIRST_X_ASSUM NHANH;
ASM_SIMP_TAC[INSERT_COMM];
SUBGOAL_THEN ` azim (vec 0) v (rho_node1 FF v) w = &0 /\
azim (vec 0) v u vv = &0 ` MP_TAC;
MATCH_MP_TAC MOST_EXPAND_IN_WEDGE_GE;
ASM_SIMP_TAC[INSERT_COMM];
DOWN THEN STRIP_TAC;
UNDISCH_TAC `~ collinear {v, w, vec 0:real^3 }`;
UNDISCH_TAC `~ collinear {v, rho_node1 FF v, vec 0:real^3 }`;
ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b /\a ==> c `];
ONCE_REWRITE_TAC[SET_RULE` {a,b,c} = {c,a,b} `];
NHANH AZIM_EQ_0_ALT;
NHANH AZIM_EQ_0_SYM;
STRIP_TAC;
ASSUME_TAC2 (SIMP_RULE[INSERT_COMM] (SPECL [` vec 0:real^3`;` v:real^3 `;`u:real^3 `;` d:real^3 `] AZIM_EQ_0_ALT));
DOWN;
ASM_SIMP_TAC[];
DOWN;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_SIMP_TAC[ivs_rho_node1];
REMOVE_TAC THEN REMOVE_TAC;
MATCH_MP_TAC (
SET_RULE` A SUBSET S /\ B SUBSET S ==> a IN A /\ b IN B ==> a IN S /\ b IN S `);
CONJ_TAC;
SUBGOAL_THEN ` affine hull {vec 0,v,w:real^3} = P ` MP_TAC;
MATCH_MP_TAC THREE_NOT_COLL_DETER_PLANE;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
DISCH_THEN (SUBST1_TAC o SYM);
REWRITE_TAC[SET_RULE` {a,b,c} = {a,b} UNION {c}`];
REWRITE_TAC[INSERT_UNION;AFF_GT_SUBSET_AFFINE_HULL; UNION_EMPTY];
SUBGOAL_THEN ` affine hull {u,v,vec 0:real^3} = P ` MP_TAC;
MATCH_MP_TAC THREE_NOT_COLL_DETER_PLANE;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
DISCH_THEN (SUBST1_TAC o SYM);
REWRITE_TAC[SET_RULE` {c,a,b} = {a,b} UNION {c}`];
REWRITE_TAC[INSERT_UNION;AFF_GT_SUBSET_AFFINE_HULL; UNION_EMPTY]]);;
(* ============================================= *)
(* ============================================= *)
(* ============================================= *)
(* ============================================= *)
(* lemma KCHMAMG *)
let REAL_LT_DIV_NEG = prove(` a < &0 /\ b < &0 ==> &0 < a /b `,
SIMP_TAC [REAL_FIELD` b < &0 ==> a / b = ( -- a) / ( -- b ) `; REAL_ARITH `
b < &0 <=> &0 < -- b `;
REAL_LT_DIV]);;
(* lemma about intersection between conv0 {x,y} and
aff {w,v} in affine hull {a,b,c} *)
let INTERSECTION_LEMMA = prove_by_refinement
(` ~ ( z = x ) /\
DISJOINT {x:real^N} {v,w} /\ ~( x = u ) /\
~(aff_gt {x} {v, w}
INTER aff_lt {x} {u} = {}) /\
z
IN affine hull {x,v,w} ==>
(? a b t. {a,b}
SUBSET {u,v,w} /\ t
IN aff {x,z}
INTER conv0 {a,b})`,
[REWRITE_TAC[
AFFINE_HULL_3;
IN_ELIM_THM; REAL_ARITH` a + b = &1 <=> &1 - b = a `];
STRIP_TAC;
DOWN;
ASM_CASES_TAC ` &0 < v' /\ &0 < w' `;
ASM_REWRITE_TAC[VECTOR_ARITH` a = x % b + c + d <=> a - x % b = c + d`];
STRIP_TAC;
EXISTS_TAC ` v:real^N `;
EXISTS_TAC `w:real^N `;
EXISTS_TAC ` (&1 / (v' + w') ) % ( z - u' % x:real^N ) `;
REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET;
IN_INSERT;
AFF2;
Geomdetail.CONV0_SET2;
IN_INTER;
IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC ` ( -- u') / (v' + w' ) `;
REWRITE_TAC[
VECTOR_SUB_LDISTRIB;
VECTOR_MUL_ASSOC; REAL_ARITH` (&1 / a ) * b = b / a `];
ASM_SIMP_TAC [REAL_FIELD` &0 < v' /\ &0 < w' ==> &1 - --u' / (v' + w') = (u' + v' + w' ) / (v' + w') `];
EXPAND_TAC "u'";
REWRITE_TAC[REAL_ARITH` &1 - ( a + b) + a + b = &1 `];
VECTOR_ARITH_TAC;
EXISTS_TAC ` v' / ( v' + w') `;
EXISTS_TAC ` w' / ( v' + w') `;
CONJ_TAC;
MATCH_MP_TAC REAL_LT_DIV;
ASM_REWRITE_TAC[];
MATCH_MP_TAC REAL_LT_ADD;
FIRST_X_ASSUM ACCEPT_TAC;
CONJ_TAC;
MATCH_MP_TAC REAL_LT_DIV;
ASM_REWRITE_TAC[];
MATCH_MP_TAC REAL_LT_ADD;
FIRST_X_ASSUM ACCEPT_TAC;
ASM_SIMP_TAC[REAL_FIELD` &0 < v' /\ &0 < w' ==> v' / (v' + w') + w' / (v' + w') = &1`];
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC];
ASM_SIMP_TAC[REAL_FIELD` &0 < v' /\ &0 < w' ==> &1 / (v' + w') * v' = v' / ( v' + w') /\ (&1 / (v' + w') * w') = w' / ( v' + w') `];
(* CASES v' < &0 and w' < &0 *)
ASM_CASES_TAC ` v' < &0 /\ w' < &0 `;
ASM_REWRITE_TAC[VECTOR_ARITH` a = x % b + c + d <=> a - x % b = c + d`];
STRIP_TAC;
EXISTS_TAC ` v:real^N `;
EXISTS_TAC `w:real^N `;
EXISTS_TAC ` (&1 / (v' + w') ) % ( z - u' % x:real^N ) `;
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT; AFF2;
Geomdetail.CONV0_SET2; IN_INTER; IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC ` ( -- u') / (v' + w' ) `;
REWRITE_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_ASSOC; REAL_ARITH` (&1 / a ) * b = b / a `];
ASM_SIMP_TAC [REAL_FIELD` v' < &0 /\ w' < &0 ==> &1 - --u' / (v' + w') = (u' + v' + w' ) / (v' + w') `];
EXPAND_TAC "u'";
REWRITE_TAC[REAL_ARITH` &1 - ( a + b) + a + b = &1 `];
VECTOR_ARITH_TAC;
EXISTS_TAC ` v' / ( v' + w') `;
EXISTS_TAC ` w' / ( v' + w') `;
CONJ_TAC;
MATCH_MP_TAC REAL_LT_DIV_NEG;
ASM_SIMP_TAC[REAL_ARITH` a < &0 /\ b < &0 ==> a + b < &0`];
CONJ_TAC;
MATCH_MP_TAC REAL_LT_DIV_NEG;
ASM_SIMP_TAC[REAL_ARITH` a < &0 /\ b < &0 ==> a + b < &0`];
ASM_SIMP_TAC[REAL_FIELD` v' < &0 /\ w' < &0 ==> v' / (v' + w') + w' / (v' + w') = &1`];
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC];
ASM_SIMP_TAC[REAL_FIELD` v' < &0 /\ w' < &0 ==> &1 / (v' + w') * v' = v' / ( v' + w') /\ (&1 / (v' + w') * w') = w' / ( v' + w') `];
UNDISCH_TAC ` ~(aff_gt {x} {v, w} INTER aff_lt {x} {u:real^N} = {})`;
UNDISCH_TAC ` ~ ( x = u:real^N) `;
ASM_SIMP_TAC[Planarity.AFF_GT_1_2; AFF_LT_1_1; SET_RULE` ~( a INTER b = {} ) <=> ? x. x IN a /\ x IN b `; IN_ELIM_THM; SET_RULE` ~( a = b ) <=> DISJOINT {a} {b} `];
REPEAT STRIP_TAC;
FIRST_ASSUM (SUBST1_TAC o SYM);
DOWN_TAC;
ASM_CASES_TAC ` v' = &0 \/ w' = &0`;
DOWN;
SPEC_TAC (`v:real^N`,`v:real^N `);
SPEC_TAC (`w:real^N`,`w:real^N `);
SPEC_TAC (`v':real`,`v':real `);
SPEC_TAC (`w':real`,`w':real `);
SPEC_TAC (`t2:real`,`t2:real `);
SPEC_TAC (`t3:real`,`t3:real `);
MATCH_MP_TAC (MESON[]` (! t3 t2 x y a b. P x y a b t3 t2 ==> P y x b a t2 t3 ) /\ (! x y a b t3 t2 . y = &0 ==> P x y a b t3 t2)
==> (! t3 t2 x y a b. (y = &0 \/ x = &0 ) ==> P x y a b t3 t2) `);
CONJ_TAC;
ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b ==> a ==> c `];
REPEAT GEN_TAC;
DISCH_TAC;
ANTS_TAC;
DOWN;
SIMP_TAC[INSERT_COMM; REAL_ADD_SYM; CONJ_SYM; VECTOR_ADD_SYM];
ONCE_REWRITE_TAC[EQ_SYM_EQ];
SIMP_TAC[];
SIMP_TAC[INSERT_COMM];
REPEAT GEN_TAC;
DISCH_THEN SUBST_ALL_TAC;
STRIP_TAC;
DOWN;
EXPAND_TAC "u'";
REWRITE_TAC[VECTOR_ARITH` z = (&1 - (&0 + w')) % x + &0 % v + w' % w <=>
z - x = w' % ( w - x ) `];
DOWN;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[VECTOR_ARITH ` t1 % x + t2 % v + t3 % w = t1' % x + t2' % u
<=> (t1 + t2 + t3 ) % x + t2 % ( v - x ) + t3 % ( w - x ) = ( t1' + t2' ) % x + t2' % (u - x ) `];
ASM_REWRITE_TAC[VECTOR_ARITH` x + a = x + b <=> a = b:real^N `; VECTOR_ARITH `
a % z + b % x = y <=> b % x = y + -- a % z `];
ASM_CASES_TAC ` w' = &0 `;
ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_EQ];
MP_TAC2 (REAL_ARITH ` &0 < t3 ==> ~( t3 = &0 ) `);
SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE];
REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB;
VECTOR_SUB_LDISTRIB; VECTOR_ARITH` a = x - y + b % d - t <=> a + y + t = x + b % d `];
REPEAT STRIP_TAC;
EXISTS_TAC `u:real^N`;
EXISTS_TAC `v:real^N `;
EXISTS_TAC ` (t3 / (w' * (t2' - t2 ))) % ( z - x + ((w' * &1 / t3) * t2') % x + ((w' * &1 / t3) * --t2) % (x:real^N) ) `;
REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET; IN_INTER;AFF2; IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC ` &1 - t3 / (w' * (t2' - t2)) `;
DOWN THEN DOWN;
REWRITE_TAC[REAL_ARITH` (w' * &1 / t3) * t2' = t2' * w' / t3 `; GSYM VECTOR_ADD_RDISTRIB; VECTOR_ADD_LDISTRIB; VECTOR_SUB_LDISTRIB];
REWRITE_TAC[REAL_ARITH` a - ( a - b ) = b `];
REWRITE_TAC[VECTOR_SUB_RDISTRIB;
VECTOR_ARITH` x - t + z = zz - t + x:real^N <=> z = zz `];
STRIP_TAC THEN STRIP_TAC;
REWRITE_TAC[VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_RDISTRIB];
MATCH_MP_TAC (MESON[]` a = b ==> a % x = b % x `);
UNDISCH_TAC ` &0 < t3 `;
UNDISCH_TAC ` ~ ( w' = &0) `;
UNDISCH_TAC ` t2' < &0 `;
UNDISCH_TAC ` &0 < t2 `;
CONV_TAC REAL_FIELD;
ASM_REWRITE_TAC[];
REWRITE_TAC[Geomdetail.CONV0_SET2; IN_ELIM_THM; VECTOR_ADD_LDISTRIB;
VECTOR_MUL_ASSOC];
EXISTS_TAC ` t3 / (w' * (t2' - t2)) * (w' * &1 / t3) * t2' `;
EXISTS_TAC` t3 / (w' * (t2' - t2)) * (w' * &1 / t3) * --t2 `;
CONJ_TAC;
ASM_SIMP_TAC[REAL_FIELD` ~(t3 = &0) ==> ~( w' = &0 )
==> t3 / (w' * (t2' - t2)) * (w' * &1 / t3) * t2' = t2' / ( t2' - t2) `];
MATCH_MP_TAC REAL_LT_DIV_NEG;
ASM_REAL_ARITH_TAC;
ASSUME_TAC2 (
REAL_FIELD` ~(t3 = &0) /\ ~( w' = &0 ) /\ t2' < &0 /\ &0 < t2
==> t3 / (w' * (t2' - t2)) * (w' * &1 / t3) * --t2 = ( -- t2 ) / ( t2' - t2 ) /\
t3 / (w' * (t2' - t2)) * (w' * &1 / t3) * t2' +
t3 / (w' * (t2' - t2)) * (w' * &1 / t3) * --t2 =
&1 `);
ASM_REWRITE_TAC[];
MATCH_MP_TAC REAL_LT_DIV_NEG;
UNDISCH_TAC ` &0 < t2 `;
UNDISCH_TAC ` t2' < &0 `;
REAL_ARITH_TAC;
DOWN;
SIMP_TAC[DE_MORGAN_THM; REAL_ARITH` ~( a < b ) <=> a = b \/ b < a `];
REWRITE_TAC[TAUT` (a \/ b) /\ c /\ d <=> ((a \/ b) /\ c ) /\ d`; REAL_ARITH` (v' < &0 \/ w' < &0) /\
(&0 < v' \/ &0 < w') <=> v' < &0 /\ &0 < w' \/ w' < &0 /\ &0 < v' `];
STRIP_TAC;
PHA;
REWRITE_TAC[TAUT` a /\ ( b \/ c ) /\ d <=> ( b \/ c) /\ a /\ d `];
SPEC_TAC (`v':real`,`v':real`);
SPEC_TAC (`t2:real`,`t2:real`);
SPEC_TAC (`v:real^N`,`v:real^N`);
SPEC_TAC (`w':real`,`w':real`);
SPEC_TAC (`t3:real`,`t3:real`);
SPEC_TAC (`w:real^N`,`w:real^N`);
IMP_TAC;
MATCH_MP_TAC (MESON[]`(! a b c x y z. P a b c x y z ==> P x y z a b c ) /\
(! a b c x y z. R c z ==> P a b c x y z ) ==> (! a b c x y z. R c z \/ R z c
==> P a b c x y z ) `);
CONJ_TAC;
ONCE_REWRITE_TAC[TAUT` a ==> b ==> c <=> b ==> a ==> c `];
REPEAT GEN_TAC THEN STRIP_TAC;
ANTS_TAC;
DOWN_TAC;
SIMP_TAC[INSERT_COMM; REAL_ADD_SYM; VECTOR_ADD_SYM];
ONCE_REWRITE_TAC[EQ_SYM_EQ];
SIMP_TAC[];
SIMP_TAC[VECTOR_ADD_SYM; INSERT_COMM];
REPEAT STRIP_TAC;
SWITCH_TAC ` x' = t1 % x + t2 % v + t3 % w:real^N`;
SWITCH_TAC `z = u' % x + v'' % v + w'' % w:real^N `;
ASM_REWRITE_TAC[];
UNDISCH_TAC ` x' = t1' % x + t2' % u:real^N `;
EXPAND_TAC "x'";
REWRITE_TAC[VECTOR_ARITH` a + b % x + c = d <=> b % x = d - a - c `];
MP_TAC2 (REAL_ARITH` &0 < t2 ==> ~( t2 = &0 ) `);
ABBREV_TAC ` set = {v,w:real^N} `;
SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE];
REPEAT STRIP_TAC;
UNDISCH_TAC ` u' % x + v'' % v + w'' % w = z:real^N `;
ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_SUB_LDISTRIB; VECTOR_ADD_LDISTRIB];
REWRITE_TAC[REAL_ARITH` a * &1 / b * c = ( a * c ) / b `;
VECTOR_ARITH ` u' % x +
(tt % x + vv % u) -
t22 % x -
ww % w +
w'' % w =
z <=> z + ( t22 - u' - tt ) % x = vv % u + (w'' - ww) % w `];
SUBGOAL_THEN ` &1 + ((v'' * t1) / t2 - u' - (v'' * t1') / t2) =
(v'' * t2') / t2 + (w'' - (v'' * t3) / t2) ` ASSUME_TAC;
ASM_SIMP_TAC[
REAL_FIELD` ~ ( m = &0 ) ==> a / m - b - c / m = ( a - m * b - c ) / m /\
&1 + a / m = ( m + a ) / m /\ a / m + b - c / m = (a + m * b - c ) / m`];
MATCH_MP_TAC (MESON[]` a = b ==> a / x = b / x`);
UNDISCH_TAC ` t1' + t2' = &1 `;
UNDISCH_TAC ` t1 + t2 + t3 = &1 `;
EXPAND_TAC "u'";
SIMP_TAC[REAL_ARITH` a + b = c <=> a = c - b `];
REAL_ARITH_TAC;
ABBREV_TAC ` tu = (v'' * t2') / t2 `;
ABBREV_TAC ` tw = (w'' - (v'' * t3) / t2) `;
STRIP_TAC;
EXISTS_TAC `u:real^N `;
EXISTS_TAC ` w:real^N `;
EXISTS_TAC ` ( &1 / (tu + tw) ) % ( tu % u + tw % w:real^N ) `;
EXPAND_TAC "set";
REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET; IN_INTER];
SUBGOAL_THEN ` &0 < tu /\ &0 < tw ` ASSUME_TAC;
CONJ_TAC;
EXPAND_TAC "tu";
MATCH_MP_TAC REAL_LT_DIV;
ASM_REWRITE_TAC[REAL_MUL_POS_LT];
EXPAND_TAC "tw";
MATCH_MP_TAC (REAL_ARITH` &0 < a /\ b < &0 ==> &0 < a - b `);
ASM_REWRITE_TAC[ REAL_ARITH` a / b < &0 <=> &0 < ( -- a ) / b `];
MATCH_MP_TAC REAL_LT_DIV;
ASM_REWRITE_TAC[REAL_ARITH` -- ( a * b ) = ( -- a ) * b `; REAL_MUL_POS_LT];
ASM_REWRITE_TAC[REAL_ARITH ` &0 < -- a <=> a < &0 `];
CONJ_TAC;
REWRITE_TAC[AFF2; IN_ELIM_THM];
FIRST_X_ASSUM (SUBST1_TAC o SYM);
EXISTS_TAC ` (&1 / (tu + tw)) * (((v'' * t1) / t2 - u' - (v'' * t1') / t2) ) `;
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC;
VECTOR_ARITH` a + z % x = z % x + b <=> a = b `];
MATCH_MP_TAC (MESON[]` a = b ==> a % x = b % x `);
UNDISCH_TAC` &1 + (v'' * t1) / t2 - u' - (v'' * t1') / t2 = tu + tw `;
DOWN;
NHANH (REAL_ARITH` &0 < a /\ &0 < b ==> ~( a + b = &0) `);
CONV_TAC REAL_FIELD;
DOWN;
REWRITE_TAC[IN_CONV0]]);;
let IN_CONV0_EQ_EQ = prove(
`! x:real^N. x
IN conv0 {a,b} ==> ( x = a <=> a = b ) `,
REWRITE_TAC[Geomdetail.CONV0_SET2;
IN_ELIM_THM] THEN
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC` a' + b' = &1 ` THEN
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `] THEN
DISCH_TAC THEN
REWRITE_TAC[VECTOR_ARITH` (&1 - b') % a + b' % b = a + b' % (b - a ) `;
VECTOR_ARITH` a + x = a <=> x =
vec 0`;
VECTOR_MUL_EQ_0] THEN
ASM_SIMP_TAC[REAL_ARITH` &0 < a ==> ~( a = &0 ) `;
VECTOR_SUB_EQ;
EQ_SYM_EQ]);;
let CONDS_FOR_INTER_AFF_CONV0 = prove_by_refinement
(`&0 < t2 /\
&0 < t3 /\
t1 + t2 + t3 = ss /\
t =
t1 % x + t2 % v + t3 % (w:real^N) /\
t1' + t2' = ss /\
t = t1' % x + t2' % u
==> (?tt. tt
IN aff {x, u} /\ tt
IN conv0 {v, w})`,
[STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[VECTOR_ARITH` a % x + y = z <=> z - a % x = y `];
REWRITE_TAC[ VECTOR_ARITH ` (t1' % x + u) -
t1 % x = (t1' -
t1 ) % x + u `];
STRIP_TAC;
EXISTS_TAC` &1 / (t2 + t3 ) % ( (t1' -
t1) % x + t2' % (u:real^N) )`;
CONJ_TAC;
REWRITE_TAC[
VECTOR_ADD_LDISTRIB;
VECTOR_MUL_ASSOC; REAL_ARITH` &1 / a * b = b / a `;
AFF2;
IN_ELIM_THM];
EXISTS_TAC ` (t1' -
t1) / (t2 + t3) `;
MATCH_MP_TAC (MESON[]` a = b ==> f a = f b `);
MATCH_MP_TAC (MESON[]` a = b ==> a % u = b % u `);
DOWN;
REMOVE_TAC;
DOWN;
DOWN THEN REMOVE_TAC;
DOWN_TAC;
CONV_TAC REAL_FIELD;
ASM_REWRITE_TAC[];
MATCH_MP_TAC
IN_CONV0;
ASM_REWRITE_TAC[]]);;
let COLLINEAR_SUBSET_AFF2 = prove_by_refinement
(` a:real^N
IN S /\ b
IN S /\ ~( a = b ) /\
collinear S
==> S
SUBSET aff {a,b} `,
[REWRITE_TAC[
collinear];
STRIP_TAC;
SUBGOAL_THEN ` ? c. a - b:real^N = c % u ` ASSUME_TAC;
ASM_SIMP_TAC[];
REWRITE_TAC[
SUBSET];
GEN_TAC;
UNDISCH_TAC ` b:real^N
IN S `;
PHA;
ONCE_REWRITE_TAC[
CONJ_SYM];
FIRST_X_ASSUM NHANH;
FIRST_X_ASSUM CHOOSE_TAC;
ASM_CASES_TAC ` c = &0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN THEN DOWN;
SIMP_TAC[
VECTOR_MUL_LZERO;
VECTOR_SUB_EQ];
UNDISCH_TAC ` a - b = c % u:real^N `;
ONCE_REWRITE_TAC[
EQ_SYM_EQ];
ASM_SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE];
REWRITE_TAC[VECTOR_ARITH` a = x - b:real^N <=> x = a + b `];
STRIP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[
AFF2;
IN_ELIM_THM;
VECTOR_MUL_ASSOC; VECTOR_ARITH` a % ( x - y ) + y = a % x + ( &1 - a ) % y `];
MESON_TAC[]]);;
let AFF_GE_EQ = prove_by_refinement
(`&0 < t /\ a - x:real^N = t % (b - x) ==>
aff_ge {x} {a} = aff_ge {x} {b} `,
[STRIP_TAC;
SUBGOAL_THEN ` a:real^N
IN aff_ge {x} {b} ` ASSUME_TAC;
MATCH_MP_TAC
CONDS_IN_HAFL_LINE;
ASM_REWRITE_TAC[];
ASM_REAL_ARITH_TAC;
SUBGOAL_THEN ` b:real^N
IN aff_ge {x} {a} ` ASSUME_TAC;
MATCH_MP_TAC (GEN_ALL
CONDS_IN_HAFL_LINE);
EXISTS_TAC ` &1 / t `;
ASSUME_TAC2 (REAL_ARITH` &0 < t ==> ~( t = &0 ) `);
SWITCH_TAC `a - x = t % (b - x:real^N)`;
DOWN;
ASM_SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE];
STRIP_TAC;
MATCH_MP_TAC
REAL_LE_DIV;
UNDISCH_TAC ` &0 < t `;
REAL_ARITH_TAC;
DOWN THEN DOWN;
NHANH
PRESERABLE_AFF_GE_SUBSET;
SET_TAC[]]);;
let FAN_INTERSECTION_PRO_EXPRESS2 =
MESON[FAN_INTERSECTION_PRO_EXPRESS]`FAN (x:real^N,V,E) /\ a IN V /\ b IN V
/\ ~(a = b) /\ &0 < t ==> ~( a - x = t % (b - x))`;;
let FAN_AFF2_INTER_CONV0_IMP_NO_IN_AF = prove_by_refinement
(`
FAN (x:real^N,V,E) /\ {u,v,w}
SUBSET V /\ t
IN aff {x,v}
INTER conv0 {u,w}
/\
CARD {u,v,w} = 3 ==> ~( u
IN aff {x,v} )`,
[NHANH
FAN_IMP_V_DIFF;
STRIP_TAC;
STRIP_TAC;
ASSUME_TAC2 (
ISPECL [` t:real^N `;` x:real^N`;` v:real^N `;`u:real^N `;` w:real^N `] (GEN_ALL
AFF_CONV0_COLL4));
SUBGOAL_THEN ` {x, v, u, w}
SUBSET aff { x,v:real^N } ` ASSUME_TAC;
MATCH_MP_TAC
COLLINEAR_SUBSET_AFF2;
ASM_REWRITE_TAC[
IN_INSERT];
DOWN_TAC;
SIMP_TAC[
EQ_SYM_EQ;
INSERT_SUBSET];
DOWN;
REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET; Planarity.POINT_IN_LINE];
ONCE_REWRITE_TAC[
INSERT_COMM];
REWRITE_TAC[Planarity.POINT_IN_LINE];
REWRITE_TAC[
AFF2;
IN_ELIM_THM];
STRIP_TAC;
ASM_CASES_TAC ` &0 < t' \/ &0 < t'' `;
(* very smart way *)
REPLICATE_TAC 5 DOWN;
REMOVE_TAC;
DOWN_TAC;
DAO;
SPEC_TAC (`t':real`,`t':real`);
SPEC_TAC (`u:real^N `,`u:real^N `);
SPEC_TAC (`t'':real`,`t'':real`);
SPEC_TAC (`w:real^N `,`w:real^N`);
MATCH_MP_TAC (
MESON[]` (! x a y b. P x a y b ==> P y b x a ) /\ (! x a y b. ~( Q b /\ P x a y b )) ==> (! x a y b. ~(( Q b \/ Q a ) /\ P x a y b )) `);
CONJ_TAC;
ONCE_REWRITE_TAC[
EQ_SYM_EQ];
SIMP_TAC[
INSERT_COMM];
REWRITE_TAC[Geomdetail.CARD3];
REPEAT STRIP_TAC;
UNDISCH_TAC` u = t' % v + (&1 - t') % x:real^N `;
REWRITE_TAC[VECTOR_ARITH` u = t' % v + (&1 - t') % x <=> u - x = t' % (v - x )`];
MATCH_MP_TAC (
MESON[
FAN_INTERSECTION_PRO_EXPRESS]`
FAN (x,V,E) /\ a
IN V /\ b
IN V /\ ~(a = b)
/\ &0 < t ==> ~( a - x = t % (b - x))`);
DOWN_TAC;
SIMP_TAC[
INSERT_SUBSET; DE_MORGAN_THM];
ASM_CASES_TAC` t' = &0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC ` u = &0 % v + (&1 - &0) % x:real^N `;
REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_SUB_RDISTRIB;
VECTOR_ADD_LID;
VECTOR_SUB_RZERO;
VECTOR_MUL_LID];
UNDISCH_TAC ` {u, v, w}
SUBSET V:real^N -> bool `;
ASM_SIMP_TAC[
INSERT_SUBSET];
ASM_CASES_TAC ` t'' = &0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC ` w = &0 % v + (&1 - &0) % x:real^N `;
REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_SUB_RDISTRIB;
VECTOR_ADD_LID;
VECTOR_SUB_RZERO;
VECTOR_MUL_LID];
UNDISCH_TAC ` {u, v, w}
SUBSET V:real^N -> bool `;
ASM_SIMP_TAC[
INSERT_SUBSET];
DOWN THEN DOWN THEN DOWN THEN PHA;
REWRITE_TAC[REAL_ARITH` ~(&0 < t' \/ &0 < t'') /\ ~(t' = &0) /\ ~(t'' = &0)
<=> t' < &0 /\ t'' < &0 `];
DOWN THEN DOWN;
REWRITE_TAC[VECTOR_ARITH` u = t' % v + (&1 - t') % x <=>
u - x = t'% ( v - x ) `];
REPEAT STRIP_TAC;
ASSUME_TAC2 (REAL_ARITH` t' < &0 ==> ~( t' = &0) `);
SWITCH_TAC ` u - x = t' % (v - x:real^N)`;
DOWN;
ASM_SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE];
STRIP_TAC;
UNDISCH_TAC ` w - x = t'' % (v - x:real^N)`;
ASM_REWRITE_TAC[
VECTOR_MUL_ASSOC];
MATCH_MP_TAC FAN_INTERSECTION_PRO_EXPRESS2;
DOWN_TAC;
SIMP_TAC[
INSERT_SUBSET; Geomdetail.CARD3; DE_MORGAN_THM; REAL_ARITH ` a * &1 / b = a / b `];
STRIP_TAC;
MATCH_MP_TAC
REAL_LT_DIV_NEG;
ASM_REWRITE_TAC[]]);;
let INTER_EQ_EM_EXPAND = SET_RULE` A INTER B = {} <=> ~( ?x. x IN A /\ x IN B )`;;
let INTER_AFF_GT_LT_IMP_INTER_AFF_CONV0 = REWRITE_RULE[TAUT` a ==> b ==> c
<=> a /\ b ==> c `] (ISPEC ` t:real^N ` (GEN_ALL
INTER_AFF_GT_LT_IMP_INTER_AFF_CONV0));;
let AFF_GT_AFF_LT_INTERPRET = prove_by_refinement
( `! x:real^N.
DISJOINT {x} {v, w} /\
DISJOINT {x} {u}
==> ((?a b c.
a < &0 /\
&0 < b /\
&0 < c /\
a % (u - x) = b % (v - x) + c % (w - x)) <=>
(?tt. tt
IN aff_gt {x} {v, w}
INTER aff_lt {x} {u})) `,
[GEN_TAC THEN STRIP_TAC;
EQ_TAC;
ASM_SIMP_TAC[Planarity.AFF_GT_1_2;
AFF_LT_1_1;
IN_INTER;
IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC ` (x:real^N) + a % (u - x) `;
CONJ_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC ` &1 - b - c `;
EXISTS_TAC `b:real `;
EXISTS_TAC `c:real `;
ASM_REWRITE_TAC[];
CONJ_TAC;
REAL_ARITH_TAC;
VECTOR_ARITH_TAC;
EXISTS_TAC ` &1 - a `;
EXISTS_TAC `a:real `;
ASM_REWRITE_TAC[];
CONJ_TAC;
REAL_ARITH_TAC;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
VECTOR_ARITH_TAC;
ASM_SIMP_TAC[Planarity.AFF_GT_1_2;
AFF_LT_1_1;
IN_INTER;
IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC ` t2':real `;
EXISTS_TAC ` t2:real ` ;
EXISTS_TAC ` t3:real `;
ASM_REWRITE_TAC[];
DOWN;
DOWN;
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `];
REMOVE_TAC;
DOWN;
REMOVE_TAC;
DOWN;
DOWN;
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `];
REMOVE_TAC;
REMOVE_TAC;
VECTOR_ARITH_TAC]);;
let AFF_GT_AFF_LT_INTERPRET2 = REWRITE_RULE[SET_RULE`DISJOINT {x} {v, w} /\
DISJOINT {x} {u} <=> DISJOINT {x} {u,v,w} `] AFF_GT_AFF_LT_INTERPRET;;
let EXISTS_IN = SET_RULE` ~( a = {} ) <=> ? x. x IN a `;;
let AFF_GT_LT_INTER_SYM = prove_by_refinement
(`! x:real^N.
DISJOINT {x} {u, v, w} ==>
~( aff_gt {x} {v,w}
INTER aff_lt {x} {u} = {} ) ==>
~( aff_gt {x} {u,v}
INTER aff_lt {x} {w} = {} )`,
[REWRITE_TAC[EXISTS_IN];
SIMP_TAC[GSYM AFF_GT_AFF_LT_INTERPRET2];
ONCE_REWRITE_TAC[SET_RULE` {a,b,c} = {c,a,b} `];
SIMP_TAC[GSYM AFF_GT_AFF_LT_INTERPRET2];
REPEAT STRIP_TAC;
EXISTS_TAC ` -- c:real `;
EXISTS_TAC ` -- a :real `;
EXISTS_TAC ` b:real `;
ASM_SIMP_TAC[VECTOR_ARITH` a % (u - x) = b % (v - x) + c % (w - x)
==> --c % (w - x) = --a % (u - x) + b % (v - x) `];
ASM_REAL_ARITH_TAC]);;
let EXISTS_INTERSECTION_PROPERPLY = prove_by_refinement
(` (~(z:real^N = x) /\
DISJOINT {x} {v, w} /\
~(x = u) /\
~(aff_gt {x} {v, w}
INTER aff_lt {x} {u} = {}) /\
z
IN affine hull {x, v, w}) /\
~
collinear {x,v,w}
==> (?a b t.
{a, b}
SUBSET {u, v, w} /\
t
IN aff {x, z}
INTER conv0 {a, b} /\
~(a
IN aff {x,z}))`,
[NHANH
INTERSECTION_LEMMA;
STRIP_TAC;
ASM_CASES_TAC` ~( a:real^N
IN aff {x,z}) `;
EXISTS_TAC ` a:real^N `;
EXISTS_TAC ` b:real^N `;
EXISTS_TAC ` t:real^N `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` {a, b}
SUBSET {u, v, w:real^N } `;
ONCE_REWRITE_TAC[
INSERT_SUBSET];
ONCE_REWRITE_TAC[
IN_INSERT];
STRIP_TAC;
EXISTS_TAC` v:real^N `;
EXISTS_TAC `w:real^N `;
REWRITE_TAC[
IN_INSERT;
INSERT_SUBSET;
EMPTY_SUBSET];
SUBGOAL_THEN` (?tt. tt
IN aff {x, u}
INTER conv0 {v, w:real^N})` MP_TAC;
MATCH_MP_TAC (GEN_ALL
INTER_AFF_GT_LT_IMP_INTER_AFF_CONV0);
ASM_SIMP_TAC[];
UNDISCH_TAC ` ~(aff_gt {x} {v, w}
INTER aff_lt {x} {u:real^N} = {}) `;
SET_TAC[];
STRIP_TAC;
EXISTS_TAC `tt:real^N `;
SUBGOAL_THEN` aff {x,z} = aff {x,u:real^N} ` SUBST_ALL_TAC;
MATCH_MP_TAC Planarity.sym_line_fan1;
UNDISCH_TAC ` ~ ~(a
IN aff {x, z:real^N}) `;
ASM_SIMP_TAC[SET_RULE`
DISJOINT {x} {u,z} <=> ~( z = x ) /\ ~ (x = u )`];
ASM_REWRITE_TAC[];
STRIP_TAC;
SUBGOAL_THEN ` w
IN aff {x, u:real^N} ` MP_TAC;
DOWN THEN DOWN;
NHANH
AFF2_ITR_CONV0_IMP_SAME_ENDS;
SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN ` {x,v,w:real^N}
SUBSET aff {x,u} ` MP_TAC;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET; Planarity.POINT_IN_LINE];
REWRITE_TAC[];
NHANH
SUBSET_AFF2_IMP_COLL;
ASM_REWRITE_TAC[];
UNDISCH_TAC` a
IN {v,w:real^N} ` ;
REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY];
DOWN_TAC;
DAO;
SPEC_TAC (`v:real^N`,`v:real^N`);
SPEC_TAC (`w:real^N`,`w:real^N`);
MATCH_MP_TAC (MESON[]` (! x y. (P x y ==> P y x) /\ ( L x y ==> L y x )) /\
(! x y. a = x /\ P x y ==> L x y ) ==>
(! y x. (a = x \/ a = y) /\ P x y ==> L x y ) `);
CONJ_TAC;
SIMP_TAC[
INSERT_COMM;
DISJ_SYM];
REPEAT STRIP_TAC;
EXISTS_TAC ` w:real^N`;
EXISTS_TAC `u:real^N`;
REWRITE_TAC[
INSERT_SUBSET;
IN_INSERT;
EMPTY_SUBSET;
RIGHT_EXISTS_AND_THM];
CONJ_TAC;
STRIP_TAC;
SUBGOAL_THEN ` {x:real^N,v,w}
SUBSET aff {x,z} ` MP_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET; Planarity.POINT_IN_LINE];
UNDISCH_TAC` ~collinear {x, v, w:real^N}`;
MESON_TAC[
SUBSET_AFF2_IMP_COLL];
SUBGOAL_THEN ` aff {x, z} = aff {x,v:real^N}` SUBST1_TAC;
MATCH_MP_TAC
AFF2_DET_BY_TWO_POINTS;
REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET; Planarity.POINT_IN_LINE];
FIRST_X_ASSUM SUBST_ALL_TAC;
ASM_SIMP_TAC[
EQ_SYM_EQ];
UNDISCH_TAC`
DISJOINT {x} {v, w:real^N}` ;
SET_TAC[];
MATCH_MP_TAC (GEN_ALL
INTER_AFF_GT_LT_IMP_INTER_AFF_CONV0);
ASM_SIMP_TAC[
INSERT_COMM;
RIGHT_EXISTS_AND_THM];
CONJ_TAC;
DOWN THEN DOWN THEN DOWN;
SET_TAC[];
REWRITE_TAC[GSYM EXISTS_IN];
MATCH_MP_TAC (
REWRITE_RULE[TAUT` a ==> b ==> c <=> a /\ b ==> c `]
AFF_GT_LT_INTER_SYM);
ASM_SIMP_TAC[
INSERT_COMM];
DOWN THEN DOWN THEN SET_TAC[]]);;
REWRITE_TAC[orbit_map; IN_ELIM_THM; ARITH_RULE` a >= 0`];
MESON_TAC[];
MP_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
NHANH FAN_IMP_V_DIFF;
ASM_SIMP_TAC[EQ_SYM_EQ];
STRIP_TAC;
SUBGOAL_THEN ` ~(b IN aff {vec 0, (rho_node1 FF POWER n') v})` MP_TAC;
DOWN;
DOWN;
NHANH AFF2_ITR_CONV0_IMP_SAME_ENDS;
SIMP_TAC[];
DOWN THEN PHA;
REWRITE_TAC[SET_RULE` ~( x IN S ) /\ ~(y IN S ) <=> {x,y} INTER S = {} `];
STRIP_TAC;
SUBGOAL_THEN ` interior_angle1 (vec 0) FF ((rho_node1 FF POWER n') v) = pi /\
rho_node1 FF ((rho_node1 FF POWER n') v) IN (affine hull {v, w, vec 0}) /\
ivs_rho_node1 FF ((rho_node1 FF POWER n') v) IN ( affine hull {v, w, vec 0})` ASSUME_TAC;
MATCH_MP_TAC (GEN_ALL OZQVSFF);
EXISTS_TAC `E:(real^3 -> bool) -> bool `;
EXISTS_TAC `V:real^3 -> bool `;
EXISTS_TAC ` a:real^3 `;
EXISTS_TAC ` b:real^3 `;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
SUBGOAL_THEN ` {a,b:real^3} SUBSET V` MP_TAC;
UNDISCH_TAC `{a, b} SUBSET {u, v, w:real^3}`;
MATCH_MP_TAC (SET_RULE` A SUBSET B ==> c SUBSET A ==> c SUBSET B `);
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
SIMP_TAC[INSERT_SUBSET];
SUBGOAL_THEN ` {u, v, w} SUBSET affine hull {v,w,vec 0:real^3}` ASSUME_TAC;
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; Ldurdpn.IN_HULL_INSERT];
ONCE_REWRITE_TAC[INSERT_COMM];
REWRITE_TAC[Ldurdpn.IN_HULL_INSERT];
ONCE_REWRITE_TAC[SET_RULE` {a,b,c} = {c,b,a} `];
MATCH_MP_TAC (GEN_ALL IN_AFF_HULL_3);
UNDISCH_TAC` ~(aff_gt {vec 0} {v:real^3, w} INTER aff_lt {vec 0} {u} = {}) `;
SET_TAC[];
ASSUME_TAC2 (ISPECL [`{a,b:real^3}`;` {u,v,w:real^3}`;
`affine hull {v,w, vec 0:real^3 }` ] SUBSET_TRANS);
DOWN;
SIMP_TAC[INSERT_SUBSET];
STRIP_TAC THEN STRIP_TAC;
ONCE_REWRITE_TAC[SET_RULE`{a,b,c} = {c,a,b} `];
REWRITE_TAC[Ldurdpn.IN_HULL_INSERT; POWER_TO_ITER];
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_VITER;
UNDISCH_TAC `v:real^3 IN V `;
FIRST_X_ASSUM (MP_TAC o (SPECL [`v:real^3`;` n': num `]));
DISCH_THEN NHANH;
SIMP_TAC[];
STRIP_TAC;
CONJ_TAC;
REWRITE_TAC[plane];
EXISTS_TAC ` vec 0:real^3 `;
EXISTS_TAC `v:real^3 `;
EXISTS_TAC `w:real^3 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC ` t IN aff {vec 0, (rho_node1 FF POWER n') v} INTER conv0 {a, b:real^3}`;
SIMP_TAC[INSERT_COMM; POWER_TO_ITER];
SET_TAC[];
DOWN;
SIMP_TAC[COM_POWER; o_THM]]);;
let CARD_RECUSIVE_EQ = prove_by_refinement
(` !k f. 0 < k ==>
(
CARD {
ITER n f x:A | n < k} = k
<=>
CARD {
ITER n f x | n < k - 1} = k - 1 /\
(!i. i < k - 1 ==> ~(
ITER i f x =
ITER (k - 1) f x))) `,
[REPEAT GEN_TAC;
STRIP_TAC;
EQ_TAC;
REWRITE_TAC[Wrgcvdr_cizmrrh.CARD_K_FIRST_ELMS_EQ_K];
SUBGOAL_THEN ` {
ITER n f x:A | n < k} =
ITER (k - 1) f x
INSERT {
ITER n f x | n < k - 1} ` SUBST1_TAC;
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_INSERT];
ASM_SIMP_TAC[ARITH_RULE`0 < b ==> ( a < b <=> a = b - 1 \/ a < b - 1 )`];
MESON_TAC[];
STRIP_TAC;
SUBGOAL_THEN ` FINITE {
ITER n f x:A | n < k - 1} /\
~(
ITER (k - 1) f x
IN {
ITER n f x | n < k - 1}) ` ASSUME_TAC;
REWRITE_TAC[
IN_ELIM_THM; SET_RULE` {
ITER n f x | n < k } = {y | ?n. n < k /\
y =
ITER n f x}`; Wrgcvdr_cizmrrh.FINITE_OF_N_FIRST_ELMS];
DOWN THEN MESON_TAC[];
DOWN THEN STRIP_TAC;
ASM_SIMP_TAC[Geomdetail.CARD_CLAUSES_IMP];
UNDISCH_TAC ` 0 < k `;
ARITH_TAC]);;
let LEMMA_SUBSET_ORBIT_MAP = REWRITE_RULE[POWER_TO_ITER] Hypermap.lemma_subset_orbit;;
REWRITE_TAC[ARITH_RULE ` a < b ==> a <= b - 1 `; LEMMA_SUBSET_ORBIT_MAP_LT];
DOWN_TAC;
SIMP_TAC[EQ_SYM_EQ];
NHANH SELF_CYCLIC_IMP_FINITE;
ONCE_REWRITE_TAC[EQ_SYM_EQ];
STRIP_TAC;
ASM_SIMP_TAC[GSYM SUBSET_CARD_EQ]]);;
let lemma_in_orbit_iter = REWRITE_RULE[POWER_TO_ITER] Hypermap.lemma_in_orbit;;
(* ==================================== *)
let KCHMAMG = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\ circular V E
==> (!v. v
IN V ==>
interior_angle1 (
vec 0)
FF v =
pi) /\
(?A.
plane A /\
vec 0
IN A /\
V
SUBSET A /\
(?e. (!x. x
IN A ==> e
dot x = &0) /\
cyclic_set V (
vec 0) e /\
(!v. v
IN V
==>
azim_cycle V (
vec 0) e v =
rho_node1 FF v /\
azim (
vec 0) e v (
rho_node1 FF v) =
dihV (
vec 0) e v (
rho_node1 FF v) /\
azim (
vec 0) e v (
rho_node1 FF v) =
arcV (
vec 0) v (
rho_node1 FF v) /\
azim (
vec 0) e v (
rho_node1 FF v) <
pi)))`,
[REWRITE_TAC[circular];
STRIP_TAC;
DOWN_TAC;
NGOAC;
NHANH
CVX_LO_IMP_LO;
ONCE_REWRITE_TAC[TAUT` ((a/\b)/\c)/\ x
IN S <=>a /\(b/\c)/\x
IN S`];
NHANH
LOFA_IN_E_IMP_IN_FF;
PHA;
SPEC_TAC (`v:real^3`,`v:real^3`);
SPEC_TAC (`w:real^3`,`w:real^3 `);
ONCE_REWRITE_TAC[TAUT` a /\a1 /\a2 /\a3/\a4 <=> a3 /\ a/\a1/\a2/\a4`];
MATCH_MP_TAC (
MESON[]`(! x y. P x y ==> P y x) /\ (! x y. Q x y /\ P x y ==> L)
==> (! x y. (Q x y \/ Q y x) /\ P x y ==> L)`);
CONJ_TAC;
SIMP_TAC[
INSERT_COMM];
REPEAT GEN_TAC THEN STRIP_TAC;
ONCE_REWRITE_TAC[TAUT` a /\ b <=> b /\ ( b ==> a ) `];
CONJ_TAC;
EXISTS_TAC `
affine hull {
vec 0, v, w:real^3}`;
REWRITE_TAC[
plane];
UNDISCH_TAC ` v,w
IN FF:real^3 # real^3 -> bool `;
UNDISCH_TAC `
local_fan (V,E,
FF) `;
PHA;
NHANH
LOCAL_FAN_IN_FF_NOT_COLLINEAR;
STRIP_TAC;
CONJ_TAC;
EXISTS_TAC `
vec 0:real^3 `;
EXISTS_TAC ` v:real^3 `;
EXISTS_TAC ` w:real^3 `;
DOWN;
SIMP_TAC[];
REWRITE_TAC[Ldurdpn.IN_HULL_INSERT];
ASSUME_TAC2
LOFA_V_SUBSET_AFF_HULL;
ASM_SIMP_TAC[
INSERT_COMM];
ABBREV_TAC ` e = v
cross (
rho_node1 FF v ) `;
EXISTS_TAC ` e:real^3 `;
SUBGOAL_THEN ` v:real^3
IN V /\ w
IN V ` MP_TAC;
MATCH_MP_TAC
LOCAL_FAN_IMP_IN_V;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2
LOFA_IN_V_SO_DO_RHO_NODE_V;
DOWN THEN DOWN;
UNDISCH_TAC ` V
SUBSET affine hull {v, w,
vec 0} /\ ~collinear {
vec 0, v, w:real^3}`;
REWRITE_TAC[
SUBSET];
STRIP_TAC;
PHA;
FIRST_ASSUM (NHANH_PAT`\x. x ==> y ` );
STRIP_TAC;
ASSUME_TAC2
DETER_RHO_NODE;
CONJ_TAC;
REWRITE_TAC[
AFFINE_HULL_3;
IN_ELIM_THM];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "e";
UNDISCH_TAC ` rho_node1 FF v = w `;
SIMP_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_RID; DOT_RADD; DOT_RMUL; DOT_CROSS_SELF;
Collect_geom.ZERO_NEUTRAL];
REWRITE_TAC[DOT_RZERO; Collect_geom.ZERO_NEUTRAL];
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_V;
DOWN THEN NHANH LOOP_SET_DETER_FIRTS_ELMS;
STRIP_TAC;
UNDISCH_TAC` v:real^3 IN V `;
FIRST_X_ASSUM (NHANH_PAT`\x. x ==> y`);
FIRST_ASSUM (NHANH_PAT`\x. x ==> y`);
STRIP_TAC;
SUBGOAL_THEN` ITER (CARD (V:real^3 -> bool)) (rho_node1 FF) v IN V ` ASSUME_TAC;
DOWN;
EXPAND_TAC "V";
REWRITE_TAC[lemma_in_orbit_iter];
SUBGOAL_THEN`ITER (CARD (V:real^3 -> bool)) (rho_node1 FF) v INSERT {ITER n (rho_node1 FF) v | n < CARD V} = {ITER n (rho_node1 FF) v | n <= CARD V} ` ASSUME_TAC;
REWRITE_TAC[EXTENSION; IN_INSERT; IN_ELIM_THM];
MESON_TAC[ARITH_RULE` a <= b <=> a = b \/ a < b:num `];
REPLICATE_TAC 3 DOWN THEN PHA;
NHANH (SET_RULE` a = b /\ x IN b /\ x INSERT a = h ==> h = b `);
STRIP_TAC;
MP_TAC2 (
SPECL [`V:real^3 -> bool`;`affine hull {v, w, vec 0:real^3} `;` CARD (V:real^3
-> bool)`] (GENL [`U:real^3 -> bool`;` P:real^3 -> bool `;`l:num`]
(SPEC_ALL KOMWBWC)));
ASSUME_TAC2 LOFA_V_SUBSET_AFF_HULL;
ASM_REWRITE_TAC[plane];
CONJ_TAC;
EXISTS_TAC` vec 0:real^3 `;
EXISTS_TAC `v:real^3 `;
EXISTS_TAC ` w:real^3 `;
ASM_REWRITE_TAC[];
SIMP_TAC[INSERT_COMM];
ONCE_REWRITE_TAC[SET_RULE` {a,b,c} = {c,a,b}`];
REWRITE_TAC[Ldurdpn.IN_HULL_INSERT];
STRIP_TAC;
GEN_TAC THEN STRIP_TAC;
CONJ_TAC;
DOWN;
UNDISCH_TAC` {ITER n (rho_node1 FF) v | n < CARD V} = V`;
STRIP_TAC;
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
ONCE_REWRITE_TAC[CONJ_SYM];
STRIP_TAC;
DOWN THEN DOWN THEN PHA;
ASM_SIMP_TAC[];
UNDISCH_TAC `!x n.
x = ITER n (rho_node1 FF) v /\ n < CARD V
==> azim_cycle V (vec 0) e (ITER n (rho_node1 FF) v) =
rho_node1 FF (ITER n (rho_node1 FF) v) `;
MESON_TAC[];
SUBGOAL_THEN` &0 < sin (azim (vec 0) e v' (rho_node1 FF v')) ` ASSUME_TAC;
MP_TAC (SPECL [`e:real^3 `;` v':real^3 `;` rho_node1 FF v' `]
Trigonometry2.JBDNJJB);
REWRITE_TAC[re_eqvl];
STRIP_TAC;
FIRST_X_ASSUM SUBST1_TAC;
MATCH_MP_TAC REAL_LT_MUL;
UNDISCH_TAC ` v':real^3 IN V `;
UNDISCH_TAC `{ITER n (rho_node1 FF) v | n < CARD V} = V `;
DISCH_THEN (SUBST1_TAC o SYM);
REWRITE_TAC[IN_ELIM_THM];
UNDISCH_TAC ` !i. i < CARD (V:real^3 -> bool)
==> &0 <
(ITER i (rho_node1 FF) v cross ITER (i + 1) (rho_node1 FF) v) dot
e `;
DISCH_THEN NHANH;
STRIP_TAC;
DOWN;
ASM_SIMP_TAC[GSYM ITER; ADD1];
ONCE_REWRITE_TAC[CROSS_TRIPLE];
ASM_REWRITE_TAC[];
MP_TAC (SPECL [`vec 0:real^3 `;` e:real^3 `;` v':real^3 `;
`rho_node1 FF v' `] AZIM_RANGE);
ASM_CASES_TAC ` pi <= azim (vec 0) e v' (rho_node1 FF v') `;
STRIP_TAC;
ABBREV_TAC ` a = azim (vec 0) e v' (rho_node1 FF v') `;
SUBGOAL_THEN ` sin a <= &0 ` MP_TAC;
ONCE_REWRITE_TAC[SIN_SUB_PERIODIC];
REWRITE_TAC[REAL_ARITH` -- a <= &0 <=> &0 <= a `];
MATCH_MP_TAC SIN_POS_PI_LE;
UNDISCH_TAC ` pi <= a `;
UNDISCH_TAC ` a < &2 * pi `;
REAL_ARITH_TAC;
UNDISCH_TAC ` &0 < sin a `;
MESON_TAC[REAL_ARITH` &0 < a ==> ~(a <= &0 ) `];
DOWN;
REWRITE_TAC[REAL_ARITH` ~( a <= b ) <=> b < a `];
SUBGOAL_THEN `~ collinear {vec 0, e, v'} /\ ~ collinear {vec 0, e, rho_node1 FF v'}` ASSUME_TAC;
SUBGOAL_THEN ` rho_node1 FF v' IN V ` ASSUME_TAC;
MATCH_MP_TAC LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[SET_RULE`{a,b,c} = {c,a,b}`];
UNDISCH_TAC` cyclic_set V (vec 0) (e:real^3) `;
NHANH Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR;
ASM_SIMP_TAC[];
DOWN;
SIMP_TAC[AZIM_DIHV_SAME];
REPEAT STRIP_TAC;
REWRITE_TAC[Trigonometry2.DIHV_FORMULAR; VECTOR_SUB_RZERO];
SUBGOAL_THEN` v' dot e = &0 /\ rho_node1 FF v' dot (e:real^3) = &0 ` MP_TAC;
SUBGOAL_THEN ` rho_node1 FF v' IN V ` ASSUME_TAC;
MATCH_MP_TAC LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
DOWN;
UNDISCH_TAC ` v':real^3 IN V `;
UNDISCH_TAC` !x. x IN V ==> x IN affine hull {v, w, vec 0:real^3}`;
DISCH_THEN NHANH;
REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
STRIP_TAC THEN STRIP_TAC;
ASM_REWRITE_TAC[];
EXPAND_TAC "e";
USE_FIRST ` rho_node1 FF v = w ` SUBST1_TAC;
REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_RID];
REWRITE_TAC[DOT_LADD; DOT_LMUL; DOT_CROSS_SELF];
REAL_ARITH_TAC;
SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_SUB_RZERO];
SUBGOAL_THEN` &0 < e dot (e:real^3)` ASSUME_TAC;
UNDISCH_TAC `cyclic_set V (vec 0) (e:real^3) `;
SIMP_TAC[DOT_POS_LT; cyclic_set; EQ_SYM_EQ];
REMOVE_TAC;
DOWN;
MESON_TAC[Trigonometry2.WHEN_A_B_POS_ARCV_STABLE];
STRIP_TAC;
REPEAT STRIP_TAC;
ASSUME_TAC2 (SPEC `v:real^3,w:real^3 ` (GEN `x:real^3# real^3 `
LOCAL_FAN_IN_FF_NOT_COLLINEAR));
SUBGOAL_THEN` affine hull {vec 0, v, w:real^3} = A ` ASSUME_TAC;
MATCH_MP_TAC THREE_NOT_COLL_DETER_PLANE;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
UNDISCH_TAC` V:real^3 -> bool SUBSET A `;
MATCH_MP_TAC (SET_RULE` x IN A /\ y IN A ==> A SUBSET B ==> x IN B /\ y IN B`);
MATCH_MP_TAC LOCAL_FAN_IMP_IN_V;
ASM_REWRITE_TAC[];
MP_TAC (ISPECL [` vec 0:real^3 `;` v':real^3 ` ] (GENL [` x:real^N `;
` z:real^N `] EXISTS_INTERSECTION_PROPERPLY));
ANTS_TAC;
ASM_REWRITE_TAC[];
MP_TAC2 (SET_RULE` v' :real^3 IN V /\ V SUBSET A ==> v' IN A`);
SIMP_TAC[];
DISCH_TAC;
SUBGOAL_THEN ` v IN V /\ w:real^3 IN V ` MP_TAC;
MATCH_MP_TAC LOCAL_FAN_IMP_IN_V;
ASM_REWRITE_TAC[];
MP_TAC2 Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
NHANH FAN_IMP_V_DIFF;
STRIP_TAC;
UNDISCH_TAC ` v':real^3 IN V `;
UNDISCH_TAC ` u:real^3 IN V `;
FIRST_X_ASSUM NHANH;
SET_TAC[];
STRIP_TAC;
SUBGOAL_THEN ` ~(b IN aff {vec 0, v':real^3}) ` MP_TAC;
DOWN THEN DOWN;
NHANH AFF2_ITR_CONV0_IMP_SAME_ENDS;
SIMP_TAC[];
DOWN THEN PHA;
REWRITE_TAC[SET_RULE` ~( a IN X) /\ ~( b IN X ) <=> {a,b} INTER X = {}`];
STRIP_TAC;
MP_TAC (SPECL [`E:(real^3 -> bool) -> bool `;` V:real^3 -> bool`;
` FF: real^3 #real^3 -> bool `;` v':real^3 ` ;`A:real^3 -> bool`;` a:real^3 `;
` b:real^3 `] (GEN_ALL OZQVSFF));
ANTS_TAC;
SUBGOAL_THEN` {a,b} SUBSET (V:real^3 -> bool) ` MP_TAC;
UNDISCH_TAC` {a, b} SUBSET {u, v, w:real^3}`;
MATCH_MP_TAC (SET_RULE` B SUBSET C ==> A SUBSET B ==> A SUBSET C `);
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
MATCH_MP_TAC LOCAL_FAN_IMP_IN_V;
ASM_REWRITE_TAC[];
UNDISCH_TAC` v':real^3 IN V `;
UNDISCH_TAC ` (V:real^3 -> bool) SUBSET A `;
SIMP_TAC[INSERT_SUBSET];
REWRITE_TAC[SUBSET];
DISCH_THEN NHANH;
ASM_SIMP_TAC[];
DOWN THEN PHA THEN REMOVE_TAC;
DOWN THEN SIMP_TAC[INSERT_COMM];
SET_TAC[];
SIMP_TAC[]]);;
(* ========================================================= *)
(* JULY *)
let WEDGE_GE_EQ_AFF_GE = prove_by_refinement
(`
azim v0 v1 w1 w2 <
pi /\ ~
collinear {v0,v1,w1} /\ ~
collinear {v0,v1,w2}
==>
wedge_ge v0 v1 w1 w2 = aff_ge {v0, v1} {w1,w2} `,
[ASM_SIMP_TAC[
wedge_ge];
NHANH Fan.th3b1;
ONCE_REWRITE_TAC[
INSERT_COMM];
NHANH Fan.th3b1;
STRIP_TAC;
SUBGOAL_THEN`
DISJOINT {v1,v0} {w2,w1:real^3}` ASSUME_TAC;
ASM SET_TAC[];
SUBGOAL_THEN ` aff_ge {v0,v1} {w1}
SUBSET aff_ge {v0,v1} {w1,w2:real^3}` ASSUME_TAC;
MATCH_MP_TAC
AFF_GE_MONO_RIGHT;
DOWN THEN SET_TAC[];
ASM_CASES_TAC`
azim v0 v1 w1 w2 = &0 `;
ASM_SIMP_TAC[
IN_ELIM_THM; REAL_LE_ANTISYM; REAL_ARITH` &0 = a <=> a = &0`];
DOWN;
UNDISCH_TAC` ~
collinear {v1,v0,w1:real^3 }`;
ONCE_REWRITE_TAC[
INSERT_COMM];
ASM_SIMP_TAC[
AZIM_EQ_0_GE_ALT2; GSYM
SUBSET_ANTISYM_EQ; SET_RULE` {x| x
IN S } = S `];
(* *)
SUBGOAL_THEN`
DISJOINT {v0,v1} {w1: real^3}` MP_TAC;
DOWN THEN SET_TAC[];
DOWN THEN DOWN;
SIMP_TAC[Collect_geom.simp_def2;
AFF_GE22;
INSERT_COMM];
REWRITE_TAC[
IN_ELIM_THM;
SUBSET];
REPEAT STRIP_TAC;
DOWN;
ASM_REWRITE_TAC[];
SIMP_TAC[];
STRIP_TAC;
EXISTS_TAC ` aa + yy * ta `;
EXISTS_TAC ` bb + yy * tb `;
EXISTS_TAC ` xx + yy * t `;
ASM_REWRITE_TAC[REAL_ARITH` (aa + yy * ta) + (bb + yy * tb) + xx + yy * t =
aa + bb + xx + yy * ( ta + tb + t ) `;
REAL_MUL_RID];
CONJ_TAC;
MATCH_MP_TAC
REAL_LE_ADD;
ASM_REWRITE_TAC[];
MATCH_MP_TAC
REAL_LE_MUL;
ASM_REWRITE_TAC[];
CONV_TAC VECTOR_ARITH;
MP_TAC (SPECL [`v0:real^3 `;` v1:real^3 `;`w1:real^3 `;` w2:real^3 `]
AZIM_RANGE);
ASM_REWRITE_TAC[REAL_ARITH` &0 <= a <=> a = &0 \/ &0 < a `];
STRIP_TAC;
DOWN_TAC THEN SIMP_TAC[
INSERT_COMM];
STRIP_TAC;
ASSUME_TAC2
WEDGE_LUNE_GT;
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM];
GEN_TAC;
EQ_TAC;
ASM_SIMP_TAC[
AZIM_EQ_0_GE_ALT2];
STRIP_TAC;
UNDISCH_TAC ` x
IN aff_ge {v0, v1} {w1:real^3}`;
UNDISCH_TAC ` aff_ge {v0, v1} {w1}
SUBSET aff_ge {v0, v1} {w1, w2:real^3}`;
REWRITE_TAC[
SUBSET];
DISCH_THEN NHANH;
SIMP_TAC[];
DOWN;
REWRITE_TAC[REAL_ARITH` a <= b <=> a = b \/ a < b `];
SUBGOAL_THEN` ~
collinear {v0,v1,x:real^3} ` ASSUME_TAC;
STRIP_TAC;
UNDISCH_TAC ` &0 <
azim v0 v1 w1 x `;
DOWN;
SIMP_TAC[
AZIM_DEGENERATE];
DISCH_TAC;
REAL_ARITH_TAC;
STRIP_TAC;
DOWN;
ASM_SIMP_TAC[
AZIM_EQ_ALT];
STRIP_TAC;
SUBGOAL_THEN ` aff_ge {v0,v1} {w2}
SUBSET aff_ge {v0,v1} {w1,w2:real^3} ` ASSUME_TAC;
MATCH_MP_TAC
AFF_GE_MONO_RIGHT;
ASM_REWRITE_TAC[];
SET_TAC[];
DOWN;
REWRITE_TAC[
SUBSET];
DISCH_THEN MATCH_MP_TAC;
MP_TAC (ISPECL [`{v0,v1:real^3} `;` {w2:real^3} `]
AFF_GT_SUBSET_AFF_GE);
REWRITE_TAC[
SUBSET];
DISCH_THEN MATCH_MP_TAC;
DOWN THEN SIMP_TAC[];
SUBGOAL_THEN` x
IN wedge v0 v1 w1 w2 ` ASSUME_TAC;
REWRITE_TAC[
wedge;
IN_ELIM_THM];
DOWN THEN DOWN THEN DOWN THEN PHA;
SIMP_TAC[];
DOWN;
MATCH_MP_TAC (SET_RULE` a
SUBSET b ==> x
IN a ==> x
IN b `);
ASM_REWRITE_TAC[
AFF_GT_SUBSET_AFF_GE];
ASM_SIMP_TAC[
AFF_GE22;
IN_ELIM_THM];
STRIP_TAC;
ASM_CASES_TAC ` yy = &0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC` ~collinear {v0, v1, w1:real^3}`;
NHANH
AZIM_EQ_0_GE_ALT2;
STRIP_TAC;
SUBGOAL_THEN `
azim v0 v1 w1 x = &0 ` ASSUME_TAC;
FIRST_X_ASSUM SUBST1_TAC;
ASSUME_TAC2 (SET_RULE`
DISJOINT {v0, v1} {w1, w2} ==>
DISJOINT {v0,v1} {w1:real^3} `);
DOWN;
SIMP_TAC[Collect_geom.simp_def2];
ASM_REWRITE_TAC[
IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` aa:real `;
EXISTS_TAC ` bb:real `;
EXISTS_TAC ` xx:real `;
ASM_REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_ADD_RID];
UNDISCH_TAC ` aa + bb + xx + &0 = &1 `;
REAL_ARITH_TAC;
FIRST_X_ASSUM SUBST_ALL_TAC;
REWRITE_TAC[
AZIM_RANGE];
ASM_CASES_TAC`
collinear {v0,v1,x:real^3} `;
DOWN;
SIMP_TAC[
AZIM_DEGENERATE;
AZIM_RANGE];
ASM_CASES_TAC ` xx = &0 `;
SUBGOAL_THEN `
azim v0 v1 w1 x =
azim v0 v1 w1 w2 ` ASSUME_TAC;
SUBGOAL_THEN `
azim v0 v1 w1 x =
azim v0 v1 w1 w2 <=> x
IN aff_gt {v0,v1} {w2}` SUBST1_TAC;
MATCH_MP_TAC
AZIM_EQ_ALT;
ASM_REWRITE_TAC[];
MP_TAC2 (SET_RULE`
DISJOINT {v0,v1} {w1,w2} ==>
DISJOINT {v0,v1} {w2:real^3}`);
SIMP_TAC[
AFF_GT_2_1;
IN_ELIM_THM];
REMOVE_TAC;
EXISTS_TAC ` aa:
real`;
EXISTS_TAC` bb:real `;
EXISTS_TAC ` yy:real `;
ASM_REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_ADD_LID];
FIRST_X_ASSUM SUBST_ALL_TAC;
UNDISCH_TAC ` &0 <= yy `;
UNDISCH_TAC ` ~( yy = &0 ) `;
UNDISCH_TAC ` aa + bb + &0 + yy = &1 `;
REAL_ARITH_TAC;
ASM_REWRITE_TAC[
REAL_LE_REFL];
SUBGOAL_THEN` x
IN wedge v0 v1 w1 w2 ` ASSUME_TAC;
ASM_SIMP_TAC[Planarity.AFF_GT_2_2;
IN_ELIM_THM];
EXISTS_TAC ` aa:real ` ;
EXISTS_TAC ` bb:real`;
EXISTS_TAC ` xx:real ` ;
EXISTS_TAC` yy:real`;
ASM_REWRITE_TAC[REAL_ARITH` a < b <=> ~( b = a ) /\ a <= b `];
DOWN;
REWRITE_TAC[
wedge;
IN_ELIM_THM];
IMP_TAC;
REMOVE_TAC;
REAL_ARITH_TAC]);;
let AZIM_PI_WEDGE_GE_SIN = prove_by_refinement(`
azim u v w ww =
pi ==>
wedge_ge u v w ww = {x| &0 <=
sin (
azim u v w x ) } `,
[REWRITE_TAC[
wedge_ge;
EXTENSION;
IN_ELIM_THM];
ONCE_REWRITE_TAC[GSYM (SPEC ` -- (u:real^3) `
AZIM_TRANSLATION)];
REWRITE_TAC[VECTOR_ARITH` -- a + (a:real^N) =
vec 0`;VECTOR_ARITH` -- a + b = b - a:real^N `;
re_eqvl];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
EQ_TAC;
REWRITE_TAC[
SIN_POS_PI_LE];
MP_TAC (SPECL [`u - u:real^3 `;` v - u:real^3 `;` w - u:real^3 `;
` x - u:real^3 `]
AZIM_RANGE);
STRIP_TAC;
ASM_CASES_TAC `
azim (u - u) (v - u) (w - u) (x - u) <=
pi `;
ASM_REWRITE_TAC[];
ABBREV_TAC ` goc =
azim (u - u) (v - u) (w - u) (x - u) `;
STRIP_TAC;
SUBGOAL_THEN`
sin goc < &0 ` MP_TAC;
ONCE_REWRITE_TAC[
SIN_SUB_PERIODIC];
REWRITE_TAC[REAL_ARITH` -- a < &0 <=> &0 < a `];
MATCH_MP_TAC
SIN_POS_PI;
ASM_REWRITE_TAC[REAL_ARITH` a - b < b <=> a < &2 * b `;REAL_ARITH` &0 < a -
pi <=> ~( a <=
pi ) `];
DOWN;
REAL_ARITH_TAC]);;
let CONDS_IN_CONV2 = prove_by_refinement
(` &0 <= t2 /\ &0 <= t3 /\ ~( t2 = &0 /\ t3 = &0)
==> t2 / (t2 + t3) % v + t3 / (t2 + t3) % w
IN conv {v, w} `,
[STRIP_TAC;
SUBGOAL_THEN ` ~( t2 + t3 = &0 ) ` ASSUME_TAC;
DOWN_TAC;
REAL_ARITH_TAC;
REWRITE_TAC[Collect_geom.CONV_SET2;
IN_ELIM_THM];
EXISTS_TAC ` t2 / (t2 + t3 ) `;
EXISTS_TAC ` t3 / (t2 + t3 ) `;
CONJ_TAC;
MATCH_MP_TAC
REAL_LE_DIV;
DOWN_TAC THEN REAL_ARITH_TAC;
CONJ_TAC;
MATCH_MP_TAC
REAL_LE_DIV;
DOWN_TAC THEN REAL_ARITH_TAC;
ASM_SIMP_TAC[GSYM Geomdetail.SUM_TWO_RATIO]]);;
let PGSQVBL = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\ {v,w}
SUBSET V /\ x
IN FF ==>
aff_ge {
vec 0} {v,w}
SUBSET wedge_in_fan_ge x E `,
[REWRITE_TAC[
convex_local_fan];
STRIP_TAC;
DOWN;
FIRST_X_ASSUM NHANH;
REWRITE_TAC[
azim_in_fan2;
wedge_in_fan_ge2];
LET_TAC;
STRIP_TAC;
SUBGOAL_THEN `
FST (x:real^3 # real^3)
IN V /\
SND x
IN V ` MP_TAC;
MATCH_MP_TAC
LOCAL_FAN_IMP_IN_V;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2 (SPEC `
FST (x:real^3 # real^3 ) ` (GEN `v:real^3 `
LOFA_CARD_EE_V_1));
UNDISCH_TAC` (if
CARD (
EE (
FST x) E) > 1
then
azim (
vec 0) (
FST x) (
SND x) d
else &2 *
pi) <=
pi `;
UNDISCH_TAC` V
SUBSET
(if
CARD (
EE (
FST x) E) > 1
then
wedge_ge (
vec 0) (
FST x) (
SND x) d
else {x | T}) `;
PHA;
ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `];
ASSUME_TAC2 (SPEC `
FST (x:real^3 #real^3 ) ` (GEN `v:real^3 `
EXISTS_INVERSE_OF_V));
DOWN THEN STRIP_TAC;
MP_TAC2 (SPEC `
FST (x:real^3 # real^3) ` (GEN `v:real^3 `
LOFA_IMP_EE_TWO_ELMS));
DISCH_THEN SUBST_ALL_TAC;
SUBGOAL_THEN `
rho_node1 FF (
FST x) =
SND (x:real^3 # real^3) ` ASSUME_TAC;
MATCH_MP_TAC
DETER_RHO_NODE;
ASM_REWRITE_TAC[];
UNDISCH_TAC `
azim_cycle {
rho_node1 FF (
FST x), vv} (
vec 0) (
FST x) (
SND x) = d `;
ASM_REWRITE_TAC[
AZIM_CYCLE_TWO_POINT_SET];
MP_TAC2
LOCAL_FAN_RHO_NODE_PROS2;
REPEAT STRIP_TAC;
UNDISCH_TAC` vv:real^3
IN V `;
FIRST_X_ASSUM NHANH;
STRIP_TAC;
DOWN;
UNDISCH_TAC `
local_fan (V,E,
FF) `;
PHA;
NHANH
LOCAL_FAN_IN_FF_NOT_COLLINEAR;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2
LOCAL_FAN_IN_FF_NOT_COLLINEAR;
SUBGOAL_THEN ` conv {v,w:real^3}
SUBSET wedge_ge (
vec 0) (
FST x) (
SND x) d ` ASSUME_TAC;
SUBGOAL_THEN `
convex (
wedge_ge (
vec 0) (
FST x ) (
SND x ) d) ` ASSUME_TAC;
MATCH_MP_TAC
CONVEX_WEDGE_LE_PI;
ASM_SIMP_TAC[];
UNDISCH_TAC` ~
collinear {
vec 0, d,
FST (x:real^3 # real^3)}`;
SIMP_TAC[
INSERT_COMM];
MATCH_MP_TAC Geomdetail.CONVEX_IM_CONV2_SU;
ASM_REWRITE_TAC[SET_RULE` a
IN S /\ b
IN S <=> {a,b}
SUBSET S `];
MATCH_MP_TAC
SUBSET_TRANS;
EXISTS_TAC` V:real^3 -> bool `;
ASM_REWRITE_TAC[];
SUBGOAL_THEN `
DISJOINT {
vec 0} {v,w:real^3} ` MP_TAC;
MP_TAC2
LOFA_IMP_NOT_INCLUDE_VEC0;
UNDISCH_TAC` {v,w:real^3}
SUBSET V `;
SET_TAC[];
SIMP_TAC[Fan.AFF_GE_1_2;
SUBSET;
IN_ELIM_THM];
REPEAT STRIP_TAC;
ASM_CASES_TAC ` t2 = &0 /\ t3 = &0 `;
ASM_REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_MUL_RZERO;
VECTOR_ADD_LID;
wedge_ge;
IN_ELIM_THM];
REWRITE_TAC[
AZIM_SPEC_DEGENERATE;
AZIM_RANGE;
REAL_LE_REFL];
SUBGOAL_THEN ` (t2 / ( t2 + t3)) % v + ( t3 / ( t2 + t3 )) % w
IN conv {v,w:real^3}` ASSUME_TAC;
MATCH_MP_TAC
CONDS_IN_CONV2;
ASM_REWRITE_TAC[];
DOWN;
UNDISCH_TAC ` conv {v, w}
SUBSET wedge_ge (
vec 0) (
FST x) (
SND x) d `;
REWRITE_TAC[
SUBSET];
DISCH_THEN NHANH;
ABBREV_TAC `p = t2 / (t2 + t3) % v + t3 / (t2 + t3) % (w:real^3) `;
SUBGOAL_THEN ` x' =
t1 % (
vec 0) + (&0) % (
FST (x:real^3 # real^3)) + (t2 + t3 ) % (p:real^3) ` ASSUME_TAC;
ASM_REWRITE_TAC[
VECTOR_MUL_LZERO;
VECTOR_MUL_RZERO;
VECTOR_ADD_LID];
EXPAND_TAC "p";
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC];
MP_TAC2 (REAL_ARITH` &0 <= t2 /\ &0 <= t3 /\ ~( t2 = &0 /\ t3 = &0)
==> ~( t2 + t3 = &0) `);
SIMP_TAC[REAL_FIELD` ~( t = &0 ) ==> t * a / t = a `];
ASM_CASES_TAC ` collinear {vec 0, FST (x:real^3 # real^3), p}`;
DOWN;
ASSUME_TAC2 LOFA_IMP_NOT_INCLUDE_VEC0;
SUBGOAL_THEN` ~( FST (x:real^3 # real^3 ) = vec 0 ) ` ASSUME_TAC;
UNDISCH_TAC ` FST (x:real^3 # real^3 ) IN V `;
DOWN;
SET_TAC[];
ASM_SIMP_TAC[COLLINEAR_LEMMA_ALT];
STRIP_TAC;
SUBGOAL_THEN ` collinear {vec 0, FST (x:real^3 # real^3), x'}` MP_TAC;
SIMP_TAC[COLLINEAR_LEMMA_ALT];
DISJ2_TAC;
EXISTS_TAC ` (t2 + t3) * c `;
UNDISCH_TAC` x' = t1 % vec 0 + &0 % FST (x:real^3 # real^3) + (t2 + t3) % (p:real^3)`;
SIMP_TAC[];
ASM_REWRITE_TAC[];
DISCH_TAC;
VECTOR_ARITH_TAC;
UNDISCH_TAC` x' = t1 % vec 0 + t2 % v + t3 % (w:real^3) `;
DISCH_THEN (SUBST1_TAC o SYM);
SIMP_TAC[AZIM_DEGENERATE; wedge_ge; IN_ELIM_THM; AZIM_RANGE; REAL_LE_REFL];
REWRITE_TAC[wedge_ge; IN_ELIM_THM];
SUBGOAL_THEN` azim (vec 0) (FST x) (SND x) p = azim (vec 0) (FST x) (SND x) x'` SUBST1_TAC;
UNDISCH_TAC` x' = t1 % vec 0 + &0 % FST (x:real^3 # real^3) + (t2 + t3) % p`;
SIMP_TAC[];
DISCH_TAC;
MATCH_MP_TAC Topology.th1;
ASSUME_TAC2 (REAL_ARITH` &0 <= t2 /\ &0 <= t3 /\ ~( t2 = &0 /\ t3 = &0 ) ==> t2 + t3 > &0 `);
ASM_REWRITE_TAC[REAL_ADD_LID];
ASM_SIMP_TAC[Fan.th3a];
SIMP_TAC[]]);;
(* begin new lemma *)
(* =============== *)
(* =============== *)
(* ======================================================================== *)
let IN_AFF_LT_IMP_IN_CONV = prove_by_refinement
(`
DISJOINT {x:real^N} {b} /\ a
IN aff_lt {x} {b} ==> x
IN conv0 {a,b} `,
[IMP_TAC;
SIMP_TAC[
AFF_LT_1_1;
IN_ELIM_THM];
REPEAT STRIP_TAC;
DOWN;
ONCE_REWRITE_TAC[VECTOR_ARITH` a = x % b + y % c <=> x % b = a + (-- y) % c`];
ASSUME_TAC2 (REAL_ARITH` t2 < &0 /\
t1 + t2 = &1 ==> ~(
t1 = &0 )`);
ASM_SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE];
ASSUME_TAC2 (REAL_ARITH` t2 < &0 /\
t1 + t2 = &1 ==> &0 <
t1`);
REWRITE_TAC[
VECTOR_ADD_LDISTRIB;REAL_ARITH` &1 / a * b = b / a `;
VECTOR_MUL_ASSOC; Collect_geom.CONV0_SET2;
IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` &1 /
t1 `;
EXISTS_TAC ` ( -- t2 ) /
t1 `;
CONJ_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
CONJ_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `];
REWRITE_TAC[];
UNDISCH_TAC`
t1 + t2 = &1 `;
UNDISCH_TAC ` ~(
t1 = &0 ) `;
CONV_TAC REAL_FIELD]);;
let IN_CONV_LINE_SEPERATABLE = prove_by_refinement
(` x
IN conv0 {a,b:real^N} ==> aff {a,b} = aff_ge {x} {a}
UNION aff_ge {x} {b} `,
[REWRITE_TAC[Collect_geom.CONV0_SET2;
IN_ELIM_THM;
EXTENSION];
STRIP_TAC THEN GEN_TAC;
EQ_TAC;
REWRITE_TAC[Collect_geom.AFF_2POINTS_INTERPRET;
IN_ELIM_THM];
STRIP_TAC;
ASSUME_TAC2 (REAL_ARITH` ta + tb = &1 /\ a' + b' = &1 ==> ta <= a' \/ tb <= b' `);
DOWN_TAC;
DAO;
SPEC_TAC (`ta:real`,`ta:real`);
SPEC_TAC (`tb:real`,`tb:real`);
SPEC_TAC (`a':real`,`a':real`);
SPEC_TAC (`b':real`,`b':real`);
SPEC_TAC (`a:real^N`,`a:real^N`);
SPEC_TAC (`b:real^N`,`b:real^N`);
MATCH_MP_TAC (MESON[]`(! x y a b aa bb. P x y a b aa bb ==> P y x b a bb aa) /\
(! x y. L x y ==> L y x ) /\ (! x y a b aa bb. bb <= b /\ P x y a b aa bb ==> L x y ) ==> (! x y a b aa bb. (bb <= b \/ aa <= a ) /\ P x y a b aa bb ==> L x y ) `);
SIMP_TAC[
UNION_COMM;
VECTOR_ADD_SYM; REAL_ADD_SYM];
ONCE_REWRITE_TAC[
EQ_SYM_EQ];
SIMP_TAC[];
REPEAT STRIP_TAC;
REWRITE_TAC[
IN_UNION;
IN_ELIM_THM;
HALFLINE];
DISJ2_TAC;
EXISTS_TAC` tb - ( ta / a' ) * b' `;
CONJ_TAC;
SUBGOAL_THEN` ta / a' <= &1 ` ASSUME_TAC;
MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ta / a' * b' <= b' ` ASSUME_TAC;
REWRITE_TAC[REAL_ARITH` a * b <= b <=> &0 <= ( &1 - a ) * b `];
MATCH_MP_TAC
REAL_LE_MUL;
DOWN THEN DOWN THEN REAL_ARITH_TAC;
ASM_REAL_ARITH_TAC;
EXPAND_TAC "x";
EXPAND_TAC "x'";
REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC; VECTOR_ARITH` ( a + b % x ) + c % x = a + ( b + c ) % x `];
MATCH_MP_TAC (MESON[]` a = aa /\ b = bb ==> a % x + b % y = aa % x + bb % y `);
CONJ_TAC;
REPLICATE_TAC 4 DOWN;
REMOVE_TAC;
DOWN THEN DOWN;
REMOVE_TAC;
DOWN;
PHA;
CONV_TAC REAL_FIELD;
REPLICATE_TAC 4 DOWN;
REMOVE_TAC;
DOWN THEN DOWN;
REMOVE_TAC;
DOWN;
PHA;
CONV_TAC REAL_FIELD;
SPEC_TAC (`x':real^N`,`x':real^N`);
REWRITE_TAC[GSYM SUBSET; UNION_SUBSET];
SUBGOAL_THEN ` x:real^N IN aff {a,b}` ASSUME_TAC;
REWRITE_TAC[Collect_geom.AFF_2POINTS_INTERPRET; IN_ELIM_THM];
EXISTS_TAC` a':real`;
EXISTS_TAC `b':real`;
ASM_REWRITE_TAC[];
ASSUME_TAC (ISPECL [` a:real^N`;`b:real^N`] Planarity.POINT_IN_LINE);
ASSUME_TAC (ISPECL [` b:real^N`;`a:real^N`] Planarity.POINT_IN_LINE);
MP_TAC (ISPECL [`x:real^N`;` a:real^N`] HALFLINE_SUBSET_AFFINE_HULL);
MP_TAC (ISPECL [`x:real^N`;` b:real^N`] HALFLINE_SUBSET_AFFINE_HULL);
SUBGOAL_THEN ` aff {x,a:real^N} SUBSET aff {a,b} ` MP_TAC;
MATCH_MP_TAC S_SUBSET_IMP_AFF_S_TOO;
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
SUBGOAL_THEN ` aff {x,b:real^N} SUBSET aff {a,b} ` MP_TAC;
MATCH_MP_TAC S_SUBSET_IMP_AFF_S_TOO;
DOWN;
ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET];
ONCE_REWRITE_TAC[INSERT_COMM];
ASM_REWRITE_TAC[];
REWRITE_TAC[GSYM aff];
PHA;
SET_TAC[]]);;
let EMPTY_NOT_EXISTS_IN = SET_RULE` a = {} <=> ~(? x. x IN a ) `;;
let LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\ lunar (v,w) V E
==>
vec 0
IN conv0 {v,w} /\
(!u. u
IN V
DIFF {v, w} ==>
interior_angle1 (
vec 0)
FF u =
pi /\
rho_node1 FF u
IN aff {u,v,w} /\
ivs_rho_node1 FF u
IN aff {u,v,w})`,
[REWRITE_TAC[lunar];
STRIP_TAC;
SUBGOAL_THEN`
vec 0
IN conv0 {v,w:real^3} ` ASSUME_TAC;
MATCH_MP_TAC
FAN_SUB_NOT_EQ_COLL_IN_CONV0;
ASSUME_TAC2
CVLF_LF_F;
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[];
GEN_TAC THEN DISCH_TAC;
ABBREV_TAC` conclusion <=>
interior_angle1 (
vec 0)
FF u =
pi /\
rho_node1 FF u
IN aff {u, v, w} /\
ivs_rho_node1 FF u
IN aff {u, v, w} `;
SUBGOAL_THEN`
vec 0
IN aff {u:real^3,
vec 0} ` ASSUME_TAC;
ONCE_REWRITE_TAC[
INSERT_COMM];
ASM_REWRITE_TAC[Planarity.POINT_IN_LINE];
SUBGOAL_THEN` ~(aff {u,
vec 0}
INTER conv0 {v,w:real^3} = {})` ASSUME_TAC;
REWRITE_TAC[INTER_EQ_EM_EXPAND];
EXISTS_TAC`
vec 0:real^3 `;
ASM_REWRITE_TAC[];
ASM_CASES_TAC ` v
IN aff {u,
vec 0:real^3} `;
SUBGOAL_THEN`aff {u,
vec 0} = aff {v,w:real^3} ` ASSUME_TAC;
MATCH_MP_TAC
AFF2_DET_BY_TWO_POINTS;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET];
DOWN THEN DOWN;
SIMP_TAC[INTER_EQ_EM_EXPAND; GSYM
IN_INTER];
MESON_TAC[
AFF2_ITR_CONV0_IMP_SAME_ENDS];
SUBGOAL_THEN` u
IN aff {u:real^3,
vec 0} ` MP_TAC;
REWRITE_TAC[Planarity.POINT_IN_LINE];
ASM_REWRITE_TAC[];
UNDISCH_TAC`
vec 0
IN conv0 {v, w:real^3}`;
NHANH
IN_CONV_LINE_SEPERATABLE;
SIMP_TAC[
IN_UNION];
REPEAT STRIP_TAC;
SUBGOAL_THEN` ~( u:real^3
IN aff_ge {
vec 0} {v} )` MP_TAC;
MATCH_MP_TAC
FAN_IMP_NOT_IN_AFF_GE;
ASSUME_TAC2
CVLF_LF_F;
ASM_REWRITE_TAC[];
UNDISCH_TAC` {v,w:real^3}
SUBSET V `;
UNDISCH_TAC `u:real^3
IN V
DIFF {v,w} `;
SET_TAC[];
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ~( u
IN aff_ge {
vec 0} {w:real^3}) ` MP_TAC;
MATCH_MP_TAC
FAN_IMP_NOT_IN_AFF_GE;
ASSUME_TAC2
CVLF_LF_F;
ASM_REWRITE_TAC[];
UNDISCH_TAC` {v,w:real^3}
SUBSET V `;
UNDISCH_TAC `u:real^3
IN V
DIFF {v,w} `;
SET_TAC[];
ASM_REWRITE_TAC[];
SUBGOAL_THEN` {v,w:real^3}
INTER aff {u,
vec 0} = {} ` ASSUME_TAC;
ASM_REWRITE_TAC[Trigonometry2.INSERT_INTER_EMPTY];
DOWN THEN DOWN;
REWRITE_TAC[
EMPTY_NOT_EXISTS_IN];
MESON_TAC[
AFF2_ITR_CONV0_IMP_SAME_ENDS];
EXPAND_TAC "conclusion";
MATCH_MP_TAC OZQVSFF;
EXISTS_TAC ` v:real^3 `;
EXISTS_TAC ` w:real^3 `;
UNDISCH_TAC` {v,w:real^3} SUBSET V `;
UNDISCH_TAC` u IN V DIFF {v,w:real^3}`;
ASM_REWRITE_TAC[INSERT_SUBSET; IN_DIFF];
SIMP_TAC[];
STRIP_TAC THEN STRIP_TAC;
CONJ_TAC;
REWRITE_TAC[plane];
SUBGOAL_THEN` ~ collinear {u,v,w:real^3} ` ASSUME_TAC;
ASM_SIMP_TAC[Collect_geom.NOT_TWO_EQ_IMP_COL_EQUAVALENT];
UNDISCH_TAC` vec 0 IN conv0 {v, w:real^3}`;
NHANH IN_CONV_LINE_SEPERATABLE;
SIMP_TAC[];
STRIP_TAC;
REWRITE_TAC[IN_UNION; DE_MORGAN_THM];
CONJ_TAC;
MATCH_MP_TAC FAN_IMP_NOT_IN_AFF_GE;
ASSUME_TAC2 CVLF_LF_F;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~( u:real^3 IN {v,w})`;
ASM_REWRITE_TAC[INSERT_SUBSET; IN_INSERT];
MESON_TAC[];
MATCH_MP_TAC FAN_IMP_NOT_IN_AFF_GE;
ASSUME_TAC2 CVLF_LF_F;
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~( u:real^3 IN {v,w})`;
ASM_REWRITE_TAC[INSERT_SUBSET; IN_INSERT];
MESON_TAC[];
DOWN;
REWRITE_TAC[aff];
MESON_TAC[];
CONJ_TAC;
MP_TAC (ISPECL [` v:real^3`;` w:real^3`] (GEN_ALL CONV02_SUBSET_AFF2));
SUBGOAL_THEN` aff {v,w} SUBSET aff {u,v,w:real^3}` ASSUME_TAC;
REWRITE_TAC[aff];
MATCH_MP_TAC HULL_MONO;
REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET];
REWRITE_TAC[EMPTY_SUBSET];
STRIP_TAC;
CONJ_TAC;
UNDISCH_TAC` aff {v, w} SUBSET aff {u, v, w:real^3}`;
REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
DOWN;
REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
REWRITE_TAC[aff];
MESON_TAC[INSERT_COMM; Trigonometry2.IN_P_HULL_INSERT];
ASM_SIMP_TAC[INSERT_COMM]]);;
let P_SET3_IMP_SET2 =
MESON[INSERT_INSERT]` (! (a:A) b c. P ({a,b,c}) ) ==> (! (a:A) b. (P {a,b})) `;;
let CONV2_SUBSET_AFF_GE_2S =
MATCH_MP P_SET3_IMP_SET2 (GEN_ALL CONV3_SUBSET_AFF_GE_3S);;
(* ------------------------------------------------------------------------- *)
(* Search (automatically updates) *)
(* ------------------------------------------------------------------------- *)
let full t = mk_comb(mk_var("<full term>",W mk_fun_ty (type_of t)),t);;
(* very rough measure of the size of a printed term *)
let rec term_length tm = match tm with
| Abs(s,x) -> 1 + term_length x
| Comb(s,x) -> if ((s = `NUMERAL`) or (s = `DECIMAL`)) then 2
else ( (term_length s) + term_length x)
| _ -> 1;;
let sortlength_thml thml =
let ltml = map
(function (s,t) as r -> (term_length (concl t),r)) thml in
let stml = sort (fun (a,_) (b,_) -> (a < b)) ltml in
map snd stml;;
let search_thml =
let rec immediatesublist l1 l2 =
match (l1,l2) with
[],_ -> true
| _,[] -> false
| (h1::t1,h2::t2) -> h1 = h2 & immediatesublist t1 t2 in
let rec sublist l1 l2 =
match (l1,l2) with
[],_ -> true
| _,[] -> false
| (h1::t1,h2::t2) -> immediatesublist l1 l2 or sublist l1 t2 in
let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th) in
let exists_fullterm_satisfying p (n,th) = p (concl th) in
let name_contains s (n,th) = sublist (explode s) (explode n) in
let rec filterpred tm =
match tm with
Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
| Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
| Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
| Comb(Var("<full term>",_),pat) -> exists_fullterm_satisfying (can (term_match [] pat))
| pat -> exists_subterm_satisfying (can (term_match [] pat)) in
fun pats thml -> update_database ();
if (pats = []) then failwith "keywords: omit, name, exactly, full" else
(itlist (filter o filterpred) pats thml);;
let (PAT_TAC:term list -> (string * thm) -> tactic) =
fun pat sth -> if (search_thml pat [sth] = []) then NO_TAC else ALL_TAC;;
let (FIRST_PAT_ASSUM: term list -> thm_tactic -> tactic) =
fun pat ttac gl -> tryfind (fun sth -> (PAT_TAC pat sth THEN ttac (snd sth)) gl) (goal_asms gl);;
let (FIRST_PAT_X_ASSUM:term list -> thm_tactic -> tactic) =
fun pat ttac ->
FIRST_PAT_ASSUM pat (fun th -> UNDISCH_THEN (concl th) ttac);;
(* ================================================================== *)
let LOFA_IMP_BIJ_FF_V = MESON[Wrgcvdr_cizmrrh.BIJ_BETWEEN_FF_AND_V]
` local_fan (V,E,FF) ==> BIJ (\x. FST x) FF V `;;
let HALF_CIRCULAR_IN_PLANE = prove_by_refinement
(` (
convex_local_fan (V,E,
FF) /\ lunar (v,w) V E ) /\
n <
CARD V /\ w =
ITER n (
rho_node1 FF) v
==> {
ITER l (
rho_node1 FF) v | l <= n }
SUBSET aff {
vec 0, v,
rho_node1 FF v}`,
[NHANH
LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
REWRITE_TAC[
SUBSET;
IN_ELIM_THM; lunar];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC ` l <= n:num`;
SPEC_TAC (`l:num`,`l:num`);
INDUCT_TAC;
REWRITE_TAC[
ITER];
DISCH_TAC;
MP_TAC (ISPECL [`affine: (real^3 -> bool) -> bool `;
` {
vec 0, v,
rho_node1 FF v } `]
HULL_SUBSET);
REWRITE_TAC[aff;
SUBSET];
DISCH_THEN MATCH_MP_TAC;
REWRITE_TAC[
IN_INSERT];
NHANH (ARITH_RULE` SUC a <= b ==> a <= b `);
FIRST_X_ASSUM NHANH;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC`
ITER l' (
rho_node1 FF) v `));
ASM_CASES_TAC` l' = 0 `;
ASM_REWRITE_TAC[
ITER];
REPEAT STRIP_TAC;
MP_TAC (ISPECL [`affine: (real^3 -> bool) -> bool `;
` {
vec 0, v,
rho_node1 FF v } `]
HULL_SUBSET);
REWRITE_TAC[aff;
SUBSET];
DISCH_THEN MATCH_MP_TAC;
REWRITE_TAC[
IN_INSERT];
ANTS_TAC;
ASSUME_TAC2
CVX_LO_IMP_LO;
ASSUME_TAC2
LOFA_IMP_CARD_FF_V_EQ;
MP_TAC2 (SPEC `n:num` (GEN `l:num`
LOFA_IMP_DIS_ELMS));
UNDISCH_TAC` !x. x
IN {v, w} ==> x
IN (V:real^3 -> bool) `;
SIMP_TAC[
IN_INSERT];
DISCH_THEN (MP_TAC o (SPEC`l': num`));
ANTS_TAC;
UNDISCH_TAC` SUC l' <= n `;
ARITH_TAC;
MP_TAC2 (SPEC `l':num` (GEN `l:num`
LOFA_IMP_DIS_ELMS));
CONJ_TAC;
UNDISCH_TAC` !x. x
IN {v, w} ==> x
IN (V:real^3 -> bool) `;
SIMP_TAC[
IN_INSERT];
UNDISCH_TAC` n <
CARD (V:real^3 -> bool) `;
UNDISCH_TAC` l' <= n:num `;
ARITH_TAC;
DISCH_THEN (MP_TAC o (SPEC`0`));
ANTS_TAC;
UNDISCH_TAC` ~( l' = 0)`;
ARITH_TAC;
ASM_SIMP_TAC[
IN_DIFF;
IN_INSERT;
NOT_IN_EMPTY; DE_MORGAN_THM;
ITER];
REPEAT STRIP_TAC;
MP_TAC2
LOCAL_FAN_ORBIT_MAP_VITER;
DISCH_THEN MATCH_MP_TAC;
UNDISCH_TAC ` !x. x
IN {v:real^3, w} ==> x
IN V`;
SIMP_TAC[
IN_INSERT];
SUBGOAL_THEN` aff {
ITER l' (
rho_node1 FF) v, v, w}
SUBSET aff {
vec 0, v,
rho_node1 FF v}` MP_TAC;
MATCH_MP_TAC
S_SUBSET_IMP_AFF_S_TOO;
ASM_REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET];
CONJ_TAC;
MESON_TAC[
FIRST_IN_AFF;
INSERT_COMM];
SUBGOAL_THEN` aff {
vec 0, v:real^3}
SUBSET aff {
vec 0, v,
rho_node1 FF v }` MP_TAC;
REWRITE_TAC[aff];
MATCH_MP_TAC
HULL_MONO;
SET_TAC[];
REWRITE_TAC[
SUBSET];
DISCH_THEN MATCH_MP_TAC;
UNDISCH_TAC `
vec 0
IN conv0 {v,w:real^3}`;
NHANH
IN_CONV0_IMP_AFF_EQ;
SIMP_TAC[
INSERT_COMM];
STRIP_TAC;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[Planarity.POINT_IN_LINE1];
SIMP_TAC[
SUBSET;
ITER]]);;
let LOFA_IMP_DIS_ELMS2 =
MESON[LOFA_IMP_DIS_ELMS]` local_fan (V,E,FF) /\ v IN V
==> (!i l. i < l /\ l < CARD FF
==> ~(ITER l (rho_node1 FF) v = ITER i (rho_node1 FF) v))`;;
REWRITE_TAC[IN_ELIM_THM];
CONJ_TAC;
EXISTS_TAC ` 0`;
REWRITE_TAC[ITER; LE_0];
FIRST_ASSUM (MP_TAC o (SPECL [`0`;` n:num`]));
FIRST_ASSUM (MP_TAC o (SPECL [`0`;` n + 1`]));
PHA;
ASM_REWRITE_TAC[GSYM ADD1];
IMP_TAC;
ANTS_TAC;
REWRITE_TAC[LT_0];
ASSUME_TAC2 LOFA_IMP_CARD_FF_V_EQ;
ASM_REWRITE_TAC[];
SIMP_TAC[ITER];
ASSUME_TAC2 LOFA_IMP_CARD_FF_V_EQ;
STRIP_TAC;
ANTS_TAC;
UNDISCH_TAC` ~( n = 0 ) `;
UNDISCH_TAC` SUC n < CARD (V:real^3 -> bool) `;
ASM_REWRITE_TAC[];
ARITH_TAC;
SIMP_TAC[];
STRIP_TAC;
UNDISCH_TAC` n < m /\ m < CARD (V:real^3 -> bool) /\ m <= l
==> azim (vec 0) e v (ITER n (rho_node1 FF) v) <
azim (vec 0) e v (ITER m (rho_node1 FF) v) ` ;
ANTS_TAC;
REPLICATE_TAC 4 DOWN THEN PHA;
ARITH_TAC;
ASSUME_TAC2 SEQUENCE_OF_RHO_NODE_IS_SUC;
FIRST_X_ASSUM (MP_TAC o (SPECL [` ITER m (rho_node1 FF) v`;` m:num`]));
REWRITE_TAC[];
ANTS_TAC;
DOWN;
ARITH_TAC;
DISCH_THEN (MP_TAC o (SPEC ` v:real^3 `));
ANTS_TAC;
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC `0`;
REWRITE_TAC[ITER; LE_0];
ASM_CASES_TAC ` m = 0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
REWRITE_TAC[ITER; AZIM_REFL];
MP_TAC (SPECL [` vec 0:real^3`;` e:real^3 `;` v:real^3 `;` rho_node1 FF v `] AZIM_RANGE);
REAL_ARITH_TAC;
ASSUME_TAC2 LOFA_IMP_DIS_ELMS2;
ANTS_TAC;
FIRST_X_ASSUM (MP_TAC o (SPECL [`0` ;` m:num `]));
PHA;
ANTS_TAC;
REPLICATE_TAC 3 DOWN THEN PHA;
ASSUME_TAC2 LOFA_IMP_CARD_FF_V_EQ;
ASM_REWRITE_TAC[];
ARITH_TAC;
SIMP_TAC[ITER];
ANTS_TAC;
FIRST_X_ASSUM (MP_TAC o (SPECL [`0` ;`SUC m`]));
PHA;
ANTS_TAC;
ASSUME_TAC2 LOFA_IMP_CARD_FF_V_EQ;
ASM_REWRITE_TAC[];
ARITH_TAC;
SIMP_TAC[ITER];
REWRITE_TAC[ITER];
REAL_ARITH_TAC]);;
let LOFA_IMP_DIS_ELMS23 = MESON[LOFA_IMP_CARD_FF_V_EQ; LOFA_IMP_DIS_ELMS2]
` local_fan (V,E,FF) /\ v IN V
==> (!i l.
i < l /\ l < CARD V
==> ~(ITER l (rho_node1 FF) v = ITER i (rho_node1 FF) v))`;;
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` n:num`;
ASM_REWRITE_TAC[SUBSET; IN_ELIM_THM];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
MP_TAC2 HALF_CIRCULAR_IN_PLANE;
SWITCH_TAC ` w = ITER n (rho_node1 FF) v `;
ASM_SIMP_TAC[convex_local_fan; lunar];
ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
EXPAND_TAC "w";
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n:num`;
ASM_REWRITE_TAC[];
ABBREV_TAC` U = {ITER l (rho_node1 FF) v | l <= n} `;
ABBREV_TAC` P = aff {vec 0, v, rho_node1 FF v} `;
ABBREV_TAC` e = v cross rho_node1 FF v `;
STRIP_TAC;
MP_TAC2 (SPEC `n:num` (GEN `l:num` FIRST_AZIM_CYCLE_EQ_RHO_NODE));
EXPAND_TAC "P";
REWRITE_TAC[plane; FIRST_IN_AFF; aff];
EXISTS_TAC` vec 0:real^3 `;
EXISTS_TAC` v:real^3`;
EXISTS_TAC` rho_node1 FF v `;
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
UNDISCH_TAC` v:real^3 IN V`;
FIRST_X_ASSUM NHANH;
SIMP_TAC[];
MP_TAC2 (SPEC `n:num ` (GEN ` l:num` RHO_NODE1_MONO_WITH_AZIM));
EXPAND_TAC "P";
REWRITE_TAC[plane; FIRST_IN_AFF];
EXISTS_TAC` vec 0:real^3 `;
EXISTS_TAC` v:real^3 `;
EXISTS_TAC ` rho_node1 FF v `;
REWRITE_TAC[aff];
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
ASM_SIMP_TAC[];
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC o (SPECL [`0`;` l:num`]));
DOWN;
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` l < n:num`;
UNDISCH_TAC` n < CARD (V:real^3 -> bool) `;
ARITH_TAC;
FIRST_ASSUM (ASSUME_TAC o (SPECL [` l:num`;`n:num`]));
DOWN;
ANTS_TAC;
ASM_REWRITE_TAC[LE_REFL];
REWRITE_TAC[ITER; AZIM_REFL];
SUBGOAL_THEN` azim (vec 0) e v (ITER n (rho_node1 FF) v) = pi <=>
v IN aff_lt {vec 0, e:real^3} {ITER n (rho_node1 FF) v}` ASSUME_TAC;
MATCH_MP_TAC AZIM_EQ_PI;
UNDISCH_TAC` vec 0 IN conv0 {v,w:real^3}`;
REWRITE_TAC[Geomdetail.CONV0_SET2; IN_ELIM_THM];
NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 ) `);
REWRITE_TAC[VECTOR_ARITH` vec 0 = a + b <=> b = -- a `];
STRIP_TAC;
SWITCH_TAC` w = ITER n (rho_node1 FF) v`;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` collinear {vec 0, &1 % e, b % w} <=> collinear {vec 0, e, w:real^3}` ASSUME_TAC;
MATCH_MP_TAC COLLINEAR_SCALE_ALL;
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[GSYM VECTOR_MUL_LNEG];
SUBGOAL_THEN` collinear {vec 0, &1 % e, ( -- a ) % v} <=> collinear {vec 0, e, v:real^3}` SUBST1_TAC;
MATCH_MP_TAC COLLINEAR_SCALE_ALL;
UNDISCH_TAC` ~( a = &0 )`;
REAL_ARITH_TAC;
REWRITE_TAC[];
EXPAND_TAC "e";
ONCE_REWRITE_TAC[SET_RULE` {a,b} = {b,a} `];
ONCE_REWRITE_TAC[GSYM COLL_IFF_COLL_CROSS];
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
UNDISCH_TAC` v:real^3 IN V`;
FIRST_X_ASSUM NHANH;
SIMP_TAC[];
SUBGOAL_THEN ` azim (vec 0) e v (ITER n (rho_node1 FF) v) = pi ` ASSUME_TAC;
FIRST_X_ASSUM SUBST1_TAC;
SUBGOAL_THEN` ~( aff {vec 0, e:real^3} INTER conv0 {w,v} = {} ) ` MP_TAC;
REWRITE_TAC[EMPTY_NOT_EXISTS_IN];
EXISTS_TAC` vec 0:real^3 `;
SWITCH_TAC` w = ITER n (rho_node1 FF) v `;
ASM_SIMP_TAC[IN_INTER; Planarity.POINT_IN_LINE; INSERT_COMM];
ASM_REWRITE_TAC[];
MATCH_MP_TAC Ldurdpn.AFF_CONV0_IN_AFF_LT;
SWITCH_TAC` w = ITER n (rho_node1 FF ) v `;
UNDISCH_TAC` vec 0 IN conv0 {v,w:real^3}`;
REWRITE_TAC[Geomdetail.CONV0_SET2; IN_ELIM_THM];
NHANH (REAL_ARITH` &0 < a ==> ~( a = &0 ) `);
REWRITE_TAC[VECTOR_ARITH` vec 0 = a + b <=> b = -- a `];
STRIP_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` collinear {vec 0, &1 % e, b % w} <=> collinear {vec 0, e, w:real^3}` ASSUME_TAC;
MATCH_MP_TAC COLLINEAR_SCALE_ALL;
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[GSYM VECTOR_MUL_LNEG];
SUBGOAL_THEN` collinear {vec 0, &1 % e, ( -- a ) % v} <=> collinear {vec 0, e, v:real^3}` SUBST1_TAC;
MATCH_MP_TAC COLLINEAR_SCALE_ALL;
UNDISCH_TAC` ~( a = &0 )`;
REAL_ARITH_TAC;
REWRITE_TAC[];
EXPAND_TAC "e";
ONCE_REWRITE_TAC[SET_RULE` {a,b} = {b,a} `];
ONCE_REWRITE_TAC[GSYM COLL_IFF_COLL_CROSS];
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
UNDISCH_TAC` v:real^3 IN V`;
FIRST_X_ASSUM NHANH;
SIMP_TAC[];
ASM_REWRITE_TAC[];
SWITCH_TAC` w = ITER n (rho_node1 FF) v `;
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
MP_TAC2 (SPEC ` azim (vec 0) e v (ITER l (rho_node1 FF) v) ` SIN_POS_PI);
MP_TAC (SPECL [`e:real^3`;`v:real^3`;` ITER l (rho_node1 FF) v `] Trigonometry2.JBDNJJB);
REWRITE_TAC[re_eqvl];
STRIP_TAC;
SUBGOAL_THEN` ITER l (rho_node1 FF) v IN aff {vec 0, v, rho_node1 FF v}` MP_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` U SUBSET (P:real^3 -> bool) `;
REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC `l:num`;
ASM_REWRITE_TAC[];
UNDISCH_TAC` l < n:num`;
ARITH_TAC;
REWRITE_TAC[aff; AFFINE_HULL_3; IN_ELIM_THM];
STRIP_TAC;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[CROSS_TRIPLE];
REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_0; CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
ASM_REWRITE_TAC[DOT_LMUL];
SUBGOAL_THEN` &0 < e dot (e:real^3)` ASSUME_TAC;
REWRITE_TAC[DOT_POS_LT];
EXPAND_TAC "e";
REWRITE_TAC[CROSS_EQ_0];
MATCH_MP_TAC LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[REAL_LT_MUL_EQ];
MP_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
NHANH Fan.th3a;
SIMP_TAC[AFF_GT_2_1; IN_ELIM_THM];
REPEAT STRIP_TAC;
EXISTS_TAC` u:real `;
EXISTS_TAC` v':real `;
EXISTS_TAC` w':real`;
ASM_REWRITE_TAC[];
VECTOR_ARITH_TAC]);;
REWRITE_TAC[lemma_in_orbit_iter];
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
DOWN;
ASM_CASES_TAC` n = 0 `;
ASM_REWRITE_TAC[ITER];
ASM_REWRITE_TAC[];
ABBREV_TAC` cc = CARD (V:A -> bool) `;
ASSUME_TAC2 (ARITH_RULE` n < cc ==> cc = (cc - n ) + (n:num) `);
ABBREV_TAC ` m = cc - (n:num)`;
ASM_REWRITE_TAC[GSYM ITER_ADD];
SUBGOAL_THEN` 0 < m ` MP_TAC;
UNDISCH_TAC` n < cc:num`;
EXPAND_TAC "m";
ARITH_TAC;
PHA;
NHANH Lvducxu.ITER_CYCLIC_ORBIT;
SUBGOAL_THEN` ITER n f (v:A) IN V ` MP_TAC;
EXPAND_TAC "V";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC `n:num`;
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[];
REPEAT STRIP_TAC;
SUBGOAL_THEN` CARD (V:A -> bool) <= m ` MP_TAC;
FIRST_X_ASSUM SUBST1_TAC;
REWRITE_TAC[Wrgcvdr_cizmrrh.CARD_LE_K_OF_SET_K_FIRST_ELMS];
ASM_REWRITE_TAC[];
UNDISCH_TAC` ~ ( n = 0 ) `;
ARITH_TAC]);;
let collinear_fan22 =
MESON[Fan.collinear_fan]`collinear {x, v,u} <=> u IN aff {x, v} \/ (x = v)`;;
(* aff_gt X Y SUBSET aff (X UNION Y) *)
(* ================================= *)
let AFF_GT_SUB_AFF_UNION =
REWRITE_RULE[SUBSET_REFL; DIFF_EQ_EMPTY; AFF_GT_EQ_AFFINE_HULL; GSYM aff]
(SPEC `Y:real^N -> bool` AFF_GT_MONO);;
ASM_SIMP_TAC[INSERT_COMM];
ASM_REWRITE_TAC[ARITH_RULE` a + 1 < b <=> a < b /\ ~(a + 1 = b )`];
STRIP_TAC;
SUBGOAL_THEN` {ITER l (rho_node1 FF) v | l <= i + 1} SUBSET
aff {vec 0, v, rho_node1 FF v}` ASSUME_TAC;
REWRITE_TAC[ARITH_RULE` a <= b + 1 <=> a = b + 1 \/ a <= b `;
SET_RULE` { f x | x = a \/ Q x } = f a INSERT { f x | Q x }`; INSERT_SUBSET];
ASM_REWRITE_TAC[];
MP_TAC (ISPECL [`{vec 0,v:real^3}`;`{rho_node1 FF v}`]
(GEN_ALL AFF_GT_SUB_AFF_UNION));
REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c}`; SUBSET];
DISCH_THEN MATCH_MP_TAC;
FIRST_X_ASSUM ACCEPT_TAC;
ABBREV_TAC` P = aff {vec 0, v, rho_node1 FF v} `;
ABBREV_TAC` U = {ITER l (rho_node1 FF) v | l <= i + 1} `;
ABBREV_TAC` l = i + 1 `;
ABBREV_TAC ` e = v cross rho_node1 FF v `;
MP_TAC2 RHO_NODE1_MONO_WITH_AZIM;
UNDISCH_TAC` lunar (v:real^3,w) V E `;
REWRITE_TAC[lunar; INSERT_SUBSET];
STRIP_TAC;
ASSUME_TAC2 CVX_LO_IMP_LO;
ASM_REWRITE_TAC[plane];
EXPAND_TAC "P";
REWRITE_TAC[FIRST_IN_AFF];
EXISTS_TAC `vec 0:real^3 `;
EXISTS_TAC` v:real^3 `;
EXISTS_TAC ` rho_node1 FF v `;
REWRITE_TAC[aff];
MP_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC o (SPECL [`i:num`;` i + 1`]));
DOWN;
ANTS_TAC;
EXPAND_TAC "l";
REWRITE_TAC[ARITH_RULE` a < a + 1`; LE_REFL; ARITH_RULE` a + 1 < b <=> a < b /\ ~( a + 1 = b )`];
ASM_REWRITE_TAC[];
SUBGOAL_THEN` azim (vec 0) e v (ITER i (rho_node1 FF) v) = pi` SUBST1_TAC;
MATCH_MP_TAC IN_CONV0_IMP_AZIM_PI;
MP_TAC2 LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
ASM_SIMP_TAC[];
EXPAND_TAC "e";
STRIP_TAC;
REWRITE_TAC[GSYM COLL_IFF_COLL_CROSS];
MP_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
UNDISCH_TAC `lunar (v:real^3,w) V E `;
ASM_SIMP_TAC[lunar; INSERT_SUBSET; CVX_LO_IMP_LO];
REWRITE_TAC[GSYM SIN_AZIM_NEG_PI_LT];
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `;
NHANH Fan.th3a;
NHANH AFF_GT_2_1;
STRIP_TAC;
UNDISCH_TAC` ITER l (rho_node1 FF) v IN aff_gt {vec 0, v} {rho_node1 FF v} `;
ASM_REWRITE_TAC[IN_ELIM_THM];
STRIP_TAC;
MP_TAC (
SPECL [`e:real^3`;` v:real^3`;` ITER l (rho_node1 FF) v`] Trigonometry2.JBDNJJB);
REWRITE_TAC[re_eqvl];
STRIP_TAC;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[CROSS_TRIPLE];
ASM_REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_REFL; CROSS_0; VECTOR_MUL_RZERO; VECTOR_ADD_LID; DOT_LMUL];
SUBGOAL_THEN ` &0 < e dot (e:real^3) ` ASSUME_TAC;
REWRITE_TAC[DOT_POS_LT];
UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `;
ASM_SIMP_TAC[GSYM CROSS_EQ_0];
ASM_SIMP_TAC[REAL_ARITH` a * b * c < &0 <=> &0 < a * ( --b ) * c `; REAL_LT_MUL_EQ];
UNDISCH_TAC` &0 < t3 `;
REAL_ARITH_TAC]);;
let FOR_AFF_GT_NOT_INTERSECTION = prove_by_refinement
(`a1 % (x:real^N) + b1 % y + t % u = a2 % x + b2 % y + tt % v /\
&0 < t /\
&0 < tt /\
a1 + b1 + t = &1 /\
a2 + b2 + tt = &1
==> u = (a2 - a1) / t % x + (b2 - b1) / t % y + tt / t % v /\
(a2 - a1) / t + (b2 - b1) / t + tt / t = &1 /\
&0 < tt / t`,
[REWRITE_TAC[VECTOR_ARITH`a + (b:real^N) = c <=> b = c - a `;
REAL_ARITH` a / t + b / t = ( a + b ) / t`];
NHANH_PAT`\x. x ==> y`
REAL_POS_NZ;
STRIP_TAC;
UNDISCH_TAC` t % u = (a2 % x + b2 % y + tt % v) - a1 % x - b1 % (y:real^N)`;
ASM_SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE; REAL_ARITH` ( a - b ) / c = a / c - b / c`;
VECTOR_SUB_LDISTRIB;
VECTOR_ADD_LDISTRIB;
VECTOR_SUB_RDISTRIB];
STRIP_TAC;
CONJ_TAC;
VECTOR_ARITH_TAC;
CONJ_TAC;
UNDISCH_TAC` a1 + b1 + t = &1 `;
UNDISCH_TAC` a2 + b2 + tt = &1 `;
SIMP_TAC[ARITH_RULE` a + b = c <=> a = c - b `];
REWRITE_TAC[REAL_POLY_CONV`&1 - (b2 + tt) - (&1 - (b1 + t)) + b2 - b1 + tt`];
REPEAT STRIP_TAC;
UNDISCH_TAC` &0 < t `;
CONV_TAC REAL_FIELD;
MATCH_MP_TAC
REAL_LT_DIV;
ASM_REWRITE_TAC[]]);;
let AFF_GT_SAME_WITH_ENDS = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\ lunar (v,w) V E
==> aff_gt {
vec 0, v} {
rho_node1 FF w} = aff_gt {
vec 0, w} {
rho_node1 FF w }`,
[NHANH
LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
NHANH
NOT_COLL_RHONODE_SND_POINT;
REWRITE_TAC[lunar;
INSERT_SUBSET;
convex_local_fan];
STRIP_TAC;
SUBGOAL_THEN` ~
collinear {
vec 0, w,
rho_node1 FF w }` ASSUME_TAC;
MATCH_MP_TAC
LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` aff_gt {
vec 0, v} {
rho_node1 FF w} = aff_gt {
vec 0, v, w} {
rho_node1 FF w}` SUBST1_TAC;
MATCH_MP_TAC
CONV0_AFF_GT_EQ;
UNDISCH_TAC` ~collinear {
vec 0, v,
rho_node1 FF w} `;
ASM_SIMP_TAC[
INSERT_COMM];
SUBGOAL_THEN` aff_gt {
vec 0, w} {
rho_node1 FF w} = aff_gt {
vec 0, w, v} {
rho_node1 FF w}` SUBST1_TAC;
MATCH_MP_TAC
CONV0_AFF_GT_EQ;
UNDISCH_TAC` ~collinear {
vec 0, w,
rho_node1 FF w} `;
ASM_SIMP_TAC[
INSERT_COMM];
SIMP_TAC[
INSERT_COMM]]);;
let CRAZY_THMMM = prove_by_refinement
(` w:real^N
IN aff {b,c} /\ z
IN aff_gt {b,c} {w}
==> z
IN aff {b,c} `,
[ASM_CASES_TAC`
DISJOINT {b,c} {w:real^N}`;
ASM_SIMP_TAC[
AFF_GT_2_1;
IN_ELIM_THM;
AFF2];
STRIP_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC`
t1 + t3 * t `;
UNDISCH_TAC`
t1 + t2 + t3 = &1 `;
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `];
DISCH_TAC;
VECTOR_ARITH_TAC;
DOWN;
REWRITE_TAC[SET_RULE`~DISJOINT {b, c} {w} <=> w = b \/ w = c`];
STRIP_TAC;
ASM_REWRITE_TAC[];
MP_TAC (SPECL [`{b,c:real^N}`;` {b:real^N}`] (GEN_ALL (REWRITE_RULE[
SUBSET_REFL;
DIFF_EQ_EMPTY;
AFF_GT_EQ_AFFINE_HULL] (SPEC `Y:real^N -> bool`
AFF_GT_MONO))));
REWRITE_TAC[aff; SET_RULE` {a,b}
UNION {a} = {a,b}`];
SET_TAC[];
ASM_REWRITE_TAC[];
MP_TAC (SPECL [`{b,c:real^N}`;` {c:real^N}`] (GEN_ALL (REWRITE_RULE[
SUBSET_REFL;
DIFF_EQ_EMPTY;
AFF_GT_EQ_AFFINE_HULL] (SPEC `Y:real^N -> bool`
AFF_GT_MONO))));
REWRITE_TAC[aff; SET_RULE` {a,b}
UNION {b} = {a,b}`];
SET_TAC[]]);;
let USEFULL_THHM = prove_by_refinement
(`(z:real^N)
IN aff {b, c} /\ z
IN aff_gt {b, c} {w} ==> w
IN aff {b, c}`,
[ASM_CASES_TAC`
DISJOINT {b,c} {w:real^N}`;
ASM_SIMP_TAC[
AFF_GT_2_1;
IN_ELIM_THM;
AFF2];
STRIP_TAC;
ASM_REWRITE_TAC[];
DOWN;
ASM_REWRITE_TAC[VECTOR_ARITH` a = x + y + c % z <=> c % z = a - x - y`];
ASSUME_TAC2 (REAL_ARITH` &0 < t3 ==> ~(t3 = &0) `);
ASM_SIMP_TAC[Ldurdpn.VECTOR_SCALE_CHANGE;
VECTOR_ADD_LDISTRIB;
VECTOR_SUB_LDISTRIB;
VECTOR_MUL_ASSOC; REAL_ARITH` &1 / a * b = b / a `];
STRIP_TAC;
EXISTS_TAC` t / t3 -
t1 / t3 `;
UNDISCH_TAC`
t1 + t2 + t3 = &1 `;
SIMP_TAC[REAL_ARITH` a + b = &1 <=> a = &1 - b `; REAL_ARITH` (a - ( b + c )) / t = a / t - b / t - c / t `];
ASM_SIMP_TAC[REAL_FIELD` ~( a = &0 ) ==> a / a = &1 `];
DISCH_TAC;
VECTOR_ARITH_TAC;
DOWN;
REWRITE_TAC[SET_RULE` ~
DISJOINT {a,b} {x} <=> x = a \/ x = b `];
MESON_TAC[Planarity.POINT_IN_LINE; Planarity.POINT_IN_LINE1]]);;
let AFF_GT_IN_IMP_SUBSET = prove_by_refinement
(`~collinear {x, y, z:real^N} /\ a
IN aff_gt {x, y} {z}
==> aff_gt {x,y} {a}
SUBSET aff_gt {x,y} {z}`,
[NHANH
COLL_IN_AFF_GT_TOO;
NHANH Fan.th3a;
STRIP_TAC;
UNDISCH_TAC` a
IN aff_gt {x,y} {z:real^N} `;
ASM_SIMP_TAC[
AFF_GT_2_1;
IN_ELIM_THM;
SUBSET];
REPEAT STRIP_TAC;
ASM_REWRITE_TAC[];
EXISTS_TAC`t1' + t3' *
t1 `;
EXISTS_TAC` t2' + t3' * t2 `;
EXISTS_TAC` t3' * t3 `;
CONJ_TAC;
MATCH_MP_TAC
REAL_LT_MUL;
ASM_REWRITE_TAC[];
CONJ_TAC;
ASM_REWRITE_TAC[REAL_ARITH` (t1' + t3' *
t1) + (t2' + t3' * t2) + t3' * t3
= t1' + t2' + t3' * (
t1 + t2 + t3 ) `;
REAL_MUL_RID];
VECTOR_ARITH_TAC]);;
let FOR_AFF_GT_NOT_INTERSECTION2 =
let t = SPECL [` &0:real`;` &0`;`&1 `] (GENL [`a2:real`;` b2:real`;`tt:real`]
FOR_AFF_GT_NOT_INTERSECTION) in REWRITE_RULE[VECTOR_MUL_LZERO; VECTOR_ADD_LID;
VECTOR_MUL_LID; REAL_ADD_LID; REAL_ARITH` &0 < &1 /\ a - &0 = a`] t;;
REWRITE_TAC[lemma_in_orbit_iter]]);;
REWRITE_TAC[lemma_in_orbit_iter];
MP_TAC NOT_INTERSECTION_BWT_AFF_GTS;
ANTS_TAC;
REWRITE_TAC[convex_local_fan];
CONJ_TAC;
CONJ_TAC;
FIRST_ASSUM ACCEPT_TAC;
FIRST_ASSUM ACCEPT_TAC;
ONCE_REWRITE_TAC[LUNAR_COMM];
FIRST_ASSUM ACCEPT_TAC;
STRIP_TAC;
SUBGOAL_THEN` v IN V /\ w:real^3 IN V ` MP_TAC;
UNDISCH_TAC` lunar (w,v:real^3) V E `;
SIMP_TAC[lunar; INSERT_SUBSET];
STRIP_TAC;
ASSUME_TAC2 LOFA_IMP_LT_CARD_SET_V;
REWRITE_TAC[SUBSET; IN_INTER];
GEN_TAC THEN STRIP_TAC;
DOWN;
EXPAND_TAC "V";
SIMP_TAC[IN_ELIM_THM];
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
SUBGOAL_THEN` ~( v IN aff_gt {vec 0, v} {rho_node1 FF v})` ASSUME_TAC;
MATCH_MP_TAC NOT_COLL_IMP_NOT_AFF_SUB;
DOWN;
SIMP_TAC[Planarity.POINT_IN_LINE1];
SUBGOAL_THEN ` convex_local_fan (V,E,FF) ` ASSUME_TAC;
REWRITE_TAC[convex_local_fan];
CONJ_TAC;
FIRST_ASSUM ACCEPT_TAC;
FIRST_ASSUM ACCEPT_TAC;
SUBGOAL_THEN` ~collinear {vec 0, w, rho_node1 FF v}` ASSUME_TAC;
MATCH_MP_TAC NOT_COLL_RHONODE_SND_POINT;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` ~( w IN aff_gt {vec 0, w:real^3} {rho_node1 FF v})` ASSUME_TAC;
MATCH_MP_TAC NOT_COLL_IMP_NOT_AFF_SUB;
DOWN THEN SIMP_TAC[Planarity.POINT_IN_LINE1];
STRIP_TAC;
ASM_CASES_TAC` n = 0 `;
FIRST_X_ASSUM SUBST_ALL_TAC;
DOWN;
REWRITE_TAC[ITER];
DISCH_THEN SUBST_ALL_TAC;
UNDISCH_TAC` ~(v IN aff_gt {vec 0, v} {rho_node1 FF v})`;
UNDISCH_TAC` (v IN aff_gt {vec 0, v} {rho_node1 FF v})`;
SIMP_TAC[];
ASM_CASES_TAC` n = i':num`;
FIRST_X_ASSUM SUBST_ALL_TAC;
SWITCH_TAC` x = ITER i' (rho_node1 FF) v `;
SWITCH_TAC` w = ITER i' (rho_node1 FF) v `;
SWITCH_TAC` v = ITER i (rho_node1 FF) w `;
UNDISCH_TAC` ~(w IN aff_gt {vec 0, w} {rho_node1 FF v}) `;
ASM_REWRITE_TAC[];
EXPAND_TAC "w";
ASM_REWRITE_TAC[];
SWITCH_TAC` w = ITER i' (rho_node1 FF) v `;
SWITCH_TAC` v = ITER i (rho_node1 FF) w `;
UNDISCH_TAC` ~( n = i':num)`;
REWRITE_TAC[ARITH_RULE` ~( a = n:num) <=> a < n \/ n < a `];
STRIP_TAC;
EXISTS_TAC` n:num`;
ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0 ) `];
SUBGOAL_THEN` x IN aff_gt {vec 0, v} {rho_node1 FF w}` ASSUME_TAC;
UNDISCH_TAC` {ITER l (rho_node1 FF) w | 0 < l /\ l < i} SUBSET
aff_gt {vec 0, w} {rho_node1 FF w} `;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (ONCE_REWRITE_RULE[LUNAR_COMM] AFF_GT_SAME_WITH_ENDS);
ASM_REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` n:num - i'`;
CONJ_TAC;
CONJ_TAC;
UNDISCH_TAC` i' < n:num`;
ARITH_TAC;
ASM_CASES_TAC` n - i' < i:num`;
DOWN THEN REWRITE_TAC[];
DOWN;
ASM_SIMP_TAC[ARITH_RULE` c < a ==> ( ~( a - c < b:num ) <=> b + c <= a )`];
UNDISCH_TAC` n < CARD (V:real^3 -> bool) `;
PHA;
NHANH (ARITH_RULE` a < b /\ c <= a:num ==> c < b `);
STRIP_TAC;
MP_TAC2 LOFA_IMP_DIS_ELMS23;
DISCH_THEN (MP_TAC o (SPECL [`0`;` (i:num) + i' `]));
ANTS_TAC;
ASM_SIMP_TAC[ARITH_RULE` ~ (a = 0 ) ==> 0 < a + b `];
ASM_REWRITE_TAC[ITER; GSYM ITER_ADD];
ASSUME_TAC2 (ARITH_RULE` i' < n:num ==> n = n - i' + i'`);
ABBREV_TAC` ll = n - i':num`;
ASM_REWRITE_TAC[GSYM ITER_ADD];
UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF w} INTER
aff_gt {vec 0, v} {rho_node1 FF v} =
{} `;
REWRITE_TAC[INTER_EQ_EM_EXPAND; NOT_EXISTS_THM];
DISCH_THEN (MP_TAC o (SPEC `x:real^3`));
ASM_REWRITE_TAC[]]);;
SIMP_TAC[];
UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `;
DISCH_THEN (SUBST1_TAC o SYM);
EXPAND_TAC "v";
DOWN;
SIMP_TAC[interior_angle1; GSYM ivs_rho_node1; AZIM_CYCLE_TWO_POINT_SET]]);;
(* x IN aff_gt S {x} *)
let X_IN_AFF_GT_X =
let t = ISPECL [`S:real^N -> bool`;` {x:real^N}`] (GEN_ALL CONV0_SUBSET_AFF_GT)
in REWRITE_RULE[Geomdetail.CONV0_SING; INSERT_SUBSET; EMPTY_SUBSET] t;;
(* ============================ END ========================== *)
(* begin lemma EGHNAVX *)
let NEXT_PRO_IMP_ALLS = prove_by_refinement(
`!(le: A -> A -> bool). (! i. le (f i) ( f (i + 1) ))/\
(! a b c. le a b /\ le b c ==> le a c )
==> (! i j. i < j ==> le (f i ) ( f j )) `,
[GEN_TAC THEN STRIP_TAC;
GEN_TAC THEN INDUCT_TAC;
REWRITE_TAC[
LT];
REWRITE_TAC[ARITH_RULE` a < SUC b <=> a = b \/ a < b `];
STRIP_TAC;
ASM_REWRITE_TAC[
ADD1];
DOWN;
FIRST_X_ASSUM NHANH;
REWRITE_TAC[
ADD1];
ASM_MESON_TAC[]]);;
let FINITE_CARD1_IMP_SINGLETON = prove
(` FINITE (S:A -> bool) /\
CARD S = 1 ==> (? x. S = {x}) `,
ASM_CASES_TAC` S:A -> bool = {} ` THENL [
ASM_REWRITE_TAC[
CARD_CLAUSES; ARITH_RULE`~( 0 = 1 )`]; DOWN THEN
REWRITE_TAC[
EMPTY_NOT_EXISTS_IN] THEN REPEAT STRIP_TAC THEN
EXISTS_TAC`x:A` THEN MATCH_MP_TAC Hypermap.set_one_point THEN
ASM_REWRITE_TAC[]]);;
let SURJ_IMP_FINITE = prove(`
SURJ (f:A -> B) A B /\ FINITE A ==> FINITE B `,
NHANH_PAT`\x. x ==> y`
FINITE_IMAGE THEN
NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1 THEN
STRIP_TAC THEN DOWN THEN ASM_REWRITE_TAC[]);;
let EQ_IFF_IMP = MESON[]`(! a b. P a b <=> P b a ) <=> (! a b. P a b ==> P b a)`;;
ASM_CASES_TAC` ?x. x IN X /\ (f: A -> B) x = x' `;
ASM_REWRITE_TAC[];
DOWN;
MESON_TAC[];
ASM_MESON_TAC[];
REPEAT STRIP_TAC;
EXISTS_TAC `(f: A -> B) x' `;
EXPAND_TAC "f1";
ASM_MESON_TAC[]]);;
ASSUME_TAC2 LOFA_V_NOT_EMP;
ASSUME_TAC2 LOCAL_FAN_FINITE_V;
DOWN THEN NHANH CARD_EQ_0;
STRIP_TAC;
UNDISCH_TAC` ~(V:real^3 -> bool = {} )`;
FIRST_ASSUM (SUBST1_TAC o SYM);
NHANH (ARITH_RULE`~( x = 0 ) ==> x = x - 1 + 1 `);
ABBREV_TAC` u = CARD (V:real^3 -> bool) -1`;
SIMP_TAC[GSYM ADD1; ITER];
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_VITER;
SUBGOAL_THEN` ITER u (rho_node1 FF) v IN V ` ASSUME_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
STRIP_TAC;
UNDISCH_TAC` ITER u (rho_node1 FF) v IN V`;
UNDISCH_TAC` local_fan (V,E,FF)`;
PHA;
NHANH IVS_RHO_IDD;
SIMP_TAC[];
REWRITE_TAC[GSYM ITER];
FIRST_X_ASSUM (SUBST1_TAC o SYM);
ASM_REWRITE_TAC[]]);;
ASM_SIMP_TAC[];
ASSUME_TAC2 (REWRITE_RULE[convex_local_fan] (SPEC `v0:real^3 `
(GEN `v:real^3 ` CONVEX_LOFA_IMP_INANGLE_LE_PI)));
DOWN;
REWRITE_TAC[interior_angle1; ivs_rho_node1]]);;
let NEXT_PRO_IMP_ALLS_STRICT = prove
(`! le. (! i. i + 1 < k ==> le ((f: num -> A) i) (f (i + 1))) /\ (! a b c. le a b /\ le b c ==> le a c )
==> (! i j. i < j /\ j < k ==> le ( f i ) ( f j )) `,
GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN INDUCT_TAC THENL [
REWRITE_TAC[
LT]; REWRITE_TAC[
ADD1]] THEN
UNDISCH_TAC` !i. i + 1 < k ==> le ((f:num -> A) i) (f (i + 1)) ` THEN
DISCH_THEN NHANH THEN REWRITE_TAC[ARITH_RULE` a < b + 1 <=> a < b \/ a = b `]
THEN NHANH (ARITH_RULE` a + 1 < b ==> a < b `) THEN ASM_MESON_TAC[]);;
let VECTOR_ADD_LDISTRIB1 = CONJ VECTOR_ADD_LDISTRIB VECTOR_MUL_ASSOC;;
let OPPOSITE_SIDES_IMP_INTER = prove_by_refinement (
` (a:real^N)
IN aff_gt {va, vb} {vc} /\ b
IN aff_lt {va, vb} {vc}
/\
DISJOINT {va, vb} {vc} ==> ~(
conv0 {a,b}
INTER aff {va, vb} = {})`,
[NHANH Planarity.AFF_LT_2_1;
NHANH
AFF_GT_2_1;
STRIP_TAC;
UNDISCH_TAC` a
IN aff_gt {va, vb} {vc: real^N}`;
UNDISCH_TAC` b
IN aff_lt {va, vb} {vc: real^N}`;
ASM_REWRITE_TAC[
IN_ELIM_THM; Geomdetail.CONV0_SET2;
Collect_geom.AFF_2POINTS_INTERPRET; INTER_EQ_EM_EXPAND];
REPEAT STRIP_TAC;
EXISTS_TAC` ( -- t3 ) / ( -- t3 + t3') % (a:real^N) + t3' / ( --t3 + t3') % b `;
CONJ_TAC;
EXISTS_TAC` --t3 / (--t3 + t3') `;
EXISTS_TAC` t3' / ( -- t3 + t3' )`;
REWRITE_TAC[ GSYM Geomdetail.SUM_TWO_RATIO];
CONJ_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
UNDISCH_TAC` t3 < &0 `;
UNDISCH_TAC` &0 < t3' `;
PHA;
REAL_ARITH_TAC;
CONJ_TAC;
MATCH_MP_TAC
REAL_LT_DIV;
UNDISCH_TAC` t3 < &0 `;
UNDISCH_TAC` &0 < t3' `;
PHA;
REAL_ARITH_TAC;
UNDISCH_TAC` t3 < &0 `;
UNDISCH_TAC` &0 < t3' `;
PHA;
REAL_ARITH_TAC;
ASM_REWRITE_TAC[
VECTOR_ADD_LDISTRIB;
VECTOR_MUL_ASSOC; GSYM (REAL_ARITH`
( x * a ) / b = ( a / b ) * x `); REAL_ARITH` -- a * b = -- (a * b)`;
VECTOR_ARITH` ( -- a / b ) % x = -- ((a / b ) % x ) `];
SIMP_TAC[REAL_MUL_SYM];
REWRITE_TAC[VECTOR_ARITH` -- (( a % va) + (b % vb) + x ) +
( aa % va + bb % vb + x ) = (-- a + aa ) % va + (-- b + bb ) % vb `];
EXISTS_TAC` (--((t1' * t3) / (--t3 + t3')) + (
t1 * t3') / (--t3 + t3'))`;
EXISTS_TAC` (--((t2' * t3) / (--t3 + t3')) + (t2 * t3') / (--t3 + t3')) `;
REWRITE_TAC[];
REWRITE_TAC[REAL_POLY_CONV `(--((t1' * t3) / (--t3 + t3')) +
(
t1 * t3') / (--t3 + t3')) + --((t2' * t3) / (--t3 + t3')) +
(t2 * t3') / (--t3 + t3')`];
REWRITE_TAC[ REAL_ARITH` -- &1 * x * y = ( -- x ) * y `;
REAL_ARITH` a * b * c = ( a * b ) * c `;
REAL_ARITH` a * x + b * x = (a + b) * x`];
UNDISCH_TAC`
t1 + t2 + t3 = &1 `;
UNDISCH_TAC` t1' + t2' + t3' = &1 `;
SIMP_TAC[ REAL_ARITH` a + b = &1 <=> a = &1 - b `; REAL_POLY_CONV` (&1 - (t2 + t3)) * t3' +
--(&1 - (t2' + t3')) * t3 +
t2 * t3' +
--t2' * t3 `];
REPEAT STRIP_TAC;
MATCH_MP_TAC
REAL_MUL_RINV;
ASM_REAL_ARITH_TAC]);;
let DISJOINT_DOUBLE_SING = SET_RULE` DISJOINT {a} {b} <=> ~( a = b ) `;;
let AFF_IN_TWO_PARTS = prove_by_refinement (
` aff {x,y:real^N} = aff_ge {x} {y}
UNION aff_lt {x} {y}`,
[REWRITE_TAC[
HALFLINE];
ASM_CASES_TAC` x = y:real^N`;
ASM_REWRITE_TAC[
AFF_XX_CASES;
AFF2;
UNION_EMPTY;
FUN_EQ_THM;
IN_ELIM_THM];
GEN_TAC THEN EQ_TAC;
STRIP_TAC;
EXISTS_TAC `&1 `;
ASM_REWRITE_TAC[REAL_ARITH` &0 <= &1 `];
CONV_TAC VECTOR_ARITH;
STRIP_TAC;
EXISTS_TAC` t:real`;
ASM_REWRITE_TAC[
VECTOR_ADD_SYM];
DOWN;
REWRITE_TAC[ GSYM DISJOINT_DOUBLE_SING];
SIMP_TAC[
AFF_LT_1_1;
AFF2;
EXTENSION;
IN_UNION;
IN_ELIM_THM];
STRIP_TAC THEN GEN_TAC;
EQ_TAC;
STRIP_TAC;
ASM_CASES_TAC` &0 <= &1 - t`;
DISJ1_TAC;
EXISTS_TAC` &1 - t `;
ASM_REWRITE_TAC[REAL_ARITH` a - ( a - b ) = b `];
DISJ2_TAC;
EXISTS_TAC` t:real`;
EXISTS_TAC` &1 - t `;
ASM_REWRITE_TAC[];
ASM_REAL_ARITH_TAC;
MESON_TAC[REAL_ARITH` t = a - ( a - t ) `;REAL_ARITH` a + b = c <=> b = c - a `]]);;
let INTER_UNION_EMPTY = SET_RULE` X INTER (A UNION B) = {} <=>
X INTER A = {} /\ X INTER B = {}`
let MONO_AZIM_AS_BTA_I = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\
v0
IN V /\
CARD V = k /\
(!v. v
IN V /\ ~(v = v0) ==> ~collinear {
vec 0, v0, v}) /\
(!i.
ITER i (
rho_node1 FF) v0 = vv i) /\
(!i.
azim (
vec 0) v0 (vv 1) (vv i) = bta i)
==> (!i j. i < j /\ j < k ==> bta i <= bta j) `,
[STRIP_TAC;
MATCH_MP_TAC
NEXT_PRO_IMP_ALLS_STRICT;
REWRITE_TAC[
REAL_LE_TRANS];
DOWN_TAC THEN REWRITE_TAC[
convex_local_fan];
REPEAT STRIP_TAC;
ASSUME_TAC2
LOFA_IMP_V_DIFF;
UNDISCH_TAC` v0:real^3
IN V `;
FIRST_ASSUM NHANH;
ONCE_REWRITE_TAC[
EQ_SYM_EQ];
NHANH Trigonometry2.NOT_EQ_IMP_EXISTS_BASIC;
STRIP_TAC;
MP_TAC (SPECL [`
vec 0:real^3 `;` v0:real^3 `;` (vv 1):real^3 `;
`(vv: num -> real^3) i `]
azim);
STRIP_TAC;
FIRST_X_ASSUM MP_TAC;
SWITCH_TAC` ~(
vec 0 = v0:real^3 )`;
DISCH_THEN ASSUME_TAC2;
DOWN;
STRIP_TAC;
MP_TAC (SPECL [`
vec 0:real^3 `;` v0:real^3 `;` (vv 1):real^3 `;
`(vv: num -> real^3) (i +1) `]
azim);
STRIP_TAC;
FIRST_X_ASSUM ASSUME_TAC2;
DOWN THEN STRIP_TAC;
DOWN_TAC;
REWRITE_TAC[
VECTOR_SUB_RZERO];
STRIP_TAC;
UNDISCH_TAC` vv 1 = (r1' *
cos psi') % e1 + (r1' *
sin psi') % e2 + h1' % (v0:real^3)`;
UNDISCH_TAC` vv 1 = (r1 *
cos psi) % e1 + (r1 *
sin psi) % e2 + h1 % v0:real^3`;
UNDISCH_TAC`
orthonormal e1 e2 e3`;
PHA;
EXPAND_TAC "v0";
REWRITE_TAC[VECTOR_MUL_ASSOC];
NHANH (MESON[Trigonometry2.th]` orthonormal e1 e2 e3 /\
x = t1 % e1 + t2 % e2 + t3 % e3 /\
x = tt1 % e1 + tt2 % e2 + tt3 % e3
==> tt1 = t1 /\ tt2 = t2 /\ tt3 = t3`);
STRIP_TAC;
SUBGOAL_THEN` ~collinear {vec 0, v0, vv 1:real^3}` ASSUME_TAC;
UNDISCH_TAC` !v. v IN V /\ ~(v = v0) ==> ~collinear {vec 0, v0, v:real^3} `;
DISCH_THEN MATCH_MP_TAC;
SWITCH_TAC` !i. ITER i (rho_node1 FF) v0 = vv i`;
FIRST_ASSUM (fun x -> REWRITE_TAC[x]);
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_VITER;
CONJ_TAC;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
REWRITE_TAC[ITER12];
UNDISCH_TAC` v0 IN (V:real^3 -> bool)`;
FIRST_X_ASSUM NHANH;
SIMP_TAC[];
USE_FIRST` ~collinear {vec 0, v0, vv 1:real^3} ==> &0 < r1 ` ASSUME_TAC2;
USE_FIRST` ~collinear {vec 0, v0, vv 1:real^3} ==> &0 < r1' ` ASSUME_TAC2;
ASSUME_TAC2 (SPECL [` r1': real`;` r1: real`;` psi': real`; `psi:real` ]
Trigonometry2.R_POS_SIN_COS_IDENT);
DOWN;
REWRITE_TAC[Trigonometry2.SIN_COS_IDEN_IFF_DIFFER_PERS];
STRIP_TAC;
SUBGOAL_THEN `vv (i:num) IN (V:real^3 -> bool) ` ASSUME_TAC;
SWITCH_TAC` !i. ITER i (rho_node1 FF) v0 = vv i `;
ASM_REWRITE_TAC[];
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_VITER;
FIRST_X_ASSUM MATCH_MP_TAC;
FIRST_ASSUM ACCEPT_TAC;
DOWN;
SUBGOAL_THEN` convex_local_fan (V,E,FF) ` MP_TAC;
ASM_REWRITE_TAC[convex_local_fan];
PHA;
NHANH IN_V_IMP_AZIM_LESS_PI;
STRIP_TAC;
UNDISCH_TAC` v0:real^3 IN V`;
FIRST_ASSUM NHANH;
SUBGOAL_THEN` rho_node1 FF (vv (i:num)) = vv ( i + 1 ) ` ASSUME_TAC;
USE_FIRST` !i. ITER i (rho_node1 FF) v0 = vv i ` (fun x -> REWRITE_TAC[GSYM x]);
REWRITE_TAC[GSYM ADD1; ITER];
FIRST_ASSUM SUBST1_TAC;
REWRITE_TAC[SYM SIN_AZIM_POS_PI_LT];
REWRITE_TAC[REAL_ARITH` &0 <= a <=> ~( a < &0 ) `;SIN_AZIM_MUTUAL_SROSS ];
ABBREV_TAC` va = azim (vec 0) v0 (vv 1) (vv i) `;
ABBREV_TAC` vb = azim (vec 0) v0 (vv 1) (vv (i + 1 )) `;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[REAL_ADD_SYM];
REWRITE_TAC[Trigonometry2.SIN_COS_PERIODIC_IN_WHOLE; REAL_ARITH` a + b + c = (a + b ) + c `];
EXPAND_TAC "v0";
REWRITE_TAC[CROSS_LADD; CROSS_RADD; VECTOR_MUL_ASSOC; CROSS_LMUL; CROSS_RMUL;
CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID; DOT_LADD; DOT_LMUL;
DOT_RMUL;DOT_CROSS_SELF; Collect_geom.ZERO_NEUTRAL];
STRIP_TAC;
DOWN;
REWRITE_TAC[DOT_LZERO; Collect_geom.ZERO_NEUTRAL];
ASSUME_TAC2 ORTHONORMAL_CROSS;
ASM_REWRITE_TAC[];
ONCE_REWRITE_TAC[CROSS_SKEW];
ASM_REWRITE_TAC[];
SUBGOAL_THEN` e3 dot (e3: real^3) = &1 ` ASSUME_TAC;
UNDISCH_TAC` orthonormal e1 e2 e3 `;
SIMP_TAC[orthonormal];
ASM_REWRITE_TAC[DOT_LNEG; REAL_RING` (r2 * a) * (r2' * b) * &1 +
(r2 * aa) * (r2' * bb) * -- &1
= r2 * r2' * (b * a - bb * aa ) `; GSYM SIN_SUB];
REWRITE_TAC[REAL_ARITH` (a + b ) - ( c + b ) = a - c `];
SUBGOAL_THEN` &0 < dist (v0, vec 0:real^3)` ASSUME_TAC;
ASM_REWRITE_TAC[GSYM DIST_NZ];
ASM_CASES_TAC` i = 0 `;
USE_FIRST` !i. azim (vec 0) v0 (vv 1) (vv i) = bta (i:num)`
(fun x -> REWRITE_TAC[GSYM x]);
USE_FIRST` i = 0 ` SUBST1_TAC;
USE_FIRST` !i. ITER i (rho_node1 FF) v0 = vv i` (fun x -> REWRITE_TAC[GSYM x]);
REWRITE_TAC[ITER; ITER12; GSYM ADD1; AZIM_SPEC_DEGENERATE; AZIM_REFL; REAL_LE_REFL];
SWITCH_TAC` vv (i:num) =
(r2 * cos (psi + va)) % e1 + (r2 * sin (psi + va)) % e2 + h2 % (v0:real^3)`;
SWITCH_TAC` vv (i + 1) =
(r2' * cos (psi' + vb)) % e1 + (r2' * sin (psi' + vb)) % e2 + h2' % (v0:real^3)`;
SWITCH_TAC` psi' = psi + real_of_int k' * &2 * pi `;
SUBGOAL_THEN` ~( vv i = v0:real^3 ) /\ ~(vv (i + 1 ) = v0 ) ` ASSUME_TAC;
UNDISCH_TAC` dist (v0:real^3,vec 0) % e3 IN (V:real^3 -> bool)`;
ASM_REWRITE_TAC[];
STRIP_TAC;
ASSUME_TAC2 (SPEC `v0: real^3 ` (GEN `v:real^3 ` LOFA_IMP_DIS_ELMS23));
FIRST_ASSUM (MP_TAC o (SPECL [`0`;` i:num`]));
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[ARITH_RULE` 0 < i <=> ~( i = 0 ) `];
UNDISCH_TAC` i + 1 < k `;
ARITH_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [`0`;` i + 1`]));
REWRITE_TAC[ARITH_RULE` 0 < i + 1 `];
ASM_REWRITE_TAC[];
USE_FIRST` !i. ITER i (rho_node1 FF) v0 = vv i ` (fun x -> REWRITE_TAC[GSYM x]);
SIMP_TAC[ITER];
STRIP_TAC;
UNDISCH_TAC` (vv:num -> real^3) i IN V `;
UNDISCH_TAC` local_fan (V,E,FF) `;
PHA;
NHANH LOFA_IN_V_SO_DO_RHO_NODE_V;
ASM_REWRITE_TAC[];
DOWN THEN DOWN THEN PHA THEN STRIP_TAC;
USE_FIRST` !v. v IN V /\ ~(v = v0) ==> ~collinear {vec 0, v0, v:real^3}`
(ASSUME_TAC2 o (SPEC` (vv:num -> real^3) i `));
USE_FIRST` !v. v IN V /\ ~(v = v0) ==> ~collinear {vec 0, v0, v:real^3}`
(ASSUME_TAC2 o (SPEC` (vv:num -> real^3) (i + 1) `));
USE_FIRST` ~collinear {vec 0, v0, (vv: num -> real^3) i} ==> &0 < r2 ` ASSUME_TAC2;
USE_FIRST` ~collinear {vec 0, v0, (vv: num -> real^3) (i + 1 )} ==> &0 < r2' ` ASSUME_TAC2;
UNDISCH_TAC` ~(dist (v0:real^3,vec 0) * r2 * r2' * sin (vb - va) < &0) `;
ASM_SIMP_TAC[REAL_LE_MUL_EQ; REAL_ARITH` ~( a < b ) <=> b <= a `];
MP_TAC (SPEC` v0:real^3 ` (GEN` v:real^3 ` IN_V_IMP_AZIM_LESS_PI));
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` dist (v0:real^3,vec 0) % (e3:real^3) IN V`;
ASM_REWRITE_TAC[];
DISCH_TAC;
FIRST_ASSUM (MP_TAC2 o (SPEC` (vv:num -> real^3) i `));
FIRST_ASSUM (MP_TAC2 o (SPEC` (vv:num -> real^3) (i + 1 ) `));
ASM_REWRITE_TAC[];
SUBGOAL_THEN` rho_node1 FF v0 = vv 1` ASSUME_TAC;
SWITCH_TAC ` !i. ITER i (rho_node1 FF) v0 = vv i `;
DOWN;
SIMP_TAC[ITER12];
FIRST_ASSUM (fun x -> REWRITE_TAC[x]);
USE_FIRST` !i. azim (vec 0) v0 (vv 1) (vv i) = bta i ` (fun x -> REWRITE_TAC[GSYM x]);
MP_TAC (SPECL [`vec 0:real^3 `;` v0:real^3 `;` (vv:num -> real^3) 1`;
` (vv:num -> real^3) i `] AZIM_RANGE);
MP_TAC (SPECL [`vec 0:real^3 `;` v0:real^3 `;` (vv:num -> real^3) 1`;
` (vv:num -> real^3) (i + 1) `] AZIM_RANGE);
REWRITE_TAC[ASSUME` azim (vec 0) v0 (vv 1) (vv (i + 1)) = vb `; ASSUME` azim (vec 0) v0 (vv 1) (vv i) = va `];
PHA;
NHANH (REAL_ARITH` &0 <= vb /\
vb < &2 * pi /\
&0 <= va /\
va < &2 * pi /\
vb <= pi /\
va <= pi /\
&0 <= sin (vb - va) ==> vb - va <= pi /\ -- pi <= vb - va `);
STRIP_TAC;
ASM_CASES_TAC ` ~(vb - va = -- pi) `;
ASM_CASES_TAC` vb - va < &0 `;
REPLICATE_TAC 3 DOWN THEN PHA;
REWRITE_TAC[REAL_ARITH` a <= b /\ ~( b = a ) /\ x < &0 <=> a < b /\ x < &0`];
STRIP_TAC;
ASSUME_TAC2 (SPEC ` vb - (va:real)` Trigonometry1.SIN_NEGPOS_PI);
SUBGOAL_THEN` sin (vb - va ) < &0 ` ASSUME_TAC;
ASM_REWRITE_TAC[];
ABBREV_TAC` xx = vb - va:real`;
UNDISCH_TAC` sin xx < &0 `;
UNDISCH_TAC` &0 <= sin xx `;
REAL_ARITH_TAC;
DOWN;
REAL_ARITH_TAC;
UNDISCH_TAC` &0 <= vb `;
UNDISCH_TAC` va <= pi `;
DOWN THEN PHA;
REWRITE_TAC[REAL_ARITH` vb - va = --pi /\ va <= pi /\ &0 <= vb <=>
vb = &0 /\ va = pi`];
STRIP_TAC;
UNDISCH_TAC` ~ collinear {vec 0, v0, vv (i + 1):real^3}`;
UNDISCH_TAC` ~ collinear {vec 0, v0, vv 1:real^3}`;
PHA;
NHANH AZIM_EQ_0_ALT;
STRIP_TAC;
UNDISCH_TAC` ~ collinear {vec 0, v0, vv (i: num) :real^3}`;
UNDISCH_TAC` ~ collinear {vec 0, v0, vv 1:real^3}`;
PHA;
NHANH AZIM_EQ_PI_ALT;
STRIP_TAC;
SWITCH_TAC` vv 1:real^3 =
(r1 * cos psi) % e1 + (r1 * sin psi) % e2 + (h1 * dist (v0:real^3,vec 0)) % e3`;
SWITCH_TAC`vv 1: real^3 =
(r1' * cos psi') % e1 +
(r1' * sin psi') % e2 +
(h1' * dist (v0: real^3,vec 0)) % e3`;
UNDISCH_TAC` va = pi `;
UNDISCH_TAC` vb = &0 `;
UNDISCH_TAC` azim (vec 0) v0 (vv 1) (vv (i + 1)) = &0 <=>
vv (i + 1) IN aff_gt {vec 0, v0} {vv 1}`;
UNDISCH_TAC`azim (vec 0) v0 (vv 1) (vv i) = pi <=>
vv i IN aff_lt {vec 0, v0} {vv 1} `;
ASM_SIMP_TAC[];
ASSUME_TAC2 (
ISPECL [` vec 0: real^3`;` v0: real^3`;` (vv:num -> real^3) 1` ] Fan.th3a) ;
REPEAT STRIP_TAC;
ASSUME_TAC2 (
ISPECL [` (vv:num -> real^3) 1 `;` (vv:num -> real^3) (i + 1)`;
` (vv:num -> real^3) i`;`vec 0: real^3`; ` v0: real^3`] (GEN_ALL OPPOSITE_SIDES_IMP_INTER));
DOWN;
REWRITE_TAC[AFF_IN_TWO_PARTS; INTER_UNION_EMPTY; DE_MORGAN_THM];
STRIP_TAC;
ASSUME_TAC (ISPECL [`{vec 0:real^3}`;`{(vv: num -> real^3) (i + 1), vv i }`]
(GEN_ALL CONV_SUBSET_AFF_GE));
(* ****************** *)
ASSUME_TAC (
ISPECL [`(vv: num -> real^3) (i + 1)`;` (vv:num -> real^3) i `]
Geomdetail.CONV02_SU_CONV2);
ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2;
DOWN THEN STRIP_TAC;
UNDISCH_TAC` (vv:num -> real^3) i IN V`;
FIRST_ASSUM NHANH;
STRIP_TAC;
DOWN;
UNDISCH_TAC ` local_fan (V,E,FF)`;
PHA;
NHANH LOCAL_FAN_IN_FF_IN_ORD_PAIRS2;
ASM_REWRITE_TAC[];
NHANH Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
REWRITE_TAC[FAN; fan7];
STRIP_TAC;
DOWN THEN DOWN;
FIRST_ASSUM (ASSUME_TAC o (ISPECL [`{v0:real^3}`;`{(vv: num -> real^3) i,
vv (i + 1)}`]));
STRIP_TAC;
SUBGOAL_THEN `{v0: real^3} IN E UNION {{v} | v IN V}` MP_TAC;
UNDISCH_TAC`dist (v0: real^3,vec 0) % (e3:real^3) IN V`;
ASM_REWRITE_TAC[IN_UNION; IN_ELIM_THM];
MESON_TAC[];
REPEAT STRIP_TAC;
UNDISCH_TAC` {v0:real^3} IN E UNION {{v} | v IN V} /\
{vv i, vv (i + 1)} IN E UNION {{v} | v IN V}
==> aff_ge {vec 0} {v0} INTER aff_ge {vec 0} {vv i, vv (i + 1)} =
aff_ge {vec 0} ({v0} INTER {vv i, vv (i + 1)}) `;
ANTS_TAC;
DOWN THEN DOWN;
PHA;
SIMP_TAC[IN_UNION];
SUBGOAL_THEN `{v0: real^3} INTER {vv i, vv (i + 1)} = {}` SUBST1_TAC;
UNDISCH_TAC` ~(vv (i:num) = v0:real^3)`;
UNDISCH_TAC` ~(vv (i + 1) = v0:real^3)`;
REWRITE_TAC[Trigonometry2.INSERT_INTER_EMPTY; IN_INSERT; NOT_IN_EMPTY];
MESON_TAC[];
REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING];
UNDISCH_TAC` conv {vv (i + 1), (vv: num -> real^3) i} SUBSET
aff_ge {vec 0} {vv (i + 1), vv i}`;
UNDISCH_TAC` conv0 {vv (i + 1), (vv: num -> real^3) i} SUBSET
conv {vv (i + 1), (vv: num -> real^3) i}`;
PHA;
SIMP_TAC[INSERT_COMM];
NHANH (
SET_RULE`a SUBSET b /\ b SUBSET c /\ x INTER c = S ==> x INTER a SUBSET S`);
STRIP_TAC;
DOWN;
UNDISCH_TAC` ~(conv0 {vv (i + 1), vv i} INTER aff_ge {vec 0} {v0:real^3} = {})`;
PHA;
SIMP_TAC[INSERT_COMM; INTER_COMM; SET_RULE` ~( s = {}) /\ s SUBSET {x} <=>
s = {x}`];
NHANH (SET_RULE` A INTER B = {x} ==> x IN B`);
NHANH CONV0_SUB_CONV;
STRIP_TAC;
SUBGOAL_THEN` collinear {vec 0, (vv:num -> real^3) i, vv (i + 1)}` ASSUME_TAC;
ASM_REWRITE_TAC[Collect_geom.COLLINEAR_AS_IN_CONV2];
ASSUME_TAC2 (SPEC `(vv:num -> real^3 ) i ` (GEN `v: real^3`
LOCAL_FAN_CHARACTER_OF_RHO_NODE2));
DOWN;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` circular (V:real^3 -> bool) E ` MP_TAC;
REWRITE_TAC[circular];
EXISTS_TAC` (vv: num -> real^3) (i + 1) `;
EXISTS_TAC` (vv: num -> real^3) i`;
EXISTS_TAC` v0: real^3`;
ASSUME_TAC (ISPECL [`{vec 0:real^3}`;` {(vv:num -> real^3) (i + 1), vv i}`]
(GEN_ALL CONV0_SUBSET_AFF_GT));
ASSUME_TAC2 LOCAL_FAN_CHARACTER_OF_RHO_NODE;
UNDISCH_TAC` (vv: num -> real^3) i IN V `;
FIRST_ASSUM (NHANH_PAT`\x. x ==> l`);
ASM_SIMP_TAC[ GSYM Wrgcvdr_cizmrrh.IN_E_IFF_IN_ORD_E; INSERT_COMM];
STRIP_TAC;
UNDISCH_TAC` dist (v0:real^3,vec 0) % (e3:real^3) IN V`;
ASM_SIMP_TAC[];
STRIP_TAC;
UNDISCH_TAC` conv0 {vv (i + 1), (vv i):real^3} SUBSET aff_gt {vec 0} {vv (i + 1), vv i}`;
UNDISCH_TAC` ~(conv0 {vv (i + 1), vv i} INTER aff_lt {vec 0} {v0:real^3} = {})`;
PHA;
SIMP_TAC[INSERT_COMM];
CONV_TAC SET_RULE;
STRIP_TAC;
ASSUME_TAC2 KCHMAMG;
DOWN THEN STRIP_TAC;
ABBREV_TAC `U = {ITER n (rho_node1 FF) v0 | n <= i + 1} `;
ABBREV_TAC` ee = v0 cross rho_node1 FF v0`;
MP_TAC (SPECL [`v0: real^3`;`A:real^3 -> bool`;` ee:real^3`;`i + 1`]
(GENL [` v:real^3 `;`P:real^3 -> bool`;`e:real^3`;`l: num`]
SEQUENCE_OF_RHO_NODE_IS_SUC));
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` dist (v0:real^3,vec 0) % (e3:real^3) IN V`;
ASM_SIMP_TAC[];
STRIP_TAC;
MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC`V:real^3 -> bool`;
ASM_REWRITE_TAC[];
EXPAND_TAC "U";
REWRITE_TAC[SUBSET; IN_ELIM_THM];
ASSUME_TAC2 LOCAL_FAN_ORBIT_MAP_VITER;
DOWN THEN DOWN;
MESON_TAC[];
DISCH_THEN (MP_TAC o (SPECL [`ITER i (rho_node1 FF) v0`;` i:num`]));
ANTS_TAC;
REWRITE_TAC[ARITH_RULE` a < a + 1 `];
DISCH_THEN (MP_TAC o (SPEC` v0:real^3`));
ANTS_TAC;
EXPAND_TAC "U";
ASM_REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC`0`;
UNDISCH_TAC` ! i. ITER i (rho_node1 FF) v0 = vv i`;
PAT_ONCE_REWRITE_TAC`\x. x ==> y ` [EQ_SYM_EQ];
SIMP_TAC[ITER; LE_0];
ASM_REWRITE_TAC[];
SUBGOAL_THEN` &0 < sin ( azim (vec 0) ee v0 (vv (i + 1)))` ASSUME_TAC;
REWRITE_TAC[SIN_AZIM_MUTUAL_SROSS];
UNDISCH_TAC` vv (i + 1) IN aff_gt {vec 0, v0: real^3} {vv 1}`;
ASM_SIMP_TAC[AFF_GT_2_1; IN_ELIM_THM];
STRIP_TAC;
ONCE_REWRITE_TAC[CROSS_TRIPLE];
ASM_REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_REFL; CROSS_0; VECTOR_MUL_RZERO;
VECTOR_ADD_LID];
UNDISCH_TAC` v0 cross rho_node1 FF v0 = ee`;
ASM_SIMP_TAC[DOT_LMUL];
STRIP_TAC;
MATCH_MP_TAC REAL_LT_MUL;
ASM_REWRITE_TAC[DOT_POS_LT];
EXPAND_TAC "ee";
ASM_REWRITE_TAC[CROSS_EQ_0];
DOWN;
NHANH (REAL_ARITH` &0 < x ==> &0 <= x `);
REWRITE_TAC[SIN_AZIM_POS_PI_LT];
PHA;
NHANH (REAL_ARITH` a <= h /\ b < a ==> b <= h `);
REWRITE_TAC[GSYM SIN_AZIM_POS_PI_LT];
REWRITE_TAC[REAL_ARITH` a <= b <=> ~( b < a)`; SIN_AZIM_MUTUAL_SROSS];
STRIP_TAC;
DOWN;
UNDISCH_TAC` (vv:num -> real^3) i IN aff_lt {vec 0, v0} {vv 1}`;
ASM_SIMP_TAC[Planarity.AFF_LT_2_1; IN_ELIM_THM];
STRIP_TAC;
ONCE_REWRITE_TAC[CROSS_TRIPLE];
ASM_REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_0; CROSS_REFL; VECTOR_MUL_RZERO;
VECTOR_ADD_LID; DOT_LMUL];
UNDISCH_TAC` v0 cross rho_node1 FF v0 = ee`;
ASM_SIMP_TAC[];
STRIP_TAC;
SUBGOAL_THEN` &0 < ee dot (ee:real^3)` MP_TAC;
REWRITE_TAC[DOT_POS_LT];
EXPAND_TAC "ee";
REWRITE_TAC[CROSS_EQ_0];
FIRST_X_ASSUM ACCEPT_TAC;
SIMP_TAC[REAL_LE_MUL_EQ; REAL_ARITH` ~( a < b) <=> b <= a`];
ASM_SIMP_TAC[REAL_ARITH` a <= b <=> ~(b < a )`]]);;
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM; GSYM ITER];
UNDISCH_TAC` i < l:num`;
MESON_TAC[ARITH_RULE` a < b:num ==> a <= b /\ SUC a <= b `];
UNDISCH_TAC` plane (P:real^3 -> bool)`;
PHA;
NHANH THREE_NOT_COLL_DETER_PLANE;
STRIP_TAC;
SUBGOAL_THEN` ITER (i - 1) (rho_node1 FF) v IN P` ASSUME_TAC;
UNDISCH_TAC` U SUBSET (P:real^3 -> bool)`;
REWRITE_TAC[SUBSET];
DISCH_THEN MATCH_MP_TAC;
EXPAND_TAC "U";
REWRITE_TAC[IN_ELIM_THM];
EXISTS_TAC` i - 1 `;
UNDISCH_TAC` i < l:num`;
REWRITE_TAC[];
CONV_TAC ARITH_RULE;
DOWN;
EXPAND_TAC "P";
REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
STRIP_TAC;
SUBGOAL_THEN` w < &0 ` ASSUME_TAC;
UNDISCH_TAC` i < l:num`;
NHANH (ARITH_RULE` a < b ==> a - 1 < b `);
UNDISCH_TAC` i < l
==> &0 <
(ITER i (rho_node1 FF) v cross ITER (i + 1) (rho_node1 FF) v) dot e`;
DISCH_THEN NHANH;
UNDISCH_TAC` i - 1 < l
==> &0 <
(ITER (i - 1) (rho_node1 FF) v cross
ITER (i - 1 + 1) (rho_node1 FF) v) dot
e`;
DISCH_THEN NHANH;
ASM_SIMP_TAC[ARITH_RULE` 0 < a ==> a - 1 + 1 = a `; GSYM ITER; ADD1;
CROSS_LADD; CROSS_LMUL; CROSS_0; CROSS_REFL];
REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];
STRIP_TAC;
DOWN;
ONCE_REWRITE_TAC[CROSS_SKEW];
REWRITE_TAC[VECTOR_MUL_RNEG];
REWRITE_TAC[GSYM VECTOR_MUL_LNEG; DOT_LMUL];
ASM_SIMP_TAC[REAL_LT_MUL_EQ];
REAL_ARITH_TAC;
UNDISCH_TAC`~collinear
{vec 0, ITER i (rho_node1 FF) v, rho_node1 FF
(ITER i (rho_node1 FF) v )}`;
NHANH Fan.th3a;
NHANH AFF_LT_2_1;
SIMP_TAC[ITER; GSYM ADD1; IN_ELIM_THM];
STRIP_TAC;
EXISTS_TAC` u:real`;
EXISTS_TAC` v': real`;
EXISTS_TAC`w:real`;
ASM_REWRITE_TAC[]]);;
EXPAND_TAC "vv";
EXPAND_TAC "w";
SIMP_TAC[];
ONCE_REWRITE_TAC[INSERT_SUBSET];
ASM_REWRITE_TAC[];
MATCH_MP_TAC SUBSET_TRANS;
EXISTS_TAC`U:real^3 -> bool`;
ASM_REWRITE_TAC[];
REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
EXPAND_TAC "U";
EXPAND_TAC "u";
EXPAND_TAC "vv";
EXPAND_TAC "w";
REWRITE_TAC[IN_ELIM_THM];
UNDISCH_TAC` i < l:num`;
NHANH (ARITH_RULE` a < b:num ==> a <= b /\ a - 1 <= b /\ a + 1 <= b`);
MESON_TAC[];
SIMP_TAC[]]);;
let INSERT_UNION2 = SET_RULE` (x INSERT S) UNION U = S UNION (x INSERT U)`;;
let EGHNAVX = prove_by_refinement
(`
convex_local_fan (V,E,
FF) /\
v0
IN V /\
CARD V = k /\
(!v. v
IN V /\ ~(v = v0) ==> ~collinear {
vec 0, v0, v}) /\
(!i.
ITER i (
rho_node1 FF) v0 = vv i) /\
(!i.
azim (
vec 0) v0 (vv 1) (vv i) = bta i)
==> bta 1 = &0 /\
bta (k - 1) <=
pi /\
(!i j. i < j /\ j < k ==> bta i <= bta j) /\
(bta i = &0 /\ i < k
==> (!j. 0 < j /\ j < i ==>
interior_angle1 (
vec 0)
FF (vv j) =
pi) /\
{vv k | 0 < k /\ k <= i}
SUBSET aff_gt {
vec 0, v0} {vv 1}) /\
(bta i = bta (k - 1) /\ 0 < i /\ i < k - 1
==> (!j. i < j /\ j < k ==>
interior_angle1 (
vec 0)
FF (vv j) =
pi) /\
{vv n | i <= n /\ n < k}
SUBSET aff_gt {
vec 0, v0} {vv (k - 1)})`,
[NHANH
MONO_AZIM_AS_BTA_I;
STRIP_TAC;
ASSUME_TAC2
FIRST_EQ0_LAST_LT_PI;
ASM_REWRITE_TAC[];
ASSUME_TAC2
CVX_LO_IMP_LO;
ASSUME_TAC2
LOCAL_FAN_ORBIT_MAP_VITER;
ASSUME_TAC2 (SPEC` v0:real^3` (GEN`v:real^3` LOFA_IMP_DIS_ELMS23));
CONJ_TAC;
STRIP_TAC;
SUBGOAL_THEN` {vv k | 0 < k /\ k <= i}
SUBSET aff_gt {
vec 0, v0:real^3} {vv 1}` ASSUME_TAC;
REWRITE_TAC[
SUBSET;
IN_ELIM_THM];
REPEAT STRIP_TAC;
SUBGOAL_THEN`
azim (
vec 0) v0 (vv 1) (vv k') = &0` ASSUME_TAC;
ASM_CASES_TAC` k' = i:num`;
ASM_REWRITE_TAC[];
UNDISCH_TAC` !i j. i < j /\ j < k ==> bta i <= (bta:num ->
real) j`;
DISCH_THEN (MP_TAC o (SPECL [`k': num`;` i: num`]));
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` k' <= i:num`;
UNDISCH_TAC` ~( k' = i:num)`;
PHA;
ARITH_TAC;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` &0 <=
azim (
vec 0) v0 (vv 1) (vv k')` MP_TAC;
REWRITE_TAC[
AZIM_RANGE];
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
ASSUME_TAC2
LOCAL_FAN_CHARACTER_OF_RHO_NODE;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v0:real^3`));
FIRST_ASSUM (MP_TAC o (SPECL [`0`;`k': num`]));
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` k' <= i:num`;
UNDISCH_TAC` i < k:num`;
ARITH_TAC;
REWRITE_TAC[
ITER];
DOWN;
SUBGOAL_THEN`
rho_node1 FF v0 =
ITER 1 (
rho_node1 FF) v0` MP_TAC;
REWRITE_TAC[
ITER12];
ASM_SIMP_TAC[];
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`v0:real^3`;`1`]));
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`v0:real^3`;`k':num`]));
DOWN THEN DOWN;
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
UNDISCH_TAC` !v. v
IN V /\ ~(v = v0) ==> ~collinear {
vec 0, v0, v:real^3}`;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC`(vv:num -> real^3) 1 `));
FIRST_ASSUM (ASSUME_TAC2 o (SPEC`(vv:num -> real^3) k' `));
DOWN THEN DOWN THEN PHA;
NHANH (GSYM
AZIM_EQ_0_ALT);
SIMP_TAC[];
ASM_REWRITE_TAC[];
ASSUME_TAC (ISPECL [`{
vec 0, v0:real^3}`;` {(vv:num -> real^3) 1}`]
AFF_GT_SUBSET_AFFINE_HULL);
ASM_REWRITE_TAC[];
UNDISCH_TAC` !i.
ITER i (
rho_node1 FF) v0 = vv i`;
STRIP_TAC;
FIRST_ASSUM (fun x -> REWRITE_TAC[GSYM x]);
MATCH_MP_TAC (GEN_ALL
CNVX_IMP_INTERIOR_ANGLE_PI);
EXISTS_TAC`E:(real^3 -> bool) -> bool`;
EXISTS_TAC` V:real^3 -> bool`;
EXISTS_TAC`{
ITER n (
rho_node1 FF) v0 | n <= i}`;
EXISTS_TAC`
affine hull ({
vec 0, v0:real^3}
UNION {vv 1})`;
ASM_REWRITE_TAC[];
ASSUME_TAC2 (SPEC` v0:real^3` (GEN `v:real^3`
LOCAL_FAN_CHARACTER_OF_RHO_NODE2));
CONJ_TAC;
REWRITE_TAC[INSERT_UNION2;
UNION_EMPTY];
DOWN;
SUBGOAL_THEN`
rho_node1 FF v0 =
ITER 1 (
rho_node1 FF) v0` ASSUME_TAC;
REWRITE_TAC[
ITER12];
ASM_REWRITE_TAC[
plane];
MESON_TAC[
INSERT_COMM];
CONJ_TAC;
REWRITE_TAC[INSERT_UNION2;
UNION_EMPTY];
MESON_TAC[Trigonometry2.IN_P_HULL_INSERT;
INSERT_COMM];
REWRITE_TAC[
SUBSET;
IN_ELIM_THM];
REPEAT STRIP_TAC;
ASM_CASES_TAC` n = 0 `;
ASM_REWRITE_TAC[];
SUBGOAL_THEN` vv 0 =
ITER 0 (
rho_node1 FF) v0` MP_TAC;
ASM_REWRITE_TAC[];
SIMP_TAC[
ITER; Trigonometry2.IN_P_HULL_INSERT; INSERT_UNION2;
UNION_EMPTY];
SUBGOAL_THEN` x
IN {(vv:num ->real^3) k | 0 < k /\ k <= i}` MP_TAC;
REWRITE_TAC[
IN_ELIM_THM];
EXISTS_TAC`n:num`;
ASM_REWRITE_TAC[];
DOWN;
ARITH_TAC;
UNDISCH_TAC` {vv k | 0 < k /\ k <= i}
SUBSET aff_gt {
vec 0, v0:real^3} {vv 1}`;
REWRITE_TAC[
SUBSET];
DISCH_THEN NHANH;
UNDISCH_TAC` aff_gt {
vec 0, v0:real^3} {vv 1}
SUBSET affine hull ({
vec 0, v0}
UNION {vv 1})`;
REWRITE_TAC[
SUBSET];
DISCH_THEN NHANH;
SIMP_TAC[INSERT_UNION2;
UNION_EMPTY];
STRIP_TAC;
SUBGOAL_THEN` {vv n | i <= n /\ n < k}
SUBSET aff_gt {
vec 0, v0:real^3} {vv (k - 1)}` ASSUME_TAC;
REWRITE_TAC[
SUBSET;
IN_ELIM_THM];
REPEAT STRIP_TAC;
SUBGOAL_THEN`
azim (
vec 0) v0 (vv 1) x =
azim (
vec 0) v0 (vv 1) (vv (k - 1))` ASSUME_TAC;
ASM_CASES_TAC` n = i:num`;
ASM_REWRITE_TAC[];
ASM_CASES_TAC` n = k - 1 `;
ASM_REWRITE_TAC[];
UNDISCH_TAC` !i j. i < j /\ j < k ==> bta i <= (bta:num ->
real) j`;
STRIP_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [`i:num`;` n:num`]));
ANTS_TAC;
ASM_ARITH_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [`n:num`;`k - 1`]));
ANTS_TAC;
ASM_ARITH_TAC;
ASM_REWRITE_TAC[];
REAL_ARITH_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`v0:real^3`;`1`]));
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`v0:real^3`;`n:num`]));
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`v0:real^3`;`k - 1`]));
FIRST_ASSUM (MP_TAC o (SPECL [`0`;`n:num`]));
PHA;
ANTS_TAC;
ASM_REWRITE_TAC[];
ASM_ARITH_TAC;
FIRST_ASSUM (MP_TAC o (SPECL [`0`;` k - 1`]));
ANTS_TAC;
ASM_REWRITE_TAC[];
ASM_ARITH_TAC;
ANTS_TAC;
ASM_REWRITE_TAC[];
ASM_ARITH_TAC;
REWRITE_TAC[
ITER];
ASM_REWRITE_TAC[];
ASSUME_TAC2
LOCAL_FAN_CHARACTER_OF_RHO_NODE;
FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC`v0: real^3`));
SUBGOAL_THEN`
rho_node1 FF v0 =
ITER 1 (
rho_node1 FF) v0` MP_TAC;
REWRITE_TAC[
ITER12];
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
UNDISCH_TAC`
ITER 1 (
rho_node1 FF) v0
IN V `;
UNDISCH_TAC`
ITER n (
rho_node1 FF) v0
IN V `;
UNDISCH_TAC`
ITER (k - 1) (
rho_node1 FF) v0
IN V `;
UNDISCH_TAC` ~(
rho_node1 FF v0 = v0) /\
v0,
rho_node1 FF v0
IN ord_pairs E /\
~collinear {
vec 0, v0,
rho_node1 FF v0}`;
ASM_REWRITE_TAC[];
REPEAT STRIP_TAC;
UNDISCH_TAC` !v. v
IN V /\ ~(v = v0) ==> ~collinear {
vec 0, v0, v:real^3}`;
STRIP_TAC;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC`(vv:num -> real^3) 1 `));
FIRST_ASSUM (ASSUME_TAC2 o (SPEC`(vv:num -> real^3) n `));
FIRST_ASSUM (ASSUME_TAC2 o (SPEC`(vv:num -> real^3) (k - 1) `));
REPLICATE_TAC 3 DOWN THEN PHA;
NHANH
AZIM_EQ_ALT;
UNDISCH_TAC`
azim (
vec 0) v0 (vv 1) x =
azim (
vec 0) v0 (vv 1) (vv (k - 1))`;
ASM_SIMP_TAC[];
ASM_REWRITE_TAC[];
ABBREV_TAC` v00 =
ITER i (
rho_node1 FF) v0`;
MP_TAC (SPECL [`E:(real^3 -> bool) -> bool`;` V:real^3 -> bool`;
` {
ITER n (
rho_node1 FF) v00 | n <= k - i}`;`
affine hull {
vec 0, v0:real^3, vv (k - 1)}`;
` k - i:num`;` FF:real^3 # real^3 -> bool`;` v00: real^3`]
(GEN_ALL
CNVX_IMP_INTERIOR_ANGLE_PI));
ANTS_TAC;
ASM_REWRITE_TAC[];
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`v0:real^3`;`i:num`]));
DOWN;
FIRST_ASSUM SUBST1_TAC;
SIMP_TAC[Trigonometry2.IN_P_HULL_INSERT];
FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`v0:real^3`;`k - 1`]));
FIRST_ASSUM (MP_TAC o (SPECL [`0`;`k - 1`]));
ANTS_TAC;
MATCH_MP_TAC
LT_TRANS;
EXISTS_TAC `i:num`;
ASM_REWRITE_TAC[];
ANTS_TAC;
ASM_REWRITE_TAC[];
UNDISCH_TAC` i < k - 1`;
ARITH_TAC;
REWRITE_TAC[
ITER];
DOWN;
ASM_REWRITE_TAC[];
STRIP_TAC THEN STRIP_TAC;
SUBGOAL_THEN` ~
collinear {
vec 0, v0:real^3, vv (k - 1)}` ASSUME_TAC;
DOWN THEN DOWN THEN PHA;
ASM_REWRITE_TAC[];
STRIP_TAC THEN CONJ_TAC;
REWRITE_TAC[
plane];
DOWN THEN DOWN;
MESON_TAC[];
ASSUME_TAC (ISPECL [`{
vec 0, v0:real^3}`;`{(vv:num -> real^3) (k - 1)}`]
AFF_GT_SUBSET_AFFINE_HULL);
REWRITE_TAC[
SUBSET;
IN_ELIM_THM];
REPEAT STRIP_TAC;
ASM_CASES_TAC` n = k - (i:num)`;
ASM_REWRITE_TAC[];
EXPAND_TAC "v00";
ASSUME_TAC2 (ARITH_RULE` i < k - 1 ==> k - i + i = (k:num) `);
ASM_REWRITE_TAC[ITER_ADD];
ASSUME_TAC2 LOFA_IMP_ITER_RHO_NODE_ID;
FIRST_ASSUM (ASSUME_TAC2 o (SPEC`v0:real^3`));
DOWN;
ONCE_REWRITE_TAC[INSERT_COMM];
ASM_REWRITE_TAC[];
ASM_SIMP_TAC[Trigonometry2.IN_P_HULL_INSERT];
UNDISCH_TAC` aff_gt {vec 0, v0:real^3} {vv (k - 1)} SUBSET
affine hull ({vec 0, v0} UNION {vv (k - 1)})`;
REWRITE_TAC[INSERT_UNION2; UNION_EMPTY; INSERT_COMM; SUBSET];
DISCH_THEN MATCH_MP_TAC;
UNDISCH_TAC` {vv n | i <= n /\ n < k} SUBSET aff_gt {vec 0, v0:real^3} {vv (k - 1)}`;
REWRITE_TAC[SUBSET; IN_ELIM_THM; INSERT_COMM];
DISCH_THEN MATCH_MP_TAC;
EXISTS_TAC `n + i:num`;
ASM_REWRITE_TAC[];
EXPAND_TAC "v00";
REWRITE_TAC[ITER_ADD];
ASM_REWRITE_TAC[];
DOWN;
UNDISCH_TAC` n <= k - (i:num)`;
ARITH_TAC;
STRIP_TAC THEN GEN_TAC;
STRIP_TAC;
FIRST_X_ASSUM (MP_TAC o (SPEC` j - (i:num)`));
ANTS_TAC;
DOWN THEN DOWN;
ARITH_TAC;
EXPAND_TAC "v00";
REWRITE_TAC[ITER_ADD];
UNDISCH_TAC` i < j:num`;
NHANH (ARITH_RULE` a < b:num ==> b - a + a = b `);
ASM_SIMP_TAC[]]);;
end;;