summaryrefslogtreecommitdiff
path: root/tactics/elim.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/elim.ml')
-rw-r--r--tactics/elim.ml149
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 16:29:03 +0000