text_formalization/fan/fan_misc.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Fan                                                               *)\r
   5 (* Author: Alexey Solovyev                                                    *)\r
   6 (* Date: 2010-04-06                                                           *)\r
   7 (*                                                                            *)\r
   8 (* Equivalence of inverse_sigma_fan and inverse1_sigma_fan                    *)\r
   9 (* ========================================================================== *)\r
  10 \r
  11 (* TODO: results from this file should be added into introduction.hl *)\r
  12 \r
  13 (* flyspeck_needs "fan/fan_defs.hl";;*)\r
  14 \r
  15 module Fan_misc = struct\r
  16 \r
  17 \r
  18 let inverse_sigma_fan = new_definition `inverse_sigma_fan x V E v = inverse(extension_sigma_fan x V E v)`;;\r
  19 \r
  20 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)\r
  21 /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)\r
  22 /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;\r
  23 \r
  24 (* We are using this definition from tame_defs.hl *)\r
  25 let dart1_of_fan = new_definition\r
  26   `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) =  { (v,w) | {v,w} IN E }`;;\r
  27 \r
  28 \r
  29 \r
  30 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;\r
  31 \r
  32 \r
  33 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)`,\r
  34    REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; Fan.extension_sigma_fan; Sphere.res] THEN\r
  35      MESON_TAC[]);;\r
  36 \r
  37 \r
  38 (* ------------------------------------------------------------------------- *)\r
  39 (* inverse_sigma_fan_bis is the inverse of extension_sigma_fan                   *)\r
  40 (* ------------------------------------------------------------------------- *)\r
  41 \r
  42 let INVERSE_SIGMA_FAN = prove(`!x V E v. FAN (x,V,E) \r
  43                               ==> (extension_sigma_fan x V E v) o (inverse_sigma_fan x V E v) = I\r
  44                                   /\ (inverse_sigma_fan x V E v) o (extension_sigma_fan x V E v) = I`,\r
  45    REPEAT GEN_TAC THEN REWRITE_TAC[inverse_sigma_fan] THEN\r
  46      DISCH_TAC THEN\r
  47      MATCH_MP_TAC PERMUTES_INVERSES_o THEN\r
  48      DISJ_CASES_TAC (MESON[] `(?u:real^3. {v, u} IN E) \/ (!u. ~({v,u} IN E))`) THENL\r
  49      [\r
  50        ASM_MESON_TAC[Fan.permutes_sigma_fan];\r
  51        ALL_TAC\r
  52      ] THEN\r
  53 \r
  54      EXISTS_TAC `{}:real^3->bool` THEN\r
  55      REWRITE_TAC[PERMUTES_EMPTY; FUN_EQ_THM] THEN\r
  56      X_GEN_TAC `w:real^3` THEN\r
  57      REWRITE_TAC[I_THM; Fan.extension_sigma_fan] THEN\r
  58      REWRITE_TAC[Fan.set_of_edge; IN_ELIM_THM] THEN\r
  59      ASM_MESON_TAC[]);;\r
  60                                \r
  61 \r
  62 \r
  63 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)`,\r
  64     REPEAT GEN_TAC THEN\r
  65       DISCH_THEN (MP_TAC o (fun th -> CONJUNCT2 (SPEC `v:real^3` (MATCH_MP INVERSE_SIGMA_FAN th)))) THEN\r
  66       ABBREV_TAC `f = extension_sigma_fan (x:real^3) V E v` THEN\r
  67       ABBREV_TAC `g = inverse_sigma_fan (x:real^3) V E v` THEN\r
  68       REPEAT STRIP_TAC THEN\r
  69       POP_ASSUM (MP_TAC o (fun th -> AP_TERM `g:real^3->real^3` th)) THEN\r
  70       POP_ASSUM MP_TAC THEN\r
  71       REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN\r
  72       MESON_TAC[]);;\r
  73      \r
  74 \r
  75 \r
  76 (* ------------------------------------------------------------------------- *)\r
  77 (* Connection between dart1_of_fan and set_of_edge                           *)\r
  78 (* ------------------------------------------------------------------------- *)\r
  79          \r
  80 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`,\r
  81    REPEAT GEN_TAC THEN STRIP_TAC THEN\r
  82      SUBGOAL_THEN `v:A IN V /\ w IN V` STRIP_ASSUME_TAC THENL\r
  83      [\r
  84        POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN\r
  85          REWRITE_TAC[SUBSET; IN_UNIONS; dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN\r
  86          STRIP_TAC THEN STRIP_TAC THEN\r
  87          FIRST_ASSUM (MP_TAC o SPEC `v:A`) THEN\r
  88          FIRST_X_ASSUM (MP_TAC o SPEC `w:A`) THEN\r
  89          ANTS_TAC THENL [EXISTS_TAC `{v':A,w'}` THEN ASM SET_TAC[]; ALL_TAC] THEN\r
  90          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN\r
  91          ANTS_TAC THENL [EXISTS_TAC `{v':A,w'}` THEN ASM SET_TAC[]; ALL_TAC] THEN\r
  92          REWRITE_TAC[];\r
  93        ALL_TAC\r
  94      ] THEN\r
  95      ASM_REWRITE_TAC[] THEN\r
  96      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN\r
  97      REWRITE_TAC[dart1_of_fan; Fan.set_of_edge; IN_ELIM_THM; PAIR_EQ] THEN\r
  98      MESON_TAC[SET_RULE `{w, v} = {v, w}`]);;\r
  99 \r
 100 \r
 101 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`,\r
 102    REPEAT GEN_TAC THEN STRIP_TAC THEN\r
 103      MATCH_MP_TAC IN_SET_OF_EDGE THEN\r
 104      REWRITE_TAC[dart1_of_fan; IN_ELIM_THM; PAIR_EQ] THEN\r
 105      CONJ_TAC THENL\r
 106      [\r
 107        REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN\r
 108          SIMP_TAC[Fan.FAN];\r
 109        ASM_MESON_TAC[]\r
 110      ] );;\r
 111          \r
 112          \r
 113 (* ------------------------------------------------------------------------- *)\r
 114 (* For fans, inverse1_sigma_fan and inverse_sigma_fan_bis are equivalent         *)\r
 115 (* ------------------------------------------------------------------------- *)\r
 116 \r
 117 let INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN = prove(`!x V E v w. FAN (x,V,E) /\ {v, w} IN E ==> \r
 118                                                       inverse1_sigma_fan x V E v w = inverse_sigma_fan x V E v w`,\r
 119     REPEAT GEN_TAC THEN\r
 120       DISCH_TAC THEN\r
 121       FIRST_ASSUM (STRIP_ASSUME_TAC o fun th -> (MATCH_MP FAN_IN_SET_OF_EDGE th)) THEN\r
 122       MP_TAC (SPECL [`x:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] EXTENSION_SIGMA_FAN_INJECTIVE) THEN\r
 123       ASM_REWRITE_TAC[] THEN\r
 124       ABBREV_TAC `f = extension_sigma_fan (x:real^3) V E v` THEN\r
 125       ABBREV_TAC `g = inverse1_sigma_fan (x:real^3) V E v` THEN\r
 126       ABBREV_TAC `h = inverse_sigma_fan (x:real^3) V E v` THEN\r
 127       DISCH_TAC THEN\r
 128       FIRST_X_ASSUM (MP_TAC o SPECL [`(g:real^3->real^3) w`; `(h:real^3->real^3) w`]) THEN\r
 129       ANTS_TAC THEN REWRITE_TAC[] THEN\r
 130 \r
 131       SUBGOAL_THEN `(f:real^3->real^3) ((g:real^3->real^3) w) = w` ASSUME_TAC THENL\r
 132       [\r
 133         REMOVE_ASSUM THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
 134           POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN\r
 135           REWRITE_TAC[Fan.extension_sigma_fan] THEN\r
 136           MP_TAC (SPECL [`x:real^3`; `V:real^3->bool`; `E:(real^3->bool)->bool`; `v:real^3`] Fan.INVERSE1_SIGMA_FAN) THEN\r
 137           ASM_REWRITE_TAC[] THEN\r
 138           STRIP_TAC THEN\r
 139           REMOVE_ASSUM THEN\r
 140           REPLICATE_TAC 2 (FIRST_X_ASSUM (MP_TAC o SPEC `w:real^3`)) THEN\r
 141           ASM_REWRITE_TAC[Fan.set_of_edge; IN_ELIM_THM] THEN\r
 142           SIMP_TAC[] THEN\r
 143           ABBREV_TAC `u:real^3 = inverse1_sigma_fan x V E v w` THEN\r
 144           DISCH_TAC THEN\r
 145           SUBGOAL_THEN `u:real^3 IN V` (fun th -> SIMP_TAC[th]) THEN\r
 146           ASM_MESON_TAC[FAN_IN_SET_OF_EDGE];\r
 147         ALL_TAC\r
 148       ] THEN\r
 149 \r
 150       POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN\r
 151       REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN\r
 152       ASM_MESON_TAC[INVERSE_SIGMA_FAN; FUN_EQ_THM; I_THM; o_THM]);;\r
 153 \r
 154 \r
 155 end;;\r