(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Packing                                                           *)
(* Lemma: TSKAJXY                                                             *)
(* Author:  Thomas Hales                                                      *)
(* Date: 2011-07-31                                                           *)
(* ========================================================================== *)

(*

TSKAJXY.

`!V X. saturated V /\ packing V /\ mcell_set V X /\ critical_edge V X = {} ==>
  gammaX V X lmfun >= &0`,

I proved a few lemmas, but I realized that I need RVFXZBU, before going
very far, and this still hasn't been formalized.
The theorem is needed for the proof that `cell_param (mcell k V ul) = (k,ul)`.

Return later.
 -thales

*)


let exists_eq = 
prove_by_refinement(
  `!P Q. (!(x:A). (P x = Q x)) ==> ((?x. P x) <=> (?x. Q x))`,

  (* {{{ proof *)
  [
MESON_TAC[]
  ]);;
  (* }}} *)

let mcell_set_alt = 
prove_by_refinement(
  `!V X. mcell_set V X = (?ul. (barV V 3 ul) /\ (X = mcell0 V ul \/ X = mcell1 V ul \/ X = mcell2 V ul \/ X = mcell3 V ul \/ X = mcell4 V ul))`,

  (* {{{ proof *)
  [
REWRITE_TAC [Pack_defs.mcell_set;IN_ELIM_THM;IN] ;
REPEAT STRIP_TAC ;
ONCE_REWRITE_TAC[SWAP_EXISTS_THM];
MATCH_MP_TAC exists_eq;
GEN_TAC ;
EQ_TAC;
REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[];
MP_TAC (ARITH_RULE `i=0 \/ i=1 \/ i=2 \/ i=3 \/ i>=4`);
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC [Marchal_cells_2.MCELL_EXPLICIT];
ASM_MESON_TAC [Marchal_cells_2.MCELL_EXPLICIT];
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
EXISTS_TAC `0` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
EXISTS_TAC `1` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
EXISTS_TAC `2` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
EXISTS_TAC `3` THEN (REWRITE_TAC[Marchal_cells_2.MCELL_EXPLICIT]);
EXISTS_TAC `4` THEN (MESON_TAC[Marchal_cells_2.MCELL_EXPLICIT;ARITH_RULE `4 >= 4`])
  ]);;
  (* }}} *)

let mcell4_convex_hull = 
prove_by_refinement(
  `!V X ul. barV V 3 vl /\ hl vl < sqrt(&2) ==> ?u0 u1 u2 u3. (vl = [u0;u1;u2;u3] /\ (mcell4 V vl = convex hull {u0,u1,u2,u3}))`,

  (* {{{ proof *)
  [
REPEAT STRIP_TAC ;
ASM_REWRITE_TAC [Pack_defs.mcell4];
SUBGOAL_THEN `?u0 u1 u2 u3. vl = [(u0:real^3);u1;u2;u3]` (fun t -> MP_TAC t THEN MESON_TAC[set_of_list]);
MATCH_MP_TAC Marchal_cells.BARV_3_EXPLICIT;
ASM_MESON_TAC []
  ]);;
  (* }}} *)