Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Tree: 9ca9644e35
Fetching contributors…

Cannot retrieve contributors at this time

176 lines (147 sloc) 5 KB
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
open Errors
open Util
open Names
open Term
open Termops
open Inductiveops
open Hipattern
open Tacmach
open Tacticals
open Tactics
open Misctypes
let introElimAssumsThen tac ba =
let nassums =
(fun acc b -> if b then acc+2 else acc+1)
0 ba.branchsign
let introElimAssums = tclDO nassums intro in
(tclTHEN introElimAssums (elim_on_ba tac ba))
let introCaseAssumsThen tac ba =
let case_thin_sign =
( (function b -> if b then [false;true] else [false])
let n1 = List.length case_thin_sign in
let n2 = List.length ba.branchnames in
let (l1,l2),l3 =
if n1 < n2 then List.chop n1 ba.branchnames, []
(ba.branchnames, []),
if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in
let introCaseAssums =
tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
(tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
(* The following tactic Decompose repeatedly applies the
elimination(s) rule(s) of the types satisfying the predicate
``recognizer'' onto a certain hypothesis. For example :
Require Elim.
Require Le.
Goal (y:nat){x:nat | (le O x)/\(le x y)}->{x:nat | (le O x)}.
Intros y H.
Decompose [sig and] H;EAuto.
Another example :
Goal (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
Intros A B C H; Decompose [and or] H; Assumption.
let elimHypThen tac id gl =
elimination_then tac ([],[]) (mkVar id) gl
let rec general_decompose_on_hyp recognizer =
ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> tclIDTAC)
and general_decompose_aux recognizer id =
(fun bas ->
tclTHEN (clear [id])
(tclMAP (general_decompose_on_hyp recognizer)
(ids_of_named_context bas.assums))))
(* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
pas si aucune élimination n'est possible *)
(* Meilleures stratégies mais perte de compatibilité *)
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)
(ifOnHyp recognizer (general_decompose_aux recognizer)
(fun id -> clear [id])));
exact_no_check c |] gl
let head_in gls indl t =
let ity,_ =
if !up_to_delta
then find_mrectype (pf_env gls) (project gls) t
else extract_mrectype t
in List.mem ity indl
with Not_found -> false
let decompose_these c l gls =
let indl = (* inductive_of*) l in
general_decompose (fun (_,t) -> head_in gls indl t) c gls
let decompose_nonrec c gls =
(fun (_,t) -> is_non_recursive_type t)
c gls
let decompose_and c gls =
(fun (_,t) -> is_record t)
c gls
let decompose_or c gls =
(fun (_,t) -> is_disjunction t)
c gls
let h_decompose l c = decompose_these c l
let h_decompose_or = decompose_or
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 induction_trailer abs_i abs_j bargs =
(tclDO (abs_j - abs_i) intro)
(fun id gls ->
let idty = pf_type_of gls (mkVar id) in
let fvty = global_vars (pf_env gls) idty in
let possible_bring_hyps =
( (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums
let (hyps,_) =
(fun (bring_ids,leave_ids) (cid,_,cidty 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
let ids = List.rev (ids_of_named_context hyps) in
[bring_hyps hyps; tclTRY (clear ids);
simple_elimination (mkVar id)])
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
(tclTHEN (tclDO abs_i intro)
(fun id ->
(introElimAssumsThen (induction_trailer abs_i abs_j))
([],[]) (mkVar id)))) gls
let h_double_induction = double_ind
Jump to Line
Something went wrong with that request. Please try again.