(* ========================================================================= *)
(*                FLYSPECK - BOOK FORMALIZATION                              *)
(*                                                                           *)
(*      Authour   : VU KHAC KY                                               *)
(*      Book lemma:  EMNWUUS                                                 *)
(*      Chaper    : Packing (Marchal Cells)                                  *)
(*      Date      : October 3, 2010                                          *)
(*                                                                           *)
(* ========================================================================= *)

(* About this lemma:

! I have proved EMNWUUS1.
! In part EMNWUUS2, I have prove the implication part (==>) 
! and haven't done the ! Inverse part (<==). 
! So the only thing to do with this lemma is to prove the following :
! 
! `mcell0 V ul = {} /\ mcell1 V ul = {} /\ mcell2 V ul = {} /\ mcell3 V ul = {}
!  ==> hl ul < sqrt (&2)`
*)

(* ========================================================================= *)
(*                     FILES NEED TO BE LOADED                               *)
(* ========================================================================= *)

flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
flyspeck_needs "packing/pack_defs.hl";;
flyspeck_needs "packing/pack_concl.hl";;
flyspeck_needs "packing/pack1.hl";;

module EMNWUUS = struct

(* dmtcp: needs "flyspeck_load.hl";; *)



open Pack_defs;;
open Pack_concl;;
open Vukhacky_tactics;;
open Pack1;;

needs "marchal_cells.hl";;

(* ============== Axioms in previous parts ===================================*)

let XNHPWAB1 = new_axiom XNHPWAB1_concl;;

let XNHPWAB4 = new_axiom XNHPWAB4_concl;;

let WAUFCHE1 = new_axiom WAUFCHE1_concl;;

let WAUFCHE2 = new_axiom WAUFCHE2_concl;;

let OAPVION2 = new_axiom OAPVION2_concl;;

let MHFTTZN1 = new_axiom MHFTTZN1_concl;;

let MHFTTZN4 = new_axiom MHFTTZN4_concl;;

(* ========================================================================= *)

let EMNWUUS1 = prove_by_refinement ( EMNWUUS1_concl,
[ (REWRITE_TAC[mcell4] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN COND_CASES_TAC);   
 (REPEAT STRIP_TAC);
 (NEW_GOAL `set_of_list (ul:(real^3)list) = {}`);
 (ASM_MESON_TAC[CONVEX_HULL_EQ_EMPTY]);
 (NEW_GOAL `ul:(real^3)list = []`);
 (NEW_GOAL `~(?h t. ul:(real^3)list = CONS h t)`);
 STRIP_TAC;
 (NEW_GOAL `(h:real^3) IN set_of_list ul`);
 (REWRITE_TAC [ASSUME `ul = CONS (h:real^3) t`; IN_SET_OF_LIST;MEM]);
 (ASM_SET_TAC[]);
 (ASM_MESON_TAC[list_CASES]);
 (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);
 (REWRITE_TAC[BARV]);
 STRIP_TAC;
 (NEW_GOAL `LENGTH (ul:(real^3)list) = 0`);
 (ASM_MESON_TAC[ASSUME `ul:(real^3)list =[]`;LENGTH]);
 (ASM_ARITH_TAC);
 (MESON_TAC[]);
 (MESON_TAC[]);
 (MESON_TAC[]) ]);;


(* ========================================================================= *)

g EMNWUUS2_concl;;
e (REPEAT GEN_TAC THEN STRIP_TAC);;
(* ! Note: The inverse part of this lemma has not been Done *)

e (EQ_TAC);;

e (REPEAT STRIP_TAC);;
(* Break into 4 cases *)

(* =============== Case 1 ================================ *) (* OK *)

e (REWRITE_TAC[mcell0]);;
e (REWRITE_TAC[SET_RULE `x DIFF y = {} <=> (!a. a IN x ==> a IN y)`]);;
e (REWRITE_TAC[ROGERS;IMAGE;IN;ball;SUBSET;IN_ELIM_THM]);;
e GEN_TAC;;
e (MATCH_MP_TAC BALL_CONVEX_HULL_LEMMA);;

