1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Authors: Thomas C. Hales, Hoang Le Truong, Alexey Solovyev *)
8 (* ========================================================================== *)
11 Definitions file for Fan
14 flyspeck_needs "general/sphere.hl";;
15 flyspeck_needs "volume/vol1.hl";;
16 flyspeck_needs "hypermap/hypermap.hl";;
18 module Fan_defs = struct
22 (* General definitions *)
24 let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
27 Maybe it is better to change names to something like fan_card, fan_origin, fan_non_parallel, fan_intersection,
28 because names like fan1, fan2, fan6, fan7 are not descriptive at all.
30 If the names are changed, then it will be required to modify fan/*.hl as well. I think,
31 it is quite easy and fast: search for all occurrences of fan1 and change it to fan_card, etc.
32 This procedure should take at most 10-20 minutes.
36 let fan1 = new_definition `fan1(x,V,E):bool <=> FINITE V /\ ~(V SUBSET {})`;;
38 let fan2 = new_definition `fan2(x,V,E):bool <=> ~(x IN V)`;;
40 let fan6 = new_definition `fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
42 let fan7 = new_definition `fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
43 ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
48 In my opinion, the name `fan` is better because it follows the general convention of naming objects
51 The file fan/introduction.hl already contains the definition of the constant `fan`. Probably, it is an earlier definition
52 of fan. Now, it should be deprecated. Again, I think it will be not difficult to make corresponding
55 let FAN = new_definition `FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
56 fan6(x,V,E)/\ fan7(x,V,E)`;;
59 let set_of_edge = new_definition `set_of_edge v V E = {w | {v,w} IN E /\ w IN V}`;;
62 let sigma_fan = new_definition `sigma_fan x (V:real^3->bool) E v u =
63 if (set_of_edge v V E = {u}) then u
64 else (@(w:real^3). w IN (set_of_edge v V E) /\ ~(w = u) /\
65 (!(w1:real^3). w1 IN (set_of_edge v V E) /\ ~(w1=u) ==> azim x v u w <= azim x v u w1))`;;
68 This definition is not very important (there is only one result involving this definition
69 which proves that extension_sigma_fan permutes set_of_edge). But I decided that it is simpler
70 to have this definition rather than modify the definition of sigma_fan
74 It appears that there are three definitions of inverse_sigma_fan from the files introduction.hl, fan_misc.hl, and fan_defs.hl
75 I am renaming the one in fan/introduction.hl inverse_sigma_fan_alt and the one in fan_misc.hl as inverse_sigma_fan_bis.
76 I take the one in fan_defs.hl to be the primary definition.
79 let extension_sigma_fan = new_definition `extension_sigma_fan x (V:real^3->bool) E v u =
80 if ~(u IN set_of_edge v V E ) then u
81 else (sigma_fan x V E v u)`;;
83 let inverse_sigma_fan = new_definition `inverse_sigma_fan x V E v = inverse (extension_sigma_fan x V E v)`;;
88 let dart1_of_fan = new_definition
89 `dart1_of_fan ((V:A->bool),(E:(A->bool)->bool)) = { (v,w) | {v,w} IN E }`;;
92 let dart_of_fan = new_definition
94 { (v,v) | v IN V /\ set_of_edge (v:real^3) V E = {} } UNION { (v,w) | {v,w} IN E }`;;
97 (* in fan/introduction.hl a dart is a 4-tuple. Here it is a pair. Here is the correspondence *)
99 Do we need this correspondence?
100 Right now, there are no results involving `extended_dart` or `contracted_dart`.
101 Ultimately, it is better to use new definition of darts as pairs everywhere.
103 let i_fan=new_definition`i_fan (x:real^3) V E=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,w,(sigma_fan x V E v w)))`;;
105 let extended_dart = new_definition
106 `extended_dart (V,E) (v,w) = i_fan (vec 0) V E (vec 0, v, w, w)`;;
108 let contracted_dart = new_definition
109 `contracted_dart (x:A,v:B,w:C,w1:D) = (v,w)`;;
111 (* e_fan, n_fan, f_fan of fan/introduction.hl, restricted to pairs *)
114 In my opinion, it is better to change the names e_fan_pair, n_fan_pair, f_fan_pair
115 to e_fan, n_fan, f_fan.
116 It will require some modifications in fan/introduction.hl, but it is not a problem
119 let e_fan_pair = new_definition `e_fan_pair (V,E) (v,w) = (w,v)`;;
121 let n_fan_pair = new_definition
122 `n_fan_pair (V,E) (v,w) = v,sigma_fan (vec 0) V E v w`;;
124 let f_fan_pair = new_definition
125 `f_fan_pair (V,E) (v,w) = w,(inverse_sigma_fan (vec 0) V E w v)`;;
128 let hypermap_of_fan = new_definition
129 `hypermap_of_fan (V,E) =
130 (let p = ( \ t. res (t (V,E) ) (dart1_of_fan (V,E)) ) in
131 hypermap( dart_of_fan (V,E) , p e_fan_pair, p n_fan_pair, p f_fan_pair))`;;
133 (* Restricted versions of e_fan_pair, n_fan_pair, f_fan_pair (for convenience) *)
134 let e_fan_pair_ext = new_definition `e_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then e_fan_pair (V,E) x else x`;;
136 let n_fan_pair_ext = new_definition `n_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then n_fan_pair (V,E) x else x`;;
138 let f_fan_pair_ext = new_definition `f_fan_pair_ext (V,E) x = if x IN dart1_of_fan (V,E) then f_fan_pair (V,E) x else x`;;
141 let E_FAN_PAIR_EXT = prove(`!V E. e_fan_pair_ext (V,E) = res (e_fan_pair (V,E)) (dart1_of_fan (V,E))`,
142 REWRITE_TAC[FUN_EQ_THM; e_fan_pair_ext; Sphere.res]);;
144 let F_FAN_PAIR_EXT = prove(`!V E. f_fan_pair_ext (V,E) = res (f_fan_pair (V,E)) (dart1_of_fan (V,E))`,
145 REWRITE_TAC[FUN_EQ_THM; f_fan_pair_ext; Sphere.res]);;
147 let N_FAN_PAIR_EXT = prove(`!V E. n_fan_pair_ext (V,E) = res (n_fan_pair (V,E)) (dart1_of_fan (V,E))`,
148 REWRITE_TAC[FUN_EQ_THM; n_fan_pair_ext; Sphere.res]);;
150 let HYPERMAP_OF_FAN_ALT = prove(`!V E. hypermap_of_fan (V,E) =
151 hypermap (dart_of_fan (V,E), e_fan_pair_ext (V,E), n_fan_pair_ext (V,E), f_fan_pair_ext (V,E))`,
153 REWRITE_TAC[CONV_RULE (DEPTH_CONV let_CONV) hypermap_of_fan] THEN
154 REWRITE_TAC[E_FAN_PAIR_EXT; F_FAN_PAIR_EXT; N_FAN_PAIR_EXT]);;
157 (* Topological component and dart *)
160 let xfan = new_definition `xfan (x,V,E) = {v | ?e. (E e) /\ (v IN aff_ge {x} e)}`;;
163 let yfan = new_definition `yfan (x,V,E) = (:real^3) DIFF xfan (x,V,E)`;;
166 The original definition of yfan (renamed yfan_deprecated in fan/introduction.hl) is the following:
167 let yfan_deprecated = new_definition `yfan_deprecated (x,V,E) = {v:real^3 | ?e. (E e) /\ (~(v IN aff_ge {x} e))}`;;
168 It seems to be wrong since the negation of (?e. (E e) /\ (v IN aff_ge {x} e)) is
169 (!e. (E e) /\ ~(v IN aff_ge {x} e)).
177 w_dart_fan x V E (v,w),
181 let w_dart_fan = new_definition `w_dart_fan x (V:real^3->bool) E (y:real^3,v,w,w1:real^3)=
182 if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
184 (if set_of_edge v V E = {w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
185 else (if set_of_edge v V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
188 (* DEPRECATED, 2011-08-01, --> wedge_ge
189 let cwedge = new_definition `cwedge v0 v1 w1 w2 =
190 {y | &0 <= azim v0 v1 w1 y /\
191 azim v0 v1 w1 y <= azim v0 v1 w1 w2}`;;
196 (* DEPRECATED, 2011-08-01
197 let cw_dart_fan=new_definition `cw_dart_fan (V:real^3->bool) E (v,w)=
198 if (CARD (set_of_edge v V E) > 1)
199 then cwedge (vec 0) v w (sigma_fan (vec 0) V E v w)
203 let azim_fan = new_definition `azim_fan x (V:real^3->bool) E v w =
204 if (CARD (set_of_edge v V E) > 1)
205 then azim x v w (sigma_fan x V E v w)
209 let azim_dart = new_definition
210 `azim_dart (V,E) (v,w) =
211 if (v=w) then &2 * pi else azim_fan (vec 0) V E v w`;;
214 let rcone_fan = new_definition `rcone_fan (x:real^3) (v:real^3) (h:real) =
215 {y:real^3 | (y-x) dot (v-x) > (dist(y,x)*dist(v,x)*h)}`;;
217 (* W^0_{dart}(x,epsilon) *)
219 It is better to have rw_dart_fan V E (v,w)
221 In the book, it is defined as ... INTER rcone_fan x v (cos h),
222 in fan/introduction.hl, it is used as rw_dart_fan x V E (...) (cos s) instead (not always but only when necessary).
223 This can lead to confusions. In my opinion, it is simpler to follow the book definition. In this case,
224 some changes in fan/introduction.hl are required.
226 let rw_dart_fan = new_definition
227 `rw_dart_fan x (V:real^3->bool) E (y:real^3,v,w,w1:real^3) h =
228 w_dart_fan x V E (y,v,w,w1) INTER rcone_fan x v h`;;
230 let topological_component_yfan = new_definition
231 `topological_component_yfan ((x:real^3),(V:real^3->bool),E) =
232 { connected_component (yfan (x,V,E)) y | y | y IN yfan (x,V,E) }`;;
234 (* there is a function dart_leads_into in fan/introduction.hl. This is a bit simpler. *)
237 It is better to change name to `dart_leads_into`.
239 For the current definition of rw_dart_fan, should be: rw_dart_fan ... (cos eps),
240 but I prefer to change the definition of rw_dart_fan instead.
242 let dart_leads_into1 = new_definition
243 `dart_leads_into1 (x,V,E) (v,u) = @s. s IN topological_component_yfan (x,V,E) /\
245 rw_dart_fan x V E (x,v,u,sigma_fan x V E v u) eps SUBSET s)`;;
247 let dartset_leads_into = new_definition
248 `dartset_leads_into (x,V,E) ds =
249 @s. (!y. (y IN ds) ==> (s = dart_leads_into1 (x,V,E) y))`;;
251 (* node(x) not needed, use FST x *)
254 (* compare fan80 and fan81, which define fully_surrounded *)
255 let surrounded_node = new_definition
256 `surrounded_node (V,E) v =
257 !x. (x IN dart_of_fan (V,E)) /\ (FST x = v) ==> azim_dart (V,E) x < pi`;;
260 let fully_surrounded = new_definition
261 `fully_surrounded (V,E) = (!x. x IN dart_of_fan (V,E) ==> azim_dart (V,E) x < pi)`;;
263 (* AS: the definitions from fan/introduction.hl are below:
264 let fan81=new_definition`fan81 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> azim_fan x V E v u <pi)`;;
266 let fan80=new_definition`fan80 (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):bool<=>(!v:real^3 u:real^3. {v,u} IN E ==> &0< azim x v u (sigma_fan x V E v u) /\ azim x v u (sigma_fan x V E v u) <pi)`;;
270 let conforming_bijection = new_definition `conforming_bijection (V,E) <=>
271 !s. s IN topological_component_yfan (vec 0,V,E) ==> (?!f. f IN face_set (hypermap_of_fan (V,E)) /\
272 s = dartset_leads_into (vec 0,V,E) f)`;;
275 let conforming_half_space = new_definition `conforming_half_space (V,E) <=>
276 !f. f IN face_set (hypermap_of_fan (V,E)) ==>
277 dartset_leads_into (vec 0,V,E) f =
278 INTERS {aff_gt {vec 0, FST x, FST (f_fan_pair (V,E) x)} {FST (inverse (f_fan_pair (V,E)) x)} | x IN f}`;;
281 let conforming_solid_angle = new_definition `conforming_solid_angle (V,E) <=>
282 !f. f IN face_set (hypermap_of_fan (V,E)) ==>
283 (let U = dartset_leads_into (vec 0,V,E) f in
284 (!r. measurable (ball (vec 0,r) INTER U)) /\
285 eventually_radial (vec 0) U /\
286 sol (vec 0) U = &2 * pi + sum (f) (\x. azim_dart (V,E) x - pi))`;;
289 let conforming_diagonal = new_definition `conforming_diagonal (V,E) <=>
290 (!f x y. f IN face_set (hypermap_of_fan (V,E)) /\ x IN f /\ y IN f /\ ~(x = y) ==>
291 ~collinear {vec 0, FST x, FST y} /\
292 (y = f_fan_pair (V,E) x \/ x = f_fan_pair (V,E) y \/
293 aff_gt {vec 0} {FST x, FST y} SUBSET dartset_leads_into (vec 0,V,E) f))`;;
296 let conforming = new_definition `conforming (V,E) <=>
297 fully_surrounded (V,E) /\
298 conforming_bijection (V,E) /\
299 conforming_half_space (V,E) /\
300 conforming_solid_angle (V,E) /\
301 conforming_diagonal (V,E)`;;