1 (* =========================================================== *)
2 (* SSReflect/HOL Light support library *)
3 (* See http://code.google.com/p/flyspeck/downloads/list *)
4 (* Author: Alexey Solovyev *)
6 (* =========================================================== *)
8 (* A special definition for introducing equalities with the construction move eq: a => b *)
9 let ssreflect_eq_def = new_definition `!v P. ssreflect_eq (v:A) (P:bool) = P`;;
12 (* Generalizes given variables in a term *)
13 let gen_variables binders tm =
14 if type_of tm <> bool_ty then
15 if length binders = 0 then tm
17 failwith "gen_variables: bool term is required"
19 let f_vars = map dest_var (frees tm) in
20 let find_type name = assoc name f_vars in
21 let gen_variable var_name tm =
23 try mk_var (var_name, find_type var_name)
25 failwith ("gen_variables: variable "^var_name
26 ^" is not free in the term "^(string_of_term tm)) in
27 mk_forall (var, tm) in
28 itlist gen_variable binders tm;;
31 (* Combined type of theorems and terms *)
32 type arg_type = Arg_theorem of thm | Arg_term of term | Arg_type of hol_type;;
36 | Arg_theorem th -> th
37 | _ -> failwith "A theorem expected";;
39 let get_arg_term arg =
42 | _ -> failwith "A term expected";;
44 let get_arg_type arg =
47 | _ -> failwith "A type expected";;
50 (* Converts a theorem tactic into a tactic which accepts thm_term arguments *)
51 let thm_tac (ttac : thm_tactic) = ttac o get_arg_thm;;
52 let term_tac (ttac : term -> tactic) = ttac o get_arg_term;;
53 let type_tac (ttac : hol_type -> tactic) arg = ttac o get_arg_type;;
56 let conv_thm_tac (ttac : thm_tactic->tactic) (arg_tac : arg_type->tactic) =
57 ttac (fun th -> arg_tac (Arg_theorem th));;
61 (* Based on the code from tactics.ml *)
62 (* Applies the second tactic to either the first subgoal or
64 let (THENL_FIRST),(THENL_LAST) =
65 let propagate_empty i [] = []
66 and propagate_thm th i [] = INSTANTIATE_ALL i th in
67 let compose_justs n just1 just2 i ths =
68 let ths1,ths2 = chop_list n ths in
69 (just1 i ths1)::(just2 i ths2) in
70 let rec seqapply l1 l2 = match (l1,l2) with
71 ([],[]) -> null_meta,[],propagate_empty
72 | ((tac:tactic)::tacs),((goal:goal)::goals) ->
73 let ((mvs1,insts1),gls1,just1) = tac goal in
74 let goals' = map (inst_goal insts1) goals in
75 let ((mvs2,insts2),gls2,just2) = seqapply tacs goals' in
76 ((union mvs1 mvs2,compose_insts insts1 insts2),
77 gls1@gls2,compose_justs (length gls1) just1 just2)
78 | _,_ -> failwith "seqapply: Length mismatch" in
79 let justsequence just1 just2 insts2 i ths =
80 just1 (compose_insts insts2 i) (just2 i ths) in
81 let tacsequence ((mvs1,insts1),gls1,just1) tacl =
82 let ((mvs2,insts2),gls2,just2) = seqapply tacl gls1 in
83 let jst = justsequence just1 just2 insts2 in
84 let just = if gls2 = [] then propagate_thm (jst null_inst []) else jst in
85 ((union mvs1 mvs2,compose_insts insts1 insts2),gls2,just) in
86 let (thenl_first: tactic -> tactic -> tactic) =
88 let _,gls,_ as gstate = tac1 g in
89 if gls = [] then failwith "No subgoals"
91 let tac_list = tac2 :: (replicate ALL_TAC (length gls - 1)) in
92 tacsequence gstate tac_list
93 and (thenl_last: tactic -> tactic -> tactic) =
95 let _,gls,_ as gstate = tac1 g in
96 if gls = [] then failwith "No subgoals"
98 let tac_list = (replicate ALL_TAC (length gls - 1)) @ [tac2] in
99 tacsequence gstate tac_list in
100 thenl_first, thenl_last;;
103 (* Rotates the goalstack *)
104 let (THENL_ROT: int -> tactic -> tactic) =
106 let gstate = tac g in
110 (* Repeats the given tactic exactly n times and then repeats the same tactic at most m times *)
111 let repeat_tactic n m tac =
112 let rec replicate_at_most m tac =
113 if m <= 0 then ALL_TAC else (tac THEN replicate_at_most (m - 1) tac) ORELSE ALL_TAC in
114 REPLICATE_TAC n tac THEN replicate_at_most m tac;;
118 (* Returns all free variables in the goal *)
119 let get_context_vars (g : goal) =
120 let list, g_tm = g in
121 let tms = g_tm :: map (concl o snd) list in
122 let f_vars = setify (flat (map frees tms)) in
123 map (fun v -> ((fst o dest_var) v, v)) f_vars;;
126 (* Clears the given assumption *)
127 let clear_assumption name =
128 TRY (REMOVE_THEN name (fun th -> ALL_TAC));;
131 (* DISCH_THEN (LABEL_TAC name) for assumptions and X_GEN_TAC name for variables *)
133 (* Automatically introduces an assumption for a top-level ssreflect_eq *)
134 let move_eq (g:goal) =
138 let eq_tm = (rator o fst o dest_imp) g_tm in
139 if (fst o dest_const o rator) eq_tm = "ssreflect_eq" then
140 let label = (fst o dest_var o rand) eq_tm in
141 DISCH_THEN (LABEL_TAC label o PURE_ONCE_REWRITE_RULE[ssreflect_eq_def])
144 with Failure _ -> ALL_TAC in
147 let move1 name (g:goal) =
150 if is_forall g_tm then
151 let tm0, g_tm1 = dest_forall g_tm in
152 let tm = mk_var (name, type_of tm0) in
160 DISCH_THEN (fun th -> ALL_TAC)
162 DISCH_THEN (LABEL_TAC name)
164 failwith "move: not (!) or (==>)" in
168 (fun name tac -> move_eq THEN move1 name THEN tac) labels ALL_TAC in
172 (* Localization tactical *)
173 let in_tac a_list in_goal tac (g:goal) =
174 let goal_tm = snd g in
175 let tmp_goal_name = "$_goal_$" in
176 let tmp_goal_var = mk_var (tmp_goal_name, bool_ty) in
177 let tmp_goal = mk_eq (tmp_goal_var, goal_tm) in
178 let tmp_goal_sym = mk_eq (goal_tm, tmp_goal_var) in
180 rev_itlist (fun name tac -> REMOVE_THEN name MP_TAC THEN tac) a_list ALL_TAC in
181 let intro_tac = move a_list in
182 let hide_goal, unfold_goal =
187 EXPAND_TAC tmp_goal_name THEN
188 UNDISCH_TAC tmp_goal_sym THEN DISCH_THEN (fun th -> ALL_TAC)
190 (hide_goal THEN disch_tac THEN tac THEN TRY intro_tac THEN unfold_goal) g;;
194 (* Finds a subterm in the given term which matches against the given
195 pattern; local_consts is a list of variable which must be fixed in
197 This function returns the path to the first matched subterm *)
198 let match_subterm local_consts pat tm =
199 let rec find tm path =
201 let inst = term_match local_consts pat tm in
202 if instantiate inst pat = tm then path else failwith "Bad instantiation"
206 | Abs(_, b_tm) -> find b_tm (path^"b")
207 | Comb(l_tm, r_tm) ->
208 try find l_tm (path^"l")
209 with Failure _ -> find r_tm (path^"r")
210 | _ -> failwith "match_subterm: no match"
212 failwith ("match_subterm: no match: "^string_of_term pat) in
217 (* Returns paths to all subterms satisfying p *)
218 let find_all_paths p tm =
219 let rec find_path p tm path =
223 find_path p b_tm (path ^ "b")
224 | Comb(l_tm, r_tm) ->
225 (find_path p l_tm (path ^ "l")) @ (find_path p r_tm (path ^ "r"))
227 if p tm then path :: paths else paths in
231 (* Instantiates types of the given context variables in the given term.*)
232 let inst_context_vars vars tm_vars tm =
234 let name, ty = dest_var var in
236 (ty, type_of (assoc name vars))
238 failwith (name^" is free in the term `"^(string_of_term tm)^"` and in the context") in
239 let ty_src, ty_dst = unzip (map find_type tm_vars) in
240 let ty_inst = itlist2 type_match ty_src ty_dst [] in
244 (* Instantiates types of all free variables in the term using the context *)
245 let inst_all_free_vars tm (g : goal) =
246 let context_vars = get_context_vars g in
247 let f_vars = frees tm in
248 inst_context_vars context_vars f_vars tm;;
251 (* Finds a subterm corresponding to the given pattern.
252 Before matching, the term types are instantiated in the given context. *)
253 let match_subterm_in_context pat tm (g : goal) =
254 let context_vars = get_context_vars g in
255 let f0_vars = filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees pat) in
256 let pattern = inst_context_vars context_vars f0_vars pat in
257 let f1_vars = filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees pattern) in
258 match_subterm f1_vars pattern tm;;
261 (*************************)
263 (*************************)
265 (* Breaks conjunctions and does other misc stuff *)
266 let rec break_conjuncts th : thm list =
267 (* Convert P ==> (!x. Q x) to !x. P ==> Q x and P ==> Q ==> R to P /\ Q ==> R *)
268 let th0 = PURE_REWRITE_RULE[GSYM RIGHT_FORALL_IMP_THM; IMP_IMP] th in
269 let th1 = SPEC_ALL th0 in
270 (* Break top level conjunctions *)
271 let th_list = CONJUNCTS th1 in
272 if length th_list > 1 then
273 List.concat (map break_conjuncts th_list)
275 let th_tm = concl th1 in
276 (* Deal with assumptions *)
278 let a_tm = lhand th_tm in
279 let th_list = break_conjuncts (UNDISCH th1) in
280 map (DISCH a_tm) th_list
282 if is_eq th_tm then [th1]
285 [PURE_ONCE_REWRITE_RULE[TAUT `~P <=> (P <=> F)`] th1]
290 (* Finds an instantination for the given term inside another term *)
291 let rec find_term_inst local_consts tm src_tm path =
292 try (term_match local_consts tm src_tm, true, path)
295 | Comb(l_tm, r_tm) ->
296 let r_inst, flag, s = find_term_inst local_consts tm l_tm (path ^ "l") in
297 if flag then (r_inst, flag, s)
299 find_term_inst local_consts tm r_tm (path ^ "r")
301 find_term_inst local_consts tm b_tm (path ^ "b")
302 | _ -> (([],[],[]), false, path);;
306 (* Rewrites the subterm at the given path using the given equation theorem *)
307 let path_rewrite path th tm =
308 let rec build path tm =
309 let n = String.length path in
314 let path' = String.sub path 1 (n - 1) in
316 let lhs, rhs = dest_comb tm in
317 let th0 = build path' lhs in
319 else if ch = 'r' then
320 let lhs, rhs = dest_comb tm in
321 let th0 = build path' rhs in
323 else if ch = 'b' then
324 let var, body = dest_abs tm in
325 let th0 = build path' body in
327 with Failure _ -> failwith ("ABS failed: (" ^ string_of_term var ^ ", " ^ string_of_thm th0)
329 failwith ("Bad path symbol: "^path) in
330 let res = build path tm in
331 let lhs = (lhand o concl) res in
332 if not (aconv lhs tm) then failwith ("path_rewrite: incorrect result [required: "^
333 (string_of_term tm)^"; obtained: "^
334 (string_of_term lhs))
339 let new_rewrite occ pat th g =
340 let goal_tm = snd g in
341 (* Free variables in the given theorem will not be matched *)
342 let local_consts = frees (concl th) in
343 (* Apply the pattern *)
344 let goal_subterm_path =
345 if pat = [] then "" else match_subterm_in_context (hd pat) goal_tm g in
346 let goal_subterm = follow_path goal_subterm_path goal_tm in
348 (* Local rewrite function *)
350 let concl_th = concl th in
351 let cond_flag = is_imp concl_th in
352 let match_fun = lhs o (if cond_flag then rand else I) in
354 (* Match the theorem *)
355 let lhs_tm = match_fun concl_th in
356 let ii, flag, path = find_term_inst local_consts lhs_tm goal_subterm goal_subterm_path in
358 failwith (string_of_term lhs_tm ^ " does not match any subterm in the goal")
360 let matched_th = INSTANTIATE ii th in
361 let matched_tm = (match_fun o concl) matched_th in
363 (* Find all matched subterms *)
364 let paths = find_all_paths (fun x -> aconv x matched_tm) goal_tm in
365 let paths = if occ = [] then paths else
366 map (fun i -> List.nth paths (i - 1)) occ in
368 (* Find all free variables in the matched theorem which do not correspond to free variables in
369 the matched subterm *)
370 let tm_frees = frees matched_tm in
371 let mth_frees = frees (concl matched_th) in
372 let vars = subtract mth_frees (union local_consts tm_frees) in
374 (* Construct the tactic for rewriting *)
375 let r_tac = fun th -> MAP_EVERY (fun path -> CONV_TAC (path_rewrite path th)) paths in
377 MP_TAC matched_th THEN ANTS_TAC THENL [ALL_TAC; DISCH_THEN r_tac]
381 let rec gen_vars vars th =
383 | v :: vs -> gen_vars vs (GEN v th)
385 let th2 = gen_vars vars matched_th in
386 MP_TAC th2 THEN PURE_REWRITE_TAC[LEFT_IMP_FORALL_THM] in
388 (* Try to rewrite with all given theorems *)
389 let th_list = break_conjuncts th in
390 let rec my_first th_list =
391 if length th_list = 1 then
392 rewrite (hd th_list) g
394 try rewrite (hd th_list) g
395 with Failure _ -> my_first (tl th_list) in
400 let th = ARITH_RULE `!n. n * 0 <= 1`;;
401 let tm = `m * 0 <= 1 <=> T`;;
403 e(new_rewrite [] [] th);;
405 let th = CONJ REAL_MUL_RINV REAL_MUL_LINV;;
406 let tm = `inv (x - y) * (x - y) + &1 = &1 + inv (x - y) * (x - y) + x * inv x`;;
407 let tm0 = `!x. inv (x - y) * (x - y) = &1`;;
411 e(new_rewrite [] [] (th));;
412 e(new_rewrite [] [] (GSYM th));;
413 e(new_rewrite [] [`_ + &1`] th);;
416 e(new_rewrite [] [] (ARITH_RULE `!x. x > 2 ==> (!n. n = 2 ==> ~(x < n))`));;
421 (* Rewrite tactic for usual and conditional theorems *)
422 let rewrite occ pat th g =
423 let rec match_theorem ffun th tm str =
424 try (PART_MATCH ffun th tm, true, str)
427 | Comb(l_tm, r_tm) ->
428 let r_th, flag, s = match_theorem ffun th l_tm (str ^ "l") in
429 if flag then (r_th, flag, s)
431 match_theorem ffun th r_tm (str ^ "r")
433 match_theorem ffun th b_tm (str ^ "b")
434 | _ -> (th, false, str) in
435 (* Initialize auxiliary variables *)
436 let goal_tm = snd g in
437 let th0 = PURE_REWRITE_RULE[IMP_IMP] th in
438 let concl_th = concl (SPEC_ALL th0) in
439 let cond_flag = is_imp concl_th in
440 let eq_tm = if cond_flag then rand concl_th else concl_th in
441 let match_fun = (if is_eq eq_tm then lhand else I) o (if cond_flag then rand else I) in
443 (* Apply the pattern *)
444 let goal_subterm_path =
445 if pat = [] then "" else match_subterm_in_context (hd pat) goal_tm g in
446 let goal_subterm = follow_path goal_subterm_path goal_tm in
448 (* Match the theorem *)
449 let matched_th, flag, path = match_theorem match_fun th0 goal_subterm goal_subterm_path in
451 failwith "lhs does not match any term in the goal"
453 let matched_tm = (match_fun o concl) matched_th in
454 (* Find all matched subterms *)
455 let paths = find_all_paths (fun x -> x = matched_tm) goal_tm in
456 let paths = if occ = [] then paths else
457 map (fun i -> List.nth paths (i - 1)) occ in
458 (* Find all free variables in the matched theorem which do not correspond to free variables in
459 the matched subterm *)
460 let tm_frees = frees matched_tm in
461 let th_frees = frees (concl th0) in
462 let mth_frees = frees (concl matched_th) in
463 let vars = subtract mth_frees (union th_frees tm_frees) in
465 let r_tac = fun th -> MAP_EVERY (fun path -> GEN_REWRITE_TAC (PATH_CONV path) [th]) paths in
467 (MP_TAC matched_th THEN ANTS_TAC THENL [ALL_TAC; DISCH_THEN r_tac]) g
471 let rec gen_vars vars th =
473 | v :: vs -> gen_vars vs (GEN v th)
475 let th2 = gen_vars vars matched_th in
476 (MP_TAC th2 THEN REWRITE_TAC[LEFT_IMP_FORALL_THM]) g;;
481 (* Analogue of the "done" tactic in SSReflect *)
482 let done_tac = ASM_REWRITE_TAC[] THEN FAIL_TAC "done: not all subgoals are proved";;
484 (* Simplification: /= *)
485 let simp_tac = SIMP_TAC[];;
488 (* Linear arithmetic simplification *)
489 let arith_tac = FIRST [ARITH_TAC; REAL_ARITH_TAC; INT_ARITH_TAC];;
493 let split_tac = FIRST [CONJ_TAC; EQ_TAC];;
497 (* Creates an abbreviation for the given term with the given name *)
498 let set_tac name tm (g : goal) =
499 let goal_tm = snd g in
502 follow_path (match_subterm_in_context tm goal_tm g) goal_tm
503 with Failure _ -> tm in
504 let tm1 = inst_all_free_vars tm0 g in
505 let abbrev_tm = mk_eq (mk_var (name, type_of tm1), tm1) in
506 (ABBREV_TAC abbrev_tm THEN POP_ASSUM (LABEL_TAC (name ^ "_def"))) g;;
508 (* Generates a fresh name for the given term *)
509 (* taking into account names of the provided variables *)
510 let generate_fresh_name names tm =
511 let rec find_name prefix n =
512 let name = prefix ^ (if n = 0 then "" else string_of_int n) in
513 if can (find (fun str -> str = name)) names then
514 find_name prefix (n + 1)
517 let prefix = if is_var tm then (fst o dest_var) tm else "x" in
521 (* Returns a variable which name does not conflict with names of given vars *)
522 let get_fresh_var var vars =
523 let names = map (fst o dest_var) vars in
524 mk_var (generate_fresh_name names var, type_of var);;
527 (* Matches all wild cards in the term and *)
528 (* instantinates all type variables in the given context *)
529 let prepare_term tm (g : goal) =
530 let goal_tm = snd g in
532 try follow_path (match_subterm_in_context tm goal_tm g) goal_tm
533 with Failure _ -> tm in
534 inst_all_free_vars tm0 g;;
536 (* Discharges a term by generalizing all occurences of this term first *)
537 let disch_tm_tac occs tm (g : goal) =
538 let tm0 = prepare_term tm g in
539 let name = generate_fresh_name ((fst o unzip) (get_context_vars g)) tm in
540 let new_tm = mk_var (name, type_of tm0) in
542 if occs = [] && is_var tm then
543 mk_var ((fst o dest_var) tm, type_of tm0)
545 let abbrev_tm = mk_eq (new_tm, tm0) in
546 (ABBREV_TAC abbrev_tm THEN
548 POP_ASSUM (fun th -> TRY (new_rewrite occs [] th)) THEN
549 SPEC_TAC (new_tm, new_tm1)) g;;
552 (* Discharges a theorem or a term *)
553 let disch_tac occs arg =
555 | Arg_theorem th -> MP_TAC th
556 | Arg_term tm -> disch_tm_tac occs tm
557 | _ -> failwith "disch_tac: a type cannot be discharged";;
563 let conj_imp = TAUT `(A /\ B ==> C) ==> (A ==> B ==> C)` in
564 let dummy_tm = `F` in
567 let ctm = concl th in
569 if is_forall ctm then
570 let (var_tm, _) = dest_forall ctm in
571 let var = get_fresh_var var_tm (thm_frees th @ local_consts) in
572 let th1 = SPEC var th in
573 let list, th0 = process th1 in
574 ("spec", var) :: list, th0
576 else if is_imp ctm then
577 let ant_tm, _ = dest_imp ctm in
579 if is_conj ant_tm then
580 let th1 = MATCH_MP conj_imp th in
581 let list, th0 = process th1 in
582 ("conj", dummy_tm) :: list, th0
585 let th1 = UNDISCH th in
586 let list, th0 = process th1 in
587 ("undisch", ant_tm) :: list, th0
594 (* reconstruct_thm *)
595 let reconstruct_thm =
596 let imp_conj = TAUT `(A ==> B ==> C) ==> (A /\ B ==> C)` in
597 let triv_ths = TAUT `((T ==> A) <=> A) /\ ((T /\ A) = A) /\ ((A /\ T) = A)` in
598 let rec reconstruct list th =
604 | ("spec", (_ as tm)) -> GEN tm th
605 | ("conj", _) -> MATCH_MP imp_conj th
606 | ("undisch", (_ as tm)) -> DISCH tm th
607 | _ -> failwith ("Unknown command: " ^ fst cmd) in
610 fun (cmd_list, th) ->
611 let th1 = reconstruct (rev cmd_list) th in
612 PURE_REWRITE_RULE[triv_ths] th1;;
616 let spec_var_th th n tm =
617 let cmd, th0 = process_thm (frees tm) th in
618 let ty = type_of tm in
619 let rec spec n list head =
621 | ("spec", (_ as var_tm)) :: t ->
623 let ty_ii = type_match (type_of var_tm) ty [] in
625 let th1 = reconstruct_thm (list, th0) in
626 let th2 = ISPEC tm th1 in
627 let tail, th0 = process_thm [] th2 in
628 let head1 = map (fun s, tm -> s, inst ty_ii tm) head in
631 spec (n - 1) t (head @ [hd list])
633 spec n t (head @ [hd list]))
634 | h :: t -> spec n t (head @ [h])
635 | [] -> failwith ("spec_var_th") in
636 reconstruct_thm (spec n cmd []);;
640 let match_mp_th ith n th =
641 let lconsts = thm_frees ith in
642 let cmd, th0 = process_thm (thm_frees th) ith in
644 let rec rec_match n list head =
646 | ("undisch", (_ as tm0)) :: t ->
648 let ii = term_match lconsts tm0 tm in
650 let th1 = INSTANTIATE_ALL ii th0 in
651 let th2 = PROVE_HYP th th1 in
652 let list0 = head @ (("undisch", `T`) :: t) in
653 let f_vars = frees tm0 in
655 (fun s, tm -> not (s = "spec" && mem tm f_vars)) list0 in
656 let list = map (fun s, tm -> s, instantiate ii tm) list1 in
659 rec_match (n - 1) t (head @ [hd list])
661 rec_match n t (head @ [hd list]))
662 | h :: t -> rec_match n t (head @ [h])
663 | [] -> failwith "match_mp_th: no match" in
664 let r = rec_match n cmd [] in
667 (* Introduces a subgoal *)
668 let have_gen_tac binders then_tac tm (g : goal) =
669 (* let tm0 = inst_all_free_vars tm g in *)
670 let tm1 = gen_variables binders tm in
671 let tm2 = prepare_term tm1 g in
672 (THENL_FIRST (SUBGOAL_THEN tm2 (fun th -> MP_TAC th THEN then_tac))
676 let have_tac then_tac tm (g : goal) =
677 (* let tm0 = inst_all_free_vars tm g in *)
678 let tm0 = prepare_term tm g in
679 (SUBGOAL_THEN tm0 (fun th -> MP_TAC th THEN then_tac)) g;;
684 let wlog_tac then_tac vars tm (g : goal) =
685 (* let tm0 = inst_all_free_vars tm g in *)
686 let tm0 = prepare_term tm g in
687 let vars0 = map (fun tm -> inst_all_free_vars tm g) vars in
689 let imp = list_mk_forall (vars0, mk_imp (tm0, g_tm)) in
690 (THENL_ROT 1 (SUBGOAL_THEN imp (fun th -> MP_TAC th THEN then_tac) THENL
691 [REPLICATE_TAC (length vars) GEN_TAC; ALL_TAC])) g;;
694 (* Provides a witness for an existential goal *)
695 let exists_tac tm (g : goal) =
696 let tm0 = inst_all_free_vars tm g in
697 let target_ty = (type_of o fst o dest_exists o snd) g in
698 let inst_ty = type_match (type_of tm0) target_ty [] in
699 let tm1 = inst inst_ty tm0 in
702 (* Instantiates the first type variable in the given theorem *)
703 let inst_first_type th ty =
704 let ty_vars = type_vars_in_term (concl th) in
706 failwith "inst_first_type: no type variables in the theorem"
708 INST_TYPE [(ty, hd ty_vars)] th;;
711 (* The first argument must be a theorem, the second argument is arbitrary *)
712 let combine_args arg1 arg2 =
713 let th1 = get_arg_thm arg1 in
717 (try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2)
719 (try ISPEC tm2 th1 with Failure _ -> spec_var_th th1 1 tm2)
720 | Arg_type ty2 -> inst_first_type th1 ty2 in
724 let use_arg_then_result = ref TRUTH;;
726 let use_arg_then id (arg_tac:arg_type->tactic) (g:goal) =
730 let assumption = assoc id list in
731 Arg_theorem assumption
734 let vars = get_context_vars g in
735 let var = assoc id vars in
739 Lexing.from_string ("use_arg_then_result := " ^ id ^ ";;") in
740 let ast = (!Toploop.parse_toplevel_phrase) lexbuf in
743 Toploop.execute_phrase false Format.std_formatter ast
744 with _ -> failwith ("Bad identifier: " ^ id) in
745 Arg_theorem !use_arg_then_result in
749 let combine_args_then (tac:arg_type->tactic) arg1 arg2 (g:goal) =
750 let th1 = get_arg_thm arg1 in
754 (try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2)
756 let tm0 = prepare_term tm2 g in
757 (try ISPEC tm0 th1 with Failure _ -> spec_var_th th1 1 tm0)
758 | Arg_type ty2 -> inst_first_type th1 ty2 in
759 tac (Arg_theorem th0) g;;
764 (* Specializes a variable and applies the next tactic *)
765 let ispec_then tm (tac : thm_tactic) th (g : goal) =
766 let tm0 = prepare_term tm g in
767 let th0 = try ISPEC tm0 th with Failure _ -> spec_var_th th 1 tm0 in
771 let ISPEC_THEN tm (tac : thm_tactic) th (g : goal) =
772 let tm0 = inst_all_free_vars tm g in
773 tac (ISPEC tm0 th) g;;
777 let USE_THM_THEN th (tac : thm_tactic) =
781 let MATCH_MP_THEN th2 (tac : thm_tactic) th1 =
782 tac (MATCH_MP th1 th2);;
784 let match_mp_then th2 (tac : thm_tactic) th1 =
785 let th0 = try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2 in
789 let GSYM_THEN (tac : thm -> tactic) th =
793 let gsym_then (tac:arg_type->tactic) arg =
794 tac (Arg_theorem (GSYM (get_arg_thm arg)));;
797 (* The 'apply' tactic *)
799 let rec try_match th =
800 try MATCH_MP_TAC th g with Failure _ ->
801 let th0 = PURE_ONCE_REWRITE_RULE[IMP_IMP] th in
802 if th = th0 then failwith "apply_tac: no match"
806 try MATCH_ACCEPT_TAC th g with Failure _ ->
810 FIRST [MATCH_ACCEPT_TAC th; MATCH_MP_TAC th];; *)
813 (* The 'exact' tactic *)
814 (* TODO: do [done | by move => top; apply top], here apply top
815 works as ACCEPT_TAC with matching (rewriting) in some cases *)
816 let exact_tac = FIRST [done_tac; DISCH_THEN (fun th -> apply_tac th) THEN done_tac];;
820 (* Specializes the theorem using the given set of variables *)
821 let spec0 names vars =
823 try (assoc name vars, true)
824 with Failure _ -> (parse_term name, false) in
826 let name, ty = dest_var var in
827 let t, flag = find name in
831 (`:bool`, `:bool`) in
833 let ty_src, ty_dst = unzip (map find_type (frees tm)) in
834 let ty_inst = itlist2 type_match ty_src ty_dst [] in
836 let list = map find names in
837 let tm_list = map (fun tm, flag -> if flag then tm else inst_term tm) list in
841 let spec names = spec0 names (get_context_vars (top_realgoal()));;
844 let spec_mp names th g = MP_TAC (spec0 names (get_context_vars g) th) g;;
848 let bool_cases = ONCE_REWRITE_RULE[CONJ_ACI] bool_INDUCT;;
849 let list_cases = prove(`!P. P [] /\ (!(h:A) t. P (CONS h t)) ==> (!l. P l)`,
850 REPEAT STRIP_TAC THEN
851 MP_TAC (SPEC `l:(A)list` list_CASES) THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
852 FIRST_X_ASSUM (CHOOSE_THEN MP_TAC) THEN DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
853 DISCH_THEN (fun th -> ASM_REWRITE_TAC[th]));;
854 let pair_cases = pair_INDUCT;;
855 let num_cases = prove(`!P. P 0 /\ (!n. P (SUC n)) ==> (!m. P m)`,
856 REPEAT STRIP_TAC THEN
857 MP_TAC (SPEC `m:num` num_CASES) THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
858 FIRST_X_ASSUM (CHOOSE_THEN (fun th -> ASM_REWRITE_TAC[th])));;
859 let option_cases = option_INDUCT;;
862 let cases_table = Hashtbl.create 10;;
863 Hashtbl.add cases_table "bool" bool_cases;;
864 Hashtbl.add cases_table "list" list_cases;;
865 Hashtbl.add cases_table "prod" pair_cases;;
866 Hashtbl.add cases_table "num" num_cases;;
867 Hashtbl.add cases_table "option" option_cases;;
870 (* Induction theorems *)
871 let bool_elim = bool_cases;;
872 let list_elim = list_INDUCT;;
873 let pair_elim = pair_INDUCT;;
874 let num_elim = num_INDUCTION;;
875 let option_elim = option_INDUCT;;
877 let elim_table = Hashtbl.create 10;;
878 Hashtbl.add elim_table "bool" bool_elim;;
879 Hashtbl.add elim_table "list" list_elim;;
880 Hashtbl.add elim_table "prod" pair_elim;;
881 Hashtbl.add elim_table "num" num_elim;;
882 Hashtbl.add elim_table "option" option_elim;;
886 (* case: works only for (A /\ B) -> C; (A \/ B) -> C; (?x. P) -> Q; !(n:num). P; !(l:list(A)). P *)
888 let goal_tm = snd g in
889 if not (is_imp goal_tm) then
891 if is_forall goal_tm then
892 let var, _ = dest_forall goal_tm in
893 let ty_name = (fst o dest_type o type_of) var in
894 let case_th = Hashtbl.find cases_table ty_name in
895 (MATCH_MP_TAC case_th THEN REPEAT CONJ_TAC) g
897 failwith "case: not imp or forall"
899 let tm = lhand goal_tm in
902 (DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN POP_ASSUM MP_TAC) g
904 else if is_disj tm then
905 (DISCH_THEN DISJ_CASES_TAC THEN POP_ASSUM MP_TAC) g
907 else if is_exists tm then
908 (ONCE_REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM]) g
910 failwith "case: not implemented";;
914 (* elim: works only for num and list *)
916 let goal_tm = snd g in
918 if is_forall goal_tm then
919 let var, _ = dest_forall goal_tm in
920 let ty_name = (fst o dest_type o type_of) var in
921 let induct_th = Hashtbl.find elim_table ty_name in
922 (MATCH_MP_TAC induct_th THEN REPEAT CONJ_TAC) g
924 failwith "elim: not forall";;
928 (* Instantiates the first type variable in the given theorem *)
929 let INST_FIRST_TYPE_THEN ty (then_tac:thm_tactic) th =
930 let ty_vars = type_vars_in_term (concl th) in
932 failwith "inst_first_type: no type variables in the theorem"
934 then_tac (INST_TYPE [(ty, hd ty_vars)] th);;
937 (* Replaces all occurrences of distinct '_' with unique variables *)
938 let transform_pattern pat_tm =
939 let names = ref (map (fst o dest_var) (frees pat_tm)) in
940 let rec transform tm =
943 let _ = names := (fst o dest_var) x_tm :: !names in
944 mk_abs (x_tm, transform b_tm)
945 | Comb(l_tm, r_tm) ->
946 mk_comb (transform l_tm, transform r_tm)
948 let name = generate_fresh_name !names tm in
949 let _ = names := name :: !names in
956 filter (fun tm -> ((fst o dest_var) tm).[0] = '_') (frees tm);;
959 filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees tm);;
963 let congr_tac pat_tm goal =
964 let goal_tm = snd goal in
965 let context_vars = get_context_vars goal in
966 let pat = transform_pattern pat_tm in
967 let f0_vars = nwild_frees pat in
968 let pattern = inst_context_vars context_vars f0_vars pat in
969 let const_pat = nwild_frees pattern in
970 let wild_pat = wild_frees pattern in
972 let lhs, rhs = dest_eq goal_tm in
974 term_match const_pat pattern lhs, term_match const_pat pattern rhs in
976 (fun tm -> mk_eq (instantiate lm tm, instantiate rm tm)) wild_pat in
977 let eq_tm = itlist (curry mk_imp) eq_tms goal_tm in
978 let eq_thm = EQT_ELIM (SIMP_CONV[] eq_tm) in
979 (apply_tac eq_thm THEN REPEAT CONJ_TAC) goal;;
982 (* Eliminates the first antecedent of a goal *)
983 let elim_fst_ants_tac =
984 let gen_elim_thm tm =
985 let vars, tm1 = strip_forall tm in
986 let ants_tm, concl_tm = dest_imp tm1 in
987 let th1 = ASSUME (itlist (curry mk_forall) vars concl_tm) in
988 let th2 = DISCH ants_tm (SPECL vars th1) in
989 DISCH_ALL (itlist GEN vars th2) in
991 let goal_tm = snd g in
992 let elim_th = gen_elim_thm goal_tm in
993 MATCH_MP_TAC elim_th g;;
996 (* If a goal has the form ssreflect_eq ==> P then the equality is introduced as
998 If a goal has the form !x. ssreflect_eq ==> P then the equality is eliminated *)
999 let process_fst_eq_tac (g:goal) =
1000 let vars, g_tm = strip_forall (snd g) in
1003 let eq_tm = (rator o fst o dest_imp) g_tm in
1004 let label = (fst o dest_var o rand) eq_tm in
1005 if (fst o dest_const o rator) eq_tm = "ssreflect_eq" then
1006 if length vars = 0 then
1007 DISCH_THEN (LABEL_TAC label o PURE_ONCE_REWRITE_RULE[ssreflect_eq_def])
1012 with Failure _ -> ALL_TAC in
1016 (* Discharges a term by generalizing all occurences of this term first *)
1017 let disch_tm_eq_tac eq_name occs tm (g : goal) =
1018 let tm0 = prepare_term tm g in
1019 let name = generate_fresh_name ((fst o unzip) (get_context_vars g)) tm in
1020 let eq_var = mk_var (eq_name, aty) in
1021 let new_tm = mk_var (name, type_of tm0) in
1022 let abbrev_tm = mk_eq (new_tm, tm0) in
1023 (ABBREV_TAC abbrev_tm THEN
1024 EXPAND_TAC name THEN
1025 FIRST_ASSUM (fun th -> TRY (new_rewrite occs [] th)) THEN
1026 POP_ASSUM (MP_TAC o PURE_ONCE_REWRITE_RULE[GSYM (SPEC eq_var ssreflect_eq_def)]) THEN
1027 SPEC_TAC (new_tm, new_tm)) g;;
1030 (* Discharges a term and generates an equality *)
1031 let disch_eq_tac eq_name occs arg =
1032 disch_tm_eq_tac eq_name occs (get_arg_term arg);;