e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
e (STRIP_TAC);;

 (* New_subgoal 1.1 *)
e (NEW_GOAL `hl (truncate_simplex x' (ul:(real^3)list)) 
          <= hl (truncate_simplex (LENGTH ul - 1) ul)`);;
e (ASM_CASES_TAC `x' < LENGTH (ul:(real^3)list) - 1`);;
e (MATCH_MP_TAC (REAL_ARITH `a < b ==> a <= b`));;
e (NEW_GOAL `x' < (LENGTH (ul:(real^3)list) - 1) /\ LENGTH ul - 1 <= 3`);;
e (ASM_REWRITE_TAC[] THEN UNDISCH_TAC `barV V 3 ul`);;
e (REWRITE_TAC[BARV] THEN ARITH_TAC);;
e (UP_ASM_TAC);;
e (NEW_GOAL `ul IN barV V 3`);;
e (ASM_MESON_TAC[IN]);;
e (ASM_MESON_TAC[XNHPWAB4; ARITH_RULE `3 <= 3`]);;
e (MATCH_MP_TAC (REAL_ARITH `a = b ==> a <= b`));;
e (REWRITE_WITH `LENGTH (ul:(real^3)list) - 1 = x'`);;
e (ASM_ARITH_TAC);;
  (* End subgoal 1.1 *)

  (* New subgoal 1.2 *)
e (NEW_GOAL `hl (truncate_simplex (LENGTH ul - 1) ul) = hl (ul:(real^3)list)`);;
e (AP_TERM_TAC);;
e (REWRITE_TAC[TRUNCATE_SIMPLEX]);;
e (MATCH_MP_TAC SELECT_UNIQUE);;
e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM;INITIAL_SUBLIST] THEN EQ_TAC);;
e STRIP_TAC;;
e (NEW_GOAL `LENGTH (ul:(real^3)list) = 
             LENGTH (y:(real^3)list) + LENGTH (yl:(real^3)list)`);;
e (ASM_MESON_TAC[LENGTH_APPEND]);;
e (NEW_GOAL `LENGTH (yl:(real^3)list) = 0`);;
e (ASM_ARITH_TAC);;
e (NEW_GOAL `(yl:(real^3)list) = []`);;
e (ASM_MESON_TAC[LENGTH_EQ_NIL]);;
e (ASM_MESON_TAC[APPEND_NIL]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ASM_ARITH_TAC);;
e (EXISTS_TAC `[]:(real^3)list`);;
e (ASM_MESON_TAC[APPEND_NIL]);;
  (* End subgoal 1.2 *)

  (* New subgoal 1.3 *)

