development/thales/session/experiment_.hl

   1
   2 (*
   3
   4
   5 The main thing that works well is the expanded SIMP_TAC, with custom local constants.
   6 To do:
   7   rehash local simp tac when new theorems are added, rather than have it rebuild with each call.
   8
   9
  10 sectioning is
  11
  12 *)
  13
  14 (* experiments in revising proof style *)
  15
  16 open Basics;;
  17
  18 let section_stack  = ref [];;
  19
  20 let context = ref [];;
  21
  22 let assumption_list = ref [];;
  23
  24 let begin_section (s:string) =
  25   section_stack := s:: !section_stack;;
  26
  27 let get_section() = hd (!section_stack);;
  28
  29 let end_section (s:string) =
  30   let s1 = hd(!section_stack) in
  31   let _ = (s1 = s) or failwith "section" in
  32   let _ = section_stack := tl !section_stack in
  33   let _ = context := filter (fun (s1,_) -> not(s1 = s)) !context in
  34     ();;
  35
  36 let declare t =
  37   let _ = context := setify ((get_section(),t) :: !context) in
  38    !context;;
  39
  40
  41 (* from Hales_tactic *)
  42
  43 let retype gls tm =
  44   let varl = filter has_stv (setify(frees tm)) in
  45   let svarl = map (fun t-> (fst(dest_var t),t)) varl in
  46   let fn = fun buff (s,t) -> try (let (_,_,m)= term_match [] t (assoc s gls) in m @ buff)
  47   with _ -> failwith ("not found: "^s) in
  48   let tyassoc = List.fold_left fn [] svarl in
  49      (instantiate ([],[],tyassoc)) tm ;;
  50
  51 let get_env () =
  52     map (fun (_,t) -> (fst (dest_var t),t)) !context;;
  53
  54 let declare_as (v,t) =
  55   let v1 = mk_var(v,mk_vartype("?1")) in
  56   let t1 = map (fun t -> (fst (dest_var t),t)) (frees t) in
  57     declare (retype (t1 @ (get_env())) v1);;
  58
  59 let mk_assumption (s,t) = assumption_list := (get_section(),s,retype (get_env()) t) :: !assumption_list;;
  60
  61 begin_section "stuff";;
  62
  63 declare_as ("V",`packing V`);;
  64
  65 declare `u0:real^3`;;
  66 declare `u1:real^3`;;
  67 declare `v1:real^3`;;
  68 declare `v2:real^3`;;
  69
  70 mk_assumption ("pV",`packing V`);;
  71 mk_assumption ("sV",`saturated V`);;
  72
  73 (* Augment simplification theorems. *)
  74
  75
  76 let simp_thm_list = ref [];;
  77 let add_simp_thm q = simp_thm_list := q::!simp_thm_list;;
  78 let get_simp_thms () = (!simp_thm_list);;
  79
  80
  81 let local_net_of_thm locals rep th =
  82   let tm = concl th in
  83   let lconsts = setify (union locals (freesl (hyp th))) in
  84   let matchable = can o term_match lconsts in
  85   match tm with
  86     Comb(Comb(Const("=",_),(Abs(x,Comb(Var(s,ty) as v,x')) as l)),v')
  87          when x' = x & v' = v & not(x = v) ->
  88         let conv tm =
  89           match tm with
  90             Abs(y,Comb(t,y')) when y = y' & not(free_in y t) ->
  91               INSTANTIATE(term_match [] v t) th
  92           | _ -> failwith "REWR_CONV (ETA_AX special case)" in
  93         enter lconsts (l,(1,conv))
  94   | Comb(Comb(Const("=",_),l),r) ->
  95       if rep & free_in l r then
  96         let th' = EQT_INTRO th in
  97         enter lconsts (l,(1,REWR_CONV th'))
  98       else if rep & matchable l r & matchable r l then
  99         enter lconsts (l,(1,ORDERED_REWR_CONV term_order th))
 100       else enter lconsts (l,(1,REWR_CONV th))
 101   | Comb(Comb(_,t),Comb(Comb(Const("=",_),l),r)) ->
 102         if rep & free_in l r then
 103           let th' = DISCH t (EQT_INTRO(UNDISCH th)) in
 104           enter lconsts (l,(3,IMP_REWR_CONV th'))
 105         else if rep & matchable l r & matchable r l then
 106           enter lconsts (l,(3,ORDERED_IMP_REWR_CONV term_order th))
 107         else enter lconsts(l,(3,IMP_REWR_CONV th));;
 108
 109 help_grep "strip";;
 110
 111 (* ex local var *)
 112
 113 let post_rewrite =
 114   let ex_local v thm =
 115     EXISTS (mk_exists(v, (concl thm)),v) thm in
 116   let ex_shared v thm =
 117     let a4 = ASSUME (mk_exists (v,hd(hyp thm))) in
 118     let a5 = EXISTS (concl a4,v) thm in
 119       CHOOSE (v,a4) a5 in
 120   let ex_comb local v thm = if (mem v local) then ex_local v thm else ex_shared v thm in
 121     fun locals th ->
 122       if (not (is_imp (concl th))) then th else
 123         let (p,q) = dest_imp (concl th) in
 124         let (evs,p') = strip_exists p in
 125         let a1 = ASSUME p' in
 126         let a2 = List.fold_right (ex_comb locals) evs a1 in
 127         let a3 = DISCH_ALL a2 in
 128           IMP_TRANS a3 th;;
 129
 130 (*
 131 let ex_local v thm =
 132   EXISTS (mk_exists(v, (concl thm)),v) thm;;
 133 let ex_shared v thm =
 134   let a4 = ASSUME (mk_exists (v,hd(hyp thm))) in
 135   let a5 = EXISTS (concl a4,v) thm in
 136     CHOOSE (v,a4) a5;;
 137 let ex_comb local v thm = if (mem v local) then ex_local v thm else ex_shared v thm;;
 138
 139 let a0 = hd(mk_rewrites true LEAF_SQRT2 []);;
 140 post_rewrite [x] a0;;
 141
 142 a2;;
 143 ex_shared x a2;;
 144 ex_local v (ex_shared x a2);;
 145
 146 let a0 = snd(post_rewrite [`V:real^3->bool`] (hd(mk_rewrites true LEAF_SQRT2 [])));;
 147 let v = `V:real^3->bool`;;
 148 let a1 = fst (EQ_IMP_RULE (REFL a0));;
 149 let a2 = UNDISCH a1;;
 150 let a3 = EXISTS (mk_exists(v, (concl a2)),v) a2;;
 151 (* shared var *)
 152 let x = `ul:(real^3)list`;;
 153 let a4 = ASSUME (mk_exists(x, a0));;
 154 let a5 = EXISTS (concl a4,x) a2;;
 155 let a6 = CHOOSE(x,a4) a5;;
 156
 157 add_simp_thm LEAF_SQRT2;;
 158 mk_rewrites true LEAF_SQRT2 [];;
 159 add_simp_thm (hd(mk_rewrites true (UNDISCH (SPEC_ALL LEAF_SQRT2)) []));;
 160
 161 get_simp_thms();;
 162
 163   (hd (hyp a2)) a2
 164     let evs'= subtract evs locals in
 165     let p'' = list_mk_exists (evs',p') in
 166    let p''p = (p''-> p) in
 167       IMP_TRANS p''p th;; *)
 168
 169
 170 let mk_local_rewrites locals thm sofar =
 171   let rw = mk_rewrites true thm [] in
 172     (map (post_rewrite locals) rw @ sofar);;
 173
 174 let local_basic_ss =
 175   fun thl ->
 176     let local = map snd !context in
 177     let rewmaker = mk_local_rewrites local in
 178     let cthms = itlist rewmaker thl [] in
 179     let net' = itlist (local_net_of_thm local true) cthms (basic_net()) in
 180     let net'' = itlist net_of_cong (basic_congs()) net' in
 181   Simpset(net'',basic_prover,[],rewmaker);;
 182
 183 simp_thm_list;;
 184
 185 let LOCAL_SIMPLIFY_CONV ss = GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV ss 8;;
 186 let LOCAL_SIMP_CONV thl = LOCAL_SIMPLIFY_CONV (local_basic_ss []) ((get_simp_thms()) @ thl);;
 187 let LOCAL_SIMP_RULE thl = CONV_RULE(LOCAL_SIMP_CONV thl);;
 188 let LOCAL_SIMP_TAC thl = CONV_TAC(LOCAL_SIMP_CONV thl);;
 189 let LOCAL_ASM_SIMP_TAC = ASM LOCAL_SIMP_TAC;;
 190 let LOCAL_STEP_TAC () = RULE_ASSUM_TAC (LOCAL_SIMP_RULE (get_simp_thms())) THEN LOCAL_ASM_SIMP_TAC (get_simp_thms());;
 191
 192
 193 (* GENERAL TACTIC KEYED TO TERMS *)
 194
 195
 196 let act_list = ref [];;
 197 let add_actionl p q = act_list := (p,q):: !act_list;;
 198 let add_action  = unlist add_actionl;;
 199
 200
 201 let matchable s t = can(term_match[] s) t;;
 202 let some_matchable s tl = exists (matchable s) tl;;
 203 let all_matchable sl tl = forall (fun s -> some_matchable s tl) sl;;
 204
 205 let actl pl =
 206   let pl = map (retype (get_env())) pl in
 207   let r = filter (fun (tl,_) -> all_matchable pl tl) !act_list in
 208   let _ = (List.length r > 0) or failwith "act -- no match" in
 209     snd(hd r);;
 210
 211 let act = unlist actl;;
 212
 213 let whatl patl =
 214   let patl = map (retype (get_env())) patl in
 215   let matcher u pat = can (find_term (can (term_match[] pat))) (concl u) in
 216   let matches = filter (fun (_,u) -> forall (matcher u) patl) (!thm_list) in
 217     matches;;
 218
 219 let getl patl =
 220   let w = whatl patl in
 221   let _ = List.length w > 0 or failwith "no patterns" in
 222     hd (map snd w);;
 223
 224 let get = unlist getl;;
 225
 226 add_action `&0 < sqrt x` (GMATCH_SIMP_TAC SQRT_POS_LT);;
 227 add_action `&0 <= sqrt x` (GMATCH_SIMP_TAC SQRT_POS_LE);;
 228 add_action `sqrt x <= sqrt y` (GMATCH_SIMP_TAC SQRT_MONO_LE_EQ);;
 229 add_action `sqrt x < sqrt y` (GMATCH_SIMP_TAC SQRT_MONO_LT_EQ);;
 230 add_action `&0 < x * y` (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);;
 231 add_action `x * x <= y * y` (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE);;
 232 add_action `&0 <= x/y` (GMATCH_SIMP_TAC REAL_LE_DIV);;
 233 add_action `&0 <= x * y` (GMATCH_SIMP_TAC REAL_LE_MUL);;
 234 add_action `&0 <= x * x` (REWRITE_TAC[ REAL_LE_SQUARE]);;
 235 add_action `&0 <= x pow 2` (REWRITE_TAC[ REAL_LE_POW_2]);;
 236 add_action `sqrt x pow 2` (GMATCH_SIMP_TAC SQRT_POW_2);;
 237 add_action `x /z <= y` (GMATCH_SIMP_TAC REAL_LE_LDIV_EQ);;
 238 add_action `&0 <= x pow 2` (REWRITE_TAC[ REAL_LE_POW_2]);;
 239 add_action `x < sqrt y` (GMATCH_SIMP_TAC REAL_LT_RSQRT);;
 240 add_action `x /z <= y/ z` (GMATCH_SIMP_TAC REAL_LE_DIV2_EQ);;
 241 add_action `sqrt(y*y)` (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);;
 242 add_action `x * y <= x * z` (GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP);;
 243 add_action `x < y/ z` (GMATCH_SIMP_TAC REAL_LT_RDIV_EQ);;
 244 add_action `&0 < x/y` (GMATCH_SIMP_TAC REAL_LT_DIV);;
 245 add_action `sqrt x * sqrt y` (GMATCH_SIMP_TAC (GSYM SQRT_MUL));;
 246 add_action `x * x < y * y` (GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE);;
 247 add_action `x * y < x * z` (GMATCH_SIMP_TAC REAL_LT_LMUL_EQ);;
 248 add_action `x <= y/z` (GMATCH_SIMP_TAC REAL_LE_RDIV_EQ);;
 249 add_action `inv y <= inv x` (GMATCH_SIMP_TAC REAL_LE_INV2);;
 250 add_action `&0 < inv x` (GMATCH_SIMP_TAC REAL_LT_INV);;
 251
 252 add_thm `(x:A) IN {}` NOT_IN_EMPTY;;
 253 add_thm `&x < &y`( REAL_OF_NUM_LT);;
 254 add_thm `&x <= &y`( REAL_OF_NUM_LE);;
 255 add_thm `&0 <= inv x`(REAL_LE_INV_EQ);;
 256 add_thm `&0 < inv x`(REAL_LT_INV_EQ);;
 257 add_thm `abs(a*b)`(REAL_ABS_MUL);;
 258 add_thm `inv (&0) = &0` REAL_INV_0;;
 259 add_thm `hl [u0:real^A; u1]` Marchal_cells_3.HL_2;;
 260
 261 add_thm `~(n = 0)` (ARITH_RULE `1 < n ==> ~(n = 0)`);;
 262
 263 get `a \/ b`;;
 264 getl [`a:bool`;`inv (&0)`];;
 265 get `hl [u0;u1]`;;
 266 get `~(t = 0)`;;
 267 !thm_list;;
 268 get `int_of_num`;;
 269
 270
 271
 272 (* auto matches pattern anywhere and does a sub1 repeatedly at the end of each proof step *)
 273
 274
 275 let LIST_PROPS = map (fun t -> prove_by_refinement(t,[ BY(REWRITE_TAC[Bump.EL_EXPLICIT;set_of_list;LENGTH])]))
 276   [
 277  `!(x:A) y. EL 0 (CONS (x:A) y) = x`;
 278   `!(x:A) y. EL 1 (CONS (x:A) y) = EL 0 y`;
 279   `!(x:A) y. EL 2 (CONS (x:A) y) = EL 1 y`;
 280   `!(x:A) y. EL 3 (CONS (x:A) y) = EL 2 y`;
 281   `!(x:A) y. set_of_list (CONS x y) = x INSERT (set_of_list y)`;
 282   `set_of_list ([]:(A)list) = {}`;
 283   `LENGTH ([]:(A)list) = 0`;
 284   `!x y. LENGTH (CONS (x:A) y) = SUC (LENGTH y)`
 285   ];;
 286
 287 map add_simp_thm LIST_PROPS;;
 288
 289 map add_simp_thm
 290   [
 291     INITIAL_SUBLIST_CONS;
 292     INITIAL_SUBLIST_NIL;
 293     TRUNCATE_SIMPLEX0;
 294     LENGTH_TRUNCATE_SIMPLEX;
 295     TRUNCATE_SIMPLEX_CONS;
 296     CONS_11;
 297     TRUNCATE_SIMPLEX_EXPLICIT;
 298   ];;
 299
 300 let XIN_BARV = prove_by_refinement(
 301   `!V u k. u IN barV V k <=> barV V k u`,
 302   (* {{{ proof *)
 303   [
 304 BY(REWRITE_TAC[IN])
 305   ]);;
 306   (* }}} *)
 307
 308 add_simp_thm XIN_BARV;;
 309
 310 let LEAF_BARV = prove_by_refinement(
 311   `!V ul. leaf V ul ==> barV V 2 ul`,
 312   (* {{{ proof *)
 313   [
 314     BY(MESON_TAC[Leaf_cell.leaf;IN])
 315   ]);;
 316   (* }}} *)
 317
 318 add_simp_thm LEAF_BARV;;
 319
 320 add_simp_thm Sphere.sqrt2;;
 321
 322
 323 (* has variable in antecedent problem *)
 324
 325 let LEAF_SQRT2 = prove_by_refinement(
 326   `!V ul. leaf V ul ==> hl ul < sqrt(&2)`,
 327   (* {{{ proof *)
 328   [
 329     BY(MESON_TAC[Leaf_cell.leaf;IN;Sphere.sqrt2])
 330   ]);;
 331   (* }}} *)
 332
 333 (*
 334
 335 auto (`EL 0 (CONS (x:A) y)`,EL0_CONS);;
 336 auto (`EL 1 (CONS (x:A) y)`,EL1_CONS);;
 337 auto (`EL 2 (CONS (x:A) y)`,EL2_CONS);;
 338 auto (`EL 3 (CONS (x:A) y)`,EL3_CONS);;
 339 auto (`set_of_list (CONS (x:A) y)`,SET_OF_LIST_CONS);;
 340 auto (`set_of_list []`,SET_OF_LIST_EMPTY);;
 341 auto (`truncate_simplex 0 (CONS x y)`,
 342 auto (`truncate_simplex 1 (CONS x y)`,
 343 auto (`truncate_simplex 2 (CONS x y)`,
 344 auto (`truncate_simplex 3 (CONS x y)`,
 345 auto (`truncate_simplex 0 ul = [EL 0 ul]`,
 346 auto (`HD ul`)
 347 auto (`x IN barV V k`)
 348 assumption `saturated V`;;
 349
 350 *)
 351
 352 add_simp_thm (arith `1 < 2`);;
 353 add_simp_thm (LE_REFL);;
 354
 355 add_simp_thm Fan.th3a;;
 356
 357 let REUHADY = prove_by_refinement(
 358   `!V u0 u1 v1 v2.
 359     saturated V /\ packing V /\ leaf V [u0;u1;v1] /\ leaf V [u0;u1;v2] /\
 360     ~(v1 =v2)  ==>
 361    sum {X | mcell_set V X /\ {u0,u1} IN edgeX V X /\ X SUBSET wedge_ge u0 u1 v1 v2}
 362              (\t. dihX V t (u0,u1)) = azim u0 u1 v1 v2`,
 363   (* {{{ proof *)
 364   [
 365   REPEAT WEAK_STRIP_TAC;
 366   MATCH_MP_TAC Reuhady.REUHADY1;
 367   GEXISTL_TAC [`[u0;u1;v1]`;`[u0;u1;v2]`];
 368   LOCAL_STEP_TAC();
 369   TYPIFY `hl [u0;u1] < sqrt(&2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
 370     INTRO_TAC Rogers.XNHPWAB4 [`V`;`[u0;u1;v1]`;`2`];
 371     LOCAL_STEP_TAC();
 372     DISCH_THEN (C INTRO_TAC [`1`;`2`]);
 373     LOCAL_STEP_TAC();
 374     TYPIFY `hl [u0;u1;v1] < sqrt (&2)` ENOUGH_TO_SHOW_TAC;
 375       BY(REAL_ARITH_TAC);
 376     BY(LOCAL_STEP_TAC());
 377   TYPIFY `~collinear (set_of_list [u0; u1; v1]) /\  ~collinear (set_of_list [u0; u1; v2])` (C SUBGOAL_THEN ASSUME_TAC);
 378     BY(ASM_MESON_TAC[Leaf_cell.GBEWYFX]);
 379   LOCAL_STEP_TAC();
 380   ASM_SIMP_TAC[Leaf_cell.WEDGE_GE_ALMOST_DISJOINT];
 381   TYPIFY `~(u0 = u1)` (C SUBGOAL_THEN ASSUME_TAC);
 382     BY(ASM_MESON_TAC[Collect_geom.NOT_COLLINEAR_IMP_2_UNEQUAL]);
 383   TYPIFY `u0 IN V /\ u1 IN V` (C SUBGOAL_THEN (unlist ASM_REWRITE_TAC));
 384     INTRO_TAC Packing3.BARV_SUBSET [`V`;`2`;`[u0;u1;v1]`];
 385     LOCAL_STEP_TAC();
 386     BY(SET_TAC[]);
 387   SUBCONJ_TAC;
 388     ASM_SIMP_TAC[Local_lemmas.AZIM_EQ_0_GE_ALT2];
 389     DISCH_TAC;
 390     INTRO_TAC Leaf_cell.FCHKUGT [`V`;`u0`;`u1`;`v1`;`v2`];
 391     LOCAL_STEP_TAC();
 392     REWRITE_TAC[Leaf_cell.cc_A0];
 393     LOCAL_STEP_TAC();
 394     MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
 395     ASM_REWRITE_TAC[];
 396     FIRST_X_ASSUM MP_TAC;
 397     GMATCH_SIMP_TAC Collect_geom.IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF;
 398     LOCAL_STEP_TAC();
 399     REWRITE_TAC[Collect_geom.aff];
 400     DISCH_THEN DISJ_CASES_TAC;
 401       BY(ASM_REWRITE_TAC[]);
 402     FIRST_X_ASSUM (MP_TAC o (MATCH_MP AFFINE_HULL_3_IMP_COLLINEAR));
 403     BY(ASM_MESON_TAC[]);
 404   DISCH_TAC;
 405   REPEAT WEAK_STRIP_TAC;
 406   MATCH_MP_TAC Leaf_cell.EWYBJUA;
 407   TYPIFY `V` EXISTS_TAC;
 408   BY(LOCAL_STEP_TAC())
 409   ]);;
 410   (* }}} *)
 411
 412 let LEAF_RANKING_LEMMA = prove_by_refinement(
 413   `!V ul w0 n.  0 < n /\ packing V /\ saturated V /\
 414     s_leaf V ul HAS_SIZE n /\
 415   ~collinear {EL 0 ul,EL 1 ul,w0} ==>
 416     (?f.  IMAGE f (:num) = s_leaf V ul /\
 417        (!i. f (i + n) = f i) /\
 418        (!i j. i < n /\ j < n /\ i < j ==> azim (EL 0 ul) (EL 1 ul) w0 (f i) < azim (EL 0 ul) (EL 1 ul) w0 (f j)))`,
 419   (* {{{ proof *)
 420   [
 421   REPEAT WEAK_STRIP_TAC;
 422   TYPIFY `(s:real^3->bool) = s_leaf V ul` TYPED_ABBREV_TAC;
 423   TYPIFY `!x. x IN s ==> ~(collinear {EL 0 ul,EL 1 ul,x})` (C SUBGOAL_THEN ASSUME_TAC);
 424     BY(ASM_MESON_TAC[s_leaf_collinear]);
 425   INTRO_TAC STRICT_SORT_FINITE [`\v w.  (azim (EL 0 ul) (EL 1 ul) w0 v <= azim (EL 0 ul) (EL 1 ul) w0 w)`;`s`;`n` ];
 426   BETA_TAC;
 427   ANTS_TAC;
 428     ASM_REWRITE_TAC[];
 429     CONJ2_TAC;
 430       BY(REAL_ARITH_TAC);
 431     REPEAT WEAK_STRIP_TAC;
 432     TYPIFY `azim (EL 0 ul) (EL 1 ul) w0 x = azim (EL 0 ul) (EL 1 ul) w0 y ==> (x = y)` ENOUGH_TO_SHOW_TAC;
 433       REPEAT WEAK_STRIP_TAC;
 434       FIRST_X_ASSUM MATCH_MP_TAC;
 435       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 436     DISCH_TAC;
 437     MATCH_MP_TAC Leaf_cell.FCHKUGT;
 438     GEXISTL_TAC [`V`;`EL 0 ul`;`EL 1 ul`];
 439     REWRITE_TAC[Leaf_cell.cc_A0];
 440     REWRITE_TAC[Bump.EL_EXPLICIT];
 441     FIRST_ASSUM (C INTRO_TAC [`x`]);
 442     FIRST_X_ASSUM (C INTRO_TAC [`y`]);
 443     ASM_REWRITE_TAC[];
 444     REPEAT WEAK_STRIP_TAC;
 445     FIRST_X_ASSUM_ST `azim` MP_TAC;
 446     ASM_SIMP_TAC[AZIM_EQ_ALT];
 447     BY(ASM_MESON_TAC[Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;s_leaf_leaf]);
 448   REPEAT WEAK_STRIP_TAC;
 449   TYPIFY `\i. f (SUC (i MOD n))` EXISTS_TAC;
 450   BETA_TAC;
 451   CONJ2_TAC;
 452     CONJ_TAC;
 453       REPEAT WEAK_STRIP_TAC;
 454       INTRO_TAC MOD_MULT_ADD [`1`;`n`;`i`];
 455       REWRITE_TAC[arith `1 * n + i = i + n`];
 456       DISCH_THEN SUBST1_TAC;
 457       BY(REWRITE_TAC[]);
 458     REPEAT WEAK_STRIP_TAC;
 459     ASM_SIMP_TAC[MOD_LT];
 460     FIRST_X_ASSUM (C INTRO_TAC [`SUC i`;`SUC j`]);
 461     REWRITE_TAC[arith `~(a <= b) <=> (b <a)`];
 462     DISCH_THEN MATCH_MP_TAC;
 463     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
 464   ASM_REWRITE_TAC[];
 465   REWRITE_TAC[EXTENSION;IMAGE;IN_ELIM_THM;IN_UNIV];
 466   GEN_TAC;
 467   MATCH_MP_TAC (TAUT `((a==> b) /\ (b ==> a)) ==> (a = b)`);
 468   CONJ_TAC;
 469     REPEAT WEAK_STRIP_TAC;
 470     TYPIFY `SUC (x' MOD n)` EXISTS_TAC;
 471     ASM_REWRITE_TAC[IN_NUMSEG];
 472     REWRITE_TAC[arith `1 <= SUC x`];
 473     REWRITE_TAC[arith `SUC x <= n <=> x < n`];
 474     BY(ASM_MESON_TAC[DIVISION;arith `~(n=0) <=> (0 < n)`]);
 475   REPEAT WEAK_STRIP_TAC;
 476   ASM_REWRITE_TAC[];
 477   TYPIFY `PRE x'` EXISTS_TAC;
 478   AP_TERM_TAC;
 479   TYPIFY `PRE x' MOD n = PRE x'` (C SUBGOAL_THEN SUBST1_TAC);
 480     MATCH_MP_TAC MOD_LT;
 481     FIRST_X_ASSUM_ST `IN` MP_TAC;
 482     REWRITE_TAC[IN_NUMSEG];
 483     BY(ARITH_TAC);
 484   FIRST_X_ASSUM_ST `IN` MP_TAC;
 485   REWRITE_TAC[IN_NUMSEG];
 486   BY(ARITH_TAC)
 487   ]);;
 488   (* }}} *)
 489