1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
10 remaining conclusions from appendix to Local Fan chapter
14 module Ayqjtmd = struct
26 open Wrgcvdr_cizmrrh;;
34 open Flyspeck_constants;;
50 open Wrgcvdr_cizmrrh;;
52 open Flyspeck_constants;;
72 let XWITCCN2=prove_by_refinement(
73 ` !s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s
74 /\ taustar_v39 s vv < &0
75 ==> ~(BBprime2_v39 s = {})`,
80 THEN MRESA_TAC XWITCCN[`s:scs_v39`;`vv:num->real^3`]
82 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv1. vv1 IN A`;BBprime2_v39;IN;BBindex_min_v39;]
84 THEN SUBGOAL_THEN`?n. (?vv1. BBprime_v39 s vv1 /\
85 BBindex_v39 s vv1=n)` ASSUME_TAC;
87 EXISTS_TAC`BBindex_v39 s vv1`
88 THEN EXISTS_TAC`vv1:num->real^3`
89 THEN ASM_REWRITE_TAC[];
92 THEN REWRITE_TAC[MINIMAL]
94 THEN EXISTS_TAC`vv1':num->real^3`
96 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th] THEN ASSUME_TAC (SYM th))
97 THEN ASM_REWRITE_TAC[Misc_defs_and_lemmas.min_num;ARITH_RULE`(A=B:num)<=> (B=A)`]
99 THEN MATCH_MP_TAC SELECT_UNIQUE
100 THEN ASM_REWRITE_TAC[BETA_THM;IMAGE;IN_ELIM_THM;]
106 THEN POP_ASSUM MP_TAC
107 THEN ASM_REWRITE_TAC[]
108 THEN SUBGOAL_THEN`(?x. BBprime_v39 s x /\ BBindex_v39 s vv1' = BBindex_v39 s x)`ASSUME_TAC;
110 EXISTS_TAC`vv1':num->real^3`
111 THEN ASM_REWRITE_TAC[];
114 THEN POP_ASSUM(fun th-> MRESA1_TAC th`BBindex_v39 s vv1'`)
115 THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <= BBindex_v39 s vv1' ==>
116 BBindex_v39 s x < BBindex_v39 s vv1' \/ BBindex_v39 s x = BBindex_v39 s vv1'`)
118 THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC)
119 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN
120 MRESA1_TAC th` BBindex_v39 s x`)
121 THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;
123 EXISTS_TAC`x:num->real^3`
124 THEN ASM_REWRITE_TAC[];
127 THEN ASM_REWRITE_TAC[];
130 THEN ASM_REWRITE_TAC[]
135 EXISTS_TAC`vv1':num->real^3`
136 THEN ASM_REWRITE_TAC[];
140 THEN ASM_REWRITE_TAC[]
141 THEN MP_TAC(ARITH_RULE`BBindex_v39 s x <BBindex_v39 s vv1' \/ BBindex_v39 s vv1' <= BBindex_v39 s x`)
146 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
147 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN
148 MRESA1_TAC th` BBindex_v39 s x`)
149 THEN SUBGOAL_THEN`(?vv1. BBprime_v39 s vv1 /\ BBindex_v39 s x = BBindex_v39 s vv1)`ASSUME_TAC;
151 EXISTS_TAC`x:num->real^3`
152 THEN ASM_REWRITE_TAC[];
156 THEN ASM_REWRITE_TAC[];
161 let unadorned_MMs=prove_by_refinement(
162 ` unadorned_v39 s ==> (MMs_v39 s = BBprime2_v39 s)`
166 REWRITE_TAC[FUN_EQ_THM]
167 THEN REWRITE_TAC[unadorned_v39;MMs_v39;]
168 THEN REPEAT STRIP_TAC
186 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;]
194 let S_INIT_IS_UNADORNED=prove(
195 `MEM s s_init_list_v39
196 ==> unadorned_v39 s`,
197 REWRITE_TAC[s_init_list_v39;JEJTVGB_assume_v39;GSYM IN_SET_OF_LIST;set_of_list;LET_DEF;LET_END_DEF
198 ;SET_RULE`A IN {A1,A2,A3,A4,A5,A6,A7,A8} <=> A= A1 \/ A= A2 \/ A= A3 \/ A= A4 \/ A= A5 \/ A= A6 \/ A= A7 \/ A= A8`]
201 THEN REWRITE_TAC[unadorned_v39]
202 THEN ASM_REWRITE_TAC[scs_lo_v39_explicit;scs_str_v39_explicit;scs_am_v39_explicit;scs_bm_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`~(4<=3)/\ 3-1=2`;mk_unadorned_v39;CS_ADJ;scs_J_v39_explicit;change_type_v2;d_tame ;change_type_v3;scs_hi_v39_explicit;]);;
207 `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
208 taustar_v39 s vv < &0
209 ==> ~(MMs_v39 s = {})`,
212 THEN MP_TAC S_INIT_IS_UNADORNED
214 THEN MP_TAC unadorned_MMs
216 THEN MATCH_MP_TAC XWITCCN2
217 THEN EXISTS_TAC`vv:num->real^3`
218 THEN ASM_REWRITE_TAC[]);;
222 let EAPGLE =prove( `(!s. MEM s s_init_list_v39 ==> MMs_v39 s = {}) ==> JEJTVGB_assume_v39`,
224 THEN MATCH_MP_TAC ZITHLQN
225 THEN REPEAT STRIP_TAC
226 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv< &0\/ &0 <= taustar_v39 s vv`)
228 THEN MRESA_TAC AYQJTMD[`s:scs_v39`;`vv:num->real^3`]
231 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
232 THEN MRESA1_TAC th`s:scs_v39`));;