e (NEW_GOAL `?u0 u1 u2 u3:real^3. ul = [u0;u1;u2;u3]`);;
e (ASM_MESON_TAC[BARV_3_EXPLICIT]);;
e (REPEAT (FIRST_X_ASSUM CHOOSE_TAC));;
e (REWRITE_TAC[ASSUME `ul = [u0:real^3; u1; u2; u3]`; HD]);;

  (* ---------------------------------------------- *)
  (* Consider case x' = 0 *)

e (ASM_CASES_TAC `x' = 0`);;
e (REWRITE_WITH `x:real^3 = u0`);;
e (MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`));;
e (ASM_MESON_TAC[OMEGA_LIST_0_EXPLICIT; GSYM IN]);;
e (ASM_REWRITE_TAC[DIST_REFL]);;
e (MESON_TAC[SQRT_LT_0;REAL_ARITH `&0 <= &2 /\ &0 < &2`]);;

  (* ---------------------------------------------- *)
  (* Consider case x' = 1 *)

e (ASM_CASES_TAC `x' = 1`);;
e (REWRITE_WITH `x:real^3 = circumcenter {u0, u1}`);;
e (MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`));;
e (ASM_MESON_TAC[OMEGA_LIST_1_EXPLICIT; GSYM IN]);;
e (ONCE_REWRITE_TAC[DIST_SYM]);;
e (REWRITE_WITH `dist (circumcenter {u0:real^3, u1},u0) 
               = hl (truncate_simplex x' (ul:(real^3)list))`);;
e (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1;HL;radV]);;
e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e (MATCH_MP_TAC SELECT_UNIQUE);;
e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; MESON[set_of_list] 
   `set_of_list [u0:real^3;u1] = {u0, u1}`] THEN EQ_TAC);;
e (DISCH_TAC THEN (FIRST_ASSUM MATCH_MP_TAC));;
e (SET_TAC[]);;
e (REPEAT STRIP_TAC);;
e (NEW_GOAL `w IN {u0,u1:real^3}`);;
e (UP_ASM_TAC THEN SET_TAC[]);;
e (NEW_GOAL 
 `(!w. w IN {u0,u1:real^3} ==> radV {u0,u1} = dist (circumcenter {u0,u1},w))`);;
e (MATCH_MP_TAC OAPVION2);;
e (REWRITE_TAC[AFFINE_INDEPENDENT_2]);;
e (ASM_REWRITE_TAC[]);;
e (NEW_GOAL `(radV {u0,u1:real^3} = dist (circumcenter {u0,u1},w))`);;
e (ASM_SIMP_TAC[]);;
e (NEW_GOAL `(radV {u0,u1:real^3} = dist (circumcenter {u0,u1},u0))`);;
e (FIRST_ASSUM MATCH_MP_TAC);;
e (SET_TAC[]);;
e (ASM_MESON_TAC[]);;
e (ASM_REAL_ARITH_TAC);;

  (* ---------------------------------------------- *)
  (* Consider case x' = 2 *)

e (ASM_CASES_TAC `x' = 2`);;
e (REWRITE_WITH `x:real^3 = circumcenter {u0, u1, u2}`);;
e (MP_TAC (ASSUME `x:real^3 = omega_list_n V ul x'`));;
e (ASM_MESON_TAC[OMEGA_LIST_2_EXPLICIT; GSYM IN]);;
e (ONCE_REWRITE_TAC[DIST_SYM]);;
e (REWRITE_WITH `dist (circumcenter {u0:real^3, u1, u2},u0) 
               = hl (truncate_simplex x' (ul:(real^3)list))`);;
e (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;HL;radV]);;
e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e (MATCH_MP_TAC SELECT_UNIQUE);;
e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM; MESON[set_of_list] 
   `set_of_list [u0:real^3;u1;u2] = {u0, u1, u2}`] THEN EQ_TAC);;
e (DISCH_TAC THEN (FIRST_ASSUM MATCH_MP_TAC));;
e (SET_TAC[]);;
e (REPEAT STRIP_TAC);;
e (NEW_GOAL `w IN {u0,u1:real^3,u2}`);;
e (UP_ASM_TAC THEN SET_TAC[]);;
e (NEW_GOAL `(!w. w IN {u0,u1:real^3, u2} ==> 
             radV {u0,u1,u2} = dist (circumcenter {u0,u1,u2},w))`);;
e (MATCH_MP_TAC OAPVION2);;
e (MATCH_MP_TAC AFFINE_INDEPENDENT_SUBSET);;
e (EXISTS_TAC `{u0, u1, u2, u3:real^3}`);;
e (REWRITE_TAC[SET_RULE `{a, b:A, c} SUBSET {a, b , c, d:A}`]);;
e (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);;
e STRIP_TAC;;
e (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);;
e (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`);;
e (REWRITE_TAC[MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);;
e (MATCH_MP_TAC MHFTTZN1);;
e (EXISTS_TAC `V:real^3->bool`);;
e (ASM_MESON_TAC[ARITH_RULE `3 <= 3`]);;
e (ONCE_ASM_REWRITE_TAC[]);;
e (NEW_GOAL `FINITE {u1, u2, u3:real^3}`);;
e (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u1, u2,u3} = set_of_list [u1;u2:real^3;u3]`]);;
e (MATCH_MP_TAC (ARITH_RULE 
  `(a = int_of_num 4) ==> (int_of_num 3 = a - int_of_num 1)`));;
