diff options
Diffstat (limited to 'tactics/elim.ml')
-rw-r--r-- | tactics/elim.ml | 149 |
1 files changed, 72 insertions, 77 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index ea5b4eed..b7d5b102 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -1,35 +1,28 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util open Names open Term open Termops -open Environ -open Libnames -open Reduction open Inductiveops -open Proof_type -open Clenv open Hipattern -open Tacmach -open Tacticals +open Tacmach.New +open Tacticals.New open Tactics -open Hiddentac -open Genarg -open Tacexpr +open Misctypes +open Proofview.Notations let introElimAssumsThen tac ba = let nassums = List.fold_left (fun acc b -> if b then acc+2 else acc+1) - 0 ba.branchsign + 0 ba.Tacticals.branchsign in let introElimAssums = tclDO nassums intro in (tclTHEN introElimAssums (elim_on_ba tac ba)) @@ -38,17 +31,17 @@ let introCaseAssumsThen tac ba = let case_thin_sign = List.flatten (List.map (function b -> if b then [false;true] else [false]) - ba.branchsign) + ba.Tacticals.branchsign) in let n1 = List.length case_thin_sign in - let n2 = List.length ba.branchnames in + let n2 = List.length ba.Tacticals.branchnames in let (l1,l2),l3 = - if n1 < n2 then list_chop n1 ba.branchnames, [] + if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, [] else - (ba.branchnames, []), - if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in + (ba.Tacticals.branchnames, []), + if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in let introCaseAssums = - tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in + tclTHEN (intro_patterns l1) (intros_clearing l3) in (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) (* The following tactic Decompose repeatedly applies the @@ -69,118 +62,120 @@ Another example : Qed. *) -let elimHypThen tac id gl = - elimination_then tac ([],[]) (mkVar id) gl +let elimHypThen tac id = + elimination_then tac (mkVar id) let rec general_decompose_on_hyp recognizer = - ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> tclIDTAC) + ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) and general_decompose_aux recognizer id = elimHypThen (introElimAssumsThen (fun bas -> - tclTHEN (clear [id]) + tclTHEN (Proofview.V82.tactic (clear [id])) (tclMAP (general_decompose_on_hyp recognizer) - (ids_of_named_context bas.assums)))) + (ids_of_named_context bas.Tacticals.assums)))) id -(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste - pas si aucune élimination n'est possible *) +(* We should add a COMPLETE to be sure that the created hypothesis + doesn't stay if no elimination is possible *) -(* Meilleures stratégies mais perte de compatibilité *) -let tmphyp_name = id_of_string "_TmpHyp" +(* Best strategies but loss of compatibility *) +let tmphyp_name = Id.of_string "_TmpHyp" let up_to_delta = ref false (* true *) -let general_decompose recognizer c gl = - let typc = pf_type_of gl c in - tclTHENSV (cut typc) - [| tclTHEN (intro_using tmphyp_name) +let general_decompose recognizer c = + Proofview.Goal.enter begin fun gl -> + let type_of = pf_type_of gl in + let typc = type_of c in + tclTHENS (cut typc) + [ tclTHEN (intro_using tmphyp_name) (onLastHypId (ifOnHyp recognizer (general_decompose_aux recognizer) - (fun id -> clear [id]))); - exact_no_check c |] gl + (fun id -> Proofview.V82.tactic (clear [id])))); + Proofview.V82.tactic (exact_no_check c) ] + end -let head_in gls indl t = +let head_in indl t gl = + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in try let ity,_ = if !up_to_delta - then find_mrectype (pf_env gls) (project gls) t + then find_mrectype env sigma t else extract_mrectype t - in List.mem ity indl + in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl with Not_found -> false -let decompose_these c l gls = - let indl = (*List.map inductive_of*) l in - general_decompose (fun (_,t) -> head_in gls indl t) c gls +let decompose_these c l = + Proofview.Goal.enter begin fun gl -> + let indl = List.map (fun x -> x, Univ.Instance.empty) l in + general_decompose (fun (_,t) -> head_in indl t gl) c + end -let decompose_nonrec c gls = - general_decompose - (fun (_,t) -> is_non_recursive_type t) - c gls - -let decompose_and c gls = +let decompose_and c = general_decompose (fun (_,t) -> is_record t) - c gls + c -let decompose_or c gls = +let decompose_or c = general_decompose (fun (_,t) -> is_disjunction t) - c gls + c -let h_decompose l c = - Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) +let h_decompose l c = decompose_these c l -let h_decompose_or c = - Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) +let h_decompose_or = decompose_or -let h_decompose_and c = - Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) +let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) -let simple_elimination c gls = - simple_elimination_then (fun _ -> tclIDTAC) c gls +let simple_elimination c = + elimination_then (fun _ -> tclIDTAC) c let induction_trailer abs_i abs_j bargs = tclTHEN (tclDO (abs_j - abs_i) intro) (onLastHypId - (fun id gls -> - let idty = pf_type_of gls (mkVar id) in - let fvty = global_vars (pf_env gls) idty in + (fun id -> + Proofview.Goal.nf_enter begin fun gl -> + let idty = pf_type_of gl (mkVar id) in + let fvty = global_vars (pf_env gl) idty in let possible_bring_hyps = - (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums + (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums in let (hyps,_) = List.fold_left - (fun (bring_ids,leave_ids) (cid,_,cidty as d) -> + (fun (bring_ids,leave_ids) (cid,_,_ as d) -> if not (List.mem cid leave_ids) then (d::bring_ids,leave_ids) else (bring_ids,cid::leave_ids)) ([],fvty) possible_bring_hyps in let ids = List.rev (ids_of_named_context hyps) in - (tclTHENSEQ - [bring_hyps hyps; tclTRY (clear ids); + (tclTHENLIST + [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids)); simple_elimination (mkVar id)]) - gls)) - -let double_ind h1 h2 gls = - let abs_i = depth_of_quantified_hypothesis true h1 gls in - let abs_j = depth_of_quantified_hypothesis true h2 gls in - let (abs_i,abs_j) = - if abs_i < abs_j then (abs_i,abs_j) else - if abs_i > abs_j then (abs_j,abs_i) else - error "Both hypotheses are the same." in + end + )) + +let double_ind h1 h2 = + Proofview.Goal.nf_enter begin fun gl -> + let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in + let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in + let abs = + if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else + if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else + tclZEROMSG (Pp.str "Both hypotheses are the same.") in + abs >>= fun (abs_i,abs_j) -> (tclTHEN (tclDO abs_i intro) (onLastHypId (fun id -> elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) - ([],[]) (mkVar id)))) gls + (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) + end -let h_double_induction h1 h2 = - Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2) +let h_double_induction = double_ind |