text_formalization/usr/thales/hales_tactic.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Author: Thomas C. Hales                                                    *)
   4 (* Date: 2011-06-18                                                           *)
   5 (* ========================================================================== *)
   6
   7
   8 (* Tactics.   *)
   9
  10 module Hales_tactic = struct
  11
  12
  13
  14 let unlist tac t = tac [t];;
  15
  16 let kill th = ALL_TAC;;
  17
  18 (* moved to strictbuild.hl.
  19 let dest_goal gl = gl;;
  20
  21 let goal_asms = fst;;
  22
  23 let goal_concl = snd;;
  24
  25 let mk_goal(asl,w) = (asl,w);;
  26
  27
  28 *)
  29
  30 let LET_THM = CONJ LET_DEF LET_END_DEF;;
  31
  32 let UNDISCH2 = repeat UNDISCH;;
  33
  34 let COMBINE_TAC ttac1 ttac2 = (fun t -> ttac1 t THEN ttac2 t);;
  35
  36 let ASM_TAC=REPEAT(POP_ASSUM MP_TAC);;
  37
  38 let RED_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC;;
  39
  40 let RES_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC;;
  41
  42 let REDA_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];;
  43
  44 let RESA_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[];;
  45
  46 let REDAL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN DISCH_TAC THEN ASM_REWRITE_TAC th;;
  47
  48 let RESAL_TAC (th: thm list) = ASM_REWRITE_TAC th THEN STRIP_TAC THEN ASM_REWRITE_TAC th;;
  49
  50 (*
  51 let REMOVE_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[]);;
  52 let SYM_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]);;
  53 *)
  54
  55 let REMOVE_ASSUM_TAC=POP_ASSUM kill THEN REWRITE_TAC[];;
  56
  57 let SYM_ASSUM_TAC=POP_ASSUM((unlist REWRITE_TAC) o SYM);;
  58
  59 let SYM_ASSUM1_TAC=POP_ASSUM(COMBINE_TAC ((unlist REWRITE_TAC) o SYM ) ASSUME_TAC);;
  60
  61 let RESP_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(unlist REWRITE_TAC);;
  62
  63 let RESPL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN STRIP_TAC THEN POP_ASSUM(unlist REWRITE_TAC);;
  64
  65 let REDUCE_ARITH_TAC=REWRITE_TAC[REAL_ARITH`&0 * a= &0`; REAL_ARITH`a * &0 = &0`; REAL_ARITH`a + &0 = a`;
  66 REAL_ARITH`a- &0 =a`;REAL_ARITH`&0 +a =a`;REAL_ARITH`&1 * a =a`;REAL_ARITH`a * &1 =a`;REAL_ARITH`(A+B)-B=A`];;
  67
  68 let REDUCE_VECTOR_TAC=REWRITE_TAC[VECTOR_ARITH`&0 % a= vec 0`; VECTOR_ARITH`a % vec 0= vec 0`;VECTOR_ARITH`a + vec 0 = a`; VECTOR_ARITH`vec 0 +a =a`; VECTOR_ARITH`a- vec 0 =a`;VECTOR_ARITH`&1 % a =a`;VECTOR_ARITH`a- b =vec 0<=> a=b`];;
  69
  70 let MRESA_TAC th1 (th: term list) = MP_TAC(ISPECL th th1) THEN RESA_TAC;;
  71
  72 let MRESA1_TAC th1 th = MP_TAC(ISPEC th th1) THEN RESA_TAC;;
  73
  74 let MRESAL_TAC th1 (th: term list) (th2: thm list) =MP_TAC(ISPECL th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;
  75
  76 let MRESAL1_TAC th1 th (th2: thm list) =MP_TAC(ISPEC th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;
  77
  78 let ASM_SET_TAC l =
  79     (TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;
  80
  81
  82 (* GSYM theorems explicit *)
  83
  84 let GSYM_EXISTS_PAIRED_THM = GSYM EXISTS_PAIRED_THM;;
  85
  86 let has_stv t =
  87   let typ = (type_vars_in_term t) in
  88   can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
  89
  90 let frees_of_goal gl =
  91   let (asl,w) = dest_goal gl in
  92   let tms = w::(map (concl o snd) asl)  in
  93   let varl = List.flatten (map frees tms) in
  94     map (fun t -> (fst (dest_var t), t)) varl;;
  95
  96 (*
  97 let retype gls tm =
  98   let varl = filter has_stv (setify(frees tm)) in
  99   let svarl = map (fun t-> (fst(dest_var t),t)) varl in
 100   let fn = fun buff (s,t) -> try (let (_,_,m)= term_match [] t (assoc s gls) in m @ buff)
 101   with _ -> failwith ("not found: "^s) in
 102   let tyassoc = List.fold_left fn [] svarl in
 103      (instantiate ([],[],tyassoc)) tm ;;
 104 *)
 105
 106 (* new version 2013-07-13. Doesn't allow any new free variables, even if type inference works *)
 107
 108 let retype gls tm =
 109   let allv = setify(frees tm) in
 110   let varl = filter has_stv allv in
 111   let svarl = map (fun t-> (fst(dest_var t),t)) varl in
 112   let fn = fun buff (s,t) -> try (let (_,_,m)= term_match [] t (assoc s gls) in m @ buff)
 113   with _ -> failwith ("not found: "^s) in
 114   let tyassoc = List.fold_left fn [] svarl in
 115   let tm' = (instantiate ([],[],tyassoc)) tm in
 116   let glt = map snd gls in
 117   let _ = map (fun x -> mem x glt or failwith ("not found: "^ fst (dest_var x))) (setify (frees tm')) in
 118     tm';;
 119
 120 let env gl tm =
 121   let gls = frees_of_goal gl in
 122     retype gls tm;;
 123
 124 let envl gl tml =
 125   let gls = frees_of_goal gl in
 126   let varl = filter has_stv (setify (List.flatten(map frees tml))) in
 127   let svarl = setify(map (fun t-> (fst(dest_var t),t)) varl) in
 128   let fn = fun buff (s,t) -> try (let (_,_,m)= term_match [] t (assoc s gls) in m @ buff)
 129   with _ -> failwith ("not found: "^s) in
 130   let tyassoc = List.fold_left fn [] svarl in
 131      map (instantiate ([],[],tyassoc)) tml ;;
 132
 133 let gtyp (ttac:term->tactic) tm gl = ttac (env gl tm) gl;;
 134
 135 let gtypl (ttacl:term list -> tactic) tml gl =
 136    ttacl (map (env gl) tml) gl;;
 137
 138 let GEXISTS_TAC = gtyp EXISTS_TAC;;
 139
 140 let GSUBGOAL_THEN t ttac gl = SUBGOAL_THEN (env gl t) ttac gl;;
 141
 142 let argthen ttac tac t = (ttac t) THEN tac;;
 143
 144 let CONJ2_TAC = let t = (TAUT `a /\ b ==> b /\ a`) in MATCH_MP_TAC t THEN CONJ_TAC;;
 145
 146 let GEXISTL_TAC tl = EVERY (map GEXISTS_TAC tl);;
 147
 148 (* ========================================================================== *)
 149 (* TACTIC                                              *)
 150
 151 let FORCE_EQ = REPEAT (CHANGED_TAC (AP_TERM_TAC ORELSE AP_THM_TAC ORELSE BINOP_TAC)) ;;
 152
 153 let FORCE_MATCH = (MATCH_MP_TAC (TAUT `(a = b) ==> (a ==> b)`)) THEN FORCE_EQ ;;
 154
 155 let FORCE_MATCH_MP_TAC th =
 156   MP_TAC th THEN ANTS_TAC THENL[ALL_TAC;FORCE_MATCH
 157       ];;
 158
 159 let HYP_CONJ_TAC =
 160   let th = TAUT `(a ==> b==> c) ==> (a /\ b ==> c)`  in
 161     FIRST_X_ASSUM (fun t-> MP_TAC t THEN MATCH_MP_TAC th THEN DISCH_TAC THEN DISCH_TAC);;
 162
 163 (* ******************************
 164 UNSORTED
 165 ****************************** *)
 166
 167 let SELECT_EXIST = prove_by_refinement(
 168   `!(P:A->bool) Q. (?y. P y) /\ (!t. (P t ==> Q t)) ==> Q ((@) P)`,
 169   (* {{{ proof *)
 170
 171   [
 172   REPEAT STRIP_TAC;
 173   ASSUME_TAC (ISPECL[`P:(A->bool)`;`y:A`] SELECT_AX);
 174   ASM_MESON_TAC[];
 175   ]);;
 176
 177   (* }}} *)
 178
 179 let SELECT_THM = MESON[SELECT_EXIST]
 180   `!(P:A->bool) Q. (((?y. P y) ==> (!t. (P t ==> Q t))) /\ ((~(?y. P y)) ==>
 181      (!t. Q t))) ==> Q ((@) P)`;;
 182
 183 let SELECT_TAC  =
 184   let unbeta = prove(
 185   `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,MESON_TAC[]) in
 186   let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in
 187   unbeta_tac THEN (MATCH_MP_TAC SELECT_THM) THEN BETA_TAC THEN
 188   REPEAT STRIP_TAC;;
 189
 190 (*
 191 let SELECT_TAC = Tactics.SELECT_TAC;;
 192 *)
 193
 194 let COMMENT s = (report s; ALL_TAC);;
 195
 196 let NAME _ = ALL_TAC;;
 197
 198 let ROT_TAC =  (* permute conjuncts *)
 199   let     t1 = TAUT `b /\ a ==> a /\ b` in
 200   let t2 = TAUT `((b /\ c) /\ a) = (b /\ c /\ a)` in
 201     MATCH_MP_TAC t1 THEN PURE_REWRITE_TAC[t2];;
 202
 203 let ENOUGH_TO_SHOW_TAC t =
 204   let u = INST [(t,`A:bool`)] (TAUT ` ((A ==> B) /\ A) ==> B`) in
 205     MATCH_MP_TAC u THEN CONJ_TAC;;
 206
 207 (* like FIRST_X_ASSUM, except some subterm has to match t *)
 208
 209 let FIRST_X_ASSUM_ST t x =
 210   FIRST_X_ASSUM (fun u ->
 211     let _ = find_term (can(term_match[] t)) (concl u) in x u);;
 212
 213 let FIRST_ASSUM_ST t x =
 214   FIRST_ASSUM (fun u ->
 215     let _ = find_term (can(term_match[] t)) (concl u) in x u);;
 216
 217 let BURY_TAC t gl  =
 218   let n = List.length (goal_asms gl) in
 219     (REPEAT (FIRST_X_ASSUM MP_TAC) THEN ASSUME_TAC t THEN
 220       REPLICATE_TAC n DISCH_TAC) gl;;
 221
 222 let BURY_MP_TAC gl =
 223      (POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN
 224                        MAP_EVERY (fun (s,th) -> LABEL_TAC s (th))
 225                                  (rev (goal_asms gl))) gl;;
 226
 227 let GOAL_TERM ttac g = (ttac g) g;;
 228
 229 let TYPIFY t u = GOAL_TERM (fun w -> u (env w t));;
 230
 231 let TYPIFY_GOAL_THEN t u = TYPIFY t (C SUBGOAL_THEN u);;
 232
 233
 234 (* puts the hypotheses of a conditional rewrite as a conjunct, rather than
 235    trying to prove them
 236   thm should have the form a ==> (b = c)  or the form  a ==> b.
 237    Doesn't do matching on bound variables.
 238   *)
 239
 240 let GMATCH_SIMP_TAC thm gl =
 241   let w = goal_concl gl in
 242   let lift_eq_thm = MESON[]   `! a b c. (a ==> ((b:B) = c)) ==> (!P. a /\ P c ==> P b)` in
 243   let lift_eq t = GEN_ALL (MATCH_MP lift_eq_thm (SPEC_ALL t)) in
 244   let thm' = hd (mk_rewrites true thm []) in
 245   let t1 = fst (dest_eq(snd (dest_imp(concl(thm'))))) in
 246   let matcher u t =
 247     let m = term_match [] t1 t in
 248     let _ = subset (frees t) (frees u) or failwith "" in
 249       m in
 250   let w' = find_term (can (matcher w)) w in
 251   let var1 = mk_var("v",type_of w') in
 252   let vv = variant (frees w) var1 in
 253   let athm = REWRITE_CONV[ ASSUME (mk_eq (w',vv))] w in
 254   let bthm = (ISPECL [mk_abs(vv,rhs (concl athm));w'] BETA_THM) in
 255   let betx = SYM(TRANS bthm (BETA_CONV (rhs (concl bthm)))) in
 256    (ONCE_REWRITE_TAC[betx] THEN MATCH_MP_TAC (lift_eq thm') THEN
 257       BETA_TAC THEN REWRITE_TAC[]) gl;;
 258
 259
 260 (*
 261 let ASM_REAL_ARITH_TAC t =
 262   REPEAT (POP_ASSUM MP_TAC) THEN MP_TAC (itlist CONJ t TRUTH) THEN
 263     REAL_ARITH_TAC;;
 264
 265 let MP_LIST t = EVERY (map MP_TAC t);;
 266 *)
 267
 268
 269
 270 (* Gonthier's script organizational tactics. *)
 271
 272 let BY (t:tactic) gl =
 273   let (a,b,c)  = t gl in
 274   let _ = (b = []) or failwith "by failed to finish goal" in
 275     (a,b,c);;
 276
 277 let BRANCH_A (t::tl) = t THENL [EVERY tl;ALL_TAC];;
 278
 279 let BRANCH_B (t::tl) = t THENL [ALL_TAC;EVERY tl];;
 280
 281 (* a few from Jordan *)
 282
 283 let X_IN  = REWRITE_RULE[IN];;
 284
 285 let SUBCONJ_TAC =
 286   MATCH_MP_TAC (TAUT `A /\ (A ==>B) ==> (A /\ B)`) THEN CONJ_TAC;;
 287
 288 let SUBCONJ2_TAC =
 289   MATCH_MP_TAC (TAUT `B /\ (B ==>A) ==> (A /\ B)`) THEN CONJ_TAC;;
 290
 291 let nCONJ_TAC n gl =
 292   let w = goal_concl gl in
 293   let w' = rhs(concl(PURE_REWRITE_CONV[GSYM CONJ_ASSOC] w)) in
 294   let wn = List.nth (conjuncts w') n in
 295       (SUBGOAL_THEN wn ASSUME_TAC) gl;;
 296
 297 let PROOF_BY_CONTR_TAC =
 298   MATCH_MP_TAC (TAUT `(~A ==> F) ==> A`) THEN DISCH_TAC;;
 299
 300 let (UNDISCH_FIND_TAC: term -> tactic) =
 301  fun tm gl ->
 302    let asl = goal_asms gl in
 303    let p = can (term_match[] tm)  in
 304    try let sthm,_ = remove
 305      (fun (_,asm) -> can (find_term p) (concl ( asm))) asl in
 306      UNDISCH_TAC (concl (snd sthm)) gl
 307    with Failure _ -> failwith "UNDISCH_FIND_TAC";;
 308
 309 let rec type_set: (string*term) list  -> (term list*term) -> (term list*term)=
 310   fun typinfo (acclist,utm) -> match acclist with
 311     | [] -> (acclist,utm)
 312     | (Var(s,_) as a)::rest ->
 313          let a' = (assocd s typinfo a) in
 314            if (a = a') then type_set typinfo (rest,utm)
 315            else let inst = instantiate (term_match [] a a') in
 316              type_set typinfo ((map inst rest),inst utm)
 317     | _ -> failwith "type_set: variable expected"
 318   ;;
 319
 320 let has_stv t =
 321   let typ = (type_vars_in_term t) in
 322   can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
 323
 324
 325 let TYPE_THEN: term  -> (term -> tactic) -> tactic =
 326   fun t (tac:term->tactic) gl ->
 327     let (asl,w) = dest_goal gl in
 328     let avoids = itlist (union o frees o concl o snd) asl
 329       (frees w) in
 330     let strip  = fun t-> (match t with
 331                             |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in
 332     let typinfo = map strip avoids in
 333     let t' = (snd (type_set typinfo ((frees t),t))) in
 334       (warn ((has_stv t')) "TYPE_THEN: unresolved type variables");
 335       tac t' gl;;
 336
 337 (* this version must take variables *)
 338
 339 let TYPEL_THEN: term list -> (term list -> tactic) -> tactic =
 340   fun t (tac:term list->tactic) gl ->
 341     let (asl,w) = dest_goal gl in
 342   let avoids = itlist (union o frees o concl o snd) asl
 343                                (frees w) in
 344   let strip  = fun t-> (match t with
 345        |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in
 346   let typinfo = map strip avoids in
 347   let t' = map (fun u -> snd (type_set typinfo ((frees u),u))) t in
 348     (warn ((can (find has_stv) t')) "TYPEL_THEN: unresolved type vars");
 349      tac t' gl;;
 350
 351 let (EXISTSv_TAC :string -> tactic) =
 352    fun s gl ->
 353      let (v,_) = dest_binder "?" (goal_concl gl) in
 354      let (_,ty) = dest_var v in
 355        EXISTS_TAC (mk_var(s,ty)) gl;;
 356
 357 let (X_GENv_TAC:string ->tactic) =
 358    fun s gl  ->
 359      let (v,_) = dest_binder "!" (goal_concl gl) in
 360      let (_,ty) = dest_var v in
 361        X_GEN_TAC (mk_var(s,ty)) gl;;
 362
 363 (* weak version doesn't do conj *)
 364
 365 let (WEAK_STRIP_TAC: tactic) =
 366   fun gl ->
 367     try (fun ttac -> FIRST [GEN_TAC; DISCH_THEN ttac]) STRIP_ASSUME_TAC gl
 368     with Failure _ -> failwith "STRIP_TAC";;
 369
 370 let WEAK_STRIP_THM_THEN =
 371   FIRST_TCL [CONJUNCTS_THEN; CHOOSE_THEN];;
 372
 373 let WEAK_STRIP_ASSUME_TAC =
 374   let DISCARD_TAC th =
 375     let tm = concl th in
 376     fun gl ->
 377        if exists (fun a -> aconv tm (concl(snd a))) (goal_asms gl) then ALL_TAC gl
 378        else failwith "DISCARD_TAC: not already present" in
 379   (REPEAT_TCL WEAK_STRIP_THM_THEN)
 380   (fun gth -> FIRST [CONTR_TAC gth; ACCEPT_TAC gth;
 381                      DISCARD_TAC gth; ASSUME_TAC gth]);;
 382
 383 let (WEAKER_STRIP_TAC: tactic) =
 384   fun gl ->
 385     try (fun ttac -> FIRST [GEN_TAC; DISCH_THEN ttac]) WEAK_STRIP_ASSUME_TAC gl
 386     with Failure _ -> failwith "STRIP_TAC";;
 387
 388 let hold_def = new_definition `(hold:A->A) = I`;;
 389
 390 let hold = MATCH_MP_TAC (prove_by_refinement(
 391   `!a. hold a ==> a`,  [REWRITE_TAC [hold_def;I_DEF]  ]));;
 392
 393 let unhold = MATCH_MP_TAC (prove_by_refinement(
 394   `!a. a ==> hold a`,  [REWRITE_TAC [hold_def;I_DEF]  ]));;
 395
 396 let MP_ASM_THEN =
 397   fun tac -> hold THEN
 398     (REPEAT (POP_ASSUM MP_TAC)) THEN
 399     tac THEN REPEAT DISCH_TAC
 400     THEN unhold;;
 401
 402 let FULL_EXPAND_TAC s = FIRST_ASSUM (fun t ->
 403   let _ = (s = fst(dest_var(rhs(concl t)))) or failwith "" in
 404     (MP_ASM_THEN (SUBST1_TAC (SYM t) THEN BETA_TAC)));;
 405
 406 (*
 407 let RENAME_VAR (t,s) = (* rename free variable *)
 408     let svar = mk_var (s,snd(dest_var t)) in
 409     MP_ASM_THEN (SPEC_TAC (t,s) THEN X_GENv_TAC s);;
 410 *)
 411 let RENAME_FREE_VAR (t,s) = (* rename free variable *)
 412     MP_ASM_THEN (SPEC_TAC (t,t) THEN X_GENv_TAC s);;
 413
 414 (* rebind bound variables *)
 415
 416 let rec rec_alpha_at (t,s) tm = match tm with
 417   | Comb (u,v) -> mk_comb (rec_alpha_at (t,s) u,rec_alpha_at (t,s) v)
 418   | Abs (a,b)  -> if (a=t) then alpha s tm else mk_abs(a,rec_alpha_at (t,s) b)
 419   | _ -> tm;;
 420
 421 let alpha_at (t,s) =
 422   rec_alpha_at (t,mk_var(s,snd(dest_var t)));;
 423
 424 let REBIND_CONV ts g = ALPHA g (alpha_at ts g);;
 425
 426 REBIND_CONV (`x:real`,"y") (`pi + (\ x . x + pi) pi`);;
 427
 428 let REBIND_RULE ts th1 = EQ_MP (REBIND_CONV ts (concl th1)) th1;;
 429
 430 REBIND_RULE (`x:real`,"y") (ASSUME (`pi + (\ x . x + pi) pi = &1`));;
 431
 432 let REBIND_TAC ts gl = (SUBST1_TAC (REBIND_CONV ts (goal_concl gl))) gl;;
 433
 434 (* MISCELL. *)
 435
 436 let arith tm  =
 437   let v = [ARITH_RULE;REAL_ARITH;(fun t -> prove(t,SIMPLE_COMPLEX_ARITH_TAC));REAL_RING;VECTOR_ARITH] in
 438     tryfind (fun h -> h tm) v;;
 439
 440 let varith = VECTOR_ARITH;;
 441
 442 let COMMENT _ = ALL_TAC;;
 443
 444 let INTRO_TAC th1 tml =
 445    GOAL_TERM (fun w -> (MP_TAC (ISPECL ( envl w tml) th1)));;
 446
 447   let COPY_TAC = DISCH_THEN (fun t -> MP_TAC t THEN ASSUME_TAC t);;
 448
 449   let TYPED_ABBREV_TAC t gl =
 450     let (a,b) = dest_eq t in
 451     let b' = env gl b in
 452     let (a',_) = dest_var a in
 453     let t' =   mk_eq(mk_var(a',type_of b'),b')
 454     in ABBREV_TAC t' gl;;
 455
 456
 457
 458 end;;