e (MATCH_MP_TAC (ARITH_RULE `a = b ==> int_of_num a = int_of_num b`));;
e (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
            (if u0 IN {u1, u2, u3}  then CARD {u1, u2, u3}  
             else SUC (CARD {u1, u2, u3} ))`);;
e (UP_ASM_TAC THEN REWRITE_TAC[CARD_CLAUSES]);;
e (UP_ASM_TAC THEN COND_CASES_TAC);;
e (DISCH_TAC);;
e (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} < &3`);;
e (REWRITE_WITH `{u0,u1,u2,u3:real^3} = {u1, u2,u3}`);;
e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e (NEW_GOAL  `CARD {u1, u2, u3} = CARD {u0, u1, u2, u3} <=> 
            {u1, u2, u3:real^3} = {u0, u1, u2, u3}`);;
e (MATCH_MP_TAC SUBSET_CARD_EQ);;
e (STRIP_TAC);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (SET_TAC[]);;
e (ASM_MESON_TAC[]);;

e (REWRITE_TAC[MESON[set_of_list] 
  `{u1:real^3,u2, u3} = set_of_list [u1;u2;u3]`]);;
e (MATCH_MP_TAC AFF_DIM_LE_LENGTH);;
e (REWRITE_TAC[LENGTH]);;
e (ARITH_TAC);;
e (NEW_GOAL `F`);;
e (ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a <  int_of_num 3 ==> F`]);;
e (ASM_MESON_TAC[]);;
e STRIP_TAC;;
e (NEW_GOAL `CARD {u1:real^3, u2, u3} = 3`);;
e (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);;
e (MATCH_MP_TAC (ARITH_RULE 
 `a <= LENGTH [u1;u2;u3:real^3] /\ LENGTH [u1;u2;u3:real^3] <= b ==> a <= b`));;
e STRIP_TAC;;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;CARD_SET_OF_LIST_LE]);;
e (REWRITE_TAC[LENGTH] THEN ARITH_TAC);;
e (ASM_CASES_TAC `CARD {u1:real^3, u2, u3} <= 2`);;
e (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} <= 3`);;
e (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
  (if u0 IN {u1,u2,u3} then CARD {u1,u2,u3} else SUC (CARD {u1,u2,u3}))`);;
e (NEW_GOAL `FINITE {u1,u2,u3:real^3}`);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (ASM_REWRITE_TAC[CARD_CLAUSES]);;
e (UP_ASM_TAC THEN COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (ASM_ARITH_TAC);;
e (ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`);;


e (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} 
           < int_of_num (CARD {u0, u1, u2, u3})`);;
e (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list (xl:(real^3)list)`);;
e (EXPAND_TAC "xl");;
e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e (MATCH_MP_TAC SET_OF_LIST_OF_SET);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (MATCH_MP_TAC AFF_DIM_LE_LENGTH);;
e (REWRITE_WITH `set_of_list (xl:(real^3)list) = {u0, u1, u2, u3:real^3}`);;
e (EXPAND_TAC "xl");;
e (MATCH_MP_TAC SET_OF_LIST_OF_SET);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (EXPAND_TAC "xl");;
e (MATCH_MP_TAC LENGTH_LIST_OF_SET);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (NEW_GOAL `F`);;
e (ASM_ARITH_TAC);;
e (ASM_MESON_TAC[]);;
e (ASM_ARITH_TAC);;
e ASM_ARITH_TAC;;
e (MATCH_MP_TAC (REAL_ARITH 
  `radV {u0,u1,u2:real^3} = a /\ radV {u0,u1,u2} = b ==> a = b`));;
