1 (* A special definition for introducing equalities with the construction move eq: a => b *)
2 let ssreflect_eq_def = new_definition `!v P. ssreflect_eq (v:A) (P:bool) = P`;;
5 (* Generalizes given variables in a term *)
6 let gen_variables binders tm =
7 if type_of tm <> bool_ty then
8 if length binders = 0 then tm
10 failwith "gen_variables: bool term is required"
12 let f_vars = map dest_var (frees tm) in
13 let find_type name = assoc name f_vars in
14 let gen_variable var_name tm =
16 try mk_var (var_name, find_type var_name)
18 failwith ("gen_variables: variable "^var_name
19 ^" is not free in the term "^(string_of_term tm)) in
20 mk_forall (var, tm) in
21 itlist gen_variable binders tm;;
24 (* Combined type of theorems and terms *)
25 type arg_type = Arg_theorem of thm | Arg_term of term | Arg_type of hol_type;;
29 | Arg_theorem th -> th
30 | _ -> failwith "A theorem expected";;
32 let get_arg_term arg =
35 | _ -> failwith "A term expected";;
37 let get_arg_type arg =
40 | _ -> failwith "A type expected";;
43 (* Converts a theorem tactic into a tactic which accepts thm_term arguments *)
44 let thm_tac (ttac : thm_tactic) = ttac o get_arg_thm;;
45 let term_tac (ttac : term -> tactic) = ttac o get_arg_term;;
46 let type_tac (ttac : hol_type -> tactic) arg = ttac o get_arg_type;;
49 let conv_thm_tac (ttac : thm_tactic->tactic) (arg_tac : arg_type->tactic) =
50 ttac (fun th -> arg_tac (Arg_theorem th));;
54 (* Based on the code from tactics.ml *)
55 (* Applies the second tactic to either the first subgoal or
57 let (THENL_FIRST),(THENL_LAST) =
58 let propagate_empty i [] = []
59 and propagate_thm th i [] = INSTANTIATE_ALL i th in
60 let compose_justs n just1 just2 i ths =
61 let ths1,ths2 = chop_list n ths in
62 (just1 i ths1)::(just2 i ths2) in
63 let rec seqapply l1 l2 = match (l1,l2) with
64 ([],[]) -> null_meta,[],propagate_empty
65 | ((tac:tactic)::tacs),((goal:goal)::goals) ->
66 let ((mvs1,insts1),gls1,just1) = tac goal in
67 let goals' = map (inst_goal insts1) goals in
68 let ((mvs2,insts2),gls2,just2) = seqapply tacs goals' in
69 ((union mvs1 mvs2,compose_insts insts1 insts2),
70 gls1@gls2,compose_justs (length gls1) just1 just2)
71 | _,_ -> failwith "seqapply: Length mismatch" in
72 let justsequence just1 just2 insts2 i ths =
73 just1 (compose_insts insts2 i) (just2 i ths) in
74 let tacsequence ((mvs1,insts1),gls1,just1) tacl =
75 let ((mvs2,insts2),gls2,just2) = seqapply tacl gls1 in
76 let jst = justsequence just1 just2 insts2 in
77 let just = if gls2 = [] then propagate_thm (jst null_inst []) else jst in
78 ((union mvs1 mvs2,compose_insts insts1 insts2),gls2,just) in
79 let (thenl_first: tactic -> tactic -> tactic) =
81 let _,gls,_ as gstate = tac1 g in
82 if gls = [] then failwith "No subgoals"
84 let tac_list = tac2 :: (replicate ALL_TAC (length gls - 1)) in
85 tacsequence gstate tac_list
86 and (thenl_last: tactic -> tactic -> tactic) =
88 let _,gls,_ as gstate = tac1 g in
89 if gls = [] then failwith "No subgoals"
91 let tac_list = (replicate ALL_TAC (length gls - 1)) @ [tac2] in
92 tacsequence gstate tac_list in
93 thenl_first, thenl_last;;
96 (* Rotates the goalstack *)
97 let (THENL_ROT: int -> tactic -> tactic) =
103 (* Repeats the given tactic exactly n times and then repeats the same tactic at most m times *)
104 let repeat_tactic n m tac =
105 let rec replicate_at_most m tac =
106 if m <= 0 then ALL_TAC else (tac THEN replicate_at_most (m - 1) tac) ORELSE ALL_TAC in
107 REPLICATE_TAC n tac THEN replicate_at_most m tac;;
111 (* Returns all free variables in the goal *)
112 let get_context_vars (g : goal) =
113 let list, g_tm = g in
114 let tms = g_tm :: map (concl o snd) list in
115 let f_vars = setify (flat (map frees tms)) in
116 map (fun v -> ((fst o dest_var) v, v)) f_vars;;
119 (* Clears the given assumption *)
120 let clear_assumption name =
121 TRY (REMOVE_THEN name (fun th -> ALL_TAC));;
124 (* DISCH_THEN (LABEL_TAC name) for assumptions and X_GEN_TAC name for variables *)
126 (* Automatically introduces an assumption for a top-level ssreflect_eq *)
127 let move_eq (g:goal) =
131 let eq_tm = (rator o fst o dest_imp) g_tm in
132 if (fst o dest_const o rator) eq_tm = "ssreflect_eq" then
133 let label = (fst o dest_var o rand) eq_tm in
134 DISCH_THEN (LABEL_TAC label o PURE_ONCE_REWRITE_RULE[ssreflect_eq_def])
137 with Failure _ -> ALL_TAC in
140 let move1 name (g:goal) =
143 if is_forall g_tm then
144 let tm0, g_tm1 = dest_forall g_tm in
145 let tm = mk_var (name, type_of tm0) in
153 DISCH_THEN (fun th -> ALL_TAC)
155 DISCH_THEN (LABEL_TAC name)
157 failwith "move: not (!) or (==>)" in
161 (fun name tac -> move_eq THEN move1 name THEN tac) labels ALL_TAC in
165 (* Localization tactical *)
166 let in_tac a_list in_goal tac (g:goal) =
167 let goal_tm = snd g in
168 let tmp_goal_name = "$_goal_$" in
169 let tmp_goal_var = mk_var (tmp_goal_name, bool_ty) in
170 let tmp_goal = mk_eq (tmp_goal_var, goal_tm) in
171 let tmp_goal_sym = mk_eq (goal_tm, tmp_goal_var) in
173 rev_itlist (fun name tac -> REMOVE_THEN name MP_TAC THEN tac) a_list ALL_TAC in
174 let intro_tac = move a_list in
175 let hide_goal, unfold_goal =
180 EXPAND_TAC tmp_goal_name THEN
181 UNDISCH_TAC tmp_goal_sym THEN DISCH_THEN (fun th -> ALL_TAC)
183 (hide_goal THEN disch_tac THEN tac THEN TRY intro_tac THEN unfold_goal) g;;
187 (* Finds a subterm in the given term which matches against the given
188 pattern; local_consts is a list of variable which must be fixed in
190 This function returns the path to the first matched subterm *)
191 let match_subterm local_consts pat tm =
192 let rec find tm path =
194 let inst = term_match local_consts pat tm in
195 if instantiate inst pat = tm then path else failwith "Bad instantiation"
199 | Abs(_, b_tm) -> find b_tm (path^"b")
200 | Comb(l_tm, r_tm) ->
201 try find l_tm (path^"l")
202 with Failure _ -> find r_tm (path^"r")
203 | _ -> failwith "match_subterm: no match"
205 failwith ("match_subterm: no match: "^string_of_term pat) in
210 (* Returns paths to all subterms satisfying p *)
211 let find_all_paths p tm =
212 let rec find_path p tm path =
216 find_path p b_tm (path ^ "b")
217 | Comb(l_tm, r_tm) ->
218 (find_path p l_tm (path ^ "l")) @ (find_path p r_tm (path ^ "r"))
220 if p tm then path :: paths else paths in
224 (* Instantiates types of the given context variables in the given term.*)
225 let inst_context_vars vars tm_vars tm =
227 let name, ty = dest_var var in
229 (ty, type_of (assoc name vars))
231 failwith (name^" is free in the term `"^(string_of_term tm)^"` and in the context") in
232 let ty_src, ty_dst = unzip (map find_type tm_vars) in
233 let ty_inst = itlist2 type_match ty_src ty_dst [] in
237 (* Instantiates types of all free variables in the term using the context *)
238 let inst_all_free_vars tm (g : goal) =
239 let context_vars = get_context_vars g in
240 let f_vars = frees tm in
241 inst_context_vars context_vars f_vars tm;;
244 (* Finds a subterm corresponding to the given pattern.
245 Before matching, the term types are instantiated in the given context. *)
246 let match_subterm_in_context pat tm (g : goal) =
247 let context_vars = get_context_vars g in
248 let f0_vars = filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees pat) in
249 let pattern = inst_context_vars context_vars f0_vars pat in
250 let f1_vars = filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees pattern) in
251 match_subterm f1_vars pattern tm;;
254 (*************************)
256 (*************************)
258 (* Breaks conjunctions and does other misc stuff *)
259 let rec break_conjuncts th : thm list =
260 (* Convert P ==> (!x. Q x) to !x. P ==> Q x and P ==> Q ==> R to P /\ Q ==> R *)
261 let th0 = PURE_REWRITE_RULE[GSYM RIGHT_FORALL_IMP_THM; IMP_IMP] th in
262 let th1 = SPEC_ALL th0 in
263 (* Break top level conjunctions *)
264 let th_list = CONJUNCTS th1 in
265 if length th_list > 1 then
266 List.concat (map break_conjuncts th_list)
268 let th_tm = concl th1 in
269 (* Deal with assumptions *)
271 let a_tm = lhand th_tm in
272 let th_list = break_conjuncts (UNDISCH th1) in
273 map (DISCH a_tm) th_list
275 if is_eq th_tm then [th1]
278 [PURE_ONCE_REWRITE_RULE[TAUT `~P <=> (P <=> F)`] th1]
283 (* Finds an instantination for the given term inside another term *)
284 let rec find_term_inst local_consts tm src_tm path =
285 try (term_match local_consts tm src_tm, true, path)
288 | Comb(l_tm, r_tm) ->
289 let r_inst, flag, s = find_term_inst local_consts tm l_tm (path ^ "l") in
290 if flag then (r_inst, flag, s)
292 find_term_inst local_consts tm r_tm (path ^ "r")
294 find_term_inst local_consts tm b_tm (path ^ "b")
295 | _ -> (([],[],[]), false, path);;
299 (* Rewrites the subterm at the given path using the given equation theorem *)
300 let path_rewrite path th tm =
301 let rec build path tm =
302 let n = String.length path in
307 let path' = String.sub path 1 (n - 1) in
309 let lhs, rhs = dest_comb tm in
310 let th0 = build path' lhs in
312 else if ch = 'r' then
313 let lhs, rhs = dest_comb tm in
314 let th0 = build path' rhs in
316 else if ch = 'b' then
317 let var, body = dest_abs tm in
318 let th0 = build path' body in
320 with Failure _ -> failwith ("ABS failed: (" ^ string_of_term var ^ ", " ^ string_of_thm th0)
322 failwith ("Bad path symbol: "^path) in
323 let res = build path tm in
324 let lhs = (lhand o concl) res in
325 if not (aconv lhs tm) then failwith ("path_rewrite: incorrect result [required: "^
326 (string_of_term tm)^"; obtained: "^
327 (string_of_term lhs))
332 let new_rewrite occ pat th g =
333 let goal_tm = snd g in
334 (* Free variables in the given theorem will not be matched *)
335 let local_consts = frees (concl th) in
336 (* Apply the pattern *)
337 let goal_subterm_path =
338 if pat = [] then "" else match_subterm_in_context (hd pat) goal_tm g in
339 let goal_subterm = follow_path goal_subterm_path goal_tm in
341 (* Local rewrite function *)
343 let concl_th = concl th in
344 let cond_flag = is_imp concl_th in
345 let match_fun = lhs o (if cond_flag then rand else I) in
347 (* Match the theorem *)
348 let lhs_tm = match_fun concl_th in
349 let ii, flag, path = find_term_inst local_consts lhs_tm goal_subterm goal_subterm_path in
351 failwith (string_of_term lhs_tm ^ " does not match any subterm in the goal")
353 let matched_th = INSTANTIATE ii th in
354 let matched_tm = (match_fun o concl) matched_th in
356 (* Find all matched subterms *)
357 let paths = find_all_paths (fun x -> aconv x matched_tm) goal_tm in
358 let paths = if occ = [] then paths else
359 map (fun i -> List.nth paths (i - 1)) occ in
361 (* Find all free variables in the matched theorem which do not correspond to free variables in
362 the matched subterm *)
363 let tm_frees = frees matched_tm in
364 let mth_frees = frees (concl matched_th) in
365 let vars = subtract mth_frees (union local_consts tm_frees) in
367 (* Construct the tactic for rewriting *)
368 let r_tac = fun th -> MAP_EVERY (fun path -> CONV_TAC (path_rewrite path th)) paths in
370 MP_TAC matched_th THEN ANTS_TAC THENL [ALL_TAC; DISCH_THEN r_tac]
374 let rec gen_vars vars th =
376 | v :: vs -> gen_vars vs (GEN v th)
378 let th2 = gen_vars vars matched_th in
379 MP_TAC th2 THEN PURE_REWRITE_TAC[LEFT_IMP_FORALL_THM] in
381 (* Try to rewrite with all given theorems *)
382 let th_list = break_conjuncts th in
383 let rec my_first th_list =
384 if length th_list = 1 then
385 rewrite (hd th_list) g
387 try rewrite (hd th_list) g
388 with Failure _ -> my_first (tl th_list) in
393 let th = ARITH_RULE `!n. n * 0 <= 1`;;
394 let tm = `m * 0 <= 1 <=> T`;;
396 e(new_rewrite [] [] th);;
398 let th = CONJ REAL_MUL_RINV REAL_MUL_LINV;;
399 let tm = `inv (x - y) * (x - y) + &1 = &1 + inv (x - y) * (x - y) + x * inv x`;;
400 let tm0 = `!x. inv (x - y) * (x - y) = &1`;;
404 e(new_rewrite [] [] (th));;
405 e(new_rewrite [] [] (GSYM th));;
406 e(new_rewrite [] [`_ + &1`] th);;
409 e(new_rewrite [] [] (ARITH_RULE `!x. x > 2 ==> (!n. n = 2 ==> ~(x < n))`));;
414 (* Rewrite tactic for usual and conditional theorems *)
415 let rewrite occ pat th g =
416 let rec match_theorem ffun th tm str =
417 try (PART_MATCH ffun th tm, true, str)
420 | Comb(l_tm, r_tm) ->
421 let r_th, flag, s = match_theorem ffun th l_tm (str ^ "l") in
422 if flag then (r_th, flag, s)
424 match_theorem ffun th r_tm (str ^ "r")
426 match_theorem ffun th b_tm (str ^ "b")
427 | _ -> (th, false, str) in
428 (* Initialize auxiliary variables *)
429 let goal_tm = snd g in
430 let th0 = PURE_REWRITE_RULE[IMP_IMP] th in
431 let concl_th = concl (SPEC_ALL th0) in
432 let cond_flag = is_imp concl_th in
433 let eq_tm = if cond_flag then rand concl_th else concl_th in
434 let match_fun = (if is_eq eq_tm then lhand else I) o (if cond_flag then rand else I) in
436 (* Apply the pattern *)
437 let goal_subterm_path =
438 if pat = [] then "" else match_subterm_in_context (hd pat) goal_tm g in
439 let goal_subterm = follow_path goal_subterm_path goal_tm in
441 (* Match the theorem *)
442 let matched_th, flag, path = match_theorem match_fun th0 goal_subterm goal_subterm_path in
444 failwith "lhs does not match any term in the goal"
446 let matched_tm = (match_fun o concl) matched_th in
447 (* Find all matched subterms *)
448 let paths = find_all_paths (fun x -> x = matched_tm) goal_tm in
449 let paths = if occ = [] then paths else
450 map (fun i -> List.nth paths (i - 1)) occ in
451 (* Find all free variables in the matched theorem which do not correspond to free variables in
452 the matched subterm *)
453 let tm_frees = frees matched_tm in
454 let th_frees = frees (concl th0) in
455 let mth_frees = frees (concl matched_th) in
456 let vars = subtract mth_frees (union th_frees tm_frees) in
458 let r_tac = fun th -> MAP_EVERY (fun path -> GEN_REWRITE_TAC (PATH_CONV path) [th]) paths in
460 (MP_TAC matched_th THEN ANTS_TAC THENL [ALL_TAC; DISCH_THEN r_tac]) g
464 let rec gen_vars vars th =
466 | v :: vs -> gen_vars vs (GEN v th)
468 let th2 = gen_vars vars matched_th in
469 (MP_TAC th2 THEN REWRITE_TAC[LEFT_IMP_FORALL_THM]) g;;
474 (* Analogue of the "done" tactic in SSReflect *)
475 let done_tac = ASM_REWRITE_TAC[] THEN FAIL_TAC "done: not all subgoals are proved";;
477 (* Simplification: /= *)
478 let simp_tac = SIMP_TAC[];;
481 (* Linear arithmetic simplification *)
482 let arith_tac = FIRST [ARITH_TAC; REAL_ARITH_TAC; INT_ARITH_TAC];;
486 let split_tac = FIRST [CONJ_TAC; EQ_TAC];;
490 (* Creates an abbreviation for the given term with the given name *)
491 let set_tac name tm (g : goal) =
492 let goal_tm = snd g in
495 follow_path (match_subterm_in_context tm goal_tm g) goal_tm
496 with Failure _ -> tm in
497 let tm1 = inst_all_free_vars tm0 g in
498 let abbrev_tm = mk_eq (mk_var (name, type_of tm1), tm1) in
499 (ABBREV_TAC abbrev_tm THEN POP_ASSUM (LABEL_TAC (name ^ "_def"))) g;;
501 (* Generates a fresh name for the given term *)
502 (* taking into account names of the provided variables *)
503 let generate_fresh_name names tm =
504 let rec find_name prefix n =
505 let name = prefix ^ (if n = 0 then "" else string_of_int n) in
506 if can (find (fun str -> str = name)) names then
507 find_name prefix (n + 1)
510 let prefix = if is_var tm then (fst o dest_var) tm else "x" in
514 (* Returns a variable which name does not conflict with names of given vars *)
515 let get_fresh_var var vars =
516 let names = map (fst o dest_var) vars in
517 mk_var (generate_fresh_name names var, type_of var);;
520 (* Matches all wild cards in the term and *)
521 (* instantinates all type variables in the given context *)
522 let prepare_term tm (g : goal) =
523 let goal_tm = snd g in
525 try follow_path (match_subterm_in_context tm goal_tm g) goal_tm
526 with Failure _ -> tm in
527 inst_all_free_vars tm0 g;;
529 (* Discharges a term by generalizing all occurences of this term first *)
530 let disch_tm_tac occs tm (g : goal) =
531 let tm0 = prepare_term tm g in
532 let name = generate_fresh_name ((fst o unzip) (get_context_vars g)) tm in
533 let new_tm = mk_var (name, type_of tm0) in
535 if occs = [] && is_var tm then
536 mk_var ((fst o dest_var) tm, type_of tm0)
538 let abbrev_tm = mk_eq (new_tm, tm0) in
539 (ABBREV_TAC abbrev_tm THEN
541 POP_ASSUM (fun th -> TRY (new_rewrite occs [] th)) THEN
542 SPEC_TAC (new_tm, new_tm1)) g;;
545 (* Discharges a theorem or a term *)
546 let disch_tac occs arg =
548 | Arg_theorem th -> MP_TAC th
549 | Arg_term tm -> disch_tm_tac occs tm
550 | _ -> failwith "disch_tac: a type cannot be discharged";;
556 let conj_imp = TAUT `(A /\ B ==> C) ==> (A ==> B ==> C)` in
557 let dummy_tm = `F` in
560 let ctm = concl th in
562 if is_forall ctm then
563 let (var_tm, _) = dest_forall ctm in
564 let var = get_fresh_var var_tm (thm_frees th @ local_consts) in
565 let th1 = SPEC var th in
566 let list, th0 = process th1 in
567 ("spec", var) :: list, th0
569 else if is_imp ctm then
570 let ant_tm, _ = dest_imp ctm in
572 if is_conj ant_tm then
573 let th1 = MATCH_MP conj_imp th in
574 let list, th0 = process th1 in
575 ("conj", dummy_tm) :: list, th0
578 let th1 = UNDISCH th in
579 let list, th0 = process th1 in
580 ("undisch", ant_tm) :: list, th0
587 (* reconstruct_thm *)
588 let reconstruct_thm =
589 let imp_conj = TAUT `(A ==> B ==> C) ==> (A /\ B ==> C)` in
590 let triv_ths = TAUT `((T ==> A) <=> A) /\ ((T /\ A) = A) /\ ((A /\ T) = A)` in
591 let rec reconstruct list th =
597 | ("spec", (_ as tm)) -> GEN tm th
598 | ("conj", _) -> MATCH_MP imp_conj th
599 | ("undisch", (_ as tm)) -> DISCH tm th
600 | _ -> failwith ("Unknown command: " ^ fst cmd) in
603 fun (cmd_list, th) ->
604 let th1 = reconstruct (rev cmd_list) th in
605 PURE_REWRITE_RULE[triv_ths] th1;;
609 let spec_var_th th n tm =
610 let cmd, th0 = process_thm (frees tm) th in
611 let ty = type_of tm in
612 let rec spec n list head =
614 | ("spec", (_ as var_tm)) :: t ->
616 let ty_ii = type_match (type_of var_tm) ty [] in
618 let th1 = reconstruct_thm (list, th0) in
619 let th2 = ISPEC tm th1 in
620 let tail, th0 = process_thm [] th2 in
621 let head1 = map (fun s, tm -> s, inst ty_ii tm) head in
624 spec (n - 1) t (head @ [hd list])
626 spec n t (head @ [hd list]))
627 | h :: t -> spec n t (head @ [h])
628 | [] -> failwith ("spec_var_th") in
629 reconstruct_thm (spec n cmd []);;
633 let match_mp_th ith n th =
634 let lconsts = thm_frees ith in
635 let cmd, th0 = process_thm (thm_frees th) ith in
637 let rec rec_match n list head =
639 | ("undisch", (_ as tm0)) :: t ->
641 let ii = term_match lconsts tm0 tm in
643 let th1 = INSTANTIATE_ALL ii th0 in
644 let th2 = PROVE_HYP th th1 in
645 let list0 = head @ (("undisch", `T`) :: t) in
646 let f_vars = frees tm0 in
648 (fun s, tm -> not (s = "spec" && mem tm f_vars)) list0 in
649 let list = map (fun s, tm -> s, instantiate ii tm) list1 in
652 rec_match (n - 1) t (head @ [hd list])
654 rec_match n t (head @ [hd list]))
655 | h :: t -> rec_match n t (head @ [h])
656 | [] -> failwith "match_mp_th: no match" in
657 let r = rec_match n cmd [] in
660 (* Introduces a subgoal *)
661 let have_gen_tac binders then_tac tm (g : goal) =
662 (* let tm0 = inst_all_free_vars tm g in *)
663 let tm1 = gen_variables binders tm in
664 let tm2 = prepare_term tm1 g in
665 (THENL_FIRST (SUBGOAL_THEN tm2 (fun th -> MP_TAC th THEN then_tac))
669 let have_tac then_tac tm (g : goal) =
670 (* let tm0 = inst_all_free_vars tm g in *)
671 let tm0 = prepare_term tm g in
672 (SUBGOAL_THEN tm0 (fun th -> MP_TAC th THEN then_tac)) g;;
677 let wlog_tac then_tac vars tm (g : goal) =
678 (* let tm0 = inst_all_free_vars tm g in *)
679 let tm0 = prepare_term tm g in
680 let vars0 = map (fun tm -> inst_all_free_vars tm g) vars in
682 let imp = list_mk_forall (vars0, mk_imp (tm0, g_tm)) in
683 (THENL_ROT 1 (SUBGOAL_THEN imp (fun th -> MP_TAC th THEN then_tac) THENL
684 [REPLICATE_TAC (length vars) GEN_TAC; ALL_TAC])) g;;
687 (* Provides a witness for an existential goal *)
688 let exists_tac tm (g : goal) =
689 let tm0 = inst_all_free_vars tm g in
690 let target_ty = (type_of o fst o dest_exists o snd) g in
691 let inst_ty = type_match (type_of tm0) target_ty [] in
692 let tm1 = inst inst_ty tm0 in
695 (* Instantiates the first type variable in the given theorem *)
696 let inst_first_type th ty =
697 let ty_vars = type_vars_in_term (concl th) in
699 failwith "inst_first_type: no type variables in the theorem"
701 INST_TYPE [(ty, hd ty_vars)] th;;
704 (* The first argument must be a theorem, the second argument is arbitrary *)
705 let combine_args arg1 arg2 =
706 let th1 = get_arg_thm arg1 in
710 (try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2)
712 (try ISPEC tm2 th1 with Failure _ -> spec_var_th th1 1 tm2)
713 | Arg_type ty2 -> inst_first_type th1 ty2 in
717 (* A temporary variable *)
718 let use_arg_then_result = ref TRUTH;;
720 (* Tests if the given id defines a theorem *)
723 Lexing.from_string ("use_arg_then_result := " ^ id ^ ";;") in
724 let ast = (!Toploop.parse_toplevel_phrase) lexbuf in
726 let _ = Toploop.execute_phrase false Format.std_formatter ast in
731 (* For a given id (string) finds an assumption or an existing theorem with the same name
732 and then applies the given tactic *)
733 let use_arg_then id (arg_tac:arg_type->tactic) (g:goal) =
737 let assumption = assoc id list in
738 Arg_theorem assumption
741 let vars = get_context_vars g in
742 let var = assoc id vars in
746 Lexing.from_string ("use_arg_then_result := " ^ id ^ ";;") in
747 let ast = (!Toploop.parse_toplevel_phrase) lexbuf in
750 Toploop.execute_phrase false Format.std_formatter ast
751 with _ -> failwith ("Bad identifier: " ^ id) in
752 Arg_theorem !use_arg_then_result in
756 (* The same effect as use_arg_then but the theorem is given explicitly*)
757 let use_arg_then2 (id, opt_thm) (arg_tac:arg_type->tactic) (g:goal) =
761 let assumption = assoc id list in
762 Arg_theorem assumption
765 let vars = get_context_vars g in
766 let var = assoc id vars in
769 if opt_thm <> [] then
770 Arg_theorem (hd opt_thm)
772 failwith ("Assumption is not found: " ^ id) in
776 let combine_args_then (tac:arg_type->tactic) arg1 arg2 (g:goal) =
777 let th1 = get_arg_thm arg1 in
781 (try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2)
783 let tm0 = prepare_term tm2 g in
784 (try ISPEC tm0 th1 with Failure _ -> spec_var_th th1 1 tm0)
785 | Arg_type ty2 -> inst_first_type th1 ty2 in
786 tac (Arg_theorem th0) g;;
791 (* Specializes a variable and applies the next tactic *)
792 let ispec_then tm (tac : thm_tactic) th (g : goal) =
793 let tm0 = prepare_term tm g in
794 let th0 = try ISPEC tm0 th with Failure _ -> spec_var_th th 1 tm0 in
798 let ISPEC_THEN tm (tac : thm_tactic) th (g : goal) =
799 let tm0 = inst_all_free_vars tm g in
800 tac (ISPEC tm0 th) g;;
804 let USE_THM_THEN th (tac : thm_tactic) =
808 let MATCH_MP_THEN th2 (tac : thm_tactic) th1 =
809 tac (MATCH_MP th1 th2);;
811 let match_mp_then th2 (tac : thm_tactic) th1 =
812 let th0 = try MATCH_MP th1 th2 with Failure _ -> match_mp_th th1 1 th2 in
816 let GSYM_THEN (tac : thm -> tactic) th =
820 let gsym_then (tac:arg_type->tactic) arg =
821 tac (Arg_theorem (GSYM (get_arg_thm arg)));;
824 (* The 'apply' tactic *)
826 let rec try_match th =
827 try MATCH_MP_TAC th g with Failure _ ->
828 let th0 = PURE_ONCE_REWRITE_RULE[IMP_IMP] th in
829 if th = th0 then failwith "apply_tac: no match"
833 try MATCH_ACCEPT_TAC th g with Failure _ ->
837 FIRST [MATCH_ACCEPT_TAC th; MATCH_MP_TAC th];; *)
840 (* The 'exact' tactic *)
841 (* TODO: do [done | by move => top; apply top], here apply top
842 works as ACCEPT_TAC with matching (rewriting) in some cases *)
843 let exact_tac = FIRST [done_tac; DISCH_THEN (fun th -> apply_tac th) THEN done_tac];;
847 (* Specializes the theorem using the given set of variables *)
848 let spec0 names vars =
850 try (assoc name vars, true)
851 with Failure _ -> (parse_term name, false) in
853 let name, ty = dest_var var in
854 let t, flag = find name in
858 (`:bool`, `:bool`) in
860 let ty_src, ty_dst = unzip (map find_type (frees tm)) in
861 let ty_inst = itlist2 type_match ty_src ty_dst [] in
863 let list = map find names in
864 let tm_list = map (fun tm, flag -> if flag then tm else inst_term tm) list in
868 let spec names = spec0 names (get_context_vars (top_realgoal()));;
871 let spec_mp names th g = MP_TAC (spec0 names (get_context_vars g) th) g;;
875 let bool_cases = ONCE_REWRITE_RULE[CONJ_ACI] bool_INDUCT;;
876 let list_cases = prove(`!P. P [] /\ (!(h:A) t. P (CONS h t)) ==> (!l. P l)`,
877 REPEAT STRIP_TAC THEN
878 MP_TAC (SPEC `l:(A)list` list_CASES) THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
879 FIRST_X_ASSUM (CHOOSE_THEN MP_TAC) THEN DISCH_THEN (CHOOSE_THEN MP_TAC) THEN
880 DISCH_THEN (fun th -> ASM_REWRITE_TAC[th]));;
881 let pair_cases = pair_INDUCT;;
882 let num_cases = prove(`!P. P 0 /\ (!n. P (SUC n)) ==> (!m. P m)`,
883 REPEAT STRIP_TAC THEN
884 MP_TAC (SPEC `m:num` num_CASES) THEN DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
885 FIRST_X_ASSUM (CHOOSE_THEN (fun th -> ASM_REWRITE_TAC[th])));;
886 let option_cases = option_INDUCT;;
889 let cases_table = Hashtbl.create 10;;
890 Hashtbl.add cases_table "bool" bool_cases;;
891 Hashtbl.add cases_table "list" list_cases;;
892 Hashtbl.add cases_table "prod" pair_cases;;
893 Hashtbl.add cases_table "num" num_cases;;
894 Hashtbl.add cases_table "option" option_cases;;
897 (* Induction theorems *)
898 let bool_elim = bool_cases;;
899 let list_elim = list_INDUCT;;
900 let pair_elim = pair_INDUCT;;
901 let num_elim = num_INDUCTION;;
902 let option_elim = option_INDUCT;;
904 let elim_table = Hashtbl.create 10;;
905 Hashtbl.add elim_table "bool" bool_elim;;
906 Hashtbl.add elim_table "list" list_elim;;
907 Hashtbl.add elim_table "prod" pair_elim;;
908 Hashtbl.add elim_table "num" num_elim;;
909 Hashtbl.add elim_table "option" option_elim;;
913 (* case: works only for (A /\ B) -> C; (A \/ B) -> C; (?x. P) -> Q; !(n:num). P; !(l:list(A)). P *)
915 let goal_tm = snd g in
916 if not (is_imp goal_tm) then
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 case_th = Hashtbl.find cases_table ty_name in
922 (MATCH_MP_TAC case_th THEN REPEAT CONJ_TAC) g
924 failwith "case: not imp or forall"
926 let tm = lhand goal_tm in
929 (DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN POP_ASSUM MP_TAC) g
931 else if is_disj tm then
932 (DISCH_THEN DISJ_CASES_TAC THEN POP_ASSUM MP_TAC) g
934 else if is_exists tm then
935 (ONCE_REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM]) g
937 failwith "case: not implemented";;
941 (* elim: works only for num and list *)
943 let goal_tm = snd g in
945 if is_forall goal_tm then
946 let var, _ = dest_forall goal_tm in
947 let ty_name = (fst o dest_type o type_of) var in
948 let induct_th = Hashtbl.find elim_table ty_name in
949 (MATCH_MP_TAC induct_th THEN REPEAT CONJ_TAC) g
951 failwith "elim: not forall";;
955 (* Instantiates the first type variable in the given theorem *)
956 let INST_FIRST_TYPE_THEN ty (then_tac:thm_tactic) th =
957 let ty_vars = type_vars_in_term (concl th) in
959 failwith "inst_first_type: no type variables in the theorem"
961 then_tac (INST_TYPE [(ty, hd ty_vars)] th);;
964 (* Replaces all occurrences of distinct '_' with unique variables *)
965 let transform_pattern pat_tm =
966 let names = ref (map (fst o dest_var) (frees pat_tm)) in
967 let rec transform tm =
970 let _ = names := (fst o dest_var) x_tm :: !names in
971 mk_abs (x_tm, transform b_tm)
972 | Comb(l_tm, r_tm) ->
973 mk_comb (transform l_tm, transform r_tm)
975 let name = generate_fresh_name !names tm in
976 let _ = names := name :: !names in
983 filter (fun tm -> ((fst o dest_var) tm).[0] = '_') (frees tm);;
986 filter (fun tm -> ((fst o dest_var) tm).[0] <> '_') (frees tm);;
990 let congr_tac pat_tm goal =
991 let goal_tm = snd goal in
992 let context_vars = get_context_vars goal in
993 let pat = transform_pattern pat_tm in
994 let f0_vars = nwild_frees pat in
995 let pattern = inst_context_vars context_vars f0_vars pat in
996 let const_pat = nwild_frees pattern in
997 let wild_pat = wild_frees pattern in
999 let lhs, rhs = dest_eq goal_tm in
1001 term_match const_pat pattern lhs, term_match const_pat pattern rhs in
1003 (fun tm -> mk_eq (instantiate lm tm, instantiate rm tm)) wild_pat in
1004 let eq_tm = itlist (curry mk_imp) eq_tms goal_tm in
1005 let eq_thm = EQT_ELIM (SIMP_CONV[] eq_tm) in
1006 (apply_tac eq_thm THEN REPEAT CONJ_TAC) goal;;
1009 (* Eliminates the first antecedent of a goal *)
1010 let elim_fst_ants_tac =
1011 let gen_elim_thm tm =
1012 let vars, tm1 = strip_forall tm in
1013 let ants_tm, concl_tm = dest_imp tm1 in
1014 let th1 = ASSUME (itlist (curry mk_forall) vars concl_tm) in
1015 let th2 = DISCH ants_tm (SPECL vars th1) in
1016 DISCH_ALL (itlist GEN vars th2) in
1018 let goal_tm = snd g in
1019 let elim_th = gen_elim_thm goal_tm in
1020 MATCH_MP_TAC elim_th g;;
1023 (* If a goal has the form ssreflect_eq ==> P then the equality is introduced as
1025 If a goal has the form !x. ssreflect_eq ==> P then the equality is eliminated *)
1026 let process_fst_eq_tac (g:goal) =
1027 let vars, g_tm = strip_forall (snd g) in
1030 let eq_tm = (rator o fst o dest_imp) g_tm in
1031 let label = (fst o dest_var o rand) eq_tm in
1032 if (fst o dest_const o rator) eq_tm = "ssreflect_eq" then
1033 if length vars = 0 then
1034 DISCH_THEN (LABEL_TAC label o PURE_ONCE_REWRITE_RULE[ssreflect_eq_def])
1039 with Failure _ -> ALL_TAC in
1043 (* Discharges a term by generalizing all occurences of this term first *)
1044 let disch_tm_eq_tac eq_name occs tm (g : goal) =
1045 let tm0 = prepare_term tm g in
1046 let name = generate_fresh_name ((fst o unzip) (get_context_vars g)) tm in
1047 let eq_var = mk_var (eq_name, aty) in
1048 let new_tm = mk_var (name, type_of tm0) in
1049 let abbrev_tm = mk_eq (new_tm, tm0) in
1050 (ABBREV_TAC abbrev_tm THEN
1051 EXPAND_TAC name THEN
1052 FIRST_ASSUM (fun th -> TRY (new_rewrite occs [] th)) THEN
1053 POP_ASSUM (MP_TAC o PURE_ONCE_REWRITE_RULE[GSYM (SPEC eq_var ssreflect_eq_def)]) THEN
1054 SPEC_TAC (new_tm, new_tm)) g;;
1057 (* Discharges a term and generates an equality *)
1058 let disch_eq_tac eq_name occs arg =
1059 disch_tm_eq_tac eq_name occs (get_arg_term arg);;