1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Author: Thomas C. Hales *)
5 (* ========================================================================== *)
10 module Hales_tactic = struct
14 let unlist tac t = tac [t];;
16 let kill th = ALL_TAC;;
18 (* moved to strictbuild.hl.
19 let dest_goal gl = gl;;
23 let goal_concl = snd;;
25 let mk_goal(asl,w) = (asl,w);;
30 let LET_THM = CONJ LET_DEF LET_END_DEF;;
32 let UNDISCH2 = repeat UNDISCH;;
34 let COMBINE_TAC ttac1 ttac2 = (fun t -> ttac1 t THEN ttac2 t);;
36 let ASM_TAC=REPEAT(POP_ASSUM MP_TAC);;
38 let RED_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC;;
40 let RES_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC;;
42 let REDA_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];;
44 let RESA_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[];;
46 let REDAL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN DISCH_TAC THEN ASM_REWRITE_TAC th;;
48 let RESAL_TAC (th: thm list) = ASM_REWRITE_TAC th THEN STRIP_TAC THEN ASM_REWRITE_TAC th;;
51 let REMOVE_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[]);;
52 let SYM_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]);;
55 let REMOVE_ASSUM_TAC=POP_ASSUM kill THEN REWRITE_TAC[];;
57 let SYM_ASSUM_TAC=POP_ASSUM((unlist REWRITE_TAC) o SYM);;
59 let SYM_ASSUM1_TAC=POP_ASSUM(COMBINE_TAC ((unlist REWRITE_TAC) o SYM ) ASSUME_TAC);;
61 let RESP_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(unlist REWRITE_TAC);;
63 let RESPL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN STRIP_TAC THEN POP_ASSUM(unlist REWRITE_TAC);;
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`];;
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`];;
70 let MRESA_TAC th1 (th: term list) = MP_TAC(ISPECL th th1) THEN RESA_TAC;;
72 let MRESA1_TAC th1 th = MP_TAC(ISPEC th th1) THEN RESA_TAC;;
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;;
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;;
79 (TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;
82 (* GSYM theorems explicit *)
84 let GSYM_EXISTS_PAIRED_THM = GSYM EXISTS_PAIRED_THM;;
87 let typ = (type_vars_in_term t) in
88 can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
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;;
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 ;;
106 (* new version 2013-07-13. Doesn't allow any new free variables, even if type inference works *)
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
121 let gls = frees_of_goal gl in
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 ;;
133 let gtyp (ttac:term->tactic) tm gl = ttac (env gl tm) gl;;
135 let gtypl (ttacl:term list -> tactic) tml gl =
136 ttacl (map (env gl) tml) gl;;
138 let GEXISTS_TAC = gtyp EXISTS_TAC;;
140 let GSUBGOAL_THEN t ttac gl = SUBGOAL_THEN (env gl t) ttac gl;;
142 let argthen ttac tac t = (ttac t) THEN tac;;
144 let CONJ2_TAC = let t = (TAUT `a /\ b ==> b /\ a`) in MATCH_MP_TAC t THEN CONJ_TAC;;
146 let GEXISTL_TAC tl = EVERY (map GEXISTS_TAC tl);;
148 (* ========================================================================== *)
151 let FORCE_EQ = REPEAT (CHANGED_TAC (AP_TERM_TAC ORELSE AP_THM_TAC ORELSE BINOP_TAC)) ;;
153 let FORCE_MATCH = (MATCH_MP_TAC (TAUT `(a = b) ==> (a ==> b)`)) THEN FORCE_EQ ;;
155 let FORCE_MATCH_MP_TAC th =
156 MP_TAC th THEN ANTS_TAC THENL[ALL_TAC;FORCE_MATCH
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);;
163 (* ******************************
165 ****************************** *)
167 let SELECT_EXIST = prove_by_refinement(
168 `!(P:A->bool) Q. (?y. P y) /\ (!t. (P t ==> Q t)) ==> Q ((@) P)`,
173 ASSUME_TAC (ISPECL[`P:(A->bool)`;`y:A`] SELECT_AX);
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)`;;
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
191 let SELECT_TAC = Tactics.SELECT_TAC;;
194 let COMMENT s = (report s; ALL_TAC);;
196 let NAME _ = ALL_TAC;;
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];;
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;;
207 (* like FIRST_X_ASSUM, except some subterm has to match t *)
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);;
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);;
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;;
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;;
227 let GOAL_TERM ttac g = (ttac g) g;;
229 let TYPIFY t u = GOAL_TERM (fun w -> u (env w t));;
231 let TYPIFY_GOAL_THEN t u = TYPIFY t (C SUBGOAL_THEN u);;
234 (* puts the hypotheses of a conditional rewrite as a conjunct, rather than
236 thm should have the form a ==> (b = c) or the form a ==> b.
237 Doesn't do matching on bound variables.
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
247 let m = term_match [] t1 t in
248 let _ = subset (frees t) (frees u) or failwith "" 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;;
261 let ASM_REAL_ARITH_TAC t =
262 REPEAT (POP_ASSUM MP_TAC) THEN MP_TAC (itlist CONJ t TRUTH) THEN
265 let MP_LIST t = EVERY (map MP_TAC t);;
270 (* Gonthier's script organizational tactics. *)
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
277 let BRANCH_A (t::tl) = t THENL [EVERY tl;ALL_TAC];;
279 let BRANCH_B (t::tl) = t THENL [ALL_TAC;EVERY tl];;
281 (* a few from Jordan *)
283 let X_IN = REWRITE_RULE[IN];;
286 MATCH_MP_TAC (TAUT `A /\ (A ==>B) ==> (A /\ B)`) THEN CONJ_TAC;;
289 MATCH_MP_TAC (TAUT `B /\ (B ==>A) ==> (A /\ B)`) THEN CONJ_TAC;;
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;;
297 let PROOF_BY_CONTR_TAC =
298 MATCH_MP_TAC (TAUT `(~A ==> F) ==> A`) THEN DISCH_TAC;;
300 let (UNDISCH_FIND_TAC: term -> tactic) =
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";;
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"
321 let typ = (type_vars_in_term t) in
322 can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
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
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");
337 (* this version must take variables *)
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
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");
351 let (EXISTSv_TAC :string -> tactic) =
353 let (v,_) = dest_binder "?" (goal_concl gl) in
354 let (_,ty) = dest_var v in
355 EXISTS_TAC (mk_var(s,ty)) gl;;
357 let (X_GENv_TAC:string ->tactic) =
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;;
363 (* weak version doesn't do conj *)
365 let (WEAK_STRIP_TAC: tactic) =
367 try (fun ttac -> FIRST [GEN_TAC; DISCH_THEN ttac]) STRIP_ASSUME_TAC gl
368 with Failure _ -> failwith "STRIP_TAC";;
370 let WEAK_STRIP_THM_THEN =
371 FIRST_TCL [CONJUNCTS_THEN; CHOOSE_THEN];;
373 let WEAK_STRIP_ASSUME_TAC =
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]);;
383 let (WEAKER_STRIP_TAC: tactic) =
385 try (fun ttac -> FIRST [GEN_TAC; DISCH_THEN ttac]) WEAK_STRIP_ASSUME_TAC gl
386 with Failure _ -> failwith "STRIP_TAC";;
388 let hold_def = new_definition `(hold:A->A) = I`;;
390 let hold = MATCH_MP_TAC (prove_by_refinement(
391 `!a. hold a ==> a`, [REWRITE_TAC [hold_def;I_DEF] ]));;
393 let unhold = MATCH_MP_TAC (prove_by_refinement(
394 `!a. a ==> hold a`, [REWRITE_TAC [hold_def;I_DEF] ]));;
398 (REPEAT (POP_ASSUM MP_TAC)) THEN
399 tac THEN REPEAT DISCH_TAC
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)));;
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);;
411 let RENAME_FREE_VAR (t,s) = (* rename free variable *)
412 MP_ASM_THEN (SPEC_TAC (t,t) THEN X_GENv_TAC s);;
414 (* rebind bound variables *)
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)
422 rec_alpha_at (t,mk_var(s,snd(dest_var t)));;
424 let REBIND_CONV ts g = ALPHA g (alpha_at ts g);;
426 REBIND_CONV (`x:real`,"y") (`pi + (\ x . x + pi) pi`);;
428 let REBIND_RULE ts th1 = EQ_MP (REBIND_CONV ts (concl th1)) th1;;
430 REBIND_RULE (`x:real`,"y") (ASSUME (`pi + (\ x . x + pi) pi = &1`));;
432 let REBIND_TAC ts gl = (SUBST1_TAC (REBIND_CONV ts (goal_concl gl))) gl;;
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;;
440 let varith = VECTOR_ARITH;;
442 let COMMENT _ = ALL_TAC;;
444 let INTRO_TAC th1 tml =
445 GOAL_TERM (fun w -> (MP_TAC (ISPECL ( envl w tml) th1)));;
447 let COPY_TAC = DISCH_THEN (fun t -> MP_TAC t THEN ASSUME_TAC t);;
449 let TYPED_ABBREV_TAC t gl =
450 let (a,b) = dest_eq t 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;;