e STRIP_TAC;;
e (ASM_REWRITE_TAC[]);;
e (FIRST_ASSUM MATCH_MP_TAC);;
e (SET_TAC[]);;
e (FIRST_ASSUM MATCH_MP_TAC);;
e (ASM_REWRITE_TAC[]);;
e (ASM_REAL_ARITH_TAC);;

  (* ---------------------------------------------- *)
  (* Consider case x' = 3 *)

e (ASM_CASES_TAC `x' = 3`);;
e (REWRITE_WITH `x = circumcenter {u0,u1,u2,u3:real^3}`);;
e (ASM_REWRITE_TAC[]);;
e (MATCH_MP_TAC OMEGA_LIST_3_EXPLICIT);;
e (ASM_MESON_TAC[GSYM IN]);;
e (NEW_GOAL `dist (u0,circumcenter {u0:real^3, u1, u2, u3}) 
           = hl (ul:(real^3)list)`);;
e (ASM_REWRITE_TAC[HL]);;
e (REWRITE_WITH `set_of_list [u0:real^3; u1; u2; u3] = {u0,u1,u2,u3}`);;
e (MESON_TAC[set_of_list]);;



e (NEW_GOAL `(!w. w IN {u0,u1:real^3, u2,u3} ==> 
             radV {u0,u1,u2,u3} = dist (circumcenter {u0,u1,u2,u3},w))`);;
e (MATCH_MP_TAC OAPVION2);;
e (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]);;
e STRIP_TAC;;
e (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);;
e (NEW_GOAL `aff_dim {u0,u1,u2,u3:real^3} = &3`);;
e (REWRITE_TAC[MESON[set_of_list] 
   `{u0, u1, u2,u3} = set_of_list [u0;u1;u2:real^3;u3]`]);;
e (MATCH_MP_TAC MHFTTZN1);;
e (EXISTS_TAC `V:real^3->bool`);;
e (ASM_MESON_TAC[ARITH_RULE `3 <= 3`]);;
e (ONCE_ASM_REWRITE_TAC[]);;
e (MATCH_MP_TAC (ARITH_RULE 
  `(a = int_of_num 4) ==> (int_of_num 3 = a - int_of_num 1)`));;
e (MATCH_MP_TAC (ARITH_RULE `a = b ==> int_of_num a = int_of_num b`));;


e (NEW_GOAL `FINITE {u1, u2, u3:real^3}`);;
e (REWRITE_TAC[FINITE_SET_OF_LIST; MESON[set_of_list] 
   `{u1, u2,u3} = set_of_list [u1;u2:real^3;u3]`]);;
e (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
            (if u0 IN {u1, u2, u3}  then CARD {u1, u2, u3}  
             else SUC (CARD {u1, u2, u3} ))`);;
e (UP_ASM_TAC THEN REWRITE_TAC[CARD_CLAUSES]);;
e (UP_ASM_TAC THEN COND_CASES_TAC);;
e (DISCH_TAC);;
e (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} < &3`);;
e (REWRITE_WITH `{u0,u1,u2,u3:real^3} = {u1, u2,u3}`);;
e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e (NEW_GOAL  `CARD {u1, u2, u3} = CARD {u0, u1, u2, u3} <=> 
            {u1, u2, u3:real^3} = {u0, u1, u2, u3}`);;
e (MATCH_MP_TAC SUBSET_CARD_EQ);;
e (STRIP_TAC);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (SET_TAC[]);;
e (ASM_MESON_TAC[]);;

e (REWRITE_TAC[MESON[set_of_list] 
  `{u1:real^3,u2, u3} = set_of_list [u1;u2;u3]`]);;
e (MATCH_MP_TAC AFF_DIM_LE_LENGTH);;
e (REWRITE_TAC[LENGTH]);;
e (ARITH_TAC);;
e (NEW_GOAL `F`);;
e (ASM_MESON_TAC[ARITH_RULE `a = int_of_num 3 /\ a <  int_of_num 3 ==> F`]);;
e (ASM_MESON_TAC[]);;
e STRIP_TAC;;
e (NEW_GOAL `CARD {u1:real^3, u2, u3} = 3`);;
e (NEW_GOAL `CARD {u1,u2,u3:real^3} <= 3`);;
e (MATCH_MP_TAC (ARITH_RULE 
 `a <= LENGTH [u1;u2;u3:real^3] /\ LENGTH [u1;u2;u3:real^3] <= b ==> a <= b`));;
e STRIP_TAC;;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;CARD_SET_OF_LIST_LE]);;
e (REWRITE_TAC[LENGTH] THEN ARITH_TAC);;
e (ASM_CASES_TAC `CARD {u1:real^3, u2, u3} <= 2`);;
e (NEW_GOAL `CARD {u0,u1,u2,u3:real^3} <= 3`);;
e (NEW_GOAL `CARD {u0:real^3, u1, u2, u3} = 
  (if u0 IN {u1,u2,u3} then CARD {u1,u2,u3} else SUC (CARD {u1,u2,u3}))`);;
