(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Appendix                                                          *)
(* Chapter: Local Fan                                                         *)
(* Author: John Harrison                                                      *)
(* Date: 2013-06-11                                                           *)
(* ========================================================================== *)

module Xivphks = struct 

  open Hales_tactic;;

(* ------------------------------------------------------------------------- *)
(* Lemma 7.141                                                               *)
(* ------------------------------------------------------------------------- *)

let FSQKWKK = 
prove (`!v0 v1 v2 v3. azim v0 v1 v2 v3 <= pi ==> azim v0 v2 v3 v1 <= pi`,
GEOM_ORIGIN_TAC `v0:real^3` THEN REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT] THEN REWRITE_TAC[GSYM REAL_NOT_LT; Local_lemmas.SIN_AZIM_MUTUAL_SROSS] THEN MESON_TAC[CROSS_TRIPLE]);;
(* ------------------------------------------------------------------------- *) (* Lemma 7.143. *) (* ------------------------------------------------------------------------- *)
let XIVPHKS = 
prove (`!W a d e n r w. 1 <= n /\ n - 1 = r /\ pairwise (\i j. ~collinear{vec 0,w i,w j}) (0..n) /\ (\(i,j,k). dihV (vec 0) (w i) (w j) (w k)) = d /\ (\(i,j,k). azim (vec 0) (w i) (w j) (w k)) = a /\ (\i. wedge_ge (vec 0) (w i) (w(i + 1)) (w(i - 1))) = W /\ &0 < &2 * e /\ (!i. i IN 1..r ==> &2 * e < a(i,i + 1,i - 1)) /\ (!i. i IN 1..r ==> a(i,i + 1,i - 1) <= pi) /\ (!p q. {p,q,q+1} SUBSET 0..r /\ ~(p = q) /\ ~(p = q + 1) ==> d(p,q,q + 1) < e) /\ (!p q. {p,p+1,q} SUBSET 0..r /\ q > p + 1 ==> d(p,p + 1,q) < e) /\ (!p q. {p+1,p,q} SUBSET 0..r /\ q < p ==> d(p + 1,p,q) < e) ==> (!k j. j + k <= r ==> w j IN W(j + k)) /\ (!k j. 1 <= j /\ j + k <= r ==> w(j + k) IN W(j))`,
REPEAT GEN_TAC THEN REWRITE_TAC[REAL_ARITH `&0 < &2 * e <=> &0 < e`] THEN REWRITE_TAC[IN_NUMSEG; GT; pairwise; LE_0] THEN STRIP_TAC THEN REWRITE_TAC[AND_FORALL_THM; TAUT `(p ==> r) /\ (q /\ p ==> s) <=> p ==> r /\ (q ==> s)`] THEN INDUCT_TAC THENL [REWRITE_TAC[ADD_CLAUSES; SUB_0] THEN EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim; REAL_LE_REFL]; ALL_TAC] THEN ASM_CASES_TAC `k = 0` THENL [ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1] THEN EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN REWRITE_TAC[ADD_SUB; azim; REAL_LE_REFL; AZIM_REFL]; ALL_TAC] THEN DISJ_CASES_TAC(ARITH_RULE `r <= 1 \/ 2 <= r`) THENL [ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `&2 * e < &2 * pi` ASSUME_TAC THENL [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `a(1,1 + 1,1 - 1):real` THEN CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[azim]]; ALL_TAC] THEN REWRITE_TAC[ADD1] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC THENL [DISCH_TAC THEN UNDISCH_THEN `!j. j + k <= r ==> (w:num->real^3) j IN W (j + k) /\ (1 <= j ==> w (j + k) IN W j)` (MP_TAC o SPEC `j:num`) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ASM_ARITH_TAC; STRIP_TAC] THEN SUBGOAL_THEN `a(j + k,j + k + 1,j) <= a(j + k,j + k + 1,j + k - 1)` ASSUME_TAC THENL [UNDISCH_TAC `(w:num->real^3) j IN W (j + k)` THEN MAP_EVERY EXPAND_TAC ["W";
"a"] THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN DISCH_THEN(MP_TAC o CONJUNCT2) THEN MATCH_MP_TAC EQ_IMP THEN REPEAT(BINOP_TAC THEN REWRITE_TAC[]) THEN AP_TERM_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `a(j + k,j + k + 1,j + k - 1) <= pi` ASSUME_TAC THENL [ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> j + k - 1 = (j + k) - 1`] THEN REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + k,j + k + 1) <= pi` ASSUME_TAC THENL [SUBGOAL_THEN `a (j + k,j + k + 1,j) <= pi` MP_TAC THENL [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]] THEN MESON_TAC[FSQKWKK]; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + k,j + k + 1) < e` ASSUME_TAC THENL [SUBGOAL_THEN `a(j,j + k,j + k + 1):real = d(j,j + k,j + k + 1)` SUBST1_TAC THENL [UNDISCH_TAC `a (j,j + k,j + k + 1) <= pi` THEN MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + 1,j + k) <= a(j,j + 1,j - 1)` ASSUME_TAC THENL [UNDISCH_TAC `(w:num->real^3) (j + k) IN W j` THEN MAP_EVERY EXPAND_TAC ["W"; "a"] THEN SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM]; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + 1,j - 1) <= pi` ASSUME_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + 1,j + k) <= pi` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + 1,j + k) < e` ASSUME_TAC THENL [ASM_CASES_TAC `k = 1` THENL [EXPAND_TAC "a" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[AZIM_REFL]; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + 1,j + k):real = d(j,j + 1,j + k)` SUBST1_TAC THENL [UNDISCH_TAC `a (j,j + 1,j + k) <= pi` THEN MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `a(j,j + 1,j + k + 1):real <= a(j,j + 1,j - 1)` MP_TAC THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `a(j,j + 1,j + k) + a(j,j + k,j + k + 1)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a (j,j + k,j + k + 1):real < e`; `a (j,j + 1,j + k):real < e`] THEN EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC Fan.sum3_azim_fan THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; MATCH_MP_TAC REAL_LT_IMP_LE] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim]]; ALL_TAC] THEN DISCH_TAC THEN UNDISCH_THEN `!j. j + k <= r ==> (w:num->real^3) j IN W (j + k) /\ (1 <= j ==> w (j + k) IN W j)` (MP_TAC o SPEC `j + 1`) THEN ASM_REWRITE_TAC[ARITH_RULE `(j + 1) + k = j + k + 1`; ARITH_RULE `1 <= j + 1`] THEN STRIP_TAC THEN SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` ASSUME_TAC THENL [UNDISCH_TAC `(w:num->real^3) (j + k + 1) IN W (j + 1)` THEN EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM] THEN EXPAND_TAC "a" THEN SIMP_TAC[ARITH_RULE `(a + 1) + 1 = a + 2`; ADD_SUB]; ALL_TAC] THEN SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) + a(j + 1,j + k + 1,j) = a(j + 1,j + 2,j)` ASSUME_TAC THENL [CONV_TAC SYM_CONV THEN UNDISCH_TAC `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` THEN EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= a(j + 1,j + 2,j)` ASSUME_TAC THENL [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`)) THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim]; ALL_TAC] THEN SUBGOAL_THEN `a(j + 1,(j + 1) + 1,(j + 1) - 1) <= pi` MP_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; REWRITE_TAC[ADD_SUB; ARITH_RULE `(n + 1) + 1 = n + 2`] THEN DISCH_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j,j + 1) <= pi` ASSUME_TAC THENL [SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= pi` MP_TAC THENL [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]] THEN MESON_TAC[FSQKWKK]; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j,j + 1) < e` ASSUME_TAC THENL [SUBGOAL_THEN `a(j + k + 1,j,j + 1):real = d(j + k + 1,j,j + 1) ` SUBST1_TAC THENL [UNDISCH_TAC `a(j + k + 1,j,j + 1) <= pi` THEN MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC THENL [UNDISCH_TAC `(w:num->real^3)(j + 1) IN W (j + k + 1)` THEN MAP_EVERY EXPAND_TAC ["W"; "a"] THEN SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) + a(j + k + 1,j + 1,j + k) = a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC THENL [CONV_TAC SYM_CONV THEN UNDISCH_TAC `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)` THEN EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1) <= pi` MP_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`] THEN DISCH_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC THENL [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`)) THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim]; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= pi` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) < e` ASSUME_TAC THENL [ASM_CASES_TAC `k = 1` THENL [ASM_REWRITE_TAC[] THEN EXPAND_TAC "a" THEN REWRITE_TAC[AZIM_REFL] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j + 1,j + k):real = d(j + k + 1,j + 1,j + k)` SUBST1_TAC THENL [UNDISCH_TAC `a(j + k + 1,j + 1,j + k) <= pi` THEN MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC THEN MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `d((j + k) + 1,j + k,j + 1) < e` MP_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC; EXPAND_TAC "d" THEN REWRITE_TAC[ADD_ASSOC; Counting_spheres.DIHV_SYM]]; ALL_TAC] THEN SUBGOAL_THEN `a(j + k + 1,j + k + 2,j) <= a(j + k + 1,j + k + 2,j + k)` MP_TAC THENL [ALL_TAC; MAP_EVERY EXPAND_TAC ["W"; "a"] THEN SIMP_TAC[Localization.wedge_ge; azim; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `a(j + k + 1,j + k + 2,j) + a(j + k + 1,j,j + k)` THEN CONJ_TAC THENL [REWRITE_TAC[REAL_LE_ADDR] THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim]; ALL_TAC] THEN MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC Fan.sum5_azim_fan THEN CONJ_TAC THENL [ALL_TAC; REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `a(j + k + 1,j,j + 1) + a(j + k + 1,j + 1,j + k)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a(j + k + 1,j,j + 1):real < e`; `a(j + k + 1,j + 1,j + k):real < e`] THEN EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC Fan.sum3_azim_fan THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ASM_REAL_ARITH_TAC]; SUBGOAL_THEN `&2 * e < a (j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1)` MP_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`] THEN REAL_ARITH_TAC]]);; (* 1..r are the straight angles. Modified from Xivphks.XIVPHKS by shifting indices. *)
let XIVPHKS_SHIFT = 
prove_by_refinement( `!W a d e r w. 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)) = d /\ (\(i,j,k). azim (vec 0) (w i) (w j) (w k)) = a /\ (\i. wedge_ge (vec 0) (w i) (w (i + 1)) (w (i - 1))) = W /\ &0 < &2 * e /\ (!i. i IN 1..(r+1) ==> &2 * e < a (i,i + 1,i - 1)) /\ (!i. i IN 1..(r+1) ==> a (i,i + 1,i - 1) <= pi) /\ (!p q. {p, q, q + 1} SUBSET 1..(r+1) /\ ~(p = q) /\ ~(p = q + 1) ==> d (p,q,q + 1) < e) /\ (!p q. {p, p + 1, q} SUBSET 1..(r+1) /\ q > p + 1 ==> d (p,p + 1,q) < e) /\ (!p q. {p + 1, p, q} SUBSET 1..(r+1) /\ q < p ==> d (p + 1,p,q) < e) ==> (!k j. 1 <= j /\ j + k <= r+1 ==> w j IN W (j + k)) /\ (!k j. 1 <= j /\ j + k <= r+1 ==> w (j + k) IN W j)`,
(* {{{ proof *) [ REPEAT GEN_TAC THEN REWRITE_TAC[REAL_ARITH `&0 < &2 * e <=> &0 < e`]; REWRITE_TAC[IN_NUMSEG; GT; pairwise; LE_0] THEN STRIP_TAC; REWRITE_TAC[AND_FORALL_THM; TAUT `(p ==> r) /\ (q /\ p ==> s) <=> p ==> r /\ (q ==> s)`]; INDUCT_TAC; REWRITE_TAC[ADD_CLAUSES; SUB_0]; EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM]; BY(REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE; azim; REAL_LE_REFL]); ASM_CASES_TAC `k = 0`; ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1]; EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM]; BY(REWRITE_TAC[ADD_SUB; azim; REAL_LE_REFL; AZIM_REFL]); SUBGOAL_THEN `&2 * e < &2 * pi` ASSUME_TAC; MATCH_MP_TAC REAL_LT_TRANS; EXISTS_TAC `a(1,1 + 1,1 - 1):real` THEN CONJ_TAC; BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]); REWRITE_TAC[ADD1] THEN X_GEN_TAC `j:num`; MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC; DISCH_TAC; FIRST_X_ASSUM (C INTRO_TAC [`j`]); REPEAT WEAKER_STRIP_TAC; FIRST_X_ASSUM MP_TAC THEN ANTS_TAC; BY(ASM_ARITH_TAC); DISCH_TAC; FIRST_X_ASSUM_ST `==>` MP_TAC THEN ANTS_TAC; BY(ASM_ARITH_TAC); DISCH_TAC; SUBGOAL_THEN `a(j + k,j + k + 1,j) <= a(j + k,j + k + 1,j + k - 1)` ASSUME_TAC; FIRST_X_ASSUM MP_TAC THEN MAP_EVERY EXPAND_TAC ["W";
"a"]; REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM]; DISCH_THEN(MP_TAC o CONJUNCT2) THEN MATCH_MP_TAC EQ_IMP; BY(REPEAT(BINOP_TAC THEN REWRITE_TAC[]) THEN AP_TERM_TAC THEN ASM_ARITH_TAC); SUBGOAL_THEN `a(j + k,j + k + 1,j + k - 1) <= pi` ASSUME_TAC; ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> j + k - 1 = (j + k) - 1`]; BY(REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); SUBGOAL_THEN `a(j,j + k,j + k + 1) <= pi` ASSUME_TAC; SUBGOAL_THEN `a (j + k,j + k + 1,j) <= pi` MP_TAC THENL [ASM_REAL_ARITH_TAC; EXPAND_TAC "a" THEN REWRITE_TAC[]]; BY(MESON_TAC[FSQKWKK]); SUBGOAL_THEN `a(j,j + k,j + k + 1) < e` ASSUME_TAC; SUBGOAL_THEN `a(j,j + k,j + k + 1):real = d(j,j + k,j + k + 1)` SUBST1_TAC; UNDISCH_TAC `a (j,j + k,j + k + 1) <= pi`; MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC; MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[]; BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC; REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG]; BY(ASM_ARITH_TAC); SUBGOAL_THEN `a(j,j + 1,j + k) <= a(j,j + 1,j - 1)` ASSUME_TAC; UNDISCH_TAC `(w:num->real^3) (j + k) IN W j`; MAP_EVERY EXPAND_TAC ["W"; "a"]; BY(SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM]); SUBGOAL_THEN `a(j,j + 1,j - 1) <= pi` ASSUME_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC; ALL_TAC]; SUBGOAL_THEN `a(j,j + 1,j + k) <= pi` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]; SUBGOAL_THEN `a(j,j + 1,j + k) < e` ASSUME_TAC; ASM_CASES_TAC `k=1`; BY(EXPAND_TAC "a" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[AZIM_REFL]); SUBGOAL_THEN `a(j,j + 1,j + k):real = d(j,j + 1,j + k)` SUBST1_TAC; UNDISCH_TAC `a (j,j + 1,j + k) <= pi`; MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC; MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[]; BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); FIRST_X_ASSUM MATCH_MP_TAC; REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG]; BY(ASM_ARITH_TAC); SUBGOAL_THEN `a(j,j + 1,j + k + 1):real <= a(j,j + 1,j - 1)` MP_TAC; MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `a(j,j + 1,j + k) + a(j,j + k,j + k + 1)` THEN CONJ_TAC; MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a (j,j + k,j + k + 1):real < e`; `a (j,j + 1,j + k):real < e`]; EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC; MATCH_MP_TAC Fan.sum3_azim_fan; CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC; BY(ASM_REAL_ARITH_TAC); MATCH_MP_TAC REAL_LT_IMP_LE; BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM]; BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]); DISCH_TAC; COMMENT "midpoint -- down to 1 goal"; DISCH_TAC; FIRST_X_ASSUM (C INTRO_TAC [`j+1`]); ASM_REWRITE_TAC[arith `1 <= j+1`;arith `(j + 1) + k = j + k + 1`;]; REPEAT WEAKER_STRIP_TAC; SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)` ASSUME_TAC; UNDISCH_TAC `(w:num->real^3) (j + k + 1) IN W (j + 1)`; EXPAND_TAC "W" THEN REWRITE_TAC[Localization.wedge_ge; IN_ELIM_THM]; BY(EXPAND_TAC "a" THEN SIMP_TAC[ARITH_RULE `(a + 1) + 1 = a + 2`; ADD_SUB]); SUBGOAL_THEN `a(j + 1,j + 2,j + k + 1) + a(j + 1,j + k + 1,j) = a(j + 1,j + 2,j)` ASSUME_TAC; CONV_TAC SYM_CONV; UNDISCH_TAC `a(j + 1,j + 2,j + k + 1) <= a(j + 1,j + 2,j)`; EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC; MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[]; TYPIFY_GOAL_THEN `~collinear {vec 0, w (j + 1), w j}` (unlist REWRITE_TAC); FIRST_X_ASSUM_ST `collinear` kill; BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN TRY ASM_ARITH_TAC); SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= a(j + 1,j + 2,j)` ASSUME_TAC; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`)); BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]); SUBGOAL_THEN `a(j + 1,(j + 1) + 1,(j + 1) - 1) <= pi` MP_TAC; BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); REWRITE_TAC[ADD_SUB; ARITH_RULE `(n + 1) + 1 = n + 2`]; DISCH_TAC; SUBGOAL_THEN `a(j + k + 1,j,j + 1) <= pi` ASSUME_TAC; SUBGOAL_THEN `a(j + 1,j + k + 1,j) <= pi` MP_TAC; BY(ASM_REAL_ARITH_TAC); EXPAND_TAC "a" THEN REWRITE_TAC[]; BY(MESON_TAC[FSQKWKK]); SUBGOAL_THEN `a(j + k + 1,j,j + 1) < e` ASSUME_TAC; ASM_CASES_TAC `k = 0`; BY(EXPAND_TAC "a" THEN ASM_REWRITE_TAC[Local_lemmas.AZIM_SPEC_DEGENERATE;arith `j + 0 + 1 = j+1`]); SUBGOAL_THEN `a(j + k + 1,j,j + 1):real = d(j + k + 1,j,j + 1) ` SUBST1_TAC; UNDISCH_TAC `a(j + k + 1,j,j + 1) <= pi`; MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC; MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[]; BY(CONJ_TAC THENL [FIRST_X_ASSUM_ST `collinear` kill;ALL_TAC] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); REWRITE_TAC[ADD_ASSOC] THEN FIRST_X_ASSUM MATCH_MP_TAC; BY(REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC); SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC; UNDISCH_TAC `(w:num->real^3)(j + 1) IN W (j + k + 1)`; MAP_EVERY EXPAND_TAC ["W"; "a"]; BY(SIMP_TAC[Localization.wedge_ge; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]); SUBGOAL_THEN `a(j + k + 1,j + k + 2,j + 1) + a(j + k + 1,j + 1,j + k) = a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC; CONV_TAC SYM_CONV; UNDISCH_TAC `a(j + k + 1,j + k + 2,j + 1) <= a(j + k + 1,j + k + 2,j + k)`; EXPAND_TAC "a" THEN REWRITE_TAC[] THEN DISCH_TAC; MATCH_MP_TAC Fan.sum4_azim_fan THEN ASM_REWRITE_TAC[]; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); COMMENT "ok"; ASM_CASES_TAC `k = 0`; ASM_REWRITE_TAC[arith `j+0+1 = j+1`]; EXPAND_TAC "W" THEN REWRITE_TAC[]; ASM_SIMP_TAC[arith `1 <= j ==> (j+1)+1 = j+2 /\ (j+1)-1 = j`]; BY(REWRITE_TAC[Local_lemmas1.FST_LST_IN_WEDGE_GE]); SUBGOAL_THEN `a(j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1) <= pi` MP_TAC; BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]; DISCH_TAC; SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= a(j + k + 1,j + k + 2,j + k)` ASSUME_TAC; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = c ==> &0 <= a ==> b <= c`)); BY(EXPAND_TAC "a" THEN REWRITE_TAC[azim]); SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) <= pi` ASSUME_TAC; BY(ASM_REAL_ARITH_TAC); SUBGOAL_THEN `a(j + k + 1,j + 1,j + k) < e` ASSUME_TAC; ASM_CASES_TAC `k = 1`; ASM_REWRITE_TAC[] THEN EXPAND_TAC "a" THEN REWRITE_TAC[AZIM_REFL]; BY(ASM_REWRITE_TAC[]); SUBGOAL_THEN `a(j + k + 1,j + 1,j + k):real = d(j + k + 1,j + 1,j + k)` SUBST1_TAC; UNDISCH_TAC `a(j + k + 1,j + 1,j + k) <= pi`; MAP_EVERY EXPAND_TAC ["a"; "d"] THEN REWRITE_TAC[] THEN DISCH_TAC; MATCH_MP_TAC Polar_fan.AZIM_DIHV_SAME_STRONG THEN ASM_REWRITE_TAC[]; BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); SUBGOAL_THEN `d((j + k) + 1,j + k,j + 1) < e` MP_TAC; FIRST_X_ASSUM MATCH_MP_TAC; BY(REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_NUMSEG] THEN ASM_ARITH_TAC); BY(EXPAND_TAC "d" THEN REWRITE_TAC[ADD_ASSOC; Counting_spheres.DIHV_SYM]); COMMENT "ok"; ENOUGH_TO_SHOW_TAC `a(j + k + 1,j + k + 2,j) <= a(j + k + 1,j + k + 2,j + k)`; MAP_EVERY EXPAND_TAC ["W"; "a"]; BY(SIMP_TAC[Localization.wedge_ge; azim; IN_ELIM_THM; ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]); MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `a(j + k + 1,j + k + 2,j) + a(j + k + 1,j,j + k)`; CONJ_TAC; BY(REWRITE_TAC[REAL_LE_ADDR] THEN EXPAND_TAC "a" THEN REWRITE_TAC[azim]); MATCH_MP_TAC REAL_EQ_IMP_LE THEN CONV_TAC SYM_CONV; EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC; MATCH_MP_TAC Fan.sum5_azim_fan; CONJ2_TAC; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * e` THEN CONJ_TAC; MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `a(j + k + 1,j,j + 1) + a(j + k + 1,j + 1,j + k)`; CONJ_TAC; MATCH_MP_TAC REAL_EQ_IMP_LE THEN MAP_EVERY UNDISCH_TAC [`a(j + k + 1,j,j + 1):real < e`; `a(j + k + 1,j + 1,j + k):real < e`]; EXPAND_TAC "a" THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC; MATCH_MP_TAC Fan.sum3_azim_fan; CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]; BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); BY(ASM_REAL_ARITH_TAC); SUBGOAL_THEN `&2 * e < a (j + k + 1,(j + k + 1) + 1,(j + k + 1) - 1)` MP_TAC; BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC); EXPAND_TAC "a"; REWRITE_TAC[ARITH_RULE `(j + k + 1) + 1 = j + k + 2`; ARITH_RULE `(j + k + 1) - 1 = j + k`]; BY(REAL_ARITH_TAC) ]);; (* }}} *) end;;