(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* Section: Conclusions *) (* Chapter: Local Fan *) (* Lemma: ZLZTHIC *) (* Author: Thomas Hales *) (* Date: 2013-07-10 *) (* ========================================================================== *) module Zlzthic = struct open Hales_tactic;; let FOR_ASM th = let th1 = REWRITE_RULE[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] th in let th2 = SPEC_ALL th1 in UNDISCH_ALL th2;; let ASSUME_TAC2 = ASSUME_TAC o FOR_ASM;; let DOWN = FIRST_X_ASSUM MP_TAC;; let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;; let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (SPEC_ALL ( tm ))];; let SWITCH_TAC tm = UNDISCH_TAC tm THEN DISCH_THEN (ASSUME_TAC o GSYM);; let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `; MESON[]` a ==> b ==> c <=> a /\ b ==> c `];; let NONCOLLINEAR_OPEN = Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR;; let NONPLANAR_OPEN = prove_by_refinement( `!(v1:real->real^3) v2 v3 v4 t. ~coplanar {v1 t,v2 t,v3 t, v4 t} /\ v1 continuous atreal t /\ v2 continuous atreal t /\ v3 continuous atreal t /\ v4 continuous atreal t ==> (?e. &0 < e /\ !t'. abs(t - t') < e ==> ~coplanar {v1 t', v2 t' ,v3 t',v4 t'})`, (* {{{ proof *) [ REWRITE_TAC[Oxlzlez.coplanar_delta_y]; REPEAT WEAKER_STRIP_TAC; TYPIFY `(\t. delta_y (dist (v1 t,v2 t)) (dist (v1 t,v3 t)) (dist (v1 t,v4 t)) (dist (v3 t,v4 t)) (dist (v2 t,v4 t)) (dist (v2 t,v3 t))) real_continuous atreal t` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[real_continuous_atreal]; DISCH_THEN (C INTRO_TAC [`delta_y (dist (v1 t,v2 t)) (dist (v1 t,v3 t)) (dist (v1 t,v4 t)) (dist (v3 t,v4 t)) (dist (v2 t,v4 t)) (dist (v2 t,v3 t))`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `d` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t'`]); ASM_REWRITE_TAC[]; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[Sphere.delta_y;Sphere.delta_x]; BY((REPEAT ( (MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE MATCH_MP_TAC REAL_CONTINUOUS_SUB ORELSE MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE MATCH_MP_TAC REAL_CONTINUOUS_NEG ORELSE MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2_REDO) THEN (REPEAT CONJ_TAC))) THEN ASM_REWRITE_TAC[]) ]);; (* }}} *) let COLL_IFF_COLL_CROSS2 = prove_by_refinement( `!v w. collinear {vec 0, v, w} <=> collinear {vec 0, w, v cross w}`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `s = {vec 0,v,w}`; (ONCE_REWRITE_TAC[CROSS_SKEW]); ONCE_REWRITE_TAC[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`]; (REWRITE_TAC[arith `-- (u:real^3) = (-- &1) % u`]); GMATCH_SIMP_TAC COLLINEAR_SPECIAL_SCALE; (ONCE_REWRITE_TAC[SET_RULE `{vec 0,a,(b:real^3)} = {vec 0,b,a}`]); RULE_ASSUM_TAC( ONCE_REWRITE_RULE[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`]); REWRITE_TAC[arith` ~( -- &1 = &0)`]; BY(ASM_MESON_TAC([Local_lemmas.COLL_IFF_COLL_CROSS])) ]);; (* }}} *) let azim_cross_0 = prove_by_refinement( `!v w. ~(collinear {vec 0,v,w}) ==> ~(azim (vec 0) (v cross w) v w = &0)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; BY(ASM_MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;Local_lemmas.NOT_COLL_IMP_COPL;SET_RULE `{vec 0,v,w,v cross w} = {vec 0,v cross w,v,(w:real^3)}`]) ]);; (* }}} *) let wedge_ge_cross = prove_by_refinement( `!v w. ~collinear {vec 0,v,w} ==> wedge_ge (vec 0) (v cross w) v w = aff_ge {vec 0, v cross w} {v, w}`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC Local_lemmas.WEDGE_GE_EQ_AFF_GE; CONJ_TAC; TYPIFY `&0 < sin(azim (vec 0) (v cross w) v w)` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`]; STRIP_TAC; CONJ_TAC; REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT]; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); BY(ASM_MESON_TAC[SIN_PI;arith `~(&0 < &0)`]); REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS]; ONCE_REWRITE_TAC[CROSS_TRIPLE]; BY(ASM_REWRITE_TAC[DOT_POS_LT;CROSS_EQ_0]); ONCE_REWRITE_TAC[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`]; BY(ASM_MESON_TAC[COLL_IFF_COLL_CROSS2;Local_lemmas.COLL_IFF_COLL_CROSS]) ]);; (* }}} *) let azim_lt_pi_cross = prove_by_refinement( `!u1 u2 u3. (&0 < azim (vec 0) u1 u2 u3 /\ azim(vec 0) u1 u2 u3 < pi) <=> &0 < (u1 cross u2) dot u3`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Trigonometry.JBDNJJB [`u1`;`u2`;`u3`]; ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM]; REWRITE_TAC[Trigonometry2.re_eqvl]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; ASM_CASES_TAC `&0 < sin(azim(vec 0) u1 u2 u3)`; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`]; REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT]; ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`]; CONJ2_TAC; DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_MESON_TAC[SIN_PI;arith `~(&0 < &0)`]); BY(ASM_MESON_TAC[Counting_spheres.AZIM_NN;SIN_0;arith `&0 < x <=> &0 <= x /\ ~(x = &0)`;arith `~(&0 < &0)`]); COMMENT "other direction"; TYPED_ABBREV_TAC `s = sin (azim (vec 0) u1 u2 u3)`; REWRITE_TAC[arith `&0 < t * s <=> ~(&0 <= t* (-- s))`]; GMATCH_SIMP_TAC REAL_LE_MUL; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `~` MP_TAC; EXPAND_TAC "s"; REWRITE_TAC[]; BY(ASM_MESON_TAC[SIN_POS_PI]) ]);; (* }}} *) let generic_alt = prove_by_refinement( `!u v w. ~collinear {vec 0,v,w} /\ ~(u = vec 0) ==> (aff_ge {vec 0} {v,w} INTER aff_lt {vec 0} {u} = {} <=> ~coplanar {vec 0,u,v,w} \/ ((-- u) IN wedge (vec 0) (v cross w) w v))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a = b)`); CONJ_TAC THEN STRIP_TAC; MATCH_MP_TAC (TAUT `(a ==> b ) ==> (~a \/ b)`); DISCH_TAC; GMATCH_SIMP_TAC (GSYM Leaf_cell.WEDGE_GE_COMPLEMENT); REWRITE_TAC[IN_DIFF;IN_UNIV]; ASM_SIMP_TAC[azim_cross_0]; ASM_SIMP_TAC[wedge_ge_cross]; COMMENT "down to three"; GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2; REWRITE_TAC[IN_ELIM_THM;arith `t1 % (vec 0):real^3 = vec 0`]; CONJ_TAC; TYPIFY `DISJOINT {v, w} {vec 0} /\ ~(v cross w = v) /\ ~(v cross w = w)` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[DISJOINT]; BY(SET_TAC[]); CONJ_TAC; MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[CROSS_EQ_SELF]; BY(CONJ_TAC THEN ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,(v:real^3),vec 0} = {vec 0,v} /\ {vec 0,vec 0,(w:real^3)} = {vec 0,w}`]); REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC( REWRITE_RULE[arith `-- (u:real^3) = w <=> u = -- w`] ); FIRST_X_ASSUM_ST `aff_ge` MP_TAC; REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;NOT_FORALL_THM]; TYPIFY `-- (u:real^3)` EXISTS_TAC; CONJ2_TAC; GMATCH_SIMP_TAC AFF_LT_1_1; REWRITE_TAC[IN_ELIM_THM;DISJOINT]; CONJ_TAC; BY(ASM_TAC THEN SET_TAC[]); GEXISTL_TAC [`&2`;`-- &1`]; BY(REPEAT CONJ_TAC THEN TRY REAL_ARITH_TAC THEN VECTOR_ARITH_TAC); RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas.CROSS_DOT_COPLANAR]); RULE_ASSUM_TAC(ONCE_REWRITE_RULE[CROSS_TRIPLE]); FIRST_X_ASSUM_ST `x = &0` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[DOT_RNEG;DOT_RADD;DOT_RMUL]; REWRITE_TAC[DOT_RZERO]; REWRITE_TAC[DOT_CROSS_SELF]; (REWRITE_TAC[arith `--(&0 + t2 * a + t3 * &0 + t4 * &0) = &0 <=> t2 * a = &0`]); REWRITE_TAC[REAL_ENTIRE]; ASM_SIMP_TAC[DOT_POS_LT;CROSS_EQ_0;arith `&0 < x ==> ~(x = &0)`]; DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); REWRITE_TAC[arith `-- --(vec 0 + &0 % a + b + (c:real^3)) = b + c`]; GMATCH_SIMP_TAC AFF_GE_1_2; CONJ_TAC; ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[IN_ELIM_THM]; GEXISTL_TAC [`t1`;`t3`;`t4`]; ASM_REWRITE_TAC[]; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(VECTOR_ARITH_TAC); COMMENT "second case"; REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER]; GMATCH_SIMP_TAC AFF_GE_1_2; CONJ_TAC; ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[IN_ELIM_THM]; GMATCH_SIMP_TAC Nkezbfc_local.AFF_LT_1_1; ASM_REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas.CROSS_DOT_COPLANAR]); RULE_ASSUM_TAC(ONCE_REWRITE_RULE[CROSS_TRIPLE]); TYPIFY `(v cross w) dot (t1 % vec 0 + t2 % v + t3 % w) = (v cross w) dot (t1' % vec 0 + t2' % u)` (C SUBGOAL_THEN MP_TAC); BY(ASM_MESON_TAC[]); REWRITE_TAC[DOT_RNEG;DOT_RADD;DOT_RMUL;DOT_RZERO;DOT_CROSS_SELF]; TYPIFY `~(t2' * ((v cross w) dot u) = &0)` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); ASM_REWRITE_TAC[REAL_ENTIRE]; BY(ASM_TAC THEN REAL_ARITH_TAC); COMMENT "third and final case"; REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER]; GMATCH_SIMP_TAC AFF_GE_1_2; CONJ_TAC; ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[IN_ELIM_THM]; GMATCH_SIMP_TAC Nkezbfc_local.AFF_LT_1_1; ASM_REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `x IN wedge (vec 0) (v cross w) w v` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `wedge` MP_TAC; REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM]; FIRST_X_ASSUM SUBST1_TAC; TYPIFY `t1' % vec 0 + t2' % u = (-- t2') % (-- u)` (C SUBGOAL_THEN SUBST1_TAC); BY(VECTOR_ARITH_TAC); FIRST_X_ASSUM_ST `t < &0` MP_TAC; BY(MESON_TAC[AZIM_SCALE_ALL;arith `&0 < &1`;arith `t < &0 ==> &0 < -- t`;arith `&1 % (v:real^3) = v`]); FIRST_X_ASSUM_ST `x = y` kill; TYPIFY `~(x IN wedge (vec 0) (v cross w) w v)` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC (GSYM Leaf_cell.WEDGE_GE_COMPLEMENT); (REWRITE_TAC[IN_DIFF;IN_UNIV]); ASM_SIMP_TAC[azim_cross_0]; ASM_SIMP_TAC[wedge_ge_cross]; GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2; REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; TYPIFY `DISJOINT {v, w} {vec 0} /\ ~(v cross w = v) /\ ~(v cross w = w)` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[DISJOINT]; BY(SET_TAC[]); CONJ_TAC; MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[CROSS_EQ_SELF]; BY(CONJ_TAC THEN ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,(v:real^3),vec 0} = {vec 0,v} /\ {vec 0,vec 0,(w:real^3)} = {vec 0,w}`]); GEXISTL_TAC [`t1`;`&0`;`t2`;`t3`]; REPEAT CONJ_TAC THEN ASM_TAC THEN TRY REAL_ARITH_TAC; BY(REPEAT WEAKER_STRIP_TAC THEN VECTOR_ARITH_TAC); BY(ASM_MESON_TAC[]) ]);; (* }}} *) let vuy1 = prove_by_refinement( `!v u0 u1. ~collinear {vec 0,u0,v} /\ ~collinear {vec 0,u0,u1} /\ v IN aff_ge {vec 0,u0} {u1} ==> (?t0 t1. &0 < t1 /\ v = t0 % u0 + t1 % u1)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `aff_ge` MP_TAC; GMATCH_SIMP_TAC AFF_GE_2_1; REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; ASM_SIMP_TAC[Fan.th3a]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; GEXISTL_TAC [`t2`;`t3`]; CONJ_TAC; PROOF_BY_CONTR_TAC; TYPIFY `t3 = &0` (C SUBGOAL_THEN MP_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); TYPIFY `v = t2 % u0` (C SUBGOAL_THEN MP_TAC); BY(ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC); DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]); BY(VECTOR_ARITH_TAC) ]);; (* }}} *) let DISJOINT_PAIR = prove_by_refinement( `!a b c. DISJOINT a {b,c} <=> DISJOINT a {b} /\ DISJOINT a {c}`, (* {{{ proof *) [ REWRITE_TAC[DISJOINT]; BY(SET_TAC[]) ]);; (* }}} *) let vuy2 = prove_by_refinement( `!v u0 u1. ~collinear {vec 0, u0, v} /\ ~collinear {vec 0, u0, u1} /\ v IN aff_ge {vec 0, u0} {u1} ==> (u0 cross u1) dot v = &0`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC vuy1 [`v`;`u0`;`u1`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_CROSS_SELF]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let vuy3 = prove_by_refinement( `!v u0 u1. ~collinear {vec 0, u0, v} /\ ~collinear {vec 0, u0, u1} /\ v IN aff_ge {vec 0, u0} {u1} ==> ~collinear {vec 0,u0 cross u1, v}`, (* {{{ proof *) [ REPEAT GEN_TAC; DISCH_TAC; REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM]; SUBCONJ_TAC; BY(ASM_REWRITE_TAC[CROSS_EQ_0]); ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; INTRO_TAC vuy1 [`v`;`u0`;`u1`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `v dot v = c % (u0 cross u1) dot (t0 % u0 + t1 % u1)` (C SUBGOAL_THEN MP_TAC); BY(ASM_MESON_TAC[]); REWRITE_TAC[DOT_RMUL;DOT_LMUL;DOT_RADD;DOT_CROSS_SELF]; TYPIFY ` c * (t0 * &0 + t1 * &0) = &0` (C SUBGOAL_THEN SUBST1_TAC); BY(REAL_ARITH_TAC); REWRITE_TAC[DOT_EQ_0]; DISCH_TAC; BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,u0,vec 0} = {vec 0,(u0:real^3)}`]) ]);; (* }}} *) let vuy4 = prove_by_refinement( `!v u0 u1. ~collinear {vec 0, u0, v} /\ ~collinear {vec 0, u0, u1} /\ v IN aff_ge {vec 0, u0} {u1} ==> azim (vec 0) (u0 cross u1) u0 v < pi`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `&0 < ((u0 cross u1) cross u0) dot v` ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[azim_lt_pi_cross]); INTRO_TAC vuy1 [`v`;`u0`;`u1`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; ONCE_REWRITE_TAC[CROSS_TRIPLE]; ASM_REWRITE_TAC[]; REWRITE_TAC[CROSS_RMUL;DOT_LMUL;CROSS_RADD;DOT_CROSS_SELF;CROSS_REFL;arith `t % vec 0 + (a:real^3) = a`]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; BY(ASM_REWRITE_TAC[DOT_POS_LT;CROSS_EQ_0]) ]);; (* }}} *) let vuy5 = prove_by_refinement( `!v u0 u1. ~collinear {vec 0, u0, u1} ==> u0 IN aff_ge {vec 0,u0} {u1}`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC AFF_GE_2_1; ASM_SIMP_TAC[Fan.th3a]; REWRITE_TAC[IN_ELIM_THM]; GEXISTL_TAC [`&0`;`&1`;`&0`]; REPEAT CONJ_TAC THEN TRY REAL_ARITH_TAC; BY(VECTOR_ARITH_TAC) ]);; (* }}} *) let cross_independent = prove_by_refinement( `!u0 u1 a b c. ~collinear {vec 0,u0,u1} /\ a % (u0 cross u1) + b % u0 + c % u1 = vec 0 ==> a = &0`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY ` (u0 cross u1) dot ( (--b) % u0 + (--c) % u1 ) = a * ((u0 cross u1) dot (u0 cross u1))` (C SUBGOAL_THEN MP_TAC); REWRITE_TAC[GSYM DOT_RMUL]; TYPIFY `a % (u0 cross u1) = -- b % u0 + -- c % u1` ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[]); BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC); REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_RZERO;DOT_CROSS_SELF]; REWRITE_TAC[arith `-- b * &0 + -- c * &0 = x <=> x = &0`]; REWRITE_TAC[REAL_ENTIRE;DOT_EQ_0]; BY(ASM_REWRITE_TAC[CROSS_EQ_0]) ]);; (* }}} *) let ybt_inj = prove_by_refinement( `!u0 u1 v1 v2 . ~collinear {vec 0, u0, v1} /\ ~collinear {vec 0, u0, v2} /\ ~collinear {vec 0, u0, u1} /\ ~collinear {vec 0,v1,v2} /\ v1 IN aff_ge {vec 0, u0} {u1} /\ v2 IN aff_ge {vec 0, u0} {u1} ==> ~( azim (vec 0) (u0 cross u1) u0 v1 = azim (vec 0) (u0 cross u1) u0 v2) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Topology.th [`(vec 0):real^3`;`u0 cross u1`;`u0`;`v2`]; REWRITE_TAC[EXTENSION;IN_ELIM_THM]; DISCH_THEN MP_TAC THEN ANTS_TAC; ASM_SIMP_TAC[vuy3]; ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`]; BY(ASM_MESON_TAC[Local_lemmas.COLL_IFF_COLL_CROSS]); DISCH_THEN (C INTRO_TAC [`v1`]); ASM_SIMP_TAC[vuy3]; DISCH_TAC; INTRO_TAC vuy1 [`v1`;`u0`;`u1`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `aff_gt` MP_TAC; REWRITE_TAC[]; GMATCH_SIMP_TAC AFF_GT_2_1; CONJ_TAC; REWRITE_TAC[DISJOINT;EXTENSION;IN_INTER;IN_SING;IN_INSERT;NOT_IN_EMPTY]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); FIRST_X_ASSUM DISJ_CASES_TAC; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,a}= {a,(b:real^3)}`]); FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); FIRST_X_ASSUM_ST `aff_ge` MP_TAC; REWRITE_TAC[]; GMATCH_SIMP_TAC AFF_GE_2_1; ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `(-- &1) % (u0 cross u1) + t2 % u0 + t3 % u1 = vec 0` (C SUBGOAL_THEN MP_TAC); BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC); BY(ASM_MESON_TAC[cross_independent;arith `~(-- &1 = &0)`]); REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `v1 = t3 % v2` ENOUGH_TO_SHOW_TAC; DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_MESON_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`;COLLINEAR_LEMMA_ALT]); PROOF_BY_CONTR_TAC; FIRST_X_ASSUM_ST `aff_ge` MP_TAC; REWRITE_TAC[]; GMATCH_SIMP_TAC AFF_GE_2_1; ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `x:real^3` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); FIRST_X_ASSUM_ST `v1 = t1' % ((vec 0):real^3) + c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); RULE_ASSUM_TAC(REWRITE_RULE[VECTOR_MUL_ASSOC;VECTOR_ADD_LDISTRIB]); TYPIFY `t2 % (u0 cross u1) + (t3 * t2' - t0) % u0 + (t3*t3' - t1) % u1 = vec 0` (C SUBGOAL_THEN MP_TAC); REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `x:real^3` MP_TAC); ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`]; DISCH_TAC; BY(VECTOR_ARITH_TAC); DISCH_TAC; TYPIFY `t2 = &0` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[cross_independent]); FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); FIRST_X_ASSUM kill; FIRST_X_ASSUM_ST `x:real^3` MP_TAC; BY(VECTOR_ARITH_TAC) ]);; (* }}} *) let ybt_inj_0 = prove_by_refinement( `!u0 u1 v2 . ~collinear {vec 0, u0, v2} /\ ~collinear {vec 0, u0, u1} /\ v2 IN aff_ge {vec 0, u0} {u1} ==> ~( azim (vec 0) (u0 cross u1) u0 v2 = &0) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; GMATCH_SIMP_TAC Local_lemmas.AZIM_EQ_0_GE_ALT2; CONJ_TAC; ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`]; BY(ASM_MESON_TAC[Local_lemmas.COLL_IFF_COLL_CROSS]); GMATCH_SIMP_TAC AFF_GE_2_1; CONJ_TAC; REWRITE_TAC[DISJOINT;EXTENSION;IN_INTER;IN_SING;IN_INSERT;NOT_IN_EMPTY]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); FIRST_X_ASSUM DISJ_CASES_TAC; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b}= {a,(b:real^3)}`]); TYPIFY `u0 dot u0 = (u0 cross u1) dot u0` (C SUBGOAL_THEN MP_TAC); BY(ASM_MESON_TAC[]); REWRITE_TAC[DOT_CROSS_SELF]; REWRITE_TAC[DOT_EQ_0]; DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b}= {a,(b:real^3)}`]); REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `aff_ge` MP_TAC; REWRITE_TAC[]; GMATCH_SIMP_TAC AFF_GE_2_1; ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `t2 % (u0 cross u1) + (t3 - t2') % u0 + (-- t3') % u1 = vec 0` (C SUBGOAL_THEN MP_TAC); BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC); DISCH_TAC; TYPIFY `t2 = &0` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[cross_independent]); FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); REPLICATE_TAC 4 (FIRST_X_ASSUM kill); TYPIFY `v2 = t3 % u0` (C SUBGOAL_THEN ASSUME_TAC); BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC); FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]) ]);; (* }}} *) let ECAU_aff_ge = prove_by_refinement( `!(u:num->real^3) r. (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) ==> (!i. 1 <= i /\ i <= r ==> u i IN aff_ge {vec 0,u 0 } {u 1} ) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `u i IN aff_gt {vec 0,u 0} {u 1}` (C SUBGOAL_THEN MP_TAC); ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); INTRO_TAC AFF_GT_SUBSET_AFF_GE [`{vec 0,u 0}`;`{u 1}`]; BY(SET_TAC[]) ]);; (* }}} *) let collinear_cross = prove_by_refinement( `!u i r. i <= r /\ 1 <= r /\ (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) ==> ~collinear {vec 0,u 0 cross u 1,u i}`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; TYPIFY `i = 0` ASM_CASES_TAC; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`]; REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN ARITH_TAC); INTRO_TAC ECAU_aff_ge [`u`;`r`]; ASM_REWRITE_TAC[]; DISCH_TAC; MATCH_MP_TAC vuy3; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN TRY ARITH_TAC) ]);; (* }}} *) let YBTASCZ1 = prove_by_refinement( `!u r j. (j <= r) /\ (1<= r) /\ (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\ cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\ (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==> (!i. i < j ==> azim (vec 0) ((u 0) cross (u 1)) (u 0) (u i) < azim (vec 0) (u 0 cross (u 1)) (u 0) (u j)) `, (* {{{ proof *) [ REPEAT GEN_TAC; DISCH_TAC; INTRO_TAC ECAU_aff_ge [`u`;`r`]; ASM_REWRITE_TAC[]; DISCH_TAC; INDUCT_TAC; DISCH_TAC; REWRITE_TAC[arith `a < b <=> (a <= b /\ ~(a = b))`]; CONJ_TAC; BY(REWRITE_TAC[AZIM_REFL;Local_lemmas.AZIM_RANGE]); REWRITE_TAC[AZIM_REFL]; ONCE_REWRITE_TAC[EQ_SYM_EQ]; MATCH_MP_TAC ybt_inj_0; ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; BY(REPEAT CONJ_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_TAC THEN TRY ARITH_TAC); COMMENT "induction step"; ONCE_REWRITE_TAC[arith `a < b <=> ~(b < a) /\ ~(a = b)`]; REPEAT WEAKER_STRIP_TAC; CONJ2_TAC; MATCH_MP_TAC ybt_inj; ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; BY(REPEAT CONJ_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_TAC THEN TRY ARITH_TAC); DISCH_TAC; TYPIFY `i < (j:num)` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) = u (i+1)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_TAC THEN ARITH_TAC); INTRO_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`{u i | (i:num) <= r}`;`u i`;`u 0 cross u 1`;`(vec 0):real^3`]; ANTS_TAC; CONJ_TAC; REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_SING]; TYPIFY `1 <= r` (C SUBGOAL_THEN MP_TAC); BY(ASM_REWRITE_TAC[]); TYPIFY (`~(u 0 = u 1)`) ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[arith `1 <= r ==> 0 <= r /\ 1 <= r`]); DISCH_TAC; FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]); ANTS_TAC; BY(ASM_TAC THEN ARITH_TAC); ASM_REWRITE_TAC[]; BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}= {a,(b:real^3)}`]); TYPIFY `{u i | i <= r } = IMAGE u {i | i <= (r:num)}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); MATCH_MP_TAC FINITE_IMAGE; BY(REWRITE_TAC[FINITE_NUMSEG_LE]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`u j`]); ANTS_TAC; CONJ_TAC; DISCH_TAC; FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`j`;`i`]); ANTS_TAC; BY(ASM_TAC THEN ARITH_TAC); ASM_REWRITE_TAC[]; BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}= {a,(b:real^3)}`]); TYPIFY_GOAL_THEN `(j:num) <=r ==> {u i | i <= r} (u j)` MATCH_MP_TAC; TYPIFY `{u i | i <= r } = IMAGE u {i | i <= (r:num)}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); REWRITE_TAC[IMAGE;IN_ELIM_THM]; BY(MESON_TAC[]); BY(ASM_TAC THEN ARITH_TAC); REWRITE_TAC[arith `i+1 = SUC i`]; REWRITE_TAC[DE_MORGAN_THM]; PROOF_BY_CONTR_TAC; COMMENT "shift"; FIRST_X_ASSUM_ST `(i:num) < j ==> b` MP_TAC; ASM_REWRITE_TAC[]; DISCH_TAC; FIRST_ASSUM MP_TAC; REWRITE_TAC[]; ONCE_REWRITE_TAC[arith `a < b <=> &0 < b - a`]; GMATCH_SIMP_TAC Leaf_cell.AZIM_BASE_SHIFT_LE; TYPIFY `u i` EXISTS_TAC; (ASM_SIMP_TAC[arith `x <= x` ;arith `x < y ==> x <= y`]); CONJ_TAC; BY(REPEAT (GMATCH_SIMP_TAC collinear_cross) THEN REPEAT CONJ_TAC THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC); REWRITE_TAC[arith `&0 < a - b <=> b < a`]; DISCH_TAC; COMMENT "second shift"; TYPIFY `azim (vec 0) (u 0 cross u 1) (u i) (u j) < azim (vec 0) (u 0 cross u 1) (u i) (u (SUC i))` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `SUC` kill; FIRST_ASSUM_ST `SUC` MP_TAC; ONCE_REWRITE_TAC[arith `a < b <=> &0 < b - a`]; MATCH_MP_TAC (arith `a = b ==> &0 < a ==> &0 < b`); MATCH_MP_TAC Leaf_cell.AZIM_BASE_SHIFT_LE; (ASM_SIMP_TAC[arith `x <= x` ;arith `x < y ==> x <= y`]); REWRITE_TAC[TAUT `(a /\ b /\ c) <=> ((a /\ b) /\ c)`]; CONJ2_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REPEAT (GMATCH_SIMP_TAC collinear_cross) THEN REPEAT CONJ_TAC THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let YBTASCZ2 = prove_by_refinement( `!u r i j. (i < j) /\ (j <= r) /\ (1<= r) /\ (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\ cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\ (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==> (azim (vec 0) ((u 0) cross (u 1)) (u i) (u j) < pi) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC YBTASCZ1 [`u`;`r`;`j`]; ASM_REWRITE_TAC[]; DISCH_THEN (C INTRO_TAC [`i`]); ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC Fan.sum4_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`;`u j`]; ANTS_TAC; ASM_SIMP_TAC[arith `x < y ==> x <= y`]; BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC collinear_cross THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC); INTRO_TAC vuy4 [`u j`;`u 0`;`u 1`]; ANTS_TAC; INTRO_TAC ECAU_aff_ge [`u`;`r`]; ASM_REWRITE_TAC[]; DISCH_TAC; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN ARITH_TAC); INTRO_TAC Counting_spheres.AZIM_NN [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let YBTASCZ3 = prove_by_refinement( `!u r i j. (i < j) /\ (j <= r) /\ (1<= r) /\ (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\ cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\ (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==> (&0 < azim (vec 0) ((u 0) cross (u 1)) (u i) (u j)) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC YBTASCZ1 [`u`;`r`;`j`]; ASM_REWRITE_TAC[]; DISCH_THEN (C INTRO_TAC [`i`]); ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC Fan.sum4_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`;`u j`]; ANTS_TAC; ASM_SIMP_TAC[arith `x < y ==> x <= y`]; BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC collinear_cross THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let KCZXLLE = prove_by_refinement( `!u r i j k. (j < k) /\ (k <= r) /\ (1<= r) /\ (i <= r) /\ ((i < j \/ k < i)) /\ (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\ cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\ (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==> (azim (vec 0) (u i) (u j) (u k) = &0) `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `?r. j < k /\ k <= r /\ 1 <= r /\ (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0, u 0} {u 1}) /\ cyclic_set {u i | i <= r} (vec 0) (u 0 cross u 1) /\ (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) = u (i + 1))` (C SUBGOAL_THEN ASSUME_TAC); TYPIFY `r` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); INTRO_TAC ECAU_aff_ge [`u`;`r`] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC; COMMENT "planarity"; TYPIFY `!i. i <= r ==> u i IN affine hull {vec 0,u 0,u 1}` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `i' = 0`; MATCH_MP_TAC HULL_INC; ASM_REWRITE_TAC[]; BY(SET_TAC[]); RULE_ASSUM_TAC(REWRITE_RULE[arith `~(i=0) <=> 1<= i`]); REWRITE_TAC[GSYM Trigonometry.UIVNNRR2]; INTRO_TAC (GEN_ALL Local_lemmas.AFF_GT_MONO) [`{vec 0,u 0}`;`{u 1}`;`{u 1}`]; ANTS_TAC; BY(SET_TAC[]); TYPIFY_GOAL_THEN `{vec 0,u 0} UNION {u 1} = {vec 0,u 0,u 1} /\ {u 1} DIFF {u 1} = {}` (unlist REWRITE_TAC); BY(SET_TAC[]); TYPIFY `u i' IN aff_gt {vec 0, u 0} {u 1}` ENOUGH_TO_SHOW_TAC; BY(SET_TAC[]); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); COMMENT "ARITH GOES HERE"; TYPIFY `j <= (r:num)` (C SUBGOAL_THEN ASSUME_TAC); REPLICATE_TAC 10 (FIRST_X_ASSUM kill); BY(ASM_TAC THEN ARITH_TAC); TYPIFY `~(i = j) /\ ~(i = k) /\ 0 <= r` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 6 (FIRST_X_ASSUM kill) THEN ASM_TAC THEN ARITH_TAC); TYPIFY `~(0 = k) /\ (1 <= k) /\ ~(0=1)` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 10 (FIRST_X_ASSUM kill) THEN ASM_TAC THEN ARITH_TAC); COMMENT "other prelims here"; TYPIFY `~collinear {vec 0, u 0, u 1} /\ ~collinear {vec 0,u i,u j} /\ ~collinear {vec 0,u i,u k}` (C SUBGOAL_THEN ASSUME_TAC); BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[arith `~(0=1)`]); TYPIFY `DISJOINT {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC Fan.th3a; BY(ASM_REWRITE_TAC[]); TYPIFY `~collinear {vec 0, u 0, u k} /\ ~collinear {vec 0, u 0, u 1} /\ u k IN aff_ge {vec 0, u 0} {u 1} /\ u k IN aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC); BY((REPEAT CONJ_TAC) THEN (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]); TYPIFY `!i. i <= r ==> ~collinear {vec 0,u 0 cross u 1, u i}` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; ASM_CASES_TAC `i' = 0`; FIRST_X_ASSUM_ST `collinear` MP_TAC; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`]; REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS]; BY(ASM_REWRITE_TAC[]); RULE_ASSUM_TAC (ONCE_REWRITE_RULE[arith `~(i'=0) <=> (1 <= i' /\ ~(i' = 0))`]); FIRST_X_ASSUM_ST `collinear` MP_TAC; REWRITE_TAC[]; MATCH_MP_TAC vuy3; BY((REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[])); COMMENT "standard"; TYPIFY `coplanar {vec 0, u i, u j, u k}` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[coplanar]; GEXISTL_TAC [`(vec 0):real^3`;`u 0`;`u 1`]; REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN (FIRST_X_ASSUM MATCH_MP_TAC ORELSE MATCH_MP_TAC HULL_INC) THEN ASM_REWRITE_TAC[]; BY(REPEAT WEAKER_STRIP_TAC THEN SET_TAC[]); RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR]); FIRST_X_ASSUM DISJ_CASES_TAC; BY(ASM_REWRITE_TAC[]); PROOF_BY_CONTR_TAC THEN FIRST_X_ASSUM kill; INTRO_TAC (GEN_ALL Ldurdpn.LDURDPN) [`u i`;`u j`;`u k`]; ANTS_TAC; BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; REWRITE_TAC[DE_MORGAN_THM]; DISJ2_TAC; TYPIFY `conv0 {u j,u k} SUBSET aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC); ASM_CASES_TAC `j=0`; ASM_REWRITE_TAC[Geomdetail.CONV0_SET2;SUBSET;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC AFF_GT_2_1; ASM_REWRITE_TAC[IN_ELIM_THM]; INTRO_TAC vuy1 [`u k`;`u 0`;`u 1`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; GEXISTL_TAC [`&1 - a - b * (t0 + t1)`;`a + b * t0`;`b*t1`]; GMATCH_SIMP_TAC REAL_LT_MUL_EQ; ASM_REWRITE_TAC[]; CONJ_TAC; BY(REAL_ARITH_TAC); BY(VECTOR_ARITH_TAC); COMMENT "~(j=0)"; MATCH_MP_TAC SUBSET_TRANS; TYPIFY `conv {u j,u k}` EXISTS_TAC; REWRITE_TAC[Geomdetail.CONV02_SU_CONV2]; MATCH_MP_TAC Geomdetail.CONVEX_IM_CONV2_SU; ASM_REWRITE_TAC[CONVEX_AFF_GT]; RULE_ASSUM_TAC(REWRITE_RULE[arith `~(j=0) <=> 1<=j`]); BY( FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INTER;NOT_IN_EMPTY]; REWRITE_TAC[TAUT `~(a /\ b) <=> (b ==> ~a)`]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `aff` MP_TAC; REWRITE_TAC[Trigonometry2.AFF2_VEC0;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `k' % u i IN aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN MP_TAC); BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]); REWRITE_TAC[]; GMATCH_SIMP_TAC AFF_GT_2_1; ASM_REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `~(i = 0)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_TAC; FIRST_X_ASSUM_ST `%` MP_TAC; ASM_REWRITE_TAC[]; TYPIFY `~collinear {vec 0, u 0, u 1}` (C SUBGOAL_THEN MP_TAC); BY(ASM_REWRITE_TAC[]); REWRITE_TAC[COLLINEAR_LEMMA_ALT]; REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`(inv t3 * (k' - t2))`]); REWRITE_TAC[]; TYPIFY `t3 % u 1 = t3 % (inv t3 * (k' - t2)) % u 0` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[VECTOR_MUL_LCANCEL]; DISCH_THEN DISJ_CASES_TAC; BY(FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)) THEN FIRST_X_ASSUM_ST `&0 < &0` MP_TAC THEN REAL_ARITH_TAC); BY(FIRST_X_ASSUM ACCEPT_TAC); FIRST_X_ASSUM MP_TAC; REWRITE_TAC[VECTOR_MUL_ASSOC]; TYPIFY `(t3 * inv t3 * (k' - t2)) = k' - t2` (C SUBGOAL_THEN SUBST1_TAC); Calc_derivative.CALC_ID_TAC; BY(FIRST_X_ASSUM_ST `&0 < t3` MP_TAC THEN REAL_ARITH_TAC); BY(VECTOR_ARITH_TAC); TYPIFY `?t. &0 < t /\ x = t % u i` (C SUBGOAL_THEN MP_TAC); FIRST_X_ASSUM_ST `aff_gt` (C INTRO_TAC [`i`]); (ANTS_TAC); BY(RULE_ASSUM_TAC(REWRITE_RULE[arith `~(i=0) <=> 1 <= i`]) THEN ASM_REWRITE_TAC[]); GMATCH_SIMP_TAC AFF_GT_2_1; ASM_REWRITE_TAC[IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `k'` EXISTS_TAC; ASM_REWRITE_TAC[]; TYPIFY `k' = t3/ t3'` ENOUGH_TO_SHOW_TAC; DISCH_THEN SUBST1_TAC; GMATCH_SIMP_TAC REAL_LT_DIV; BY(ASM_REWRITE_TAC[]); FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); TYPIFY `t3 = k' * t3'` ENOUGH_TO_SHOW_TAC; DISCH_THEN SUBST1_TAC; Calc_derivative.CALC_ID_TAC; BY((FIRST_X_ASSUM_ST `&0 < t` MP_TAC) THEN REAL_ARITH_TAC); PROOF_BY_CONTR_TAC; TYPIFY `(k'*t2' - t2) % u 0 + (k'*t3' - t3) % u 1 = vec 0` (C SUBGOAL_THEN MP_TAC); BY(FIRST_X_ASSUM_ST `%` MP_TAC THEN VECTOR_ARITH_TAC); DISCH_TAC; TYPIFY `inv (k' * t3' - t3) % (k' * t3' - t3) % u 1 = inv(k' * t3' - t3) % (t2 - k' * t2') % u 0` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[VECTOR_MUL_LCANCEL]; DISJ2_TAC; BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC); FIRST_X_ASSUM MP_TAC; REWRITE_TAC[VECTOR_MUL_ASSOC]; TYPIFY `inv (k' * t3' - t3) * (k' * t3' - t3) = &1` (C SUBGOAL_THEN SUBST1_TAC); Calc_derivative.CALC_ID_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); REWRITE_TAC[VECTOR_MUL_LID]; DISCH_TAC; FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]); ANTS_TAC; BY(ASM_REWRITE_TAC[]); BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]); REPEAT WEAKER_STRIP_TAC; (COMMENT "wedge"); TYPIFY `conv0 {u j,u k} SUBSET wedge (vec 0) (u 0 cross u 1) (u j) (u k)` (C SUBGOAL_THEN ASSUME_TAC); TYPIFY `wedge (vec 0) (u 0 cross u 1) (u j) (u k) = aff_gt {vec 0,u 0 cross u 1} {u j,u k}` ENOUGH_TO_SHOW_TAC; DISCH_THEN SUBST1_TAC; REWRITE_TAC[CONV0_AFF_GT]; MATCH_MP_TAC AFF_GT_MONO_LEFT; BY(SET_TAC[]); MATCH_MP_TAC WEDGE_LUNE_GT; TYPIFY_GOAL_THEN `~collinear {vec 0, u 0 cross u 1, u j}` (unlist REWRITE_TAC); ASM_CASES_TAC `j= 0`; ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`]; REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS]; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); GMATCH_SIMP_TAC YBTASCZ3; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC YBTASCZ2; BY(ASM_REWRITE_TAC[]); TYPIFY `x IN wedge (vec 0) (u 0 cross u 1) (u j) (u k)` (C SUBGOAL_THEN MP_TAC); BY(REPEAT (FIRST_X_ASSUM_ST `conv0` MP_TAC) THEN SET_TAC[]); REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM]; FIRST_X_ASSUM_ST `x = (y:real^3)` SUBST1_TAC; TYPIFY `azim (vec 0) (u 0 cross u 1) (u j) (t % u i) = azim (vec 0) (u 0 cross u 1) (u j) (u i)` (C SUBGOAL_THEN SUBST1_TAC); FIRST_X_ASSUM_ST `&0 < t` MP_TAC; BY(MESON_TAC[AZIM_SCALE_ALL;arith `&0 < &1`;arith `&1 % v = v`]); COMMENT "two cases"; REWRITE_TAC[DE_MORGAN_THM]; DISJ2_TAC; FIRST_X_ASSUM DISJ_CASES_TAC; REWRITE_TAC[arith `~(a < b) <=> b <= a`]; MATCH_MP_TAC REAL_LE_TRANS; TYPIFY `pi` EXISTS_TAC; SUBCONJ_TAC; MATCH_MP_TAC (arith `x < pi ==> x <= pi`); MATCH_MP_TAC YBTASCZ2; EXISTS_TAC `r:num`; BY(ASM_REWRITE_TAC[]); DISCH_TAC; ONCE_REWRITE_TAC[Rogers.AZIM_COMPL_EXT]; COND_CASES_TAC; TYPIFY `&0 < azim (vec 0) (u 0 cross u 1) (u i) (u j)` ENOUGH_TO_SHOW_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); MATCH_MP_TAC YBTASCZ3; TYPIFY `r` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); MATCH_MP_TAC (arith `x < pi ==> pi <= &2 * pi - x`); MATCH_MP_TAC YBTASCZ2; EXISTS_TAC `r:num`; BY(ASM_REWRITE_TAC[]); COMMENT "last case"; REWRITE_TAC[arith `~(a < b) <=> b <= a`]; INTRO_TAC Fan.sum3_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u j`;`u k`;`u i`]; ANTS_TAC; CONJ_TAC; MATCH_MP_TAC (arith `x < pi /\ y < pi ==> x + y < &2 * pi`); CONJ_TAC THEN (MATCH_MP_TAC YBTASCZ2); TYPIFY `r` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); TYPIFY `r` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); TYPIFY `&0 <= azim (vec 0) (u 0 cross u 1) (u k) (u i)` ENOUGH_TO_SHOW_TAC; BY(REAL_ARITH_TAC); BY(REWRITE_TAC[Counting_spheres.AZIM_NN]) ]);; (* }}} *) let KCZXLLE_SYM = prove_by_refinement( `!u r i j k. k <= r /\ j <= r /\ 1 <= r /\ i <= r /\ ((j < k /\ (i < j \/ k < i)) \/ (k < j /\ (i < k \/ j < i))) /\ (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0, u 0} {u 1}) /\ cyclic_set {u i | i <= r} (vec 0) (u 0 cross u 1) /\ (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) = u (i + 1)) ==> azim (vec 0) (u i) (u j) (u k) = &0`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM DISJ_CASES_TAC; MATCH_MP_TAC KCZXLLE; TYPIFY `r` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); ONCE_REWRITE_TAC[Local_lemmas.AZIM_EQ_0_SYM2]; MATCH_MP_TAC KCZXLLE; TYPIFY `r` EXISTS_TAC; BY(ASM_REWRITE_TAC[]) ]);; (* }}} *) let open_continuous_eps = prove_by_refinement( `!U f t a b. (t IN real_interval (a,b)) /\ f t IN U /\ (!x. x IN real_interval (a,b) ==> f real_continuous atreal x) /\ real_open U ==> (?e. &0 < e /\ (!x. abs (x-t) < e ==> f x IN U))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Pent_hex.continuous_preimage_open [`f`;`real_interval (a,b)`;`U`]; ASM_REWRITE_TAC[]; ANTS_TAC; BY(ASM_SIMP_TAC[ Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT ]); REWRITE_TAC[real_open;IN_ELIM_THM]; DISCH_THEN (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; BY(ASM_MESON_TAC[]) ]);; (* }}} *) let coplanar_in_affine_hull = prove_by_refinement( `!(u:real^A) v w x. ~collinear {u,v,w} /\ coplanar {x,u,v,w} ==> x IN affine hull {u,v,w}`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Counting_spheres.NOT_COLLINEAR_AFF_DIM_2 [`u`;`v`;`w`]; ASM_REWRITE_TAC[] THEN DISCH_TAC; MATCH_MP_TAC Leaf_cell.COPLANAR_INSERT; BY(ASM_REWRITE_TAC[]) ]);; (* }}} *) let azim_0_as_closed = prove_by_refinement( `!(v2:real^3) v3 v4. ~collinear {vec 0, v2,v3} /\ ~collinear {vec 0,v2,v4} ==> (azim (vec 0) v2 v3 v4 = &0 <=> (coplanar {vec 0,v2,v3,v4} /\ &0 <= ((v2 cross v3) cross v2) dot v4))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `~coplanar {vec 0,v2,v3,v4}` ASM_CASES_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[]) THEN ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[AZIM_EQ_0_PI_IMP_COPLANAR]); INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`v2`;`v3`;`v4`]; ANTS_TAC; ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,c,d,a}`]; BY(ASM_REWRITE_TAC[]); DISCH_TAC; INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`v2`;`v3`;`v4`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `&0 <= ((v2 cross v3) cross v2) dot v4 <=> &0 <= t2` (C SUBGOAL_THEN SUBST1_TAC); ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL]; ONCE_REWRITE_TAC[CROSS_TRIPLE]; REWRITE_TAC[CROSS_REFL;DOT_LZERO]; REWRITE_TAC[arith `t1 * &0 + c = c`]; GMATCH_SIMP_TAC (CONJUNCT2 REAL_LE_MUL_EQ); REWRITE_TAC[DOT_POS_LT]; BY(ASM_REWRITE_TAC[CROSS_EQ_0]); TYPIFY `azim (vec 0) v2 v3 v4 = &0 <=> ~(azim (vec 0) v2 v3 v4 = pi)` (C SUBGOAL_THEN SUBST1_TAC); BY(ASM_MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;PI_POS;arith `&0 < pi ==> ~(&0 = pi)`]); GMATCH_SIMP_TAC Ldurdpn.LDURDPN; CONJ_TAC; BY(ASM_MESON_TAC[]); TYPIFY_GOAL_THEN `(?A. plane A /\ {vec 0, v2, v3, v4} SUBSET A)` (unlist REWRITE_TAC); FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `affine hull {vec 0,v2,v3}` EXISTS_TAC; CONJ2_TAC; TYPIFY `v4 IN affine hull {vec 0,v2,v3} /\ {vec 0 ,v2,v3} SUBSET affine hull {vec 0,v2,v3}` ENOUGH_TO_SHOW_TAC; BY(SET_TAC[]); BY(CONJ_TAC THEN ASM_MESON_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL]); REWRITE_TAC[plane]; BY(ASM_MESON_TAC[]); ASM_REWRITE_TAC[]; REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY]; REWRITE_TAC[Trigonometry2.AFF2_VEC0;IN_ELIM_THM;Geomdetail.CONV0_SET2;DE_MORGAN_THM;NOT_EXISTS_THM]; TYPIFY `(!x. (!k. ~(x = k % v2)) \/ (!a b. ~(&0 < a) \/ ~(&0 < b) \/ ~(a + b = &1) \/ ~(x = a % v3 + b % (t1 % v2 + t2 % v3)))) <=> (!k a b. &0 < a /\ &0 < b /\ a + b = &1 ==> ~(k % v2 = a % v3 + b % (t1 % v2 + t2 % v3)))` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[]); COMMENT "first case"; ASM_CASES_TAC `&0 <= t2`; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `v3 = (inv (b * t2 + a) * (-- (b * t1 - k))) % v2` ENOUGH_TO_SHOW_TAC; BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]); MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP; TYPIFY `(b * t2 + a)` EXISTS_TAC; SUBCONJ_TAC; MATCH_MP_TAC (arith `&0 <= b' /\ &0 < a ==> ~(b' + a = &0)`); GMATCH_SIMP_TAC REAL_LE_MUL; BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[VECTOR_MUL_ASSOC]; DISCH_TAC; TYPIFY `((b * t2 + a) * inv (b * t2 + a) * --(b * t1 - k)) = -- (b * t1 - k)` (C SUBGOAL_THEN SUBST1_TAC); Calc_derivative.CALC_ID_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); BY(FIRST_X_ASSUM_ST `%` MP_TAC THEN VECTOR_ARITH_TAC); ASM_REWRITE_TAC[NOT_FORALL_THM]; TYPIFY `~(t2 = &1)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); BY(ASM_TAC THEN REAL_ARITH_TAC); GEXISTL_TAC [`t1 / (&1 - t2)`;`-- t2 / (&1 - t2)`;`&1 / (&1 - t2)`;]; DISCH_THEN MP_TAC THEN ANTS_TAC; GMATCH_SIMP_TAC REAL_LT_DIV; GMATCH_SIMP_TAC REAL_LT_DIV; TYPIFY `--t2 / (&1 - t2) + &1 / (&1 - t2) = &1` (C SUBGOAL_THEN SUBST1_TAC); Calc_derivative.CALC_ID_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[]; TYPIFY `&1 / (&1 - t2) % (t1 % v2 + t2 % v3) = t1 / (&1 - t2) % v2 - --t2 / (&1 - t2) % v3` ENOUGH_TO_SHOW_TAC; DISCH_THEN SUBST1_TAC; BY(VECTOR_ARITH_TAC); REWRITE_TAC[VECTOR_ADD_LDISTRIB]; REWRITE_TAC[VECTOR_MUL_ASSOC]; TYPIFY `(&1 / (&1 - t2) * t1) = t1 / (&1 - t2)` (C SUBGOAL_THEN SUBST1_TAC); BY(REAL_ARITH_TAC); BY(VECTOR_ARITH_TAC) ]);; (* }}} *) (* let CONTINUOUS_LIFT_DOT2 = prove (`!net f:A->real^N g. f continuous net /\ g continuous net ==> (\x. lift(f x dot g x)) continuous net`, REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`] BILINEAR_CONTINUOUS_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);; let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement( `!(f:real->real^A) g x. f continuous atreal x /\ g continuous atreal x ==> (\x. (f x dot g x)) real_continuous atreal x`, (* {{{ proof *) [ REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1]; REPEAT WEAKER_STRIP_TAC; TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC); BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]); INTRO_TAC CONTINUOUS_AT_LIFT_DOT2 [`f o drop`;`g o drop`;`lift x`]; TYPIFY `(\x. lift ((f o drop) x dot (g o drop) x)) = (\x. lift (f x dot g x)) o drop` (C SUBGOAL_THEN SUBST1_TAC); BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]); BY(ASM_REWRITE_TAC[GSYM (* Xbjrphc. *) CONTINUOUS_CONTINUOUS_ATREAL]) ]);; (* }}} *) *) let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement( `!(f:real->real^A) g x. f continuous atreal x /\ g continuous atreal x ==> (\x. (f x dot g x)) real_continuous atreal x`, (* {{{ proof *) [ REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1]; REPEAT WEAKER_STRIP_TAC; TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC); BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]); MATCH_MP_TAC CONTINUOUS_LIFT_DOT2; ASM_REWRITE_TAC[]; ]);; (* }}} *) let azim_pos_open = prove_by_refinement( `!v2 v3 v4 t a b. (!x. x IN real_interval (a,b) ==> v2 continuous (atreal x)) /\ (!x. x IN real_interval (a,b) ==> v3 continuous (atreal x)) /\ (!x. x IN real_interval (a,b) ==> v4 continuous (atreal x)) /\ t IN real_interval(a,b) /\ ~collinear {(vec 0) ,(v2 t) ,(v3 t)} /\ ~collinear {(vec 0), (v2 t), (v4 t)} /\ ~(azim (vec 0) (v2 t) (v3 t) (v4 t) = &0) ==> (?e. &0 < e /\ (!t'. abs(t' - t) < e ==> ~(azim (vec 0) (v2 t') (v3 t') (v4 t') = &0))) `, (* {{{ proof *) [ REWRITE_TAC[real_open;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN ) [`t`;`(vec 0):real^3`;`v2`;`v3`]; ANTS_TAC; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN ) [`t`;`(vec 0):real^3`;`v2`;`v4`]; ANTS_TAC; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC azim_0_as_closed [`v2 t`;`v3 t`;`v4 t`]; ASM_REWRITE_TAC[DE_MORGAN_THM]; DISCH_TAC; TYPIFY `?e. &0 < e /\ (!t'. abs(t - t') < e ==> (~coplanar {vec 0, v2 t', v3 t', v4 t'} \/ ~(&0 <= ((v2 t' cross v3 t') cross v2 t') dot v4 t')))` (C SUBGOAL_THEN MP_TAC); FIRST_X_ASSUM DISJ_CASES_TAC; INTRO_TAC NONPLANAR_OPEN [`\(t:real). ((vec 0):real^3)`;`v2`;`v3`;`v4`;`t`]; ANTS_TAC; ASM_REWRITE_TAC[CONTINUOUS_CONST]; BY(ASM_MESON_TAC[]); REWRITE_TAC[]; BY(MESON_TAC[]); TYPIFY `(\t. ((v2 t cross v3 t) cross v2 t) dot -- (v4 t)) real_continuous_on ( real_interval(a,b) )` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT; REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC REAL_CONTINUOUS_AT_DOT2; CONJ2_TAC; MATCH_MP_TAC CONTINUOUS_NEG; BY(ASM_MESON_TAC[]); MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS; CONJ2_TAC; BY(ASM_MESON_TAC[]); MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS; BY(ASM_MESON_TAC[]); INTRO_TAC Pent_hex.continuous_preimage_open [`(\x. ((v2 x cross v3 x) cross v2 x) dot -- v4 x)`;`real_interval(a,b)`;`{u | &0 < u}`]; ANTS_TAC; ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL]; BY(REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`]); REWRITE_TAC[IN_ELIM_THM]; REWRITE_TAC[real_open;DOT_RNEG;arith `&0 < -- x <=> ~(&0 <= x)`;IN_ELIM_THM]; DISCH_THEN (C INTRO_TAC [`t`]); ANTS_TAC; BY(ASM_REWRITE_TAC[]); BY(MESON_TAC[arith `abs (x' - t) < e <=> abs (t - x') < e`]); REPEAT WEAKER_STRIP_TAC; TYPIFY `?e'''. e''' <= e /\ e''' <= e' /\ e''' <= e'' /\ &0 < e'''` (C SUBGOAL_THEN MP_TAC); TYPIFY `if (e'' <= e' /\ e'' <= e) then e'' else (if (e' <= e'' /\ e' <= e) then e' else e)` EXISTS_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `e'''` EXISTS_TAC; ASM_REWRITE_TAC[]; GEN_TAC; DISCH_TAC; GMATCH_SIMP_TAC azim_0_as_closed; REWRITE_TAC[DE_MORGAN_THM]; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN TRY REAL_ARITH_TAC) ]);; (* }}} *) let azim_real_continuous_on = prove_by_refinement( `!v2 v3 v4 t a b. (!x. x IN real_interval (a,b) ==> v2 continuous (atreal x)) /\ (!x. x IN real_interval (a,b) ==> v3 continuous (atreal x)) /\ (!x. x IN real_interval (a,b) ==> v4 continuous (atreal x)) /\ t IN real_interval(a,b) /\ ~collinear {(vec 0) ,(v2 t) ,(v3 t)} /\ ~collinear {(vec 0), (v2 t), (v4 t)} /\ ~(azim (vec 0) (v2 t) (v3 t) (v4 t) = &0) ==> (?e. &0 < e /\ (\q. azim (vec 0) (v2 q) (v3 q) (v4 q)) real_continuous_on (real_interval (t - e, t+ e)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`t`;`(vec 0):real^3`;`v2`;`v3`]; ANTS_TAC; BY(ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`t`;`(vec 0):real^3`;`v2`;`v4`]; ANTS_TAC; BY(ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC azim_pos_open [`v2`;`v3`;`v4`;`t`;`a`;`b`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `?e'''. &0 < e''' /\ (!x. t - e''' < x /\ x < t + e''' ==> x IN real_interval (a,b))` (C SUBGOAL_THEN MP_TAC); TYPIFY `if (b-t <= t -a) then b - t else t - a` EXISTS_TAC; FIRST_X_ASSUM_ST `IN` MP_TAC; REWRITE_TAC[IN_REAL_INTERVAL]; BY(REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `?e''''. e'''' <= e /\ e'''' <= e' /\ e'''' <= e'' /\ e'''' <= e''' /\ &0 < e''''` (C SUBGOAL_THEN MP_TAC); INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e,e',e'',e'''}`]; ANTS_TAC; CONJ_TAC; BY(MESON_TAC[FINITE_RULES]); BY(SET_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT;NOT_IN_EMPTY]); REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN (REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC)); BY(MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `e''''` EXISTS_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT; REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;IN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE; ASM_REWRITE_TAC[CONTINUOUS_CONST]; GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2); TYPIFY `x IN real_interval (a,b)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN (REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC)) THEN TRY REAL_ARITH_TAC) ]);; (* }}} *) let azim_pos_iff_nz = prove_by_refinement( `!v1 v2 v3 v4. &0 < azim v1 v2 v3 v4 <=> ~(azim v1 v2 v3 v4 = &0)`, (* {{{ proof *) [ BY(MESON_TAC[Counting_spheres.AZIM_NN;arith `&0 < x <=> (&0 <= x /\ ~(x = &0))`]) ]);; (* }}} *) (* was NHCXLRV_PREP *) let NHCXLRV = prove_by_refinement( `!v w0 w1 w2 f a b. deformation f {w0,w1,w2,v} (a,b) /\ ~collinear {vec 0, f w1 (&0), f w2 (&0)} /\ ~collinear {vec 0, f w1 (&0), f w0 (&0)} /\ ~collinear {vec 0, f w1 (&0), f v (&0)} /\ v IN wedge (vec 0) w1 w2 w0 ==> (?e. &0 < e /\ (!t. abs t < e ==> (f v t) IN wedge (vec 0) (f w1 t) (f w2 t) (f w0 t)))`, (* {{{ proof *) [ REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY;Localization.deformation]; REPEAT WEAKER_STRIP_TAC; TYPIFY `?c. azim (vec 0) w1 w2 v < c /\ c < azim (vec 0) w1 w2 w0` (C SUBGOAL_THEN MP_TAC); TYPIFY `(azim (vec 0) w1 w2 v + azim (vec 0) w1 w2 w0)/ &2` EXISTS_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `(?e1. &0 < e1 /\ (!t. abs t < e1 ==> &0 < azim (vec 0) (f w1 t) (f w2 t) (f v t))) /\(?e2. &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f w1 t) (f w2 t) (f v t) < c)) /\ (?e3. &0 < e3 /\ (!t. abs t < e3 ==> c < azim (vec 0) (f w1 t) (f w2 t) (f w0 t)))` ENOUGH_TO_SHOW_TAC; REPEAT WEAKER_STRIP_TAC; TYPIFY `if (e1 <= e2 /\ e1 <= e3) then e1 else if (e2 <= e3 /\ e2 <= e1) then e2 else e3` EXISTS_TAC; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); MATCH_MP_TAC REAL_LT_TRANS; TYPIFY `c` EXISTS_TAC; BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f w0`;`&0`;`a`;`b`]; ANTS_TAC; ASM_REWRITE_TAC[GSYM azim_pos_iff_nz]; FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC); TYPIFY_GOAL_THEN `&0 < azim (vec 0) w1 w2 w0` (unlist REWRITE_TAC); BY(ASM_MESON_TAC[Counting_spheres.AZIM_NN;arith `&0 <= x /\ x < y ==> &0 < y`]); BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f v`;`&0`;`a`;`b`]; ANTS_TAC; ASM_REWRITE_TAC[GSYM azim_pos_iff_nz]; FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC); ASM_REWRITE_TAC[]; BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC (REWRITE_RULE[arith `&0 - e = -- e /\ &0 + e = e`]); INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f v q))`;`real_interval (-- e',e')`;`{x | &0 < x}`]; ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`]; INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f v q))`;`real_interval (-- e',e')`;`{x | x < c }`]; ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_LT]; INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f w0 q))`;`real_interval (-- e,e)`;`{x | c < x}`]; ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_GT;arith ` c < x <=> x > c`]; REWRITE_TAC[IN_REAL_INTERVAL;IN_ELIM_THM;real_open]; REWRITE_TAC[arith `x > c <=> c < x`]; REPEAT (DISCH_THEN (C INTRO_TAC [`&0`]) THEN (FIRST_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC)) THEN ASM_SIMP_TAC[arith `&0 < e ==> -- e < &0`] THEN DISCH_TAC); RULE_ASSUM_TAC (REWRITE_RULE[arith `x - &0 = x`]); BY(ASM_MESON_TAC[]) ]);; (* }}} *) let NHCXLRV_ALT = prove_by_refinement( `!v w0 w1 w2 f a b. deformation f {w0, w1, w2, v} (a,b) /\ ~collinear {vec 0, w1, w2} /\ ~collinear {vec 0, w1, w0} /\ ~collinear {vec 0, w1, v} /\ v IN wedge (vec 0) w1 w2 w0 ==> (?e. &0 < e /\ (!t. abs t < e ==> f v t IN wedge (vec 0) (f w1 t) (f w2 t) (f w0 t)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC NHCXLRV; GEXISTL_TAC [`a`;`b`]; ASM_REWRITE_TAC[]; TYPIFY `!u. u IN {w0,w1,w2,v} ==> f u (&0) = u` (C SUBGOAL_THEN ASSUME_TAC); RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]); ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC); ASM_REWRITE_TAC[]; BY(SET_TAC[]) ]);; (* }}} *) let WNWSHJT = prove_by_refinement( `!w0 w1 w2 f a b. deformation f {w0,w1,w2} (a,b) /\ ~collinear {vec 0, f w1 (&0), f w2 (&0)} /\ ~collinear {vec 0, f w1 (&0), f w0 (&0)} /\ &0 < azim (vec 0) w1 w2 w0 /\ azim (vec 0) w1 w2 w0 < pi ==> (?e. &0 < e /\ (!t. abs t < e ==> azim (vec 0) (f w1 t) (f w2 t) (f w0 t) < pi))`, (* {{{ proof *) [ REWRITE_TAC[IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY;Localization.deformation]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f w0`;`&0`;`a`;`b`]; ANTS_TAC; ASM_REWRITE_TAC[GSYM azim_pos_iff_nz]; FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC); ASM_REWRITE_TAC[]; BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC (REWRITE_RULE[arith `&0 - e = -- e /\ &0 + e = e`]); INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f w0 q))`;`real_interval (-- e,e)`;`{x | x < pi}`]; ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_LT]; REWRITE_TAC[IN_REAL_INTERVAL;IN_ELIM_THM;real_open]; REPEAT (DISCH_THEN (C INTRO_TAC [`&0`]) THEN (FIRST_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC)) THEN ASM_SIMP_TAC[arith `&0 < e ==> -- e < &0`] THEN DISCH_TAC); RULE_ASSUM_TAC (REWRITE_RULE[arith `x - &0 = x`]); BY(ASM_MESON_TAC[]) ]);; (* }}} *) let LOFA_IMP_INANGLE_EQ_AZIM = prove_by_refinement (`!V E FF v. local_fan (V,E,FF) /\ v IN V ==> interior_angle1 (vec 0) FF v = azim_in_fan (v, rho_node1 FF v) E `, [ REWRITE_TAC[Localization.convex_local_fan; Local_lemmas.azim_in_fan2]; REPEAT STRIP_TAC; ASSUME_TAC2 Local_lemmas.EXISTS_INVERSE_OF_V; DOWN THEN STRIP_TAC; ASSUME_TAC2 Local_lemmas.LOFA_IMP_EE_TWO_ELMS; ASSUME_TAC2 Local_lemmas.LOFA_CARD_EE_V_1; ASSUME_TAC2 Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2; DOWN THEN STRIP_TAC; UNDISCH_TAC` v:real^3 IN V `; FIRST_ASSUM NHANH; LET_TAC; SWITCH_TAC` EE v E = {rho_node1 FF v, vv} `; ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `]; STRIP_TAC; DOWN THEN DOWN THEN PHA; ASSUME_TAC2 (SPEC `vv:real^3 ` (GEN` v:real^3 ` Local_lemmas.IVS_RHO_IDD)); EXPAND_TAC "d"; SIMP_TAC[]; UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `; DISCH_THEN (SUBST1_TAC o SYM); EXPAND_TAC "v"; DOWN; BY(SIMP_TAC[Local_lemmas.interior_angle1; GSYM Local_lemmas.ivs_rho_node1; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]) ]);; let deformation_rho_node1_equivariant1 = prove_by_refinement( `!f V E FF a b v t. deformation f V (a,b) /\ local_fan (V,E,FF) /\ local_fan (IMAGE (\v. f v t) V, IMAGE (\s. IMAGE (\v. f v t) s) E, IMAGE (\ (u,v). f u t,f v t) FF) /\ v IN V ==> f (rho_node1 FF v) t = rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC EQ_SYM; MATCH_MP_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE); GEXISTL_TAC [`IMAGE (\v. f v t) V`;` IMAGE (\s. IMAGE (\v. f v t) s) E`]; CONJ_TAC; TYPIFY `IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` ENOUGH_TO_SHOW_TAC; DISCH_THEN (SUBST1_TAC o GSYM); BY(ASM_REWRITE_TAC[]); BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]); REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM]; GEXISTL_TAC [`v`;`rho_node1 FF v`]; REWRITE_TAC[]; BY(ASM_MESON_TAC[Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2]) ]);; (* }}} *) let deformation_ivs_rho_node1_equivariant1 = prove_by_refinement( `!f V E FF a b v t. deformation f V (a,b) /\ local_fan (V,E,FF) /\ local_fan (IMAGE (\v. f v t) V, IMAGE (\s. IMAGE (\v. f v t) s) E, IMAGE (\ (u,v). f u t,f v t) FF) /\ v IN V ==> f (ivs_rho_node1 FF v) t = ivs_rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC EQ_SYM; MATCH_MP_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE); GEXISTL_TAC [`IMAGE (\v. f v t) V`;` IMAGE (\s. IMAGE (\v. f v t) s) E`]; CONJ_TAC; TYPIFY `IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` ENOUGH_TO_SHOW_TAC; DISCH_THEN (SUBST1_TAC o GSYM); BY(ASM_REWRITE_TAC[]); BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]); REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM]; GEXISTL_TAC [`ivs_rho_node1 FF v`;`v`]; REWRITE_TAC[]; BY(ASM_MESON_TAC[Lunar_deform.IVS_RHO_NODE_V_IN_FF]) ]);; (* }}} *) let deformation_rho_node1_equivariant = prove_by_refinement( `!f V E FF a b v . deformation f V (a,b) /\ local_fan (V,E,FF) /\ v IN V ==> (?e. &0 < e /\ (!t. abs t < e ==> f (rho_node1 FF v) t = rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[deformation_rho_node1_equivariant1]) ]);; (* }}} *) let deformation_subset = prove_by_refinement( `!f U V a b. U SUBSET V /\ deformation f V (a,b) ==> deformation f U (a,b)`, (* {{{ proof *) [ REWRITE_TAC[Localization.deformation;SUBSET]; BY(MESON_TAC[]) ]);; (* }}} *) let EXISTS_TRIPLE_THM = prove_by_refinement( `!P. (?p1 p2 p3. P p1 p2 p3) <=> (?x. P (FST x) (FST (SND x)) (SND (SND x)))`, (* {{{ proof *) [ BY(REWRITE_TAC[EXISTS_PAIR_THM]) ]);; (* }}} *) let zlz_reduction = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) /\ (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) /\ (!u v w. ?e4. v,w IN FF /\ u IN V ==> &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> aff_ge {vec 0} {f v t, f w t} INTER aff_lt {vec 0} {f u t} = {})) /\ (!x. ?e3. x IN FF ==> &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge (f (FST x) t,f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E))) /\ (!x. ?e2. x IN FF ==> &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> azim_in_fan (f (FST x) t,f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E) <= pi)) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> convex_local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\ generic (IMAGE (\v. f v t) V) (IMAGE (IMAGE (\v. f v t)) E)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Localization.convex_local_fan]; REWRITE_TAC[Localization.generic]; COMMENT "preliminaries"; TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]); INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`]; ASM_REWRITE_TAC[]; DISCH_TAC; TYPIFY `FINITE FF` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF; BY(ASM_REWRITE_TAC[]); TYPIFY `~(FF = {})` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Polar_fan.LOCAL_FAN_NOT_EMPTY_FF; BY(ASM_MESON_TAC[]); TYPIFY `(?e1. &0 < e1 /\ (!t. --e1 < t /\ t < e1 ==> (local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF)))) /\ (?e2. &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> ((!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> azim_in_fan x (IMAGE (IMAGE (\v. f v t)) E) <= pi)))) /\ (?e3. &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge x (IMAGE (IMAGE (\v. f v t)) E)))) /\ (?e4. &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> (!v w u. {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\ u IN IMAGE (\v. f v t) V ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})))` ENOUGH_TO_SHOW_TAC; REPEAT WEAKER_STRIP_TAC; TYPIFY `?e. e <= e1 /\ e <= e2 /\ e <= e3 /\ e <= e4 /\ &0 < e` (C SUBGOAL_THEN MP_TAC); INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e1,e2,e3,e4}`]; ANTS_TAC; CONJ_TAC; BY(MESON_TAC[FINITE_RULES]); BY(SET_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT;NOT_IN_EMPTY]); REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN (REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC)); BY(MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; BY(ASM_MESON_TAC[arith `-- e < t /\ t < e /\ e <= e' ==> (-- e' < t /\ t < e')`]); COMMENT "local_fan"; SUBCONJ_TAC; INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); BY(ASM_REWRITE_TAC[]); DISCH_TAC; COMMENT "skolemize all variables"; COMMENT "angle <= pi"; TYPIFY_GOAL_THEN `(!x. ?e2. x IN FF ==> ( &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> azim_in_fan ( (\uv. f (FST uv) t,f (SND uv) t) x) (IMAGE (IMAGE (\v. f v t)) E) <= pi))) ==> (?e2. &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> azim_in_fan x (IMAGE (IMAGE (\v. f v t)) E) <= pi)))` GMATCH_SIMP_TAC; REWRITE_TAC[SKOLEM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `?e. &0 < e /\ (!x. x IN FF ==> e <= e2 x)` (C SUBGOAL_THEN MP_TAC); INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e2 FF`]; ANTS_TAC; CONJ_TAC; (MATCH_MP_TAC FINITE_IMAGE); BY(ASM_REWRITE_TAC[]); (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE); BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC); REWRITE_TAC[EXTENSION;NOT_IN_EMPTY]; REWRITE_TAC[IN_IMAGE]; BY(MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM]; REPEAT WEAKER_STRIP_TAC; REPEAT (FIRST_X_ASSUM (C INTRO_TAC [`p1,p2`])); DISCH_TAC; ASM_REWRITE_TAC[]; DISCH_TAC; FIRST_X_ASSUM_ST `IMAGE` MP_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); COMMENT "skolemize wedge_in_fan"; TYPIFY_GOAL_THEN `(!x. ?e3. x IN FF ==> &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge (f (FST x) t, f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E)))) ==> ( (?e3. &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge x (IMAGE (IMAGE (\v. f v t)) E)))))` GMATCH_SIMP_TAC; REWRITE_TAC[SKOLEM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `?e. &0 < e /\ (!x. x IN FF ==> e <= e3 x)` (C SUBGOAL_THEN MP_TAC); INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e3 FF`]; ANTS_TAC; CONJ_TAC; (MATCH_MP_TAC FINITE_IMAGE); BY(ASM_REWRITE_TAC[]); (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE); BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC); REWRITE_TAC[EXTENSION;NOT_IN_EMPTY]; REWRITE_TAC[IN_IMAGE]; BY(MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM]; REPEAT WEAKER_STRIP_TAC; REPEAT (FIRST_X_ASSUM (C INTRO_TAC [`p1,p2`])); DISCH_TAC; ASM_REWRITE_TAC[]; DISCH_TAC; FIRST_X_ASSUM_ST `IMAGE` MP_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ANTS_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]); TYPIFY_GOAL_THEN `(!u v w. ?e4. (v,w) IN FF /\ u IN V ==> &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> aff_ge {vec 0} {f v t, f w t} INTER aff_lt {vec 0} {f u t} = {})) ==> (?e4. &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> (!v w u. {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\ u IN IMAGE (\v. f v t) V ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {}))) ` GMATCH_SIMP_TAC; REWRITE_TAC[SKOLEM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `?e. &0 < e /\ (!u v w. (u,(v,w)) IN V CROSS FF ==> e <= e4 u v w)` (C SUBGOAL_THEN MP_TAC); INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE (\ x. e4 (FST x) (FST (SND x)) (SND(SND x))) (V CROSS FF)`]; ANTS_TAC; CONJ_TAC; (MATCH_MP_TAC FINITE_IMAGE); MATCH_MP_TAC FINITE_CROSS; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]); (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE); REWRITE_TAC[CROSS_EQ_EMPTY]; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[Local_lemmas.LOFA_V_NOT_EMP]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC); REWRITE_TAC[EXTENSION;NOT_IN_EMPTY]; REWRITE_TAC[IN_IMAGE]; REWRITE_TAC[EXISTS_PAIR_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`p1`;`p1'`;`p2`]); ANTS_TAC; RULE_ASSUM_TAC(REWRITE_RULE[IN_CROSS]); BY(ASM_REWRITE_TAC[]); (REPEAT WEAKER_STRIP_TAC); ASM_REWRITE_TAC[]; TYPIFY `m = e4 p1 p1' p2` UNDISCH_TAC; DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_MESON_TAC[IN_CROSS]); REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `IMAGE` MP_TAC; REWRITE_TAC[IN_IMAGE]; REPEAT WEAKER_STRIP_TAC; TYPIFY `?v' w'. x' = {v',w'}` (C SUBGOAL_THEN MP_TAC); TYPIFY `graph E` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Fan_defs.FAN;Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN]); RULE_ASSUM_TAC(REWRITE_RULE[Fan_defs.graph]); TYPIFY`x' HAS_SIZE 2` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[IN]); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[Local_lemmas1.HAS_SIZE_2_EXISTS2]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); FIRST_X_ASSUM_ST `IMAGE` MP_TAC; REWRITE_TAC[SET_RULE `IMAGE f {u,v} = {f u,f v}`]; DISCH_THEN ( SUBST1_TAC ); ASM_REWRITE_TAC[]; TYPIFY `?v'' w''. {v',w'} = {v'',w''} /\ (v'',w'') IN FF` (C SUBGOAL_THEN MP_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOFA_IN_E_IMP_IN_FF;SET_RULE `{a,b} = {b,a}`]); REPEAT WEAKER_STRIP_TAC; TYPIFY `{f v' t,f w' t} = {f v'' t,f w'' t}` (C SUBGOAL_THEN SUBST1_TAC); FIRST_X_ASSUM_ST `{a,b}` MP_TAC; REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND]; BY(MESON_TAC[]); FIRST_X_ASSUM (C INTRO_TAC [`x`;`v''`;`w''`]); REWRITE_TAC[IN_CROSS]; ASM_REWRITE_TAC[]; DISCH_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x`;`v''`;`w''`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(ASM_REWRITE_TAC[]) ]);; (* }}} *) let real_interval_contains_0_ball = prove_by_refinement( `!a b e1. a < &0 /\ &0 < b /\ &0 < e1 ==> (?e. &0 < e /\ e <= e1 /\ (!t. abs t < e ==> t IN real_interval (a,b)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `if (b <= -- a) /\ b <= e1 then b else (if e1 <= b /\ e1 <= --a then e1 else -- a)` EXISTS_TAC; REWRITE_TAC[IN_REAL_INTERVAL]; ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); CONJ_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); GEN_TAC; BY(REAL_ARITH_TAC) ]);; (* }}} *) let zlz_azim = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) /\ (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==> (!x. ?e2. x IN FF ==> &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> azim_in_fan (f (FST x) t,f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E) <= pi)) `, (* {{{ proof *) [ REWRITE_TAC[Localization.convex_local_fan]; REWRITE_TAC[Localization.generic]; REPEAT WEAKER_STRIP_TAC; COMMENT "preliminaries"; TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]); INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`]; ASM_REWRITE_TAC[]; TYPIFY `FINITE FF` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF; BY(ASM_REWRITE_TAC[]); TYPIFY `~(FF = {})` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Polar_fan.LOCAL_FAN_NOT_EMPTY_FF; BY(ASM_MESON_TAC[]); COMMENT "local_fan"; INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`]; ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; REPEAT WEAKER_STRIP_TAC; COMMENT "restart here"; TYPIFY `?p1 p2. (x = p1,p2)` (C SUBGOAL_THEN MP_TAC); BY(REWRITE_TAC[PAIR_SURJECTIVE]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[FST;SND]; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; DISCH_TAC; TYPIFY `p1 IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]); TYPIFY `p2 = rho_node1 FF p1` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC EQ_SYM; MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE; BY(ASM_REWRITE_TAC[]); TYPIFY `interior_angle1 (vec 0) FF p1 = azim_in_fan (p1,p2) E` (C SUBGOAL_THEN ASSUME_TAC); INTRO_TAC LOFA_IMP_INANGLE_EQ_AZIM [`V`;`E`;`FF`;`p1`]; BY(ASM_MESON_TAC[]); TYPIFY `?e2. &0 < e2 /\ e2 <= e /\ (!t. abs t < e2 ==> t IN real_interval (a,b))` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC real_interval_contains_0_ball; RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_REAL_INTERVAL]); BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; COMMENT "first case"; TYPIFY `interior_angle1 (vec 0) FF p1 = pi` ASM_CASES_TAC; TYPIFY `e2` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; COMMENT "new insert"; TYPIFY `local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) (t),f (SND uv) (t)) FF) /\ f p1 (t) IN IMAGE (\v. f v t) V` (C SUBGOAL_THEN ASSUME_TAC); CONJ_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); REWRITE_TAC[IN_IMAGE]; TYPIFY `p1` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); GMATCH_SIMP_TAC deformation_rho_node1_equivariant1; CONJ_TAC; GEXISTL_TAC [`a`;`b`;`E`;`V`]; BY(ASM_REWRITE_TAC[]); INTRO_TAC (GSYM LOFA_IMP_INANGLE_EQ_AZIM) [`IMAGE (\v. f v t) V`;`IMAGE (IMAGE (\v. f v t)) E`;`IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF`;`f p1 t`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(ASM_MESON_TAC[]); COMMENT "second case here"; COMMENT "case azim < pi"; TYPIFY `interior_angle1 (vec 0) FF p1 < pi` (C SUBGOAL_THEN ASSUME_TAC); RULE_ASSUM_TAC (REWRITE_RULE[Localization.convex_local_fan]); FIRST_X_ASSUM_ST `wedge_in_fan_ge` MP_TAC THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `interior_angle1 (vec 0) FF p1 <= pi` ENOUGH_TO_SHOW_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[]); INTRO_TAC WNWSHJT [`ivs_rho_node1 FF p1`;`p1`;`p2`;`f`;`a`;`b`]; ASM_REWRITE_TAC[]; REPEAT (GMATCH_SIMP_TAC (GSYM Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND)); TYPIFY `E` EXISTS_TAC; CONJ_TAC; BY(ASM_MESON_TAC[]); ANTS_TAC; CONJ_TAC; MATCH_MP_TAC deformation_subset; TYPIFY `V` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY]; BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_IVS_IN_V;Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]); (GMATCH_SIMP_TAC deformation_rho_node1_equivariant1); GMATCH_SIMP_TAC deformation_ivs_rho_node1_equivariant1; CONJ_TAC; GEXISTL_TAC [`a`;`b`;`E`;`V`]; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e1` MP_TAC) THEN REAL_ARITH_TAC); CONJ_TAC; GEXISTL_TAC [`a`;`b`;`E`;`V`]; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e1` MP_TAC) THEN REAL_ARITH_TAC); TYPIFY `!v. v IN V ==> f v (&0) = v` (C SUBGOAL_THEN ASSUME_TAC); RULE_ASSUM_TAC (REWRITE_RULE[Localization.deformation]); BY(ASM_REWRITE_TAC[]); TYPIFY `f p1 (&0) = p1` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_SIMP_TAC[]); ASM_REWRITE_TAC[]; TYPIFY `IMAGE (\uv. f (FST uv) (&0),f (SND uv) (&0)) FF = FF` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[IN_IMAGE;EXTENSION;EXISTS_PAIR_THM]; GEN_TAC; INTRO_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V) [`E`;`FF`;`FST x`;`SND x`;`V`]; ASM_REWRITE_TAC[]; DISCH_TAC; TYPIFY `x IN FF` ASM_CASES_TAC; ASM_REWRITE_TAC[]; GEXISTL_TAC [ `FST x`;`SND x`]; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[PAIR;FST;SND]); ASM_REWRITE_TAC[]; REWRITE_TAC[NOT_EXISTS_THM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V) [`E`;`FF`;`p1'`;`p2'`;`V`]; ASM_REWRITE_TAC[]; BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[PAIR;FST;SND]); TYPIFY `p1 IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]); CONJ_TAC; BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]); CONJ_TAC; BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]); CONJ_TAC; INTRO_TAC (GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS) [`E`;`V`;`FF`;`p1`]; BY(ASM_REWRITE_TAC[]); BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `(!t. abs t < e ==> azim_in_fan (f p1 t,f (rho_node1 FF p1) t) (IMAGE (IMAGE (\v. f v t)) E) = azim (vec 0) (f p1 t) (f (rho_node1 FF p1) t) (f (ivs_rho_node1 FF p1) t))` (C SUBGOAL_THEN MP_TAC); REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC deformation_rho_node1_equivariant1; CONJ_TAC; GEXISTL_TAC [`a`;`b`;`E`;`V`]; (ASM_REWRITE_TAC[]); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); GMATCH_SIMP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND; CONJ_TAC; TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC; CONJ_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); REWRITE_TAC[IN_IMAGE]; TYPIFY `p1` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); GMATCH_SIMP_TAC deformation_ivs_rho_node1_equivariant1; GEXISTL_TAC [`a`;`b`;`E`;`V`]; (ASM_REWRITE_TAC[]); FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPIFY `if (e2 <= e') then e2 else e'` EXISTS_TAC; CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ANTS_TAC; BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); DISCH_THEN SUBST1_TAC; MATCH_MP_TAC (arith `x < pi ==> x <= pi`); FIRST_X_ASSUM MATCH_MP_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let zlz_generic = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) ==> (!u v w. ?e4. v,w IN FF /\ u IN V ==> &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> aff_ge {vec 0} {f v t, f w t} INTER aff_lt {vec 0} {f u t} = {}))`, (* {{{ proof *) [ COMMENT "prelims"; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO; BY(ASM_REWRITE_TAC[]); TYPIFY `v IN V /\ w IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V; BY(ASM_REWRITE_TAC[]); TYPIFY `~(u = vec 0)` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_V_DIFF]); TYPIFY `rho_node1 FF v = w` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE; BY(ASM_REWRITE_TAC[]); TYPIFY `~collinear {vec 0,v, rho_node1 FF v}` (C SUBGOAL_THEN MP_TAC); MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; BY(ASM_REWRITE_TAC[]); ASM_REWRITE_TAC[]; DISCH_TAC; COMMENT "expand generic"; RULE_ASSUM_TAC(REWRITE_RULE[Localization.generic]); FIRST_X_ASSUM (C INTRO_TAC [`v`;`rho_node1 FF v`;`u`]); ANTS_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.LOCAL_FAN_IN_FF_IN_ORD_PAIRS2; BY(ASM_REWRITE_TAC[]); (GMATCH_SIMP_TAC generic_alt); ASM_REWRITE_TAC[]; DISCH_TAC; TYPIFY `?e. &0 < e /\ (!t. -- e < t /\ t < e ==> ~(f u t = vec 0) /\ ~collinear {vec 0,f v t,f w t} /\ (~coplanar {vec 0,f u t,f v t,f w t} \/ -- (f u t) IN wedge (vec 0) (f v t cross f w t) (f w t) (f v t)))` ENOUGH_TO_SHOW_TAC; REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC generic_alt; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; BY(ASM_REWRITE_TAC[]); TYPIFY `?e1. &0 < e1 /\ (!t. abs t < e1 ==> ~(f u t = vec 0))` (C SUBGOAL_THEN MP_TAC); REWRITE_TAC[GSYM NORM_POS_LT]; INTRO_TAC Pent_hex.continuous_preimage_open [`norm o (f u)`;`real_interval (a,b)`;`{x | &0 < x}`]; REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL]; REWRITE_TAC[IN_ELIM_THM;o_THM]; ANTS_TAC; REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`]; GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT; REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL]; REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC REAL_CONTINUOUS_CONTINUOUS_ATREAL_COMPOSE; CONJ_TAC; RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]); BY(ASM_MESON_TAC[]); BY(REWRITE_TAC[REAL_CONTINUOUS_NORM_WITHIN]); REWRITE_TAC[real_open;IN_ELIM_THM]; DISCH_THEN (C INTRO_TAC [`&0`]); ANTS_TAC; RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]); ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[NORM_POS_LT]); BY(MESON_TAC[arith `abs (x - &0) = abs x`]); REPEAT WEAKER_STRIP_TAC; COMMENT "collinearity"; TYPIFY `f v (&0) = v /\ f w (&0) = w /\ f u (&0) = u /\ f v continuous atreal (&0) /\ f w continuous atreal (&0) /\ f u continuous atreal (&0)` (C SUBGOAL_THEN ASSUME_TAC); RULE_ASSUM_TAC (REWRITE_RULE[Localization.deformation]); BY(ASM_MESON_TAC[]); TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> ~collinear {vec 0,f v t, f w t})` (C SUBGOAL_THEN MP_TAC); INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`&0`;`(vec 0):real^3`;`f v`;`f w`]; ASM_REWRITE_TAC[]; BY(MESON_TAC[arith `abs(&0 - r') = abs(r')`]); REPEAT WEAKER_STRIP_TAC; TYPIFY `?e3. &0 < e3 /\ (!t. abs t < e3 ==> ((~coplanar {vec 0, f u t, f v t, f w t} \/ --f u t IN wedge (vec 0) (f v t cross f w t) (f w t) (f v t))))` (C SUBGOAL_THEN MP_TAC); FIRST_X_ASSUM DISJ_CASES_TAC; INTRO_TAC NONPLANAR_OPEN [`\ (t:real). (vec 0):real^3`;`f u`;`f v`;`f w`;`&0`]; ASM_REWRITE_TAC[CONTINUOUS_CONST;arith `abs(&0 - t') = abs(t')`]; BY(MESON_TAC[]); COMMENT "disjointness"; TYPIFY `~(v cross w = v) /\ ~(v cross w = w) ` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[CROSS_EQ_SELF]; BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b} = {a,b}`;SET_RULE `{a,b,a} = {a,b}`]); TYPIFY `~(v cross w = -- u)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `wedge` MP_TAC; REWRITE_TAC[wedge;IN_ELIM_THM]; BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}={a,b}`]); TYPIFY `~( ( -- (u:real^3) = v) \/ (-- u = w))` (C SUBGOAL_THEN MP_TAC); DISCH_TAC; FIRST_X_ASSUM_ST `wedge` MP_TAC; REWRITE_TAC[Reuhady.WEDGE_SIMPLE]; FIRST_X_ASSUM DISJ_CASES_TAC; ASM_REWRITE_TAC[IN_ELIM_THM]; BY(REWRITE_TAC[arith `~(x < x)`]); ASM_REWRITE_TAC[IN_ELIM_THM]; BY(REWRITE_TAC[AZIM_REFL;arith `~(&0 < &0)`]); REWRITE_TAC[DE_MORGAN_THM]; REPEAT WEAKER_STRIP_TAC; COMMENT "wedge"; TYPIFY `?g. deformation g {v, v cross w, w, --u} (a,b) /\ ( g (v cross w) = (\t. f v t cross f w t)) /\ (g v = f v) /\ (g w = f w) /\ (g (-- u) = (\t. -- f u t))` (C SUBGOAL_THEN MP_TAC); TYPIFY `\x. if (x = --u) then (\t. -- f u t) else if (x = v cross w) then (\t. f v t cross f w t) else f x` EXISTS_TAC; ASM_TAC THEN ASM_REWRITE_TAC[Localization.deformation;IN_INSERT;NOT_IN_EMPTY] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[]; CONJ2_TAC; BY(REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC)) THEN ASM_REWRITE_TAC[] THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC)) THEN ASM_REWRITE_TAC[] THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]; BY(MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS THEN REWRITE_TAC[ETA_AX] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); MATCH_MP_TAC CONTINUOUS_NEG; BY(REWRITE_TAC[ETA_AX] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC NHCXLRV [`-- (u:real^3)`;`v`;`v cross w`;`w`;`g`;`a`;`b`]; ASM_REWRITE_TAC[]; ANTS_TAC; TYPIFY_GOAL_THEN `~collinear {vec 0, v cross w, --u}` (unlist REWRITE_TAC); FIRST_X_ASSUM_ST `wedge` MP_TAC; REWRITE_TAC[wedge;IN_ELIM_THM]; BY(MESON_TAC[]); ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`]; BY(ASM_REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS;GSYM COLL_IFF_COLL_CROSS2]); BY(MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `(?e. (&0 < e /\ e <= e1 /\ e <= e2 /\ e <= e3))` (C SUBGOAL_THEN MP_TAC); INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e1,e2,e3}`]; ANTS_TAC; CONJ_TAC; REWRITE_TAC[FINITE_RULES]; BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]); BY(SET_TAC[]); REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]; REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; CONJ_TAC; REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN (REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN TRY REAL_ARITH_TAC)) ]);; (* }}} *) let zlz_wedge_skolem = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ (!x v. ?e3. x IN FF /\ v IN V ==> &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (f v t) IN wedge_in_fan_ge (f (FST x) t,f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E))) ==> (!x. ?e3. x IN FF ==> &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge (f (FST x) t,f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; DISCH_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x`]); REWRITE_TAC[SKOLEM_THM]; REPEAT WEAKER_STRIP_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO; BY(ASM_REWRITE_TAC[]); TYPIFY `~(V = {})` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.LOFA_V_NOT_EMP; BY(ASM_REWRITE_TAC[]); TYPIFY `?e. &0 < e /\ (!v. v IN V ==> e <= e3 v)` (C SUBGOAL_THEN MP_TAC); INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e3 V`]; ANTS_TAC; CONJ_TAC; (MATCH_MP_TAC FINITE_IMAGE); MATCH_MP_TAC Local_lemmas.LOCAL_FAN_FINITE_V; BY(ASM_REWRITE_TAC[]); (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE); BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC); REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`x'`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[SUBSET;IN_IMAGE]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`x''`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`x''`]); ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) let wedge_ge_refl = prove_by_refinement( `!v1 v2 v3 v4. v2 IN wedge_ge v1 v2 v3 v4`, (* {{{ proof *) [ REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE;Local_lemmas.AZIM_SPEC_DEGENERATE]; BY(REWRITE_TAC[Counting_spheres.AZIM_NN]) ]);; (* }}} *) let zlz_wedge_refl = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) /\ (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==> (!v w. (w IN V /\ v IN {w, rho_node1 FF w, ivs_rho_node1 FF w}) ==> ?e. &0 < e /\ (!t. -- e < t /\ t < e ==> f v t IN wedge_in_fan_ge (f w t , f (rho_node1 FF w) t) (IMAGE (IMAGE (\v. f v t)) E)))`, (* {{{ proof *) [ REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]; REPEAT WEAKER_STRIP_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO; BY(ASM_REWRITE_TAC[]); INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]); INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`]; ASM_REWRITE_TAC[]; TYPIFY `e` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND; CONJ_TAC; TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[IN_IMAGE]); REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_REWRITE_TAC[Local_lemmas1.FST_LST_IN_WEDGE_GE]; BY(REWRITE_TAC[wedge_ge_refl]) ]);; (* }}} *) let zlz_wedge_open = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) /\ (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==> (!v w. (v IN V /\ w IN V /\ v IN wedge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)) ==> ?e. &0 < e /\ (!t. -- e < t /\ t < e ==> f v t IN wedge_in_fan_ge (f w t , f (rho_node1 FF w) t) (IMAGE (IMAGE (\v. f v t)) E)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO; BY(ASM_REWRITE_TAC[]); INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]); TYPIFY `v = w` ASM_CASES_TAC; INTRO_TAC zlz_wedge_refl [`a`;`b`;`V`;`E`;`FF`;`f`]; ASM_REWRITE_TAC[]; DISCH_THEN (C INTRO_TAC [`w`;`w`]); BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]); INTRO_TAC NHCXLRV_ALT [`v`;`(ivs_rho_node1 FF w)`;`w`;`(rho_node1 FF w)`;`f`;`a`;`b`]; ASM_REWRITE_TAC[]; TYPIFY `rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; BY(ASM_REWRITE_TAC[]); TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V; BY(ASM_REWRITE_TAC[]); GMATCH_SIMP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2; CONJ_TAC; BY(ASM_MESON_TAC[]); GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS; CONJ_TAC; BY(ASM_MESON_TAC[]); ANTS_TAC; CONJ_TAC; MATCH_MP_TAC deformation_subset; TYPIFY `V` EXISTS_TAC; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY]; BY(ASM_MESON_TAC[]); BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN]); REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[arith `--e < t /\ t < e <=> abs t < e`]; TYPIFY `?e''. (&0 < e'') /\ e'' <= e /\ e'' <= e'` (C SUBGOAL_THEN MP_TAC); TYPIFY `if (e <= e') then e else e'` EXISTS_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `e''` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; ANTS_TAC; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); DISCH_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ANTS_TAC; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); DISCH_TAC; INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND; CONJ_TAC; TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[IN_IMAGE]); FIRST_X_ASSUM_ST `wedge` MP_TAC; ASM_REWRITE_TAC[]; BY(SET_TAC[Leaf_cell.WEDGE_SUBSET_WEDGE_GE]) ]);; (* }}} *) let PROPERTIES_GENERIC_LOCAL_FAN_ALT = prove_by_refinement( `!V E FF u v. local_fan (V,E,FF) /\ u IN V /\ v IN V /\ ~(u = v) /\ generic V E ==> ~collinear {vec 0,u,v}`, (* {{{ proof *) [ BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN]) ]);; (* }}} *) let skolem_epsilon_old = prove_by_refinement( `!P Q s. (!e e' i. &0 < e /\ e <= e' /\ (i:A) IN s /\ P i==> (Q e' i ==> Q e i)) /\ FINITE s ==> ((!i. ?e. (i IN s /\ P i) ==> (&0 < e /\ Q e i)) <=> (?e. !i. (i IN s /\ P i) ==> (&0 < e /\ Q e i)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `~(?i. i IN s /\ P i)` ASM_CASES_TAC; BY(ASM_MESON_TAC[]); RULE_ASSUM_TAC(REWRITE_RULE[]); MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a <=> b)`); CONJ_TAC; REWRITE_TAC[SKOLEM_THM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e {i | i IN s /\ P i}`]; ANTS_TAC; CONJ_TAC; (MATCH_MP_TAC FINITE_IMAGE); MATCH_MP_TAC FINITE_SUBSET; TYPIFY `s` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(SET_TAC[]); (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE); ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC); REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; SUBCONJ_TAC; BY(ASM_MESON_TAC[]); BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; BY(ASM_MESON_TAC[]) ]);; (* }}} *) let SKOLEM_EPSILON = prove_by_refinement( `!Q s. (!e e' i. &0 < e /\ e <= e' /\ (i:A) IN s ==> (Q e' i ==> Q e i)) /\ FINITE s ==> ((!i. ?e. (&0 < e) /\ (i IN s ==> (Q e i))) <=> (?e. !i. (&0 < e) /\ (i IN s ==> ( Q e i))))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `~(?i. i IN s)` ASM_CASES_TAC; BY(ASM_MESON_TAC[]); RULE_ASSUM_TAC(REWRITE_RULE[]); MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a <=> b)`); CONJ2_TAC; BY(ASM_MESON_TAC[]); REWRITE_TAC[SKOLEM_THM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e s`]; ANTS_TAC; CONJ_TAC; (MATCH_MP_TAC FINITE_IMAGE); BY(ASM_REWRITE_TAC[]); (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE); ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY]; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `m` EXISTS_TAC; GEN_TAC; REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC); REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[]) ]);; (* }}} *) let EXISTS_AND_IMP = prove_by_refinement( `!P Q R. (?(d:A). (P /\ Q d ==> R d)) <=> (P ==> (?d. Q d ==> R d))`, (* {{{ proof *) [ MESON_TAC[] ]);; (* }}} *) let XIV_DEFORMATION = prove_by_refinement( `!f dh r w a b. deformation f {w i | i <= r + 2} (a,b) /\ pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\ pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\ (\ (i,j,k). dihV (vec 0) (w i) (w j) (w k)) = dh /\ (!i. ?e2. i IN 1..r+1 ==> &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\ (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1))) /\ (!p q. {p, q, q + 1} SUBSET 1..r+1 /\ ~(p = q) /\ ~(p = q + 1) ==> dh (p,q,q + 1) = &0) /\ (!p q. {p, p + 1, q} SUBSET 1..r+1 /\ q > p + 1 ==> dh (p,p + 1,q) = &0) /\ (!p q. {p + 1, p, q} SUBSET 1..r+1 /\ q < p ==> dh (p + 1,p,q) = &0) ==> (?e. &0 < e /\ (!t. abs t < e ==> f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\ f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; COMMENT "prelims"; COMMENT "find collinear epsilon"; TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC)); RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]); BY(ASM_MESON_TAC[]); TYPIFY `!i j. i IN 0..r+2 /\ j IN 0..r+2 /\ ~collinear {vec 0,w i,w j} ==> (?dc. &0 < dc /\ (!t. abs t < dc ==> ~collinear {vec 0, f (w i) t, f (w j) t}))` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`&0`;`(vec 0):real^3`;`f (w i)`;`f (w j)`]; RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;IN_NUMSEG]); ANTS_TAC; BY(ASM_MESON_TAC[]); BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]); COMMENT "skolemize collinear"; TYPIFY `?dc. !i. (&0 < dc) /\ (i IN 0..r+2 ==> (!j. j IN 0..r+2 /\ ~collinear {vec 0,w i,w j} ==> (!t. abs t < dc ==> ~collinear {vec 0, f (w i) t, f (w j) t})))` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`j`]); ANTS_TAC; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]); DISCH_THEN (C INTRO_TAC [`t`]); ANTS_TAC; BY(REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]); GEN_TAC; REWRITE_TAC[MESON [arith `&0 < &1`] `(?dc. &0 < dc /\ (a ==> (!j. b j /\ c j ==> r dc j))) <=> (a ==> (?dc. !j. &0 < dc /\ (b j ==> (c j ==> r dc j))))`]; DISCH_TAC; GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `!` MP_TAC; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_THEN (C INTRO_TAC [`t`]); ANTS_TAC; BY(REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`]); BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[arith `&0 < &1`]); FIRST_X_ASSUM_ST `collinear` MP_TAC THEN BURY_MP_TAC; FIRST_X_ASSUM_ST `collinear` kill; COMMENT "find dih epsilon"; TYPIFY `!i j k e. &0 < e /\ i IN 1..r+1 /\ j IN 1 ..r+1 /\ k IN 1..r+1 /\ ~(i=j) /\ ~(i=k) /\ dh (i,j,k) = &0 ==> (? d. &0 < d /\ (!t. abs t < d ==> dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t) < e))` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "dh" THEN REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC)); RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]); BY(ASM_MESON_TAC[]); INTRO_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE [`\(t:real). (vec 0):real^3`;`f (w i)`;`f (w j)`;`f (w k)`;`&0`]; ANTS_TAC; RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;pairwise]); REWRITE_TAC[CONTINUOUS_CONST]; FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC); ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]); TYPIFY_GOAL_THEN `k <= r + 2 /\ j <= r + 2 /\ i <= r + 2 ` (unlist REWRITE_TAC); BY(ASM_ARITH_TAC); REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC; BY(TYPIFY `i` EXISTS_TAC THEN ASM_ARITH_TAC); BY(TYPIFY `j` EXISTS_TAC THEN ASM_ARITH_TAC); BY(TYPIFY `k` EXISTS_TAC THEN ASM_ARITH_TAC); REWRITE_TAC[real_continuous_atreal]; DISCH_THEN (C INTRO_TAC [`e`]); ASM_REWRITE_TAC[arith `abs (x' - &0) = abs x'`] THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `d` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `i <= r + 2` (REPEAT o GMATCH_SIMP_TAC); ASM_REWRITE_TAC[]; RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]); ASM_SIMP_TAC[arith `i <= r + 1 ==> i <= r + 2`]; BY(REAL_ARITH_TAC); COMMENT "merge dih epsilon"; TYPIFY `!e. &0 < e ==> (?d. !i. (&0 < d) /\ (i IN 1..r+1 ==> (!j k. j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i=k) /\ dh(i,j,k)= &0 ==> (!t. abs t < d ==> dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t) < e))))` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`j`;`k`]); ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); GEN_TAC; REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (p ==> (!j k. a j /\ r j k ==> u j k d))) <=> (p ==> (?d. !j. &0 < d /\ (a j ==> (!k. r j k ==> u j k d))))`]; DISCH_TAC; GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`k`]); ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); GEN_TAC; REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (p ==> (!k. a k /\ r k ==> u k d))) <=> (p ==> (?d. !k. &0 < d /\ (a k ==> (r k ==> u k d))))`]; DISCH_TAC; GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `dihV` MP_TAC; ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); GEN_TAC; REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (a ==> b ==> c d)) <=> (a /\ b ==> (?d. &0 < d /\ c d))`]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`;`k`;`e`]); DISCH_THEN MATCH_MP_TAC; BY(ASM_REWRITE_TAC[]); FIRST_X_ASSUM MP_TAC; FIRST_X_ASSUM kill; REPEAT WEAKER_STRIP_TAC; COMMENT "azim lb"; TYPIFY `?c. !i. (&0 < c) /\ (i IN 1..r+1 ==> c < azim (vec 0) (w i) (w (i+1)) (w (i-1)))` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; BY(REAL_ARITH_TAC); GEN_TAC; REWRITE_TAC[MESON[arith `&0 < &1`] `(?c. &0 < c /\ (b ==> r c)) <=> (b ==> (?c. &0 < c /\ r c))`]; DISCH_TAC; TYPIFY `azim (vec 0) (w i) (w (i+1)) (w (i-1)) / &2` EXISTS_TAC; FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`i`]); ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC; COMMENT "azim deform lower bound"; TYPIFY `!i. i IN 1..r+1 ==> (?d. &0 < d /\ (!t. abs t < d ==> (c < azim (vec 0) (f (w i) t) (f (w(i+1)) t) (f (w(i-1)) t))))` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC)); RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]); BY(ASM_MESON_TAC[]); INTRO_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE [`\(t:real). (vec 0):real^3`;`f (w i)`;`f (w (i+1))`;`f (w (i-1))`;`&0`]; ANTS_TAC; RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;pairwise]); REWRITE_TAC[CONTINUOUS_CONST]; FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC); ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]); TYPIFY_GOAL_THEN `i - 1 <= r + 2 /\ i + 1 <= r + 2 /\ i <= r + 2` (unlist REWRITE_TAC); BY(ASM_ARITH_TAC); GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2); REWRITE_TAC[GSYM azim_pos_iff_nz]; TYPIFY_GOAL_THEN ` ~collinear {vec 0, w i, w (i - 1)}` (unlist REWRITE_TAC); FIRST_X_ASSUM_ST `collinear` kill; BY((FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC); REPEAT CONJ_TAC THEN (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC; BY(TYPIFY `i` EXISTS_TAC THEN ASM_ARITH_TAC); BY(TYPIFY `i+1` EXISTS_TAC THEN ASM_ARITH_TAC); BY(TYPIFY `i-1` EXISTS_TAC THEN ASM_ARITH_TAC); REWRITE_TAC[real_continuous_atreal]; FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC); RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]); TYPIFY_GOAL_THEN `i - 1 <= r + 2 /\ i + 1 <= r + 2 /\ i <= r + 2` (unlist REWRITE_TAC); BY(ASM_ARITH_TAC); DISCH_THEN (C INTRO_TAC [`abs(azim (vec 0) (w i) (w (i+1)) (w (i-1)) - c)`]); FIRST_X_ASSUM (C INTRO_TAC [`i`]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `c < azim a1 a2 a3 a4` MP_TAC; ASM_REWRITE_TAC[]; DISCH_TAC; FIRST_X_ASSUM_ST `abs` MP_TAC; ANTS_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); ASM_REWRITE_TAC[arith `abs (x' - &0) = abs x'`] THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `d` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); COMMENT "skolemize the azim delta"; TYPIFY `?d. !i. &0 < d /\ (i IN 1..r+1 ==> (!t. abs t < d ==> c < azim (vec 0) (f (w i) t) (f (w (i + 1)) t) (f (w (i - 1)) t)))` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[arith `&0< &1`]); FIRST_X_ASSUM_ST `!i. i IN s ==> u` kill; COMMENT "skolemize azim<=pi"; TYPIFY `?d2. !i. &0 < d2 /\ (i IN 1..r+1 ==> (!t. abs t < d2 ==> azim (vec 0) (f (w i) t) (f (w (i + 1)) t) (f (w (i - 1)) t) <= pi))` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_NUMSEG]; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(FIRST_X_ASSUM_ST `azim a b c d <= pi` MP_TAC THEN MESON_TAC[arith `&0< &1`]); FIRST_X_ASSUM_ST `!i. i IN s ==> u` kill; COMMENT "pick eps"; TYPIFY `?e. &0 < e /\ &2 * e = c` (C SUBGOAL_THEN MP_TAC); RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]); TYPIFY `c / &2` EXISTS_TAC; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE) o GSYM); FIRST_X_ASSUM (C INTRO_TAC [`e`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `?d'3. !d''. (&0 < d'3) /\ (d'' IN {d,d',d2,dc} ==> d'3 <= d'')` (C SUBGOAL_THEN MP_TAC); GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON); REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]; CONJ_TAC; BY(REAL_ARITH_TAC); GEN_TAC; RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]); TYPIFY `if (d'' IN {d,d',d2,dc}) then d'' else &1` EXISTS_TAC; CONJ_TAC; ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < d` MP_TAC) THEN REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY] THEN REAL_ARITH_TAC); BY(REAL_ARITH_TAC); REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]; REPEAT WEAKER_STRIP_TAC; TYPIFY `d'3` EXISTS_TAC; RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]); ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC Xivphks.XIVPHKS_SHIFT [`\i. wedge_ge (vec 0) (f (w (i)) t) (f (w (i + 1)) t) (f (w (i-1)) t)`;`\ (i,j,k). azim (vec 0) (f (w i) t) (f (w (j)) t) (f (w (k)) t)`;`\ (i,j,k). dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t)`;`e`;`r`;`\i. f (w i) t`]; ASM_REWRITE_TAC[]; ANTS_TAC; REWRITE_TAC[pairwise]; RULE_ASSUM_TAC(REWRITE_RULE[pairwise]); TYPIFY `!j. j IN 0..r+1 ==> j IN 0..r+2` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); TYPIFY `!t. abs t < d'3 ==> abs t < dc` (C SUBGOAL_THEN ASSUME_TAC); REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`dc`]); BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); CONJ_TAC; REPEAT (FIRST_X_ASSUM_ST `azim` kill); BY(ASM_MESON_TAC[]); CONJ_TAC; REPEAT (FIRST_X_ASSUM_ST `azim` kill); TYPIFY `!j. j IN 1..r+2 ==> j IN 0..r+2` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); BY(ASM_MESON_TAC[]); CONJ_TAC; TYPIFY `abs t < d'` (C SUBGOAL_THEN ASSUME_TAC); REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d'`]); BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(ASM_MESON_TAC[]); CONJ_TAC; TYPIFY `abs t < d2` (C SUBGOAL_THEN ASSUME_TAC); REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d2`]); BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); BY(ASM_MESON_TAC[]); REPEAT (FIRST_X_ASSUM_ST `azim` kill); TYPIFY `abs t < d` (C SUBGOAL_THEN ASSUME_TAC); REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d`]); BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); TYPIFY `!i j k. {i,j,k} SUBSET 1..r+1 ==> i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1` (C SUBGOAL_THEN ASSUME_TAC); BY(SET_TAC[]); CONJ_TAC; BY(ASM_MESON_TAC[]); CONJ_TAC; REPEAT (FIRST_X_ASSUM_ST `collinear` kill); BY(ASM_MESON_TAC[arith `~(p = p+1)`;arith `q > p+1 ==> ~(p = q)`]); BY(ASM_MESON_TAC[arith `~(p = p+1)`;arith `q < p ==> ~(p+1 = q)`]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`r`;`1`]); FIRST_X_ASSUM (C INTRO_TAC [`r`;`1`]); REWRITE_TAC[arith `(r:num) <= r`;arith `1 + 1 = 2 /\ 1 - 1 = 0 /\ (1+r)+1 = r + 2 /\ 1 + r <= r + 1 /\ (1 + r) - 1 = r`]; REWRITE_TAC[arith `1 + r = r + 1`]; BY(MESON_TAC[]) ]);; (* }}} *) let XIV_ECAU = prove_by_refinement( `!f r w a b. deformation f {w i | i <= r + 2} (a,b) /\ (!i. i IN 2..r+1 ==> w i IN aff_gt {vec 0,w 1 } {w 2} ) /\ cyclic_set {w i | i IN 1..r+1 } (vec 0) ((w 1) cross (w 2)) /\ (!i. i IN 1..r ==> azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w i) = w (i+1)) /\ pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\ pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\ (!i. ?e2. i IN 1..r+1 ==> &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\ (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1))) ==> (?e. &0 < e /\ (!t. abs t < e ==> f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\ f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC XIV_DEFORMATION; TYPED_ABBREV_TAC `dh = \ (i,j,k). dihV (vec 0) (w i) (w j) (w k)`; GEXISTL_TAC [`dh`;`a`;`b`]; ASM_REWRITE_TAC[]; INTRO_TAC KCZXLLE_SYM [`w o SUC`;`r`]; REWRITE_TAC[o_THM;arith `1 <= r+1 /\ SUC 0 = 1 /\ SUC 1 = 2`]; TYPIFY `{w (SUC i) | i <= r } = {w i | i IN 1..r+1}` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG]; BY(MESON_TAC[arith `i <= r ==> (1 <= SUC i /\ SUC i <= r + 1)`;arith `(1 <= i /\ i <= r+1) ==> (PRE i <= r /\ SUC (PRE i) = i)`]); ASM_REWRITE_TAC[]; TYPIFY_GOAL_THEN `(!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, w (SUC i), w (SUC j)})` (unlist REWRITE_TAC); REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC(REWRITE_RULE[pairwise]); FIRST_X_ASSUM (C INTRO_TAC [`SUC i`;`SUC j`]); REWRITE_TAC[SUC_INJ]; ASM_REWRITE_TAC[]; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); TYPIFY_GOAL_THEN ` (!i. 1 <= i /\ i <= r ==> w (SUC i) IN aff_gt {vec 0, w 1} {w 2})` (unlist REWRITE_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); TYPIFY_GOAL_THEN `(!i. i < r ==> azim_cycle {w i | i IN 1..r + 1} (vec 0) (w 1 cross w 2) (w (SUC i)) = w (SUC (i + 1)))` (unlist REWRITE_TAC); REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[arith `SUC (i + 1) = SUC i + 1`]; FIRST_X_ASSUM MATCH_MP_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); TYPIFY `!i j k. i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i = k) /\ azim (vec 0) (w i) (w j) (w k) = &0 ==> dihV (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC (GSYM Polar_fan.AZIM_DIHV_SAME_STRONG); RULE_ASSUM_TAC (REWRITE_RULE[pairwise]); TYPIFY_GOAL_THEN `~collinear {vec 0, w i, w j} /\ ~collinear {vec 0, w i, w k}` (unlist REWRITE_TAC); BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); ASM_REWRITE_TAC[]; BY(MP_TAC PI_POS THEN REAL_ARITH_TAC); DISCH_TAC; EXPAND_TAC "dh" THEN REWRITE_TAC[]; REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY]; FIRST_X_ASSUM MP_TAC; TYPIFY_GOAL_THEN `(!i j k. k <= r /\ j <= r /\ 1 <= r /\ i <= r /\ (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i)) ==> azim (vec 0) (w (SUC i)) (w (SUC j)) (w (SUC k)) = &0) <=> (!i j k. k IN 1..r+1 /\ i IN 1..r+1 /\ j IN 1..r+1 /\ (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i)) ==> azim (vec 0) (w (i)) (w (j)) (w ( k)) = &0)` (unlist REWRITE_TAC); REWRITE_TAC[IN_NUMSEG]; MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`); CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`PRE i`;`PRE j`;`PRE k`]); ASM_SIMP_TAC[arith `1 <= i ==> SUC (PRE i) = i`]; DISCH_THEN MATCH_MP_TAC; BY(FIRST_X_ASSUM DISJ_CASES_TAC THEN REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); FIRST_X_ASSUM MATCH_MP_TAC; BY(FIRST_X_ASSUM DISJ_CASES_TAC THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); DISCH_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC; FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC); REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC); BY(ARITH_TAC); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC; FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC); BY(REPLICATE_TAC 1(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC; FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC); BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC) ]);; (* }}} *) (* was cycle_set_scale *) let cyclic_set_scale = prove_by_refinement( `!U t (e:real^A). ~(t = &0) ==> (cyclic_set U (vec 0) (t % e) <=> cyclic_set U (vec 0) e)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.cyclic_set]; REPEAT WEAKER_STRIP_TAC; TYPIFY `~FINITE U` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); ONCE_REWRITE_TAC[varith `vec 0 = a <=> a = vec 0`]; ASM_REWRITE_TAC[VECTOR_MUL_EQ_0]; TYPIFY `(e = vec 0)` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); RULE_ASSUM_TAC(REWRITE_RULE[]); ASM_REWRITE_TAC[]; TYPIFY `affine hull {vec 0, t % e} = affine hull {vec 0,e}` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[AFFINE_HULL_2_ALT]; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_UNIV;arith `vec 0 + a = a /\ x - vec 0 = x`]; GEN_TAC; REWRITE_TAC[VECTOR_MUL_ASSOC]; BY(ASM_MESON_TAC[arith `~(t = &0) ==> u = (u * inv t) * t`]); TYPIFY `~(U INTER affine hull {vec 0, e} = {})` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[]); RULE_ASSUM_TAC(REWRITE_RULE[]) THEN ASM_REWRITE_TAC[]; REWRITE_TAC[arith `vec 0 - x = -- x`]; REWRITE_TAC[arith `-- (t % e) = t % (-- e)`]; REWRITE_TAC[VECTOR_MUL_ASSOC]; BY(ASM_MESON_TAC[arith `~(t = &0) ==> u = (u * inv t) * t`]) ]);; (* }}} *) let projection_scale = prove_by_refinement( `!e u t. (~(t = &0)) ==> projection (t % e) u = projection e u`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[Sphere.projection]; REWRITE_TAC[DOT_LMUL;DOT_RMUL]; REWRITE_TAC[VECTOR_MUL_ASSOC]; TYPIFY ` ((t * (u dot e)) / (t * t * (e dot e)) * t) = (u dot e) / (e dot e)` (C SUBGOAL_THEN SUBST1_TAC); TYPIFY `e dot e = &0` ASM_CASES_TAC; ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); Calc_derivative.CALC_ID_TAC; BY(ASM_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[]) ]);; (* }}} *) let azim_cycle_scale = prove_by_refinement( `!U t e . (&0 < t) ==> azim_cycle U (vec 0) (t % e) = azim_cycle U (vec 0) e `, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[FUN_EQ_THM]; GEN_TAC; TYPIFY `U SUBSET {x}` ASM_CASES_TAC; BY(ASM_SIMP_TAC[Wrgcvdr_cizmrrh.W_SUBSET_SINGLETON_IMP_IDE]); REWRITE_TAC[Trigonometry.YESEEWW]; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `x - vec 0 = x`]; TYPIFY `(!x u. azim (vec 0) (t % e) x u = azim (vec 0) e x u) /\ (!u. projection (t % e) u = projection e u)` ENOUGH_TO_SHOW_TAC; BY(DISCH_THEN (unlist REWRITE_TAC)); ASM_SIMP_TAC[AZIM_SPECIAL_SCALE]; GEN_TAC; BY(ASM_SIMP_TAC[projection_scale;arith `&0 < t ==> ~(t = &0)`]) ]);; (* }}} *) let AZIM_CYCLE_SING_ALT = prove_by_refinement( `!x u v w. azim_cycle {v} x u w = v`, (* {{{ proof *) [ REWRITE_TAC[Sphere.azim_cycle]; REPEAT WEAKER_STRIP_TAC; TYPIFY `v = w` ASM_CASES_TAC; BY(ASM_REWRITE_TAC[SUBSET_REFL]); TYPIFY_GOAL_THEN `~({v} SUBSET {w})` (unlist REWRITE_TAC); BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]); TYPIFY_GOAL_THEN `!a b. {a} (b:real^3) <=> b IN {a}` (unlist REWRITE_TAC); BY(MESON_TAC[IN]); REWRITE_TAC[IN_SING]; SELECT_TAC; PROOF_BY_CONTR_TAC; FIRST_X_ASSUM_ST `azim` MP_TAC; REWRITE_TAC[]; TYPIFY `v` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; BY(ASM_REWRITE_TAC[arith `x <= x`]) ]);; (* }}} *) let IDENTIFY_AZIM_CYCLE_SIMPLE = prove_by_refinement( `!W v w p u. ~(W SUBSET {p}) /\ p IN W /\ cyclic_set W v w /\ (~(u = p) /\ u IN W) /\ (!q. ~(q = p) /\ q IN W /\ ~(q =u) ==> azim v w p u < azim v w p q) ==> azim_cycle W v w p = u`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC Wrgcvdr_cizmrrh.IDENTIFY_AZIM_CYCLE; ASM_REWRITE_TAC[]; CONJ_TAC; BY(ASM_MESON_TAC [Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR]); CONJ_TAC; BY(ASM_MESON_TAC[IN]); REPEAT WEAKER_STRIP_TAC; TYPIFY `q = u` ASM_CASES_TAC; ASM_REWRITE_TAC[]; BY(MESON_TAC[arith `x<=x`]); DISJ1_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(ASM_MESON_TAC[IN]) ]);; (* }}} *) let coplanar_cross_scale = prove_by_refinement( `!u1 u2 v1 v2. coplanar {vec 0,u1,u2,v1,v2} /\ &0 < (v1 cross v2) dot (u1 cross u2) ==> (?t. &0 < t /\ v1 cross v2 = t % (u1 cross u2))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `~collinear {vec 0,u1,u2}` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[GSYM CROSS_EQ_0]; DISCH_TAC; FIRST_X_ASSUM_ST `dot` MP_TAC THEN ASM_REWRITE_TAC[]; REWRITE_TAC[DOT_RZERO]; BY(REAL_ARITH_TAC); INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`u1`;`u2`;`v1`]; INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`u1`;`u2`;`v2`]; ASM_REWRITE_TAC[]; TYPIFY_GOAL_THEN `coplanar {v2,vec 0,u1,u2} /\ coplanar {v1,vec 0,u1,u2} ` (unlist REWRITE_TAC); BY(ASM_MESON_TAC[COPLANAR_SUBSET;SET_RULE `{v2,v0,u1,u2} SUBSET {v0,u1,u2,v1,v2}`;SET_RULE `{v1,v0,u1,u2} SUBSET {v0,u1,u2,v1,v2}`]); REPEAT WEAKER_STRIP_TAC; INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`u1`;`u2`;`v1`]; INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`u1`;`u2`;`v2`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `v1 cross v2 = (t1' * t2 - t2' * t1) % (u1 cross u2)` (C SUBGOAL_THEN ASSUME_TAC); ASM_REWRITE_TAC[CROSS_RADD;CROSS_LADD;CROSS_RMUL;CROSS_LMUL;CROSS_REFL]; TYPIFY `u2 cross u1 = -- (u1 cross u2)` (C SUBGOAL_THEN SUBST1_TAC); BY(MESON_TAC[CROSS_SKEW]); BY(VECTOR_ARITH_TAC); TYPIFY `t1' * t2 - t2' * t1` EXISTS_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `dot` MP_TAC; ASM_REWRITE_TAC[DOT_LMUL]; GMATCH_SIMP_TAC (CONJUNCT2 Real_ext.REAL_PROP_POS_LMUL); REWRITE_TAC[DOT_POS_LT]; BY(ASM_MESON_TAC[CROSS_EQ_0]) ]);; (* }}} *) let azim_cycle_distinct = prove_by_refinement( `!U e v w. FINITE U /\ v IN U /\ w IN U /\ ~(v = w) /\ (!v. v IN U ==> ~(e dot (v cross azim_cycle U (vec 0) e v) = &0)) ==> (&0 < azim (vec 0) e v w)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `~(e = vec 0)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_TAC; FIRST_X_ASSUM (C INTRO_TAC [`v`]); BY(ASM_REWRITE_TAC[DOT_LZERO]); TYPIFY `!v. v IN U ==> ~collinear {vec 0,e,v}` (C SUBGOAL_THEN ASSUME_TAC); GEN_TAC THEN DISCH_TAC; ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`v'`]); ASM_REWRITE_TAC[CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF]; BY(REAL_ARITH_TAC); TYPIFY `~collinear {vec 0,e,azim_cycle U (vec 0) e v}` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]); TYPIFY `&0 < azim (vec 0) e v (azim_cycle U (vec 0) e v)` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[azim_pos_iff_nz]; GMATCH_SIMP_TAC AZIM_EQ_0; ASM_SIMP_TAC[]; GMATCH_SIMP_TAC AFF_GT_2_1; REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; BY(ASM_MESON_TAC[Fan.th3a]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `dot` (C INTRO_TAC [`v`]); ASM_REWRITE_TAC[]; TYPED_ABBREV_TAC `u = azim_cycle U (vec 0) e v`; FIRST_X_ASSUM_ST `%` SUBST1_TAC; REWRITE_TAC[DOT_RMUL;DOT_RADD;DOT_RZERO;CROSS_LADD;CROSS_LMUL;CROSS_LZERO;CROSS_REFL;DOT_CROSS_SELF]; BY(REAL_ARITH_TAC); TYPIFY `w = azim_cycle U (vec 0) e v` ASM_CASES_TAC; BY(ASM_MESON_TAC[]); INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`e`;`v`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`w`]); ASM_REWRITE_TAC[]; BY(ASM_TAC THEN REAL_ARITH_TAC) ]);; (* }}} *) (* let azim_cycle_nondeg = prove_by_refinement( `!U uu r. 1 < r /\ U = {uu i | i IN 1..r+1 } /\ (!i. i IN 1..r ==> u i IN aff_gt{vec 0,u (r+1)} {u (r)} /\ (!i. i IN 1..r ==> azim_cycle U (vec 0) (uu 1 cross uu 2) (uu i) = (uu (i+1))) /\ azim_cycle U (vec 0) (uu 1 cross uu 2) (uu (r+1)) = u 1 /\ (!i. i IN 1..r ==> &0 < (uu i cross uu (i+1)) dot (uu 1 cross uu 2)) ==> ((!i. i IN 1..r ==> ~((uu 1 cross uu 2) dot (uu i cross uu (i+1)) = &0)) (!i. (`, (* {{{ proof *) [ # ]);; (* }}} *) *) let azim_cycle_neg = prove_by_refinement( `!U e v w. FINITE U /\ v IN U /\ azim_cycle U (vec 0) e v = w /\ (!v. v IN U ==> ~(e dot (v cross azim_cycle U (vec 0) e v) = &0)) ==> (azim_cycle U (vec 0) (-- e) w = v)`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `~(e = vec 0)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_TAC; FIRST_X_ASSUM (C INTRO_TAC [`v`]); BY(ASM_REWRITE_TAC[DOT_LZERO]); TYPIFY `!v. v IN U ==> ~collinear {vec 0,e,v}` (C SUBGOAL_THEN ASSUME_TAC); GEN_TAC THEN DISCH_TAC; ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`v'`]); ASM_REWRITE_TAC[CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF]; BY(REAL_ARITH_TAC); TYPIFY `w IN U` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]); PROOF_BY_CONTR_TAC; INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`-- (e:real^3)`;`w`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `~(v = w)` (C SUBGOAL_THEN ASSUME_TAC); DISCH_TAC; FIRST_X_ASSUM_ST `dot` (C INTRO_TAC [`v`]); BY(ASM_REWRITE_TAC[CROSS_REFL;DOT_RZERO]); TYPIFY `&0 < azim (vec 0) e v w` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC azim_cycle_distinct; BY(ASM_MESON_TAC[]); FIRST_X_ASSUM_ST `IN` (C INTRO_TAC [`v`]); ASM_REWRITE_TAC[]; TYPED_ABBREV_TAC `w' = azim_cycle U (vec 0) (-- e) w`; TYPIFY `w' IN U` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]); REPEAT (GMATCH_SIMP_TAC Yxionxl2.AZIM_COMPL_NEG); CONJ_TAC; BY(ASM_MESON_TAC[]); CONJ_TAC; BY(ASM_MESON_TAC[]); DISCH_TAC; TYPIFY `azim (vec 0) e v w' + azim (vec 0) e w' w = azim (vec 0) e v w` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC (GSYM Fan.sum5_azim_fan); BY(ASM_SIMP_TAC[]); INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`(e:real^3)`;`v`]; ASM_REWRITE_TAC[]; DISCH_THEN (C INTRO_TAC [`w'`]); ASM_REWRITE_TAC[]; DISCH_TAC; TYPIFY `azim (vec 0) e v w + azim (vec 0) e w w' = azim (vec 0) e v w'` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC (GSYM Fan.sum4_azim_fan); BY(ASM_SIMP_TAC[]); TYPIFY `&0 <= azim (vec 0) e w w' /\ &0 <= azim (vec 0) e w' w` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[Counting_spheres.AZIM_NN]); TYPIFY `azim (vec 0) e w w' = &0` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_TAC THEN REAL_ARITH_TAC); TYPIFY `(w' = w)` (C SUBGOAL_THEN ASSUME_TAC); PROOF_BY_CONTR_TAC; INTRO_TAC azim_cycle_distinct [`U`;` (e:real^3)`;`w`;`w'`]; ASM_REWRITE_TAC[]; BY(REAL_ARITH_TAC); INTRO_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`U`;`w`;`-- (e:real^3)`;`(vec 0):real^3`]; ASM_REWRITE_TAC[]; BY(ASM_TAC THEN SET_TAC[]) ]);; (* }}} *) (* let azim_cycle_neg = prove_by_refinement( `!U e v w. ~(U SUBSET {w}) /\ FINITE U /\ cyclic_set U (vec 0) e /\ v IN U /\ ~(e dot (v cross w) = &0) /\ azim_cycle U (vec 0) (e ) v = w ==> azim_cycle U (vec 0) (-- e) w = v`, (* {{{ proof *) [ g/r typ `U SUBSET {v}` asmcase art[Sphere.azim_cycle] amt[] st/r intro (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`U`;`v`;`e`;`(vec 0):real^3`] art[] st/r mmp IDENTIFY_AZIM_CYCLE_SIMPLE art[] conj art[IN] conj rt[arith `-- e = (-- &1) % e`] gm cyclic_set_scale art[] rat st/r fxa (C intro [`q`]) ants amt[IN] dt repeat (gm Yxionxl2.AZIM_COMPL_NEG) typ `~collinear {vec 0, e, w} /\ ~collinear {vec 0, e, q} /\ ~collinear {vec 0, e, v}` sat ort[setr `{a,e,w} = {w,a,e}`] repeat (gm Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR) amt[IN] art[] rt[arith `x < y <=> ~(y <= x)`] dt (* COME BACK. TO HERE. still problems with degenerate cases. make azim progression condition on all of U *) ]);; (* }}} *) *) let XIV_ECAU_BACK = prove_by_refinement( `!f r w a b. deformation f {w i | i <= r + 2} (a,b) /\ 1 <= r /\ (!i. i IN 1..r ==> w i IN aff_gt {vec 0,w (r+1) } {w r} ) /\ cyclic_set {w i | i IN 1..r+1 } (vec 0) ((w 1) cross (w 2)) /\ // &0 < (w r cross (w (r+1))) dot (w 1 cross w 2) /\ (!i. i IN 1..r ==> &0 < (w i cross (w (i+1))) dot (w 1 cross w 2)) /\ {w 1, w 2} SUBSET aff_gt {vec 0,w (r+1)} {w r} /\ (!i. i IN 1..r ==> azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w i) = w (i+1)) /\ azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w (r+1)) = w 1 /\ pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\ pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\ (!i. ?e2. i IN 1..r+1 ==> &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\ (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1))) ==> (?e. &0 < e /\ (!t. abs t < e ==> f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\ f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; TYPIFY `&0 < (w r cross (w (r+1))) dot (w 1 cross w 2)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM MATCH_MP_TAC; REWRITE_TAC[IN_NUMSEG]; BY(ASM_REWRITE_TAC[arith `r <= (r:num)`]); MATCH_MP_TAC XIV_DEFORMATION; TYPED_ABBREV_TAC `dh = \ (i,j,k). dihV (vec 0) (w i) (w j) (w k)`; GEXISTL_TAC [`dh`;`a`;`b`]; ASM_REWRITE_TAC[]; INTRO_TAC KCZXLLE_SYM [`\i. w((r+1)-i) `;`r`]; REWRITE_TAC[arith `1 <= r+1 /\ ((r+1)-0 = (r+1)) /\ ((r+1)-1 = r)`]; TYPIFY `{w ((r+1)-i) | i | i <= r } = {w i | i IN 1..r+1}` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG]; GEN_TAC; MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`); CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; TYPIFY `(r+1)-i` EXISTS_TAC; REWRITE_TAC[]; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); ASM_REWRITE_TAC[]; TYPIFY `(r+1)-i` EXISTS_TAC; CONJ_TAC; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); AP_TERM_TAC; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); COMMENT "collinear"; TYPIFY_GOAL_THEN `(!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, w ((r+1)-i), w ((r+1)-j)})` (unlist REWRITE_TAC); REPEAT WEAKER_STRIP_TAC; RULE_ASSUM_TAC(REWRITE_RULE[pairwise]); FIRST_X_ASSUM (C INTRO_TAC [`(r+1)-i`;`(r+1)-j`]); ASM_REWRITE_TAC[]; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); COMMENT "aff_gt"; TYPIFY_GOAL_THEN ` (!i. 1 <= i /\ i <= r ==> w ((r+1)-i) IN aff_gt {vec 0, w (r+1)} {w r})` (unlist REWRITE_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); COMMENT "cyclic set"; INTRO_TAC coplanar_cross_scale [`w 1`;`w 2`;`w r`;`w (r+1)`]; ANTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[coplanar]; GEXISTL_TAC [`(vec 0):real^3`;`w r`;`w (r+1)`]; TYPIFY `{vec 0,w r, w (r+1)} SUBSET affine hull {vec 0, w r, w (r + 1)} /\ {w 1, w 2} SUBSET affine hull {vec 0, w r, w (r + 1)}` ENOUGH_TO_SHOW_TAC; BY(SET_TAC[]); CONJ_TAC; BY(REWRITE_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL]); MATCH_MP_TAC SUBSET_TRANS; TYPIFY `aff_gt {vec 0,w(r+1)} {w r}` EXISTS_TAC; CONJ_TAC; BY(ASM_REWRITE_TAC[]); TYPIFY `{vec 0,w r, w(r+1)} = {vec 0,w (r+1)} UNION {w (r)}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]); REPEAT WEAKER_STRIP_TAC; TYPIFY ` cyclic_set {w i | i IN 1..r + 1} (vec 0) (w (r + 1) cross w r)` (C SUBGOAL_THEN ASSUME_TAC); ONCE_REWRITE_TAC[CROSS_SKEW]; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `-- (t % v) = (-- t) % v`]; GMATCH_SIMP_TAC cyclic_set_scale; ASM_REWRITE_TAC[]; BY(FIRST_X_ASSUM_ST `&0 < t` MP_TAC THEN REAL_ARITH_TAC); COMMENT "azim_cycle"; TYPIFY `(!i. i < r ==> azim_cycle {w i | i IN 1..r + 1} (vec 0) (w (r + 1) cross w r) (w ((r + 1) - i)) = w ((r + 1) - (i + 1)))` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; ONCE_REWRITE_TAC[CROSS_SKEW]; ASM_REWRITE_TAC[]; REWRITE_TAC[arith `-- (t % v) = t % (-- v)`]; GMATCH_SIMP_TAC azim_cycle_scale; ASM_REWRITE_TAC[]; MATCH_MP_TAC azim_cycle_neg; ASM_REWRITE_TAC[]; CONJ_TAC; TYPIFY `{w i | i IN 1..r+1} = IMAGE w (1..r+1)` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); MATCH_MP_TAC FINITE_IMAGE; BY(REWRITE_TAC[FINITE_NUMSEG]); TYPIFY `(r+1)-(i+1) = r - i` (C SUBGOAL_THEN SUBST1_TAC); BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); CONJ_TAC; REWRITE_TAC[IN_ELIM_THM;IN_NUMSEG]; TYPIFY `r- (i:num)` EXISTS_TAC; BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); CONJ_TAC; TYPIFY `(r+1) - i = (r - i) + 1` (C SUBGOAL_THEN SUBST1_TAC); BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); FIRST_X_ASSUM MATCH_MP_TAC; BY(REWRITE_TAC[IN_NUMSEG] THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); REWRITE_TAC[IN_NUMSEG;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; ASM_REWRITE_TAC[]; TYPIFY `(i':num) < r+1` ASM_CASES_TAC; TYPIFY `azim_cycle {w i | 1 <= i /\ i <= r + 1} (vec 0) (w 1 cross w 2) (w i') = w (i'+1)` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[GSYM IN_NUMSEG]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); MATCH_MP_TAC (arith `&0 < x ==> ~(x = &0)`); REWRITE_TAC[DOT_SYM]; FIRST_X_ASSUM MATCH_MP_TAC; BY(REWRITE_TAC[IN_NUMSEG] THEN REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); TYPIFY `i' = r+1` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); ASM_REWRITE_TAC[GSYM IN_NUMSEG]; TYPIFY `w 1 IN aff_gt {vec 0, w(r+1)} {w r}` (C SUBGOAL_THEN MP_TAC); BY(FIRST_X_ASSUM_ST `aff_gt` MP_TAC THEN SET_TAC[]); GMATCH_SIMP_TAC AFF_GT_2_1; REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; MATCH_MP_TAC Fan.th3a; RULE_ASSUM_TAC(REWRITE_RULE[pairwise]); FIRST_X_ASSUM MATCH_MP_TAC; REWRITE_TAC[IN_NUMSEG]; BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `e = w 1 cross w 2`; FIRST_X_ASSUM_ST `dot` MP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_RZERO;CROSS_REFL;DOT_RMUL;DOT_RADD;DOT_RZERO]; REWRITE_TAC[arith `t * &0 + x = x`]; ONCE_REWRITE_TAC[CROSS_SKEW]; REWRITE_TAC[DOT_RNEG;REAL_ENTIRE]; ONCE_REWRITE_TAC[DOT_SYM]; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < x` MP_TAC) THEN REAL_ARITH_TAC); FIRST_X_ASSUM_ST `!i j k. P` MP_TAC; ASM_REWRITE_TAC[]; REPLICATE_TAC 4 (FIRST_X_ASSUM kill); DISCH_TAC; COMMENT "work on dihedral angles"; TYPIFY `!i j k. k IN 1..r+1 /\ j IN 1..r+1 /\ i IN 1..r+1 /\ (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i)) ==> azim (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[IN_NUMSEG]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`(r+1)-i`;`(r+1)-j`;`(r+1)-k`]); ASM_SIMP_TAC[arith `i <= r+1 ==> (r+1)-((r+1)-i) = i`]; DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); FIRST_X_ASSUM_ST `(r+1)-i` kill; TYPIFY `!i j k. i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i = k) /\ azim (vec 0) (w i) (w j) (w k) = &0 ==> dihV (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC (GSYM Polar_fan.AZIM_DIHV_SAME_STRONG); RULE_ASSUM_TAC (REWRITE_RULE[pairwise]); TYPIFY_GOAL_THEN `~collinear {vec 0, w i, w j} /\ ~collinear {vec 0, w i, w k}` (unlist REWRITE_TAC); BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC); ASM_REWRITE_TAC[]; BY(MP_TAC PI_POS THEN REAL_ARITH_TAC); EXPAND_TAC "dh" THEN REWRITE_TAC[]; REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY]; FIRST_X_ASSUM MP_TAC; DISCH_TAC; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC; FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC); REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC); BY(ARITH_TAC); CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC; FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC); BY(REPLICATE_TAC 1(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC; FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC); BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC) ]);; (* }}} *) let zlz_wedge_boundary = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) /\ (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==> (!x v. ?e3. x IN FF /\ v IN V ==> &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (f v t) IN wedge_in_fan_ge (f (FST x) t,f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E)))`, (* {{{ proof *) [ COMMENT "start here"; REPEAT WEAKER_STRIP_TAC; TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO; BY(ASM_REWRITE_TAC[]); INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`]; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC); BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]); REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `w = FST x`; TYPIFY `x = (w,rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC); TYPIFY `FST x,SND x = (w,rho_node1 FF w)` ENOUGH_TO_SHOW_TAC; BY(REWRITE_TAC[PAIR]); ASM_REWRITE_TAC[PAIR_EQ]; MATCH_MP_TAC EQ_SYM; MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE; BY(ASM_MESON_TAC[PAIR]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); TYPIFY `w IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]); TYPIFY `v IN {w, rho_node1 FF w, ivs_rho_node1 FF w}` ASM_CASES_TAC; INTRO_TAC zlz_wedge_refl [`a`;`b`;`V`;`E`;`FF`;`f`]; ASM_REWRITE_TAC[]; DISCH_THEN (C INTRO_TAC [`v`;`w`]); BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]); TYPIFY `rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V; BY(ASM_REWRITE_TAC[]); TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V; BY(ASM_REWRITE_TAC[]); TYPIFY `v IN wedge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` ASM_CASES_TAC; INTRO_TAC zlz_wedge_open [`a`;`b`;`V`;`E`;`FF`;`f`]; ASM_REWRITE_TAC[]; DISCH_THEN (C INTRO_TAC [`v`;`w`]); BY(ASM_REWRITE_TAC[]); TYPIFY `v IN wedge_ge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC); RULE_ASSUM_TAC(REWRITE_RULE[Localization.convex_local_fan]); ASM_TAC THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`w,rho_node1 FF w`]); ASM_REWRITE_TAC[]; REWRITE_TAC[SUBSET]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`v`]); ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND; BY(ASM_MESON_TAC[]); TYPIFY `azim (vec 0) w (rho_node1 FF w) v = &0 \/ azim (vec 0) w (rho_node1 FF w) v = azim (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM MP_TAC; BY(ASM_REWRITE_TAC[Reuhady.WEDGE_GE_WEDGE;IN_UNION;IN_ELIM_THM]); TYPIFY `?r. r < CARD V /\ v = ITER r (rho_node1 FF) w` (C SUBGOAL_THEN MP_TAC); INTRO_TAC (GEN_ALL Local_lemmas.LOFA_IMP_LT_CARD_SET_V) [`E`;`FF`;`V`;`w`]; REWRITE_TAC[EXTENSION;IN_ELIM_THM]; ASM_REWRITE_TAC[]; DISCH_THEN (C INTRO_TAC [`v`]); BY(ASM_REWRITE_TAC[]); REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)); TYPIFY `1 < r /\ r < CARD V - 1` (C SUBGOAL_THEN ASSUME_TAC); TYPIFY `~(r = 0) /\ ~(r = 1) /\ ~(r = CARD V - 1)` ENOUGH_TO_SHOW_TAC; BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); REWRITE_TAC[GSYM DE_MORGAN_THM]; DISCH_TAC; FIRST_X_ASSUM_ST `~(ITER r f w IN s INSERT t)` MP_TAC; REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]; REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_REWRITE_TAC[ITER;ITER_1]; BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]); BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]); INTRO_TAC (GEN_ALL Local_lemmas.EGHNAVX) [`E`;`V`;`(\i. azim (vec 0) w (rho_node1 FF w) (ITER i (rho_node1 FF) w))`;`FF`;`r`;`w`;`(\i. ITER i (rho_node1 FF) w)`;`CARD V` ]; ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;ITER_1]; ANTS_TAC; MATCH_MP_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN; BY(ASM_MESON_TAC[]); REWRITE_TAC[LEFT_IMP_EXISTS_THM]; ASM_SIMP_TAC[arith `1 < r ==> 0 < r`]; (REPEAT WEAKER_STRIP_TAC); COMMENT "added material here"; COMMENT "eliminate wedge_in_fan_ge"; TYPIFY `?e3. &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> f (ITER r (rho_node1 FF) w) t IN wedge_ge (vec 0) (f w t) (f (rho_node1 FF w) t) (f (ivs_rho_node1 FF w) t))` ENOUGH_TO_SHOW_TAC; REPEAT WEAKER_STRIP_TAC; TYPIFY `if (e <= e3) then e else e3` EXISTS_TAC; CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `abs t < e` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND; CONJ_TAC; TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_IMAGE]; TYPIFY `w` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); FIRST_X_ASSUM_ST `wedge_ge` (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; DISCH_THEN MATCH_MP_TAC; BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); INTRO_TAC zlz_azim [`a`;`b`;`V`;`E`;`FF`;`f`]; ANTS_TAC; BY(ASM_REWRITE_TAC[]); DISCH_TAC; TYPIFY `!v. v IN V ==> &0 < azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v)` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; INTRO_TAC (GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) [`E`;`V`;`FF`]; ASM_REWRITE_TAC[]; DISCH_THEN (GMATCH_SIMP_TAC o GSYM); ASM_REWRITE_TAC[]; MATCH_MP_TAC Local_lemmas.INTERIOR_ANGLE1_POS; BY(ASM_REWRITE_TAC[]); COMMENT "azim_in_fan -> azim"; TYPIFY `!v. ?e2. v IN V ==> &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> azim (vec 0) (f v t) (f (rho_node1 FF v) t) (f (ivs_rho_node1 FF v) t) <= pi)` (C SUBGOAL_THEN ASSUME_TAC); REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`v', rho_node1 FF v'`]); REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; GMATCH_SIMP_TAC Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2; CONJ_TAC; BY(ASM_MESON_TAC[]); REPEAT WEAKER_STRIP_TAC; TYPIFY `if (e <= e2) then e else e2` EXISTS_TAC; CONJ_TAC; BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `abs t < e /\ abs t < e2` (C SUBGOAL_THEN ASSUME_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC); FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`v'`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`v'`;`t`]; ASM_REWRITE_TAC[]; DISCH_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM_ST `azim_in_fan` (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[arith `-- e2 < t /\ t < e2 <=> abs t < e2`]; MATCH_MP_TAC (arith `(a = b) ==> (a <= pi ==> b <= pi)`); ASM_REWRITE_TAC[]; GMATCH_SIMP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND; TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[IN_IMAGE]; TYPIFY `v'` EXISTS_TAC; BY(ASM_REWRITE_TAC[]); REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC); FIRST_X_ASSUM kill; COMMENT "end added"; COMMENT "MAIN BRANCH: follow forward azim = 0"; FIRST_X_ASSUM DISJ_CASES_TAC; FIRST_X_ASSUM MP_TAC; FIRST_X_ASSUM kill; DISCH_TAC; FIRST_X_ASSUM_ST `interior_angle1` MP_TAC; ASM_REWRITE_TAC[]; FIRST_X_ASSUM MP_TAC; REPLICATE_TAC 2 (FIRST_X_ASSUM kill); REPEAT WEAKER_STRIP_TAC; COMMENT "add KOM"; INTRO_TAC Local_lemmas.KOMWBWC [`E`;`V`;`affine hull {(vec 0),w,rho_node1 FF w}`;`r`;`FF`;`{ITER i (rho_node1 FF) w | i <= r}`;`w cross rho_node1 FF w`;`ITER r (rho_node1 FF) w`;`w`]; ASM_REWRITE_TAC[]; ANTS_TAC; REWRITE_TAC[plane]; CONJ_TAC; GEXISTL_TAC [`(vec 0):real^3`;`w`;`rho_node1 FF w`]; REWRITE_TAC[]; BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]); CONJ_TAC; MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1; BY(SET_TAC[]); REWRITE_TAC[SUBSET;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; ASM_CASES_TAC `i=0`; ASM_REWRITE_TAC[ITER]; MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1; BY(SET_TAC[]); TYPIFY `aff_gt {vec 0,w} {rho_node1 FF w} SUBSET affine hull {vec 0,w,rho_node1 FF w}` ENOUGH_TO_SHOW_TAC; FIRST_X_ASSUM (C INTRO_TAC [`ITER i (rho_node1 FF) w`;`i`]); ASM_SIMP_TAC[arith `~(i=0) ==> (0 < i)`]; BY(SET_TAC[]); TYPIFY `{vec 0,w,rho_node1 FF w } = {vec 0,w} UNION {rho_node1 FF w}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); BY(REWRITE_TAC[AFF_GT_SUBSET_AFFINE_HULL]); REPEAT WEAKER_STRIP_TAC; COMMENT "abbreviate uu"; TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V; BY(ASM_REWRITE_TAC[]); TYPIFY `!i. ITER i (rho_node1 FF) (ivs_rho_node1 FF w) IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V; BY(ASM_REWRITE_TAC[]); TYPED_ABBREV_TAC `w0 = ivs_rho_node1 FF w`; TYPED_ABBREV_TAC `uu = (\i. ITER i (rho_node1 FF) w0)`; TYPIFY `!i. ITER i (rho_node1 FF) w0 = uu i` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "uu"; BY(REWRITE_TAC[]); TYPIFY `w0 = uu 0 /\ w = uu 1 /\ rho_node1 FF w = uu 2 /\ (!i. ITER i (rho_node1 FF) w = uu (i+1))` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "uu"; REWRITE_TAC[ITER;ITER_1]; EXPAND_TAC "w0"; REWRITE_TAC[arith `2 = 1+1`;GSYM ITER_ADD;ITER_1]; REPEAT (GMATCH_SIMP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS); BY(ASM_MESON_TAC[]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM (fun t -> RULE_ASSUM_TAC(REWRITE_RULE[t]) THEN ASSUME_TAC t); COMMENT "apply XIV_ECAU"; TYPIFY `(?e3. &0 < e3 /\ (!t. abs t < e3 ==> f (uu 1) t IN wedge_ge (vec 0) (f (uu (r + 1)) t) (f (uu (r + 2)) t) (f (uu r) t) /\ f (uu (r + 1)) t IN wedge_ge (vec 0) (f (uu 1) t) (f (uu 2) t) (f (uu 0) t)))` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; BY(MESON_TAC[]); MATCH_MP_TAC XIV_ECAU; GEXISTL_TAC [`a`;`b`]; COMMENT "cyclic set condition"; TYPIFY `{uu i | i IN 1 .. r+1} = {uu (i+1) | i <= r}` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG]; GEN_TAC; MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`); CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `PRE i` EXISTS_TAC; ASM_SIMP_TAC[arith `1 <= i ==> PRE i + 1 = i`]; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); TYPIFY `i+1` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); ASM_REWRITE_TAC[]; COMMENT "deformation condition"; CONJ_TAC; MATCH_MP_TAC deformation_subset; TYPIFY `V` EXISTS_TAC; ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]); COMMENT "aff_gt"; CONJ_TAC; REWRITE_TAC[IN_NUMSEG]; REPEAT WEAKER_STRIP_TAC; GMATCH_SIMP_TAC (arith `2 <= i ==> i = PRE i + 1`); ASM_REWRITE_TAC[]; FIRST_X_ASSUM MATCH_MP_TAC; TYPIFY `uu (PRE i + 1)` EXISTS_TAC; BY(REWRITE_TAC[] THEN (REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC)); COMMENT "azim_cycle"; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`uu i`;`PRE i`]); DISCH_THEN GMATCH_SIMP_TAC; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN (REWRITE_TAC[IN_NUMSEG]) THEN MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`;arith `i <= r /\ 1 <= i ==> PRE i < r`]); TYPIFY `uu i = ITER i (rho_node1 FF) (uu 0) /\ uu (i+1) = ITER (i+1) (rho_node1 FF) (uu 0)` ENOUGH_TO_SHOW_TAC; DISCH_THEN (unlist REWRITE_TAC); REWRITE_TAC[arith `i + 1 = 1 +i`]; BY(REWRITE_TAC[GSYM ITER_ADD;ITER_1]); BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]); TYPIFY `!i. 1 <= i ==> rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` (C SUBGOAL_THEN ASSUME_TAC); (FIRST_X_ASSUM_ST `ITER` kill); FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM); REPEAT WEAKER_STRIP_TAC; REWRITE_TAC[arith `i+1 = 1+i`]; REWRITE_TAC[GSYM ITER_ADD;ITER_1]; GMATCH_SIMP_TAC (arith `1 <= i ==> i = 1 + (i - 1)`); ASM_REWRITE_TAC[GSYM ITER_ADD;ITER_1]; GMATCH_SIMP_TAC Local_lemmas.IVS_RHO_IDD; CONJ_TAC; BY(ASM_MESON_TAC[]); REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); COMMENT "0 < azim"; TYPIFY_GOAL_THEN ` (!i. i IN 1..r + 1 ==> &0 < azim (vec 0) (uu i) (uu (i + 1)) (uu (i - 1)))` (unlist REWRITE_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `&0 < azim a b c d` (C INTRO_TAC [`uu i`]); ANTS_TAC; BY(ASM_MESON_TAC[]); TYPIFY `rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` ENOUGH_TO_SHOW_TAC; BY(DISCH_THEN (unlist REWRITE_TAC)); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]); COMMENT "azim <= pi"; TYPIFY_GOAL_THEN `(!i. ?e2. i IN 1..r + 1 ==> &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (uu i) t) (f (uu (i + 1)) t) (f (uu (i - 1)) t) <= pi))` (unlist REWRITE_TAC); GEN_TAC; REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; DISCH_TAC; FIRST_X_ASSUM_ST `azim a b c d <= pi` (C INTRO_TAC [`uu i`]); REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; ANTS_TAC; BY(ASM_MESON_TAC[]); (REPEAT WEAKER_STRIP_TAC); TYPIFY `e2` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; TYPIFY `rho_node1 FF (uu i) = uu(i+1) /\ ivs_rho_node1 FF (uu i) = uu (i - 1)` ENOUGH_TO_SHOW_TAC; BY(DISCH_THEN (unlist REWRITE_TAC)); BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]); COMMENT "pairwise"; REWRITE_TAC[pairwise]; TYPIFY `!i. uu (i) IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]); TYPIFY `(!i j. i IN 0..r+1 /\ j IN 0..r+1 /\ ~(i = j)==> ~(uu i = uu j)) /\ (!i j. i IN 1..r+2 /\ j IN 1..r+2 /\ ~(i=j) ==> ~(uu i = uu j))` ENOUGH_TO_SHOW_TAC; REPEAT (FIRST_X_ASSUM_ST `azim` kill); BY(ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN_ALT]); CONJ_TAC; REWRITE_TAC[IN_NUMSEG]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; FIRST_X_ASSUM_ST `ITER` kill; REWRITE_TAC[]; FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM); BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `i <= r+1 /\ 1 < r /\ r < CARD V - 1 ==> i < CARD V`]); TYPIFY `!i. 1 <= i ==> uu i = ITER (PRE i) (rho_node1 FF) (w)` (C SUBGOAL_THEN ASSUME_TAC); ASM_REWRITE_TAC[]; BY(MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`]); REWRITE_TAC[IN_NUMSEG]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; FIRST_X_ASSUM_ST `ITER` (REPEAT o GMATCH_SIMP_TAC); TYPIFY `w IN V` (C SUBGOAL_THEN MP_TAC); BY(ASM_REWRITE_TAC[]); TYPIFY `PRE i < CARD V /\ PRE j < CARD V` (C SUBGOAL_THEN MP_TAC); BY(REPEAT (FIRST_X_ASSUM_ST `CARD` MP_TAC) THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[arith `1<= i /\ i <= r+2 /\ 1 < r /\ r < CARD V - 1 ==> PRE i < CARD V`]); REPEAT (FIRST_X_ASSUM_ST `local_fan` MP_TAC); REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC); BY(MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `1 <= i /\ 1 <= j /\ PRE i = PRE j ==> (i = j)`]); (COMMENT "SECOND MAIN BRANCH"); FIRST_X_ASSUM_ST `azim a b c d = &0` kill; TYPIFY `ITER (CARD V - 1) (rho_node1 FF) w = ivs_rho_node1 FF w` (C SUBGOAL_THEN ASSUME_TAC); GMATCH_SIMP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1; BY(ASM_MESON_TAC[]); FIRST_X_ASSUM_ST `interior_angle1` MP_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `r' = CARD V - r`; TYPED_ABBREV_TAC `w' = ITER r (rho_node1 FF) w`; COMMENT "add KOM"; INTRO_TAC Local_lemmas.KOMWBWC [`E`;`V`;`affine hull {(vec 0),w,ivs_rho_node1 FF w}`;`r'`;`FF`;`{ITER i (rho_node1 FF) w' | i <= r'}`;`w' cross rho_node1 FF w'`;`w`;`w'`]; ASM_REWRITE_TAC[]; ANTS_TAC; REWRITE_TAC[plane]; CONJ_TAC; GEXISTL_TAC [`(vec 0):real^3`;`w`;`ivs_rho_node1 FF w`]; REWRITE_TAC[]; BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]); CONJ_TAC; MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1; BY(SET_TAC[]); REWRITE_TAC[SUBSET;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; EXPAND_TAC "w'"; REWRITE_TAC[ITER_ADD]; ASM_CASES_TAC `(i:num)=r'`; ASM_REWRITE_TAC[]; TYPIFY `r' + r = CARD V` (C SUBGOAL_THEN SUBST1_TAC); BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `r < CARD V - 1` MP_TAC THEN ARITH_TAC); GMATCH_SIMP_TAC Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2; CONJ_TAC; BY(ASM_MESON_TAC[]); MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1; BY(SET_TAC[]); TYPIFY `aff_gt {vec 0,w} {ivs_rho_node1 FF w} SUBSET affine hull {vec 0,w,ivs_rho_node1 FF w}` ENOUGH_TO_SHOW_TAC; FIRST_X_ASSUM (C INTRO_TAC [`ITER (i+r) (rho_node1 FF) w`;`i+(r:num)`]); ANTS_TAC; ASM_REWRITE_TAC[arith `r <= (i:num) + r`]; BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `r < CARD V - 1` MP_TAC THEN ARITH_TAC); BY(SET_TAC[]); TYPIFY `{vec 0,w,ivs_rho_node1 FF w } = {vec 0,w} UNION {ivs_rho_node1 FF w}` (C SUBGOAL_THEN SUBST1_TAC); BY(SET_TAC[]); BY(REWRITE_TAC[AFF_GT_SUBSET_AFFINE_HULL]); REPEAT WEAKER_STRIP_TAC; COMMENT "abbreviate uu, forward order"; TYPIFY `ivs_rho_node1 FF w' IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V; BY(ASM_REWRITE_TAC[]); TYPIFY `!i. ITER i (rho_node1 FF) (ivs_rho_node1 FF w') IN V` (C SUBGOAL_THEN ASSUME_TAC); MATCH_MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V; BY(ASM_REWRITE_TAC[]); TYPED_ABBREV_TAC `w0 = ivs_rho_node1 FF w'`; TYPED_ABBREV_TAC `uu = (\i. ITER i (rho_node1 FF) w0)`; TYPIFY `!i. ITER i (rho_node1 FF) w0 = uu i` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "uu"; BY(REWRITE_TAC[]); TYPIFY `w0 = uu 0 /\ w' = uu 1 /\ rho_node1 FF w' = uu 2 /\ (!i. ITER i (rho_node1 FF) w' = uu (i+1))` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "uu"; REWRITE_TAC[ITER;ITER_1]; EXPAND_TAC "w0"; REWRITE_TAC[arith `2 = 1+1`;GSYM ITER_ADD;ITER_1]; REPEAT (GMATCH_SIMP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS); BY(ASM_MESON_TAC[]); ASM_REWRITE_TAC[]; FIRST_X_ASSUM (fun t -> RULE_ASSUM_TAC(REWRITE_RULE[t]) THEN ASSUME_TAC t); TYPIFY `1 < r' /\ r' < CARD V - 1` (C SUBGOAL_THEN ASSUME_TAC); EXPAND_TAC "r'"; BY(FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC THEN ARITH_TAC); TYPIFY `ivs_rho_node1 FF w = uu(r')` (C SUBGOAL_THEN ASSUME_TAC); TYPIFY `r' = PRE r' + 1` (C SUBGOAL_THEN SUBST1_TAC); BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); TYPIFY `uu (PRE r' + 1) = ITER (PRE r') (rho_node1 FF) (ITER r (rho_node1 FF) w)` (C SUBGOAL_THEN SUBST1_TAC); BY(ASM_MESON_TAC[]); REWRITE_TAC[ITER_ADD]; TYPIFY `PRE r' + r = CARD V - 1` (C SUBGOAL_THEN SUBST1_TAC); EXPAND_TAC "r'"; BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V-1` MP_TAC) THEN ARITH_TAC); GMATCH_SIMP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1; BY(ASM_MESON_TAC[]); TYPIFY `!i j. ITER i (rho_node1 FF) (uu j) = uu (i+j)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM_ST `ITER` kill; FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM); BY(REWRITE_TAC[ITER_ADD]); TYPIFY `w = uu (r'+1)` (C SUBGOAL_THEN ASSUME_TAC); ONCE_REWRITE_TAC[arith `r' + 1 = 1 + r'`]; FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM); REWRITE_TAC[ITER_1]; FIRST_X_ASSUM ((unlist REWRITE_TAC) o GSYM); BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]); TYPIFY `rho_node1 FF w = uu (r'+2)` (C SUBGOAL_THEN ASSUME_TAC); FIRST_X_ASSUM SUBST1_TAC; REWRITE_TAC[arith `r' + 2 = 1 + (r' + 1)`]; BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[ITER_1]); ASM_REWRITE_TAC[]; COMMENT "apply XIV_ECAU"; TYPIFY `(?e3. &0 < e3 /\ (!t. abs t < e3 ==> f (uu 1) t IN wedge_ge (vec 0) (f (uu (r' + 1)) t) (f (uu (r' + 2)) t) (f (uu r') t) /\ f (uu (r' + 1)) t IN wedge_ge (vec 0) (f (uu 1) t) (f (uu 2) t) (f (uu 0) t)))` ENOUGH_TO_SHOW_TAC; REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; BY(MESON_TAC[]); MATCH_MP_TAC XIV_ECAU_BACK; GEXISTL_TAC [`a`;`b`]; COMMENT "cyclic set condition"; TYPIFY `{uu i | i IN 1 .. r'+1} = {uu (i+1) | i <= r'}` (C SUBGOAL_THEN SUBST1_TAC); REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG]; GEN_TAC; MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`); CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC; TYPIFY `PRE i` EXISTS_TAC; ASM_SIMP_TAC[arith `1 <= i ==> PRE i + 1 = i`]; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); TYPIFY `i+1` EXISTS_TAC; ASM_REWRITE_TAC[]; BY(REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); ASM_REWRITE_TAC[]; COMMENT "deformation condition"; CONJ_TAC; MATCH_MP_TAC deformation_subset; TYPIFY `V` EXISTS_TAC; ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]; BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]); ASM_SIMP_TAC[arith `1 < r' ==> 1 <= r'`]; COMMENT "aff_gt"; TYPIFY `!i. uu(i+ CARD V) = uu i` (C SUBGOAL_THEN ASSUME_TAC); GEN_TAC; INTRO_TAC Localization.PERIODIC_RHO_NODE1 [`V`;`E`;`FF`;`uu 0`]; ANTS_TAC; BY(ASM_MESON_TAC[]); REWRITE_TAC[Oxl_def.periodic]; ASM_REWRITE_TAC[]; BY(MESON_TAC[]); TYPIFY `!i. r <= i ==> ITER i (rho_node1 FF) w = uu (i - (r-1))` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; TYPIFY `ITER i = ITER ((i-r) + r)` (C SUBGOAL_THEN SUBST1_TAC); AP_TERM_TAC; BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC); ASM_REWRITE_TAC[]; FIRST_X_ASSUM (C INTRO_TAC [`i - (r-1)`]); DISCH_THEN (SUBST1_TAC o GSYM); AP_TERM_TAC; EXPAND_TAC "r'"; BY(FIRST_X_ASSUM MP_TAC THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN ARITH_TAC); SUBCONJ_TAC; REWRITE_TAC[IN_NUMSEG] THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `aff_gt` (C INTRO_TAC [`ITER (i+(r-1)) (rho_node1 FF) w`;`(i+(r-1))`]); ASM_REWRITE_TAC[]; ANTS_TAC; REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC); EXPAND_TAC "r'"; BY(ARITH_TAC); TYPIFY `(i+r-1) + r'+ 1 = i+ CARD V` ENOUGH_TO_SHOW_TAC; BY(DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC); DISCH_TAC; TYPIFY_GOAL_THEN `{uu 1, uu 2} SUBSET aff_gt {vec 0, uu (r' + 1)} {uu r'}` (unlist REWRITE_TAC); REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY;SUBSET]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_NUMSEG;arith `1 <= 1 /\ 1 <= 2`]; BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC); BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC); COMMENT "cross"; CONJ_TAC; REWRITE_TAC[IN_NUMSEG] THEN REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `&0 < (a cross b) dot c` (C INTRO_TAC [`PRE i`]); TYPIFY `PRE i < r' /\ PRE i + 1 = i /\ (PRE i+1)+1 = i+1` ENOUGH_TO_SHOW_TAC; BY(MESON_TAC[]); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); COMMENT "azim_cycle"; CONJ_TAC; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`uu i`;`PRE i`]); DISCH_THEN GMATCH_SIMP_TAC; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN (REWRITE_TAC[IN_NUMSEG]) THEN MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`;arith `i <= r' /\ 1 <= i ==> PRE i < r'`]); FIRST_X_ASSUM (C INTRO_TAC [`1`;`i`]); BY(REWRITE_TAC[ITER_1;arith `1 + i = i + 1`]); CONJ_TAC; FIRST_X_ASSUM_ST `azim_cycle` MP_TAC; TYPIFY_GOAL_THEN `r' < CARD FF` (unlist REWRITE_TAC); GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_CARD_FF_V_EQ; TYPIFY `V` EXISTS_TAC; CONJ_TAC; BY(ASM_MESON_TAC[]); BY(FIRST_X_ASSUM_ST `r' < CARD V - 1` MP_TAC THEN ARITH_TAC); BY(FIRST_X_ASSUM_ST `w = uu(r'+1)` MP_TAC THEN MESON_TAC[]); COMMENT "0 < azim"; TYPIFY `!i. rho_node1 FF (uu i) = uu(i+1)` (C SUBGOAL_THEN ASSUME_TAC); GEN_TAC; FIRST_X_ASSUM (C INTRO_TAC [`1`;`i`]); BY(REWRITE_TAC[ITER_1;arith `1+i = i+1`]); TYPIFY `!i. 1 <= i ==> ivs_rho_node1 FF (uu i) = uu (i-1)` (C SUBGOAL_THEN ASSUME_TAC); REPEAT WEAKER_STRIP_TAC; TYPED_ABBREV_TAC `a = uu(i-1)`; TYPIFY `i = 1 + (i-1)` (C SUBGOAL_THEN SUBST1_TAC); BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC); FIRST_X_ASSUM (C INTRO_TAC [`1`;`i-1`]); REWRITE_TAC[ITER_1]; DISCH_THEN (SUBST1_TAC o GSYM); EXPAND_TAC "a'"; GMATCH_SIMP_TAC Local_lemmas.IVS_RHO_IDD; BY(ASM_MESON_TAC[]); TYPIFY_GOAL_THEN ` (!i. i IN 1..r' + 1 ==> &0 < azim (vec 0) (uu i) (uu (i + 1)) (uu (i - 1)))` (unlist REWRITE_TAC); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM_ST `&0 < azim a b c d` (C INTRO_TAC [`uu i`]); ANTS_TAC; BY(ASM_MESON_TAC[]); TYPIFY `rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` ENOUGH_TO_SHOW_TAC; BY(DISCH_THEN (unlist REWRITE_TAC)); BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]); COMMENT "azim <= pi"; TYPIFY_GOAL_THEN `(!i. ?e2. i IN 1..r' + 1 ==> &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (uu i) t) (f (uu (i + 1)) t) (f (uu (i - 1)) t) <= pi))` (unlist REWRITE_TAC); GEN_TAC; REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; DISCH_TAC; FIRST_X_ASSUM_ST `azim a b c d <= pi` (C INTRO_TAC [`uu i`]); REWRITE_TAC[RIGHT_EXISTS_IMP_THM]; ANTS_TAC; BY(ASM_MESON_TAC[]); (REPEAT WEAKER_STRIP_TAC); TYPIFY `e2` EXISTS_TAC; ASM_REWRITE_TAC[]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM (C INTRO_TAC [`t`]); ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`]; TYPIFY `ivs_rho_node1 FF (uu i) = uu (i - 1)` ENOUGH_TO_SHOW_TAC; BY(DISCH_THEN (unlist REWRITE_TAC)); FIRST_X_ASSUM MATCH_MP_TAC; BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]); COMMENT "pairwise"; REWRITE_TAC[pairwise]; TYPIFY `!i. uu (i) IN V` (C SUBGOAL_THEN ASSUME_TAC); BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]); TYPIFY `(!i j. i IN 0..r'+1 /\ j IN 0..r'+1 /\ ~(i = j)==> ~(uu i = uu j)) /\ (!i j. i IN 1..r'+2 /\ j IN 1..r'+2 /\ ~(i=j) ==> ~(uu i = uu j))` ENOUGH_TO_SHOW_TAC; REPEAT (FIRST_X_ASSUM_ST `azim` kill); BY(ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN_ALT]); CONJ_TAC; REWRITE_TAC[IN_NUMSEG]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; (REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `ITER` kill)); REWRITE_TAC[]; FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM); BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `i <= r'+1 /\ 1 < r' /\ r' < CARD V - 1 ==> i < CARD V`]); TYPIFY `!i. 1 <= i ==> uu i = ITER (PRE i) (rho_node1 FF) (w')` (C SUBGOAL_THEN ASSUME_TAC); ASM_REWRITE_TAC[]; BY(MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`]); REWRITE_TAC[IN_NUMSEG]; REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC; REWRITE_TAC[]; FIRST_X_ASSUM_ST `ITER` (REPEAT o GMATCH_SIMP_TAC); TYPIFY `w' IN V` (C SUBGOAL_THEN MP_TAC); BY(ASM_REWRITE_TAC[]); TYPIFY `PRE i < CARD V /\ PRE j < CARD V` (C SUBGOAL_THEN MP_TAC); BY(REPEAT (FIRST_X_ASSUM_ST `CARD` MP_TAC) THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[arith `1<= i /\ i <= r'+2 /\ 1 < r' /\ r' < CARD V - 1 ==> PRE i < CARD V`]); REPEAT (FIRST_X_ASSUM_ST `local_fan` MP_TAC); REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC); BY(MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `1 <= i /\ 1 <= j /\ PRE i = PRE j ==> (i = j)`]) ]);; (* }}} *) (* let ZLZTHIC_concl = `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) /\ (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> convex_local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\ generic (IMAGE (\v. f v t) V) (IMAGE (IMAGE (\v. f v t)) E)))`;; *) let ZLZTHIC = prove_by_refinement( `!a b V E FF f. convex_local_fan (V,E,FF) /\ generic V E /\ deformation f V (a,b) /\ (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==> (?e. &0 < e /\ (!t. --e < t /\ t < e ==> convex_local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\ generic (IMAGE (\v. f v t) V) (IMAGE (IMAGE (\v. f v t)) E)))`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; MATCH_MP_TAC zlz_reduction; GEXISTL_TAC [`a`;`b`]; ASM_REWRITE_TAC[]; CONJ_TAC; MATCH_MP_TAC zlz_generic; GEXISTL_TAC [`a`;`b`;`E`]; BY(ASM_REWRITE_TAC[]); CONJ_TAC; MATCH_MP_TAC zlz_wedge_skolem; ASM_REWRITE_TAC[]; MATCH_MP_TAC zlz_wedge_boundary; GEXISTL_TAC [`a`;`b`]; BY(ASM_REWRITE_TAC[]); MATCH_MP_TAC zlz_azim; GEXISTL_TAC [`a`;`b`;`V`]; BY(ASM_REWRITE_TAC[]) ]);; (* }}} *) end;;