e (NEW_GOAL `FINITE {u1,u2,u3:real^3}`);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u1,u2,u3:real^3} = set_of_list [u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (ASM_REWRITE_TAC[CARD_CLAUSES]);;
e (UP_ASM_TAC THEN COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (ASM_ARITH_TAC);;
e (ABBREV_TAC `xl = list_of_set {u0, u1, u2, u3:real^3}`);;


e (NEW_GOAL `aff_dim {u0:real^3, u1, u2, u3} 
           < int_of_num (CARD {u0, u1, u2, u3})`);;
e (REWRITE_WITH `{u0,u1,u2,u3:real^3} = set_of_list (xl:(real^3)list)`);;
e (EXPAND_TAC "xl");;
e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
e (MATCH_MP_TAC SET_OF_LIST_OF_SET);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0, u1, u2, u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (MATCH_MP_TAC AFF_DIM_LE_LENGTH);;
e (REWRITE_WITH `set_of_list (xl:(real^3)list) = {u0, u1, u2, u3:real^3}`);;
e (EXPAND_TAC "xl");;
e (MATCH_MP_TAC SET_OF_LIST_OF_SET);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (EXPAND_TAC "xl");;
e (MATCH_MP_TAC LENGTH_LIST_OF_SET);;
e (REWRITE_TAC[MESON[set_of_list] 
 `{u0,u1,u2,u3:real^3} = set_of_list [u0;u1;u2;u3]`;FINITE_SET_OF_LIST]);;
e (NEW_GOAL `F`);;
e (ASM_ARITH_TAC);;
e (ASM_MESON_TAC[]);;
e (ASM_ARITH_TAC);;
e ASM_ARITH_TAC;;
e (MATCH_MP_TAC (REAL_ARITH 
  `radV {u0,u1,u2:real^3,u3} = a /\ radV {u0,u1,u2,u3} = b ==> a = b`));;
e STRIP_TAC;;
e (ONCE_REWRITE_TAC[DIST_SYM] THEN FIRST_ASSUM MATCH_MP_TAC);;
e (SET_TAC[]);;
e (MESON_TAC[]);;

e (ASM_MESON_TAC[]);;

(* --------------------------------------------- *)

e (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`);;
e (REWRITE_TAC[BARV]);;
e (STRIP_TAC);;
e (NEW_GOAL `F`);;
e (ASM_ARITH_TAC);;
e (ASM_MESON_TAC[]);;

(* 
Here we have finished the first part `mcell0 V ul = {}`;there are 3 parts left:
mcell1 V ul = {}
mcell2 V ul = {}
mcell3 V ul = {}
*)

(* =============== Case 2 =================================== *) ( Finished *)

e (REWRITE_TAC[mcell1]);;
e (COND_CASES_TAC);;
e (NEW_GOAL `F`);;
e (UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC);;
e (UP_ASM_TAC THEN MESON_TAC[]);;
e (REWRITE_TAC[]);;

(* =============== Case 3 =================================== *) (* Finished *)

e (REWRITE_TAC[mcell2]);;
e (COND_CASES_TAC);;
e (NEW_GOAL `F`);;
e (UP_ASM_TAC THEN UP_ASM_TAC THEN REAL_ARITH_TAC);;
e (UP_ASM_TAC THEN MESON_TAC[]);;
e (REWRITE_TAC[]);;

(* =============== Case 4 =================================== *) ( Finished *)

e (REWRITE_TAC[mcell3]);;
e (COND_CASES_TAC);;
e (NEW_GOAL `F`);;
e (ASM_REAL_ARITH_TAC);;
e (ASM_MESON_TAC[]);;
e (MESON_TAC[]);;


(* =============== Reverse part =============================== *)

(* .............................................................*)


(* ! Need to be done later ...................................... *)

(* Good luck *)

end;;