1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Cqaoqlr = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
95 let K_SUC_2_MOD_SUB=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 1) MOD k= (k- SUC((i+1) MOD k)) MOD k`,
98 THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)`]);;
100 let K_SUC_2_MOD_SUB_ID=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 2) MOD k= (k- SUC((i) MOD k)) MOD k`,
103 THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)`
105 THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`SUC i`;`k`]
106 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i) MOD k`;`k`]
109 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i MOD k)`;`k`]
110 THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (SUC i MOD k))=k - SUC i MOD k`]
113 let A_B_J_SCS_OPP=prove(`scs_a_v39 (scs_opp_v39 s) i j = scs_a_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))
114 /\ scs_b_v39 (scs_opp_v39 s) i j = scs_b_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))
115 /\ scs_J_v39 (scs_opp_v39 s) i j = scs_J_v39 s (scs_k_v39 s- SUC(i MOD scs_k_v39 s)) (scs_k_v39 s- SUC(j MOD scs_k_v39 s))`,
116 REWRITE_TAC[scs_opp_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;peropp2]);;
118 let SUC_OPP_ID=prove(`1<k ==> SUC (k - SUC i MOD k) MOD k= (k- i MOD k) MOD k`,
120 THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`(i)`;`k`]
121 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (i) MOD k`;`k`]
122 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC ( i) MOD k)`;`k`]
126 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (i MOD k)`;`k`]
127 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (i MOD k))`;`k`]
128 THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (i MOD k))=k - i MOD k`]);;
133 let K_SUC_2_MOD_F_SUB_ID=prove(`1<k ==> (k - SUC ((i + 2) MOD k) + 3) MOD k= (k- SUC((i+k-1) MOD k)) MOD k`,
136 THEN ASM_SIMP_TAC [SUC_MOD_EQ_MOD_SUC;ARITH_RULE`1<k ==> SUC (k - SUC ((i + 2) MOD k)) = k- (i+2) MOD k`;ARITH_RULE`i+2=SUC(SUC i)/\ i+3=SUC(i+2)`
138 THEN MRESA_TAC SUC_MOD_EQ_MOD_SUC[`(SUC i)`;`k`]
139 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i) MOD k`;`k`]
140 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (SUC i) MOD k)`;`k`]
144 THEN MRESA_TAC MOD_SUC_MOD[`k - SUC (SUC i MOD k)`;`k`]
145 THEN MRESA_TAC MOD_SUC_MOD[`SUC(k - SUC (SUC i MOD k))`;`k`]
146 THEN ASM_SIMP_TAC[ARITH_RULE`1<k==>SUC (k - SUC (SUC i MOD k))=k - SUC i MOD k/\ SUC (i + k - 1)= 1*k+i`;SUC_OPP_ID;MOD_MULT_ADD]);;
148 let ELEMENT1_SYM_0=prove(`{--a}= IMAGE (\x:real^N. --x) {a}`,
149 REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION;IN_SING;SET_RULE`a IN{b,c} <=> a=b\/ a=c`]
153 THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]
156 let SCS_GENERIC_SYM_0=prove(`BBs_v39 s v/\ is_scs_v39 s/\ scs_generic v
157 ==> scs_generic (\i. --v (scs_k_v39 s - SUC (i MOD scs_k_v39 s)))`,
158 REWRITE_TAC[scs_generic;BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
160 THEN ABBREV_TAC`k= scs_k_v39 s`
161 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
162 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
163 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
165 THEN ASM_SIMP_TAC[OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_E_EQ_NEG;]
167 THEN REWRITE_TAC[generic]
169 THEN MRESAL_TAC IN_SYM_0[`u`;`IMAGE (\i. --(v:num->real^3) i) (:num)`][IMAGE_V_SYM_0;REFL_SYM_0]
170 THEN MRESAL_TAC IMAGE_E_SYM_0[`{v',w}`;`v:num->real^3`][GSYM ELEMENT2_SYM_0]
171 THEN THAYTHES_TAC (33-24)[`-- v':real^3`;`-- w:real^3`;`-- u:real^3`][ ELEMENT2_SYM_0;AFF_GE_VEC0_SYM_0;AFF_LT_VEC0_SYM_0;ELEMENT1_SYM_0;GSYM INTER_SYM_0]
172 THEN POP_ASSUM MP_TAC
173 THEN MRESAL_TAC SET_EQ_SYM_0[`IMAGE (\x:real^3. --x) (aff_ge {vec 0:real^3} {v', w} INTER aff_lt {vec 0} {u})`;`{}:real^3->bool`][REFL_SYM_0;IMAGE_CLAUSES]);;
175 let UNADORNED_OPP=prove(`is_scs_v39 s /\ unadorned_v39 s
176 ==> unadorned_v39 (scs_opp_v39 s)`,
177 REWRITE_TAC[LET_DEF;LET_END_DEF;unadorned_v39;scs_opp_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;peropp;EXTENSION;IN]
181 let BASIC_OPP=prove(`is_scs_v39 s /\ scs_basic_v39 s
182 ==> scs_basic_v39 (scs_opp_v39 s)`,
183 SIMP_TAC[scs_basic;UNADORNED_OPP;A_B_J_SCS_OPP]);;
186 let DIAG_OPP=prove_by_refinement(`3<k /\ scs_diag k i j ==> scs_diag k (k - SUC (i MOD k)) (k - SUC (j MOD k))`,
187 [REWRITE_TAC[scs_diag]
188 THEN REPEAT RESA_TAC;
192 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
194 THEN MRESA_TAC OPP_SUC_MOD[`i`;`k`]
195 THEN MRESA_TAC OPP_SUC_MOD[`j`;`k`];
199 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ SUC (k - SUC (i MOD k))= k- i MOD k/\ SUC (k - SUC (SUC (k - SUC i MOD k) MOD k))
200 =(k - (SUC (k - SUC i MOD k) MOD k))`)
202 THEN MRESA_TAC OPP_SUC_MOD[`j`;`k`]
203 THEN POP_ASSUM MP_TAC
207 THEN MRESA_TAC SUC_OPP_ID[`i`;`k`]
209 THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`k - SUC (SUC (k - SUC i MOD k) MOD k)`;`j`;`k`][MOD_REFL;]
212 THEN ASM_SIMP_TAC[MOD_REFL;GSYM SUC_MOD_EQ_MOD_SUC;OPP_SUC_MOD];
215 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
217 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ SUC (k - SUC (j MOD k))= k- j MOD k/\ SUC (k - SUC (SUC (k - SUC j MOD k) MOD k))
218 =(k - (SUC (k - SUC j MOD k) MOD k))`)
220 THEN MRESA_TAC OPP_SUC_MOD[`i`;`k`]
221 THEN POP_ASSUM MP_TAC
225 THEN MRESA_TAC SUC_OPP_ID[`j`;`k`]
227 THEN MRESAS_TAC Zithlqn.IMP_SUC_MOD_EQ[`k - SUC (SUC (k - SUC j MOD k) MOD k)`;`i`;`k`][MOD_REFL;]
230 THEN ASM_SIMP_TAC[MOD_REFL;GSYM SUC_MOD_EQ_MOD_SUC;OPP_SUC_MOD]]);;
234 `main_nonlinear_terminal_v11
235 ==> (!s (v:num->real^3) i.
237 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
238 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j)) /\
239 &2< scs_b_v39 s i (i+1) /\ &2< scs_b_v39 s (i+1) (i+2)/\
240 scs_a_v39 s (i+2) (i+3)< scs_b_v39 s (i+2) (i+3) /\
241 scs_a_v39 s (i+ scs_k_v39 s -1) i< scs_b_v39 s (i+scs_k_v39 s -1) i
243 scs_a_v39 s (i) (i+1) = &2 /\ scs_b_v39 s (i) (i+1) <= &2 * h0 /\
244 scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0 ==>
245 (dist(v i,v (i+1)) = &2 <=> dist(v(i+1),v(i+2)) = &2))`;;
247 let CQAOQLR = prove_by_refinement( CQAOQLR_concl,
255 THEN MATCH_DICH_TAC 0
256 THEN EXISTS_TAC`s:scs_v39`
257 THEN ASM_REWRITE_TAC[];
261 THEN REPEAT STRIP_TAC
262 THEN ABBREV_TAC`k=scs_k_v39 s`
263 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
264 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
265 THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
266 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ ~(k<=3)/\ 1<k`)
268 THEN MRESA_TAC MM_SCS_OPP[`s`;`v`;`k`]
269 THEN MRESA_TAC(GEN_ALL OPP_IS_SCS)[`(scs_opp_v39 s)`;`s:scs_v39`]
272 THEN THAYTHES_TAC 0[`(scs_opp_v39 s)`;`(\i. -- peropp (v:num->real^3) k i)`;`k- SUC((i+2) MOD k)`][IN]
273 THEN POP_ASSUM MP_TAC
274 THEN ASM_SIMP_TAC[peropp;OPP_SUC_MOD;K_SUC_2_MOD_SUB;K_SUC_2_MOD_SUB_ID;DIST_SYM_0;K_SCS_OPP;A_B_J_SCS_OPP;K_SUC_2_MOD_F_SUB_ID]
275 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
276 THEN MP_TAC SCS_GENERIC_SYM_0
278 THEN MP_TAC BASIC_OPP
280 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(i+1) MOD k`;`v:num->real^3`;`i+1`][MOD_REFL;]
281 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i MOD k`;`v:num->real^3`;`i`][MOD_REFL;]
282 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(i+2) MOD k`;`v:num->real^3`;`i+2`][MOD_REFL;]
283 THEN ONCE_REWRITE_TAC[DIST_SYM]
284 THEN ASM_REWRITE_TAC[]
285 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(i+1) MOD k`;`i MOD k `;`s:scs_v39`;`i+1`;`i`][MOD_REFL]
286 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i+1) MOD k`;`i MOD k `;`s:scs_v39`;`i+1`;`i`][MOD_REFL]
287 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`(i) MOD k`;`(i+k-1) MOD k `;`s:scs_v39`;`i`;`i+k-1`][MOD_REFL]
288 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i) MOD k`;`(i+k-1) MOD k `;`s:scs_v39`;`i`;`i+k-1`][MOD_REFL]
289 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(i+2) MOD k`;`(i+1) MOD k `;`s:scs_v39`;`i+2`;`i+1`][MOD_REFL]
291 THEN ONCE_REWRITE_TAC[DIST_SYM]
292 THEN MATCH_DICH_TAC 0
296 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
297 THEN REPEAT RESA_TAC;
302 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
303 THEN REPEAT RESA_TAC;
308 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
309 THEN REPEAT RESA_TAC;
314 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
315 THEN REPEAT RESA_TAC;
319 THEN ONCE_REWRITE_TAC[DIST_SYM]
320 THEN MATCH_DICH_TAC(36-6)
321 THEN MATCH_MP_TAC DIAG_OPP
322 THEN ASM_REWRITE_TAC[]]);;
329 let check_completeness_claimA_concl =
330 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)