(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Fan                                                               *)
(* Author: Alexey Solovyev                                                    *)
(* Date: 2010-04-06                                                           *)
(*                                                                            *)
(* Equivalence of inverse_sigma_fan and inverse1_sigma_fan                    *)
(* ========================================================================== *)

(* TODO: results from this file should be added into introduction.hl *)

(* flyspeck_needs "fan/fan_defs.hl";;*)

module Fan_misc = struct


let inverse_sigma_fan = new_definition `inverse_sigma_fan x V E v = inverse(extension_sigma_fan x V E v)`;;
let inverse1_sigma_fan=new_definition`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)= @g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
/\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
/\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
(* We are using this definition from tame_defs.hl *)
let dart1_of_fan = new_definition
  `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) =  { (v,w) | {v,w} IN E }`;;
let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
let EXTENSION_SIGMA_FAN_EQ_RES = 
prove(`!x V E v. extension_sigma_fan x V E v = res (sigma_fan x V E v) (set_of_edge v V E)`,
REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; Fan.extension_sigma_fan; Sphere.res] THEN MESON_TAC[]);;
(* ------------------------------------------------------------------------- *) (* inverse_sigma_fan_bis is the inverse of extension_sigma_fan *) (* ------------------------------------------------------------------------- *)
let INVERSE_SIGMA_FAN = 
prove(`!x V E v. FAN (x,V,E) ==> (extension_sigma_fan x V E v) o (inverse_sigma_fan x V E v) = I /\ (inverse_sigma_fan x V E v) o (extension_sigma_fan x V E v) = I`,
REPEAT GEN_TAC THEN REWRITE_TAC[inverse_sigma_fan] THEN DISCH_TAC THEN MATCH_MP_TAC PERMUTES_INVERSES_o THEN DISJ_CASES_TAC (MESON[] `(?u:real^3. {v, u} IN E) \/ (!u. ~({v,u} IN E))`) THENL [ ASM_MESON_TAC[Fan.permutes_sigma_fan]; ALL_TAC ] THEN EXISTS_TAC `{}:real^3->bool` THEN REWRITE_TAC[PERMUTES_EMPTY; FUN_EQ_THM] THEN X_GEN_TAC `w:real^3` THEN REWRITE_TAC[I_THM; Fan.extension_sigma_fan] THEN REWRITE_TAC[Fan.set_of_edge; IN_ELIM_THM] THEN ASM_MESON_TAC[]);;
let EXTENSION_SIGMA_FAN_INJECTIVE = 
prove(`!x V E v. FAN (x,V,E) ==> (!u w. extension_sigma_fan x V E v u = extension_sigma_fan x V E v w ==> u = w)`,
REPEAT GEN_TAC THEN DISCH_THEN (MP_TAC o (fun th -> CONJUNCT2 (SPEC `v:real^3` (MATCH_MP INVERSE_SIGMA_FAN th)))) THEN ABBREV_TAC `f = extension_sigma_fan (x:real^3) V E v` THEN ABBREV_TAC `g = inverse_sigma_fan (x:real^3) V E v` THEN REPEAT STRIP_TAC THEN POP_ASSUM (MP_TAC o (fun th -> AP_TERM `g:real^3->real^3` th)) THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN MESON_TAC[]);;
(* ------------------------------------------------------------------------- *) (* Connection between dart1_of_fan and set_of_edge *) (* ------------------------------------------------------------------------- *)
let IN_SET_OF_EDGE = 
prove(`!V E (v:A) w. UNIONS E SUBSET V /\ (v, w) IN dart1_of_fan (V,E) ==> v IN V /\ w IN V /\ w IN set_of_edge v V E /\ v IN set_of_edge w V E`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `v:A IN V /\ w IN V` STRIP_ASSUME_TAC THENL [ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET; IN_UNIONS; dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN STRIP_TAC THEN STRIP_TAC THEN FIRST_ASSUM (MP_TAC o SPEC `v:A`) THEN FIRST_X_ASSUM (MP_TAC o SPEC `w:A`) THEN ANTS_TAC THENL [EXISTS_TAC `{v':A,w'}` THEN ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN ANTS_TAC THENL [EXISTS_TAC `{v':A,w'}` THEN ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[]; ALL_TAC ] THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[dart1_of_fan; Fan.set_of_edge; IN_ELIM_THM; PAIR_EQ] THEN MESON_TAC[SET_RULE `{w, v} = {v, w}`]);;
let FAN_IN_SET_OF_EDGE = 
prove(`!x V E v w. FAN (x,V,E) /\ {v,w} IN E ==> v IN V /\ w IN V /\ w IN set_of_edge v V E /\ v IN set_of_edge w V E`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC IN_SET_OF_EDGE THEN REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN CONJ_TAC THENL [ REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN SIMP_TAC[Fan.FAN]; ASM_MESON_TAC[] ] );;
(* ------------------------------------------------------------------------- *) (* For fans, inverse1_sigma_fan and inverse_sigma_fan_bis are equivalent *) (* ------------------------------------------------------------------------- *)
let INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN = 
prove(`!x V E v w. FAN (x,V,E) /\ {v, w} IN E ==> inverse1_sigma_fan x V E v w = inverse_sigma_fan x V E v w`,
REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM (STRIP_ASSUME_TAC o fun th -> (MATCH_MP FAN_IN_SET_OF_EDGE th)) THEN MP_TAC (SPECL [`x:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] EXTENSION_SIGMA_FAN_INJECTIVE) THEN ASM_REWRITE_TAC[] THEN ABBREV_TAC `f = extension_sigma_fan (x:real^3) V E v` THEN ABBREV_TAC `g = inverse1_sigma_fan (x:real^3) V E v` THEN ABBREV_TAC `h = inverse_sigma_fan (x:real^3) V E v` THEN DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o SPECL [`(g:real^3->real^3) w`; `(h:real^3->real^3) w`]) THEN ANTS_TAC THEN REWRITE_TAC[] THEN SUBGOAL_THEN `(f:real^3->real^3) ((g:real^3->real^3) w) = w` ASSUME_TAC THENL [ REMOVE_ASSUM THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN REWRITE_TAC[Fan.extension_sigma_fan] THEN MP_TAC (SPECL [`x:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] Fan.INVERSE1_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN REMOVE_ASSUM THEN REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`)) THEN ASM_REWRITE_TAC[Fan.set_of_edge; IN_ELIM_THM] THEN SIMP_TAC[] THEN ABBREV_TAC `u:real^3 = inverse1_sigma_fan x V E v w` THEN DISCH_TAC THEN SUBGOAL_THEN `u:real^3 IN V` (fun th -> SIMP_TAC[th]) THEN ASM_MESON_TAC[FAN_IN_SET_OF_EDGE]; ALL_TAC ] THEN POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN ASM_MESON_TAC[INVERSE_SIGMA_FAN; FUN_EQ_THM; I_THM; o_THM]);;
end;;