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 Yrtafyh = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
90 let SUR_MOD_FUN=prove(`~(k=0)==> ?i. (i+p) MOD k = p' MOD k`,
92 THEN MP_TAC(ARITH_RULE`p MOD k<= p' MOD k\/ p' MOD k< p MOD k`)
95 EXISTS_TAC`p' MOD k- p MOD k`
96 THEN MRESA_TAC DIVISION[`p'`;`k`]
97 THEN MP_TAC(ARITH_RULE`p' MOD k< k /\ p MOD k<= p' MOD k ==> p' MOD k - p MOD k < k /\ p' MOD k - p MOD k + p MOD k= p' MOD k`)
99 THEN MRESAS_TAC MOD_LT[`p' MOD k- p MOD k`;`k`][DIVISION]
100 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL]
101 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
103 EXISTS_TAC`p' MOD k +k - p MOD k`
104 THEN MRESA_TAC DIVISION[`p`;`k`]
105 THEN MP_TAC(ARITH_RULE`p MOD k< k /\ p' MOD k< p MOD k ==> p' MOD k +k - p MOD k < k /\ (p' MOD k + k - p MOD k) + p MOD k=1*k+ p' MOD k`)
107 THEN MRESAS_TAC MOD_LT[`p' MOD k+k- p MOD k`;`k`][DIVISION]
108 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k+k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL;MOD_MULT_ADD]
109 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
111 let TRANS_DIAG=prove(`~(k=0)/\ (i+p) MOD k = p' MOD k /\ p' + q = p + q'
112 ==> (i+q) MOD k= q' MOD k `,
114 THEN MATCH_MP_TAC Hdplygy.MOD_EQ_MOD
115 THEN EXISTS_TAC`p:num`
116 THEN ASM_REWRITE_TAC[]
117 THEN ONCE_REWRITE_TAC[ARITH_RULE`p + i + q= (i +p)+ q:num`]
118 THEN MRESA_TAC MOD_ADD_MOD[`i+p:num`;`q`;`k`]
119 THEN POP_ASSUM(fun th-> ASM_SIMP_TAC[SYM th;MOD_ADD_MOD]));;
125 (*******************)
128 let scs_components = prove_by_refinement(
129 `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39
130 s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s,
131 scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,
134 REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
135 REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
136 REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
137 REWRITE_TAC[scs_str_v39];
139 BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4;
140 Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop0;Misc_defs_and_lemmas.drop3;Misc_defs_and_lemmas.drop1;Misc_defs_and_lemmas.part0;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop2])
144 let scs_inj = prove_by_refinement(
145 `!s s'. scs_basic_v39 s /\ scs_basic_v39 s' /\
146 scs_d_v39 s = scs_d_v39 s' /\
147 scs_k_v39 s = scs_k_v39 s' /\
148 (scs_a_v39 s = scs_a_v39 s') /\
149 (scs_b_v39 s = scs_b_v39 s')
154 REPEAT WEAKER_STRIP_TAC;
155 REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
156 REWRITE_TAC[scs_basic;unadorned_v39];
157 ONCE_REWRITE_TAC[EQ_SYM_EQ];
158 REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
159 REPEAT WEAKER_STRIP_TAC;
160 ONCE_REWRITE_TAC[GSYM scs_v39];
162 ASM_REWRITE_TAC[scs_components];
163 TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
164 BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
171 let DIAG_PSORT1=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
172 p' + q = p + q' /\ ~(k=0) /\ (psort k (i',j) = psort k (p,q))
173 ==> (psort k (i+i',i+j) = psort k (p',q'))`,
176 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
179 THEN POP_ASSUM MP_TAC
180 THEN MP_TAC TRANS_DIAG
182 THEN MP_TAC(SET_RULE`i' MOD k <= j MOD k \/ ~(i' MOD k <= j MOD k)`)
185 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
190 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
191 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
195 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
196 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]
197 THEN MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
200 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
203 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
206 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
211 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
212 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`];
215 MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
218 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
221 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
226 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
227 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
233 let DIAG_PSORT2=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
234 p' + q = p + q' /\ ~(k=0) /\ (psort k (i+i',i+j) = psort k (p',q'))
236 (psort k (i',j) = psort k (p,q))`,
238 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
241 THEN POP_ASSUM MP_TAC
242 THEN MP_TAC TRANS_DIAG
244 THEN MP_TAC(SET_RULE`(i+i') MOD k <= (i+j) MOD k \/ ~((i+i') MOD k <= (i+j) MOD k)`)
247 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
252 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
253 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
257 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
258 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
260 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
264 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
267 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
270 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
275 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
276 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
278 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
281 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
284 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
289 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
290 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
295 let DIAG_PSORT=prove(
296 ` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
297 p' + q = p + q' /\ ~(k=0)
299 ((psort k (i+i',i+j) = psort k (p',q'))
301 (psort k (i',j) = psort k (p,q)))`,
306 MATCH_MP_TAC DIAG_PSORT2
308 MATCH_MP_TAC DIAG_PSORT1
311 let TRANS_DIAG=prove(`
313 ==> (scs_diag k i' j<=> scs_diag k (i+i') (i+j)) `,
314 SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + i') = i + (i' + 1)/\ SUC i= i+1`;Ocbicby.MOD_EQ_MOD_SHIFT]);;
317 let A_EQ_PSORT=prove(` is_scs_v39 s /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
318 ==> scs_a_v39 s i j= scs_a_v39 s p q`,
319 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
321 THEN POP_ASSUM MP_TAC
322 THEN ABBREV_TAC`k=scs_k_v39 s`
323 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
325 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
330 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
331 THEN MRESA_TAC CHANGE_A_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
333 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
334 THEN REPEAT RESA_TAC);;
337 let B_EQ_PSORT=prove(` is_scs_v39 s /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
338 ==> scs_b_v39 s i j= scs_b_v39 s p q`,
339 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
341 THEN POP_ASSUM MP_TAC
342 THEN ABBREV_TAC`k=scs_k_v39 s`
343 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
345 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
350 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
351 THEN MRESA_TAC CHANGE_B_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
353 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
354 THEN REPEAT RESA_TAC);;
356 let PROPERTY_OF_K_SCS=prove(`is_scs_v39 s==> ~(scs_k_v39 s= 0)/\ 0< scs_k_v39 s/\ 1< scs_k_v39 s/\ 2< scs_k_v39 s`,
358 THEN MP_TAC Axjrpnc.is_scs_k_le_3
364 let PSORT_PERIODIC=prove(`~(k=0) ==> psort (k) (i + k,j) = psort (k) (i,j)
365 /\ psort (k) (i,j+k) = psort (k) (i,j)`,
367 THEN REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
368 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+k=1*k+i`]
369 THEN ASM_SIMP_TAC[MOD_MULT_ADD]);;
372 let DIAG_NOT_PSORT = prove_by_refinement(
373 `~(k=0) /\ scs_diag k i j ==> !i'. ~(psort k (i,j) = psort k (i',SUC i'))`,
375 REWRITE_TAC[scs_diag;psort;LET_DEF;LET_END_DEF]
378 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k\/ ~(i MOD k <= j MOD k)`)
381 MP_TAC(ARITH_RULE`i' MOD k <= SUC i' MOD k\/ ~(i' MOD k <= SUC i' MOD k)`)
386 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
387 THEN POP_ASSUM MP_TAC
389 THEN ASM_REWRITE_TAC[];
393 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`i'`;`k`]
394 THEN POP_ASSUM MP_TAC
395 THEN REMOVE_ASSUM_TAC
397 THEN ASM_REWRITE_TAC[];
399 MP_TAC(ARITH_RULE`i' MOD k <= SUC i' MOD k\/ ~(i' MOD k <= SUC i' MOD k)`)
405 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`i'`;`k`]
406 THEN POP_ASSUM MP_TAC
408 THEN ASM_REWRITE_TAC[];
412 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
413 THEN POP_ASSUM MP_TAC
414 THEN REMOVE_ASSUM_TAC
416 THEN ASM_REWRITE_TAC[]]);;
424 scs_diag (scs_k_v39 s) i j /\
425 scs_a_v39 s i j <= cstab ==>
426 is_scs_v39 (scs_stab_diag_v39 s i j) /\ scs_basic_v39 (scs_stab_diag_v39 s i j)
430 let YRTAFYH= prove_by_refinement(YRTAFYH_concl,
434 THEN MP_TAC PROPERTY_OF_K_SCS
439 THEN POP_ASSUM(fun th-> MP_TAC th THEN ASSUME_TAC(th))
440 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;scs_stab_diag_v39;is_scs_v39;scs_v39_explicit;mk_unadorned_v39;scs_basic;periodic;periodic2]
442 THEN ABBREV_TAC`k= scs_k_v39 s`;
452 ASM_SIMP_TAC[PSORT_PERIODIC];
454 ASM_SIMP_TAC[PSORT_PERIODIC];
456 ASM_SIMP_TAC[PSORT_PERIODIC];
458 ASM_SIMP_TAC[PSORT_PERIODIC];
460 ASM_SIMP_TAC[Terminal.psort_sym];
464 MP_TAC(SET_RULE`psort k (i,j) = psort k (i',j') \/ ~(psort k (i,j) = psort k (i',j'))`)
467 MRESAL_TAC A_EQ_PSORT[`i'`;`j'`;`s`;`i`;`j`][];
469 THAYTHE_TAC (30-21)[`i'`;`j'`]
475 MP_TAC(SET_RULE`psort k (i,j) = psort k (i',j') \/ ~(psort k (i,j) = psort k (i',j'))`)
479 MP_TAC(SET_RULE`psort 3 (i,j) = psort 3 (i',SUC i') \/ ~(psort 3 (i,j) = psort 3 (i', SUC i'))`)
485 MATCH_DICH_TAC (31-24)
486 THEN ASM_REWRITE_TAC[];
488 MP_TAC(SET_RULE`psort k (i,j) = psort k (i',SUC i') \/ ~(psort k (i,j) = psort k (i', SUC i'))`)
493 MP_TAC DIAG_NOT_PSORT
496 REWRITE_TAC[scs_basic;scs_stab_diag_v39;LET_DEF;LET_END_DEF;unadorned_v39;mk_unadorned_v39;scs_v39_explicit]]);;
500 let STAB_IS_SCS=prove(`!s i j.
504 scs_diag (scs_k_v39 s) i j /\
505 scs_a_v39 s i j <= cstab ==>
506 is_scs_v39 (scs_stab_diag_v39 s i j) `,
514 let check_completeness_claimA_concl =
515 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)