From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tactics/tactics.ml | 1922 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1922 insertions(+) create mode 100644 tactics/tactics.ml (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml new file mode 100644 index 00000000..cab4f025 --- /dev/null +++ b/tactics/tactics.ml @@ -0,0 +1,1922 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* count (n+1) t + | LetIn(_,a,_,t) -> count n (subst1 a t) + | Cast(c,_) -> count n c + | _ -> n + in count 0 x + +(*********************************************) +(* Tactics *) +(*********************************************) + +(****************************************) +(* General functions *) +(****************************************) + +(* +let get_pairs_from_bindings = + let pair_from_binding = function + | [(Bindings binds)] -> binds + | _ -> error "not a binding list!" + in + List.map pair_from_binding +*) + +let string_of_inductive c = + try match kind_of_term c with + | Ind ind_sp -> + let (mib,mip) = Global.lookup_inductive ind_sp in + string_of_id mip.mind_typename + | _ -> raise Bound + with Bound -> error "Bound head variable" + +let rec head_constr_bound t l = + let t = strip_outer_cast(collapse_appl t) in + match kind_of_term t with + | Prod (_,_,c2) -> head_constr_bound c2 l + | LetIn (_,_,_,c2) -> head_constr_bound c2 l + | App (f,args) -> + head_constr_bound f (Array.fold_right (fun a l -> a::l) args l) + | Const _ -> t::l + | Ind _ -> t::l + | Construct _ -> t::l + | Var _ -> t::l + | _ -> raise Bound + +let head_constr c = + try head_constr_bound c [] with Bound -> error "Bound head variable" + +(* +let bad_tactic_args s l = + raise (RefinerError (BadTacticArgs (s,l))) +*) + +(******************************************) +(* Primitive tactics *) +(******************************************) + +let introduction = Tacmach.introduction +let intro_replacing = Tacmach.intro_replacing +let internal_cut = Tacmach.internal_cut +let internal_cut_rev = Tacmach.internal_cut_rev +let refine = Tacmach.refine +let convert_concl = Tacmach.convert_concl +let convert_hyp = Tacmach.convert_hyp +let thin = Tacmach.thin +let thin_body = Tacmach.thin_body + +(* Moving hypotheses *) +let move_hyp = Tacmach.move_hyp + +(* Renaming hypotheses *) +let rename_hyp = Tacmach.rename_hyp + +(* Refine as a fixpoint *) +let mutual_fix = Tacmach.mutual_fix + +let fix ido n = match ido with + | None -> mutual_fix (Pfedit.get_current_proof_name ()) n [] + | Some id -> mutual_fix id n [] + +(* Refine as a cofixpoint *) +let mutual_cofix = Tacmach.mutual_cofix + +let cofix = function + | None -> mutual_cofix (Pfedit.get_current_proof_name ()) [] + | Some id -> mutual_cofix id [] + +(**************************************************************) +(* Reduction and conversion tactics *) +(**************************************************************) + +type tactic_reduction = env -> evar_map -> constr -> constr + +(* The following two tactics apply an arbitrary + reduction function either to the conclusion or to a + certain hypothesis *) + +let reduct_in_concl redfun gl = + convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl + +let reduct_in_hyp redfun (id,_,(where,where')) gl = + let (_,c, ty) = pf_get_hyp gl id in + let redfun' = (*under_casts*) (pf_reduce redfun gl) in + match c with + | None -> + if where = InHypValueOnly then + errorlabstrm "" (pr_id id ++ str "has no value"); + if Options.do_translate () then where' := Some where; + convert_hyp_no_check (id,None,redfun' ty) gl + | Some b -> + let where = + if !Options.v7 & where = InHyp then InHypValueOnly else where in + let b' = if where <> InHypTypeOnly then redfun' b else b in + let ty' = if where <> InHypValueOnly then redfun' ty else ty in + if Options.do_translate () then where' := Some where; + convert_hyp_no_check (id,Some b',ty') gl + +let reduct_option redfun = function + | Some id -> reduct_in_hyp redfun id + | None -> reduct_in_concl redfun + +(* The following tactic determines whether the reduction + function has to be applied to the conclusion or + to the hypotheses. *) + +let redin_combinator redfun = + onClauses (reduct_option redfun) + +(* Now we introduce different instances of the previous tacticals *) +let change_and_check cv_pb t env sigma c = + if is_fconv cv_pb env sigma t c then + t + else + errorlabstrm "convert-check-hyp" (str "Not convertible") + +(* Use cumulutavity only if changing the conclusion not a subterm *) +let change_on_subterm cv_pb t = function + | None -> change_and_check cv_pb t + | Some occl -> contextually false occl (change_and_check CONV t) + +let change_in_concl occl t = reduct_in_concl (change_on_subterm CUMUL t occl) +let change_in_hyp occl t = reduct_in_hyp (change_on_subterm CONV t occl) + +let change_option occl t = function + Some id -> change_in_hyp occl t id + | None -> change_in_concl occl t + +let change occl c cls = + (match cls, occl with + ({onhyps=(Some(_::_::_)|None)}|{onhyps=Some(_::_);onconcl=true}), + Some _ -> + error "No occurrences expected when changing several hypotheses" + | _ -> ()); + onClauses (change_option occl c) cls + +(* Pour usage interne (le niveau User est pris en compte par reduce) *) +let red_in_concl = reduct_in_concl red_product +let red_in_hyp = reduct_in_hyp red_product +let red_option = reduct_option red_product +let hnf_in_concl = reduct_in_concl hnf_constr +let hnf_in_hyp = reduct_in_hyp hnf_constr +let hnf_option = reduct_option hnf_constr +let simpl_in_concl = reduct_in_concl nf +let simpl_in_hyp = reduct_in_hyp nf +let simpl_option = reduct_option nf +let normalise_in_concl = reduct_in_concl compute +let normalise_in_hyp = reduct_in_hyp compute +let normalise_option = reduct_option compute +let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname) +let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) +let unfold_option loccname = reduct_option (unfoldn loccname) +let pattern_option l = reduct_option (pattern_occs l) + +(* A function which reduces accordingly to a reduction expression, + as the command Eval does. *) + +let reduce redexp cl goal = + redin_combinator (reduction_of_redexp redexp) cl goal + +(* Unfolding occurrences of a constant *) + +let unfold_constr = function + | ConstRef sp -> unfold_in_concl [[],EvalConstRef sp] + | VarRef id -> unfold_in_concl [[],EvalVarRef id] + | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.") + +(*******************************************) +(* Introduction tactics *) +(*******************************************) + +let fresh_id avoid id gl = + next_global_ident_away true id (avoid@(pf_ids_of_hyps gl)) + +let id_of_name_with_default s = function + | Anonymous -> id_of_string s + | Name id -> id + +let default_id gl = function + | (name,None,t) -> + (match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl t)) with + | Sort (Prop _) -> (id_of_name_with_default "H" name) + | Sort (Type _) -> (id_of_name_with_default "X" name) + | _ -> anomaly "Wrong sort") + | (name,Some b,_) -> id_of_name_using_hdchar (pf_env gl) b name + +(* Non primitive introduction tactics are treated by central_intro + There is possibly renaming, with possibly names to avoid and + possibly a move to do after the introduction *) + +type intro_name_flag = + | IntroAvoid of identifier list + | IntroBasedOn of identifier * identifier list + | IntroMustBe of identifier + +let find_name decl gl = function + | IntroAvoid idl -> + let id = fresh_id idl (default_id gl decl) gl in id + | IntroBasedOn (id,idl) -> fresh_id idl id gl + | IntroMustBe id -> + let id' = fresh_id [] id gl in + if id' <> id then error ((string_of_id id)^" is already used"); + id' + +let build_intro_tac id = function + | None -> introduction id + | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) + +let rec intro_gen name_flag move_flag force_flag gl = + match kind_of_term (pf_concl gl) with + | Prod (name,t,_) -> + build_intro_tac (find_name (name,None,t) gl name_flag) move_flag gl + | LetIn (name,b,t,_) -> + build_intro_tac (find_name (name,Some b,t) gl name_flag) move_flag gl + | _ -> + if not force_flag then raise (RefinerError IntroNeedsProduct); + try + tclTHEN + (reduce (Red true) onConcl) + (intro_gen name_flag move_flag force_flag) gl + with Redelimination -> + errorlabstrm "Intro" (str "No product even after head-reduction") + +let intro_mustbe_force id = intro_gen (IntroMustBe id) None true +let intro_using id = intro_gen (IntroBasedOn (id,[])) None false +let intro_force force_flag = intro_gen (IntroAvoid []) None force_flag +let intro = intro_force false +let introf = intro_force true + +let introf_move_name destopt = intro_gen (IntroAvoid []) destopt true + +(* For backwards compatibility *) +let central_intro = intro_gen + +(**** Multiple introduction tactics ****) + +let rec intros_using = function + [] -> tclIDTAC + | str::l -> tclTHEN (intro_using str) (intros_using l) + +let intros = tclREPEAT (intro_force false) + +let intro_erasing id = tclTHEN (thin [id]) (intro_using id) + +let intros_replacing ids gls = + let rec introrec = function + | [] -> tclIDTAC + | id::tl -> + (tclTHEN (tclORELSE (intro_replacing id) + (tclORELSE (intro_erasing id) (* ?? *) + (intro_using id))) + (introrec tl)) + in + introrec ids gls + +(* User-level introduction tactics *) + +let intro_move idopt idopt' = match idopt with + | None -> intro_gen (IntroAvoid []) idopt' true + | Some id -> intro_gen (IntroMustBe id) idopt' true + +let pf_lookup_hypothesis_as_renamed env ccl = function + | AnonHyp n -> pf_lookup_index_as_renamed env ccl n + | NamedHyp id -> pf_lookup_name_as_renamed env ccl id + +let pf_lookup_hypothesis_as_renamed_gen red h gl = + let env = pf_env gl in + let rec aux ccl = + match pf_lookup_hypothesis_as_renamed env ccl h with + | None when red -> + aux (reduction_of_redexp (Red true) env (project gl) ccl) + | x -> x + in + try aux (pf_concl gl) + with Redelimination -> None + +let is_quantified_hypothesis id g = + match pf_lookup_hypothesis_as_renamed_gen true (NamedHyp id) g with + | Some _ -> true + | None -> false + +let msg_quantified_hypothesis = function + | NamedHyp id -> + str "hypothesis " ++ pr_id id + | AnonHyp n -> + int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++ + str " non dependent hypothesis" + +let depth_of_quantified_hypothesis red h gl = + match pf_lookup_hypothesis_as_renamed_gen red h gl with + | Some depth -> depth + | None -> + errorlabstrm "lookup_quantified_hypothesis" + (str "No " ++ msg_quantified_hypothesis h ++ + str " in current goal" ++ + if red then str " even after head-reduction" else mt ()) + +let intros_until_gen red h g = + tclDO (depth_of_quantified_hypothesis red h g) intro g + +let intros_until_id id = intros_until_gen true (NamedHyp id) +let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) + +let intros_until = intros_until_gen true +let intros_until_n = intros_until_n_gen true +let intros_until_n_wored = intros_until_n_gen false + +let try_intros_until tac = function + | NamedHyp id -> tclTHEN (tclTRY (intros_until_id id)) (tac id) + | AnonHyp n -> tclTHEN (intros_until_n n) (onLastHyp tac) + +let rec intros_move = function + | [] -> tclIDTAC + | (hyp,destopt) :: rest -> + tclTHEN (intro_gen (IntroMustBe hyp) destopt false) + (intros_move rest) + +let dependent_in_decl a (_,c,t) = + match c with + | None -> dependent a t + | Some body -> dependent a body || dependent a t + +let move_to_rhyp rhyp gl = + let rec get_lhyp lastfixed depdecls = function + | [] -> + (match rhyp with + | None -> lastfixed + | Some h -> anomaly ("Hypothesis should occur: "^ (string_of_id h))) + | (hyp,c,typ) as ht :: rest -> + if Some hyp = rhyp then + lastfixed + else if List.exists (occur_var_in_decl (pf_env gl) hyp) depdecls then + get_lhyp lastfixed (ht::depdecls) rest + else + get_lhyp (Some hyp) depdecls rest + in + let sign = pf_hyps gl in + let (hyp,c,typ as decl) = List.hd sign in + match get_lhyp None [decl] (List.tl sign) with + | None -> tclIDTAC gl + | Some hypto -> move_hyp true hyp hypto gl + +let rec intros_rmove = function + | [] -> tclIDTAC + | (hyp,destopt) :: rest -> + tclTHENLIST [ introduction hyp; + move_to_rhyp destopt; + intros_rmove rest ] + +(****************************************************) +(* Resolution tactics *) +(****************************************************) + +(* Refinement tactic: unification with the head of the head normal form + * of the type of a term. *) + +let apply_type hdcty argl gl = + refine (applist (mkCast (mkMeta (new_meta()),hdcty),argl)) gl + +let apply_term hdc argl gl = + refine (applist (hdc,argl)) gl + +let bring_hyps hyps = + if hyps = [] then Refiner.tclIDTAC + else + (fun gl -> + let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in + let f = mkCast (mkMeta (new_meta()),newcl) in + refine_no_check (mkApp (f, instance_from_named_context hyps)) gl) + +(* Resolution with missing arguments *) + +let apply_with_bindings (c,lbind) gl = + let apply = + match kind_of_term c with + | Lambda _ -> res_pf_cast + | _ -> res_pf + in + let (wc,kONT) = startWalk gl in + (* The actual type of the theorem. It will be matched against the + goal. If this fails, then the head constant will be unfolded step by + step. *) + let thm_ty0 = nf_betaiota (w_type_of wc c) in + let rec try_apply thm_ty = + try + let n = nb_prod thm_ty - nb_prod (pf_concl gl) in + if n<0 then error "Apply: theorem has not enough premisses."; + let clause = make_clenv_binding_apply wc n (c,thm_ty) lbind in + apply kONT clause gl + with (RefinerError _|UserError _|Failure _) as exn -> + let red_thm = + try red_product (w_env wc) (w_Underlying wc) thm_ty + with (Redelimination | UserError _) -> raise exn in + try_apply red_thm in + try try_apply thm_ty0 + with (RefinerError _|UserError _|Failure _) -> + (* Last chance: if the head is a variable, apply may try + second order unification *) + let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in + apply kONT clause gl + +let apply c = apply_with_bindings (c,NoBindings) + +let apply_list = function + | c::l -> apply_with_bindings (c,ImplicitBindings l) + | _ -> assert false + +(* Resolution with no reduction on the type *) + +let apply_without_reduce c gl = + let (wc,kONT) = startWalk gl in + let clause = mk_clenv_type_of wc c in + res_pf kONT clause gl + +(* A useful resolution tactic which, if c:A->B, transforms |- C into + |- B -> C and |- A + + ------------------- + Gamma |- c : A -> B Gamma |- ?2 : A + ---------------------------------------- + Gamma |- B Gamma |- ?1 : B -> C + ----------------------------------------------------- + Gamma |- ? : C + + Ltac lapply c := + let ty := check c in + match eval hnf in ty with + ?A -> ?B => cut B; [ idtac | apply c ] + end. +*) + +let cut_and_apply c gl = + let goal_constr = pf_concl gl in + match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with + | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> + tclTHENLAST + (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())]) + (apply_term c [mkMeta (new_meta())]) gl + | _ -> error "Imp_elim needs a non-dependent product" + +(**************************) +(* Cut tactics *) +(**************************) + +let assert_tac first na c gl = + match kind_of_term (hnf_type_of gl c) with + | Sort s -> + let id = match na with + | Anonymous -> + let d = match s with Prop _ -> "H" | Type _ -> "X" in + fresh_id [] (id_of_string d) gl + | Name id -> id + in + (if first then internal_cut else internal_cut_rev) id c gl + | _ -> error "Not a proposition or a type" + +let true_cut = assert_tac true + +let cut c gl = + match kind_of_term (hnf_type_of gl c) with + | Sort _ -> + let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in + let t = mkProd (Anonymous, c, pf_concl gl) in + tclTHENFIRST + (internal_cut_rev id c) + (tclTHEN (apply_type t [mkVar id]) (thin [id])) + gl + | _ -> error "Not a proposition or a type" + +let cut_intro t = tclTHENFIRST (cut t) intro + +let cut_replacing id t = + tclTHENFIRST + (cut t) + (tclORELSE + (intro_replacing id) + (tclORELSE (intro_erasing id) + (intro_using id))) + +let cut_in_parallel l = + let rec prec = function + | [] -> tclIDTAC + | h::t -> tclTHENFIRST (cut h) (prec t) + in + prec (List.rev l) + +(**************************) +(* Generalize tactics *) +(**************************) + +let generalize_goal gl c cl = + let t = pf_type_of gl c in + match kind_of_term c with + | Var id -> + (* The choice of remembering or not a non dependent name has an impact + on the future Intro naming strategy! *) + (* if dependent c cl then mkNamedProd id t cl + else mkProd (Anonymous,t,cl) *) + mkNamedProd id t cl + | _ -> + let cl' = subst_term c cl in + if noccurn 1 cl' then + mkProd (Anonymous,t,cl) + (* On ne se casse pas la tete : on prend pour nom de variable + la premiere lettre du type, meme si "ci" est une + constante et qu'on pourrait prendre directement son nom *) + else + prod_name (Global.env()) (Anonymous, t, cl') + +let generalize_dep c gl = + let env = pf_env gl in + let sign = pf_hyps gl in + let init_ids = ids_of_named_context (Global.named_context()) in + let rec seek d toquant = + if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant + or dependent_in_decl c d then + d::toquant + else + toquant in + let to_quantify = Sign.fold_named_context seek sign ~init:[] in + let to_quantify_rev = List.rev to_quantify in + let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in + let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in + let tothin' = + match kind_of_term c with + | Var id when mem_named_context id sign & not (List.mem id init_ids) + -> id::tothin + | _ -> tothin + in + let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in + let cl'' = generalize_goal gl c cl' in + let args = Array.to_list (instance_from_named_context to_quantify_rev) in + tclTHEN + (apply_type cl'' (c::args)) + (thin (List.rev tothin')) + gl + +let generalize lconstr gl = + let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in + apply_type newcl lconstr gl + +(* Faudra-t-il une version avec plusieurs args de generalize_dep ? +Cela peut-être troublant de faire "Generalize Dependent H n" dans +"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la +généralisation dépendante par n. + +let quantify lconstr = + List.fold_right + (fun com tac -> tclTHEN tac (tactic_com generalize_dep c)) + lconstr + tclIDTAC +*) + +(* A dependent cut rule à la sequent calculus + ------------------------------------------ + Sera simplifiable le jour où il y aura un let in primitif dans constr + + [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms + [...x1:T1(c),...,x2:T2(c),... |- G(c)] into + [...x:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or + [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true + + [occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted; + if [occ_hyp = []] and [occ_ccl = None] then [c] is substituted + wherever it occurs, otherwise [c] is substituted only in hyps + present in [occ_hyps] at the specified occurrences (everywhere if + the list of occurrences is empty), and in the goal at the specified + occurrences if [occ_goal] is not [None]; + + if name = Anonymous, the name is build from the first letter of the type; + + The tactic first quantify the goal over x1, x2,... then substitute then + re-intro x1, x2,... at their initial place ([marks] is internally + used to remember the place of x1, x2, ...: it is the list of hypotheses on + the left of each x1, ...). +*) + + + +let occurrences_of_hyp id cls = + let rec hyp_occ = function + [] -> None + | (id',occs,hl)::_ when id=id' -> Some occs + | _::l -> hyp_occ l in + match cls.onhyps with + None -> Some [] + | Some l -> hyp_occ l + +let occurrences_of_goal cls = + if cls.onconcl then Some cls.concl_occs else None + +let everywhere cls = (cls=allClauses) + +(* +(* Implementation with generalisation then re-intro: introduces noise *) +(* in proofs *) + +let letin_abstract id c occs gl = + let env = pf_env gl in + let compute_dependency _ (hyp,_,_ as d) ctxt = + let d' = + try + match occurrences_of_hyp hyp occs with + | None -> raise Not_found + | Some occ -> + let newdecl = subst_term_occ_decl occ c d in + if d = newdecl then + if not (everywhere occs) + then raise (RefinerError (DoesNotOccurIn (c,hyp))) + else raise Not_found + else + (subst1_decl (mkVar id) newdecl, true) + with Not_found -> + (d,List.exists + (fun ((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt) + in d'::ctxt + in + let ctxt' = fold_named_context compute_dependency env ~init:[] in + let compute_marks ((depdecls,marks as accu),lhyp) ((hyp,_,_) as d,b) = + if b then ((d::depdecls,(hyp,lhyp)::marks), lhyp) + else (accu, Some hyp) in + let (depdecls,marks),_ = List.fold_left compute_marks (([],[]),None) ctxt' in + let ccl = match occurrences_of_goal occs with + | None -> pf_concl gl + | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) + in + (depdecls,marks,ccl) + +let letin_tac with_eq name c occs gl = + let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in + let id = + if name = Anonymous then fresh_id [] x gl else + if not (mem_named_context x (pf_hyps gl)) then x else + error ("The variable "^(string_of_id x)^" is already declared") in + let (depdecls,marks,ccl)= letin_abstract id c occs gl in + let t = pf_type_of gl c in + let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in + let args = Array.to_list (instance_from_named_context depdecls) in + let newcl = mkNamedLetIn id c t tmpcl in + let lastlhyp = if marks=[] then None else snd (List.hd marks) in + tclTHENLIST + [ apply_type newcl args; + thin (List.map (fun (id,_,_) -> id) depdecls); + intro_gen (IntroMustBe id) lastlhyp false; + if with_eq then tclIDTAC else thin_body [id]; + intros_move marks ] gl +*) + +(* Implementation without generalisation: abbrev will be lost in hyps in *) +(* in the extracted proof *) + +let letin_abstract id c occs gl = + let env = pf_env gl in + let compute_dependency _ (hyp,_,_ as d) depdecls = + match occurrences_of_hyp hyp occs with + | None -> depdecls + | Some occ -> + let newdecl = subst_term_occ_decl occ c d in + if d = newdecl then + if not (everywhere occs) + then raise (RefinerError (DoesNotOccurIn (c,hyp))) + else depdecls + else + (subst1_decl (mkVar id) newdecl)::depdecls in + let depdecls = fold_named_context compute_dependency env ~init:[] in + let ccl = match occurrences_of_goal occs with + | None -> pf_concl gl + | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in + let lastlhyp = if depdecls = [] then None else Some(pi1(list_last depdecls)) in + (depdecls,lastlhyp,ccl) + +let letin_tac with_eq name c occs gl = + let id = + let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in + if name = Anonymous then fresh_id [] x gl else + if not (mem_named_context x (pf_hyps gl)) then x else + error ("The variable "^(string_of_id x)^" is already declared") in + let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in + let t = pf_type_of gl c in + let newcl = mkNamedLetIn id c t ccl in + tclTHENLIST + [ convert_concl_no_check newcl; + intro_gen (IntroMustBe id) lastlhyp true; + if with_eq then tclIDTAC else thin_body [id]; + tclMAP convert_hyp_no_check depdecls ] gl + +let check_hypotheses_occurrences_list env (_,occl) = + let rec check acc = function + | (hyp,_) :: rest -> + if List.mem hyp acc then + error ("Hypothesis "^(string_of_id hyp)^" occurs twice"); + if not (mem_named_context hyp (named_context env)) then + error ("No such hypothesis: " ^ (string_of_id hyp)); + check (hyp::acc) rest + | [] -> () + in check [] occl + +let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} + +(* Tactic Assert (b=false) and Pose (b=true): + the behaviour of Pose is corrected by the translator. + not that of Assert *) +let forward b na c = + let wh = if !Options.v7 && b then onConcl else nowhere in + letin_tac b na c wh + +(********************************************************************) +(* Exact tactics *) +(********************************************************************) + +let exact_check c gl = + let concl = (pf_concl gl) in + let ct = pf_type_of gl c in + if pf_conv_x_leq gl ct concl then + refine_no_check c gl + else + error "Not an exact proof" + +let exact_no_check = refine_no_check + +let exact_proof c gl = + (* on experimente la synthese d'ise dans exact *) + let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl) + in refine_no_check c gl + +let (assumption : tactic) = fun gl -> + let concl = pf_concl gl in + let hyps = pf_hyps gl in + let rec arec only_eq = function + | [] -> + if only_eq then arec false hyps else error "No such assumption" + | (id,c,t)::rest -> + if (only_eq & eq_constr t concl) + or (not only_eq & pf_conv_x_leq gl t concl) + then refine_no_check (mkVar id) gl + else arec only_eq rest + in + arec true hyps + +(*****************************************************************) +(* Modification of a local context *) +(*****************************************************************) + +(* This tactic enables the user to remove hypotheses from the signature. + * Some care is taken to prevent him from removing variables that are + * subsequently used in other hypotheses or in the conclusion of the + * goal. *) + +let clear ids gl = (* avant seul dyn_clear n'echouait pas en [] *) + if ids=[] then tclIDTAC gl else with_check (thin ids) gl + +let clear_body = thin_body + +(* Takes a list of booleans, and introduces all the variables + * quantified in the goal which are associated with a value + * true in the boolean list. *) + +let rec intros_clearing = function + | [] -> tclIDTAC + | (false::tl) -> tclTHEN intro (intros_clearing tl) + | (true::tl) -> + tclTHENLIST + [ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl] + +(* Adding new hypotheses *) + +let new_hyp mopt (c,lbind) g = + let (wc,kONT) = startWalk g in + let clause = make_clenv_binding wc (c,w_type_of wc c) lbind in + let (thd,tstack) = whd_stack (clenv_instance_template clause) in + let nargs = List.length tstack in + let cut_pf = + applist(thd, + match mopt with + | Some m -> if m < nargs then list_firstn m tstack else tstack + | None -> tstack) + in + (tclTHENLAST (tclTHEN (kONT clause.hook) + (cut (pf_type_of g cut_pf))) + ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g + +(************************) +(* Introduction tactics *) +(************************) + +let constructor_tac boundopt i lbind gl = + let cl = pf_concl gl in + let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in + let nconstr = + Array.length (snd (Global.lookup_inductive mind)).mind_consnames + and sigma = project gl in + if i=0 then error "The constructors are numbered starting from 1"; + if i > nconstr then error "Not enough constructors"; + begin match boundopt with + | Some expctdnum -> + if expctdnum <> nconstr then + error "Not the expected number of constructors" + | None -> () + end; + let cons = mkConstruct (ith_constructor_of_inductive mind i) in + let apply_tac = apply_with_bindings (cons,lbind) in + (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl + +let one_constructor i = constructor_tac None i + +(* Try to apply the constructor of the inductive definition followed by + a tactic t given as an argument. + Should be generalize in Constructor (Fun c : I -> tactic) + *) + +let any_constructor tacopt gl = + let t = match tacopt with None -> tclIDTAC | Some t -> t in + let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in + let nconstr = + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in + if nconstr = 0 then error "The type has no constructors"; + tclFIRST (List.map (fun i -> tclTHEN (one_constructor i NoBindings) t) + (interval 1 nconstr)) gl + +let left = constructor_tac (Some 2) 1 +let simplest_left = left NoBindings + +let right = constructor_tac (Some 2) 2 +let simplest_right = right NoBindings + +let split = constructor_tac (Some 1) 1 +let simplest_split = split NoBindings + +(********************************************) +(* Elimination tactics *) +(********************************************) + + +(* kONT : ?? + * wc : ?? + * elimclause : ?? + * inclause : ?? + * gl : the current goal +*) + +let last_arg c = match kind_of_term c with + | App (f,cl) -> array_last cl + | _ -> anomaly "last_arg" + +let elimination_clause_scheme kONT elimclause indclause allow_K gl = + let indmv = + (match kind_of_term (last_arg (clenv_template elimclause).rebus) with + | Meta mv -> mv + | _ -> errorlabstrm "elimination_clause" + (str "The type of elimination clause is not well-formed")) + in + let elimclause' = clenv_fchain indmv elimclause indclause in + elim_res_pf kONT elimclause' allow_K gl + +(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and + * refine fails *) + +let type_clenv_binding wc (c,t) lbind = + clenv_instance_template_type (make_clenv_binding wc (c,t) lbind) + +(* + * Elimination tactic with bindings and using an arbitrary + * elimination constant called elimc. This constant should end + * with a clause (x:I)(P .. ), where P is a bound variable. + * The term c is of type t, which is a product ending with a type + * matching I, lbindc are the expected terms for c arguments + *) + +let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl = + let (wc,kONT) = startWalk gl in + let ct = pf_type_of gl c in + let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in + let indclause = make_clenv_binding wc (c,t) lbindc in + let elimt = w_type_of wc elimc in + let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in + elimination_clause_scheme kONT elimclause indclause allow_K gl + +(* Elimination tactic with bindings but using the default elimination + * constant associated with the type. *) + +let find_eliminator c gl = + let env = pf_env gl in + let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in + let s = elimination_sort_of_goal gl in + Indrec.lookup_eliminator ind s +(* with Not_found -> + let dir, base = repr_path (path_of_inductive env ind) in + let id = Indrec.make_elimination_ident base s in + errorlabstrm "default_elim" + (str "Cannot find the elimination combinator :" ++ + pr_id id ++ spc () ++ + str "The elimination of the inductive definition :" ++ + pr_id base ++ spc () ++ str "on sort " ++ + spc () ++ print_sort (new_sort_in_family s) ++ + str " is probably not allowed") +(* lookup_eliminator prints the message *) *) +let default_elim (c,lbindc) gl = + general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl + +let elim_in_context (c,_ as cx) elim gl = + match elim with + | Some (elimc,lbindelimc) -> general_elim cx (elimc,lbindelimc) gl + | None -> general_elim cx (find_eliminator c gl,NoBindings) gl + +let elim (c,lbindc as cx) elim = + match kind_of_term c with + | Var id when lbindc = NoBindings -> + tclTHEN (tclTRY (intros_until_id id)) (elim_in_context cx elim) + | _ -> elim_in_context cx elim + +(* The simplest elimination tactic, with no substitutions at all. *) + +let simplest_elim c = default_elim (c,NoBindings) + +(* Elimination in hypothesis *) + +let elimination_in_clause_scheme kONT id elimclause indclause = + let (hypmv,indmv) = + match clenv_independent elimclause with + [k1;k2] -> (k1,k2) + | _ -> errorlabstrm "elimination_clause" + (str "The type of elimination clause is not well-formed") in + let elimclause' = clenv_fchain indmv elimclause indclause in + let hyp = mkVar id in + let hyp_typ = clenv_type_of elimclause' hyp in + let hypclause = + mk_clenv_from_n elimclause'.hook (Some 0) (hyp, hyp_typ) in + let elimclause'' = clenv_fchain hypmv elimclause' hypclause in + let new_hyp_prf = clenv_instance_template elimclause'' in + let new_hyp_typ = clenv_instance_template_type elimclause'' in + if eq_constr hyp_typ new_hyp_typ then + errorlabstrm "general_rewrite_in" + (str "Nothing to rewrite in " ++ pr_id id); + tclTHEN + (kONT elimclause''.hook) + (tclTHENS + (cut new_hyp_typ) + [ (* Try to insert the new hyp at the same place *) + tclORELSE (intro_replacing id) + (tclTHEN (clear [id]) (introduction id)); + refine_no_check new_hyp_prf]) + +let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = + let (wc,kONT) = startWalk gl in + let ct = pf_type_of gl c in + let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in + let indclause = make_clenv_binding wc (c,t) lbindc in + let elimt = w_type_of wc elimc in + let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in + elimination_in_clause_scheme kONT id elimclause indclause gl + +(* Case analysis tactics *) + +let general_case_analysis_in_context (c,lbindc) gl = + let env = pf_env gl in + let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let sigma = project gl in + let sort = elimination_sort_of_goal gl in + let case = if occur_term c (pf_concl gl) then Indrec.make_case_dep + else Indrec.make_case_gen in + let elim = case env sigma mind sort in + general_elim (c,lbindc) (elim,NoBindings) gl + +let general_case_analysis (c,lbindc as cx) = + match kind_of_term c with + | Var id when lbindc = NoBindings -> + tclTHEN (tclTRY (intros_until_id id)) + (general_case_analysis_in_context cx) + | _ -> + general_case_analysis_in_context cx + +let simplest_case c = general_case_analysis (c,NoBindings) + +(*****************************) +(* Decomposing introductions *) +(*****************************) + +let clear_last = tclLAST_HYP (fun c -> (clear [destVar c])) +let case_last = tclLAST_HYP simplest_case + +let rec intro_pattern destopt = function + | IntroWildcard -> + tclTHEN intro clear_last + | IntroIdentifier id -> + intro_gen (IntroMustBe id) destopt true + | IntroOrAndPattern l -> + tclTHEN introf + (tclTHENS + (tclTHEN case_last clear_last) + (List.map (intros_pattern destopt) l)) + +and intros_pattern destopt l = tclMAP (intro_pattern destopt) l + +let intro_patterns = function + | [] -> tclREPEAT intro + | l -> intros_pattern None l + +(* + * A "natural" induction tactic + * + - [H0:T0, ..., Hi:Ti, hyp0:P->I(args), Hi+1:Ti+1, ..., Hn:Tn |-G] is the goal + - [hyp0] is the induction hypothesis + - we extract from [args] the variables which are not rigid parameters + of the inductive type, this is [indvars] (other terms are forgotten); + [indhyps] are the ones which actually are declared in context + (done in [find_atomic_param_of_ind]) + - we look for all hyps depending of [hyp0] or one of [indvars]: + this is [dephyps] of types [deptyps] respectively + - [statuslist] tells for each hyps in [dephyps] after which other hyp + fixed in the context they must be moved (when induction is done) + - [hyp0succ] is the name of the hyp fixed in the context after which to + move the subterms of [hyp0succ] in the i-th branch where it is supposed + to be the i-th constructor of the inductive type. + + Strategy: (cf in [induction_from_context]) + - requantify and clear all [dephyps] + - apply induction on [hyp0] + - clear [indhyps] and [hyp0] + - in the i-th subgoal, intro the arguments of the i-th constructor + of the inductive type after [hyp0succ] (done in + [induct_discharge]) let the induction hypotheses on top of the + hyps because they may depend on variables between [hyp0] and the + top. A counterpart is that the dep hyps programmed to be intro-ed + on top must now be intro-ed after the induction hypotheses + - move each of [dephyps] at the right place following the + [statuslist] + + *) + +let rec str_intro_pattern = function + | IntroOrAndPattern pll -> + "["^(String.concat "|" + (List.map + (fun pl -> String.concat " " (List.map str_intro_pattern pl)) pll)) + ^"]" + | IntroWildcard -> "_" + | IntroIdentifier id -> string_of_id id + +let check_unused_names names = + if names <> [] & Options.is_verbose () then + let s = if List.tl names = [] then " " else "s " in + let names = String.concat " " (List.map str_intro_pattern names) in + warning ("Unused introduction pattern"^s^": "^names) + +let rec first_name_buggy = function + | IntroOrAndPattern [] -> None + | IntroOrAndPattern ([]::l) -> first_name_buggy (IntroOrAndPattern l) + | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p + | IntroWildcard -> None + | IntroIdentifier id -> Some id + +type elim_arg_kind = RecArg | IndArg | OtherArg + +let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,force,rnames) gl = + let avoid7 = avoid7 @ avoid' in + let avoid8 = avoid8 @ avoid' in + let (lstatus,rstatus) = statuslists in + let tophyp = ref None in + let rec peel_tac ra names gl = match ra with + | (RecArg,(recvarname7,recvarname8)) :: + (IndArg,(hyprecname7,hyprecname8)) :: ra' -> + let recpat,hyprec,names = match names with + | [] -> + let idrec7 = (fresh_id avoid7 recvarname7 gl) in + let idrec8 = (fresh_id avoid8 recvarname8 gl) in + let idhyp7 = (fresh_id avoid7 hyprecname7 gl) in + let idhyp8 = (fresh_id avoid8 hyprecname8 gl) in + if Options.do_translate() & + (idrec7 <> idrec8 or idhyp7 <> idhyp8) + then force := true; + let idrec = if !Options.v7 then idrec7 else idrec8 in + let idhyp = if !Options.v7 then idhyp7 else idhyp8 in + (IntroIdentifier idrec, IntroIdentifier idhyp, []) + | [IntroIdentifier id as pat] -> + let id7 = next_ident_away (add_prefix "IH" id) avoid7 in + let id8 = next_ident_away (add_prefix "IH" id) avoid8 in + if Options.do_translate() & id7 <> id8 then force := true; + let id = if !Options.v7 then id7 else id8 in + (pat, IntroIdentifier id, []) + | [pat] -> + let idhyp7 = (fresh_id avoid7 hyprecname7 gl) in + let idhyp8 = (fresh_id avoid8 hyprecname8 gl) in + if Options.do_translate() & idhyp7 <> idhyp8 then force := true; + let idhyp = if !Options.v7 then idhyp7 else idhyp8 in + (pat, IntroIdentifier idhyp, []) + | pat1::pat2::names -> (pat1,pat2,names) in + (* This is buggy for intro-or-patterns with different first hypnames *) + if !tophyp=None then tophyp := first_name_buggy hyprec; + rnames := !rnames @ [recpat; hyprec]; + tclTHENLIST + [ intros_pattern destopt [recpat]; + intros_pattern None [hyprec]; + peel_tac ra' names ] gl + | (IndArg,(hyprecname7,hyprecname8)) :: ra' -> + (* Rem: does not happen in Coq schemes, only in user-defined schemes *) + let pat,names = match names with + | [] -> IntroIdentifier (fresh_id avoid8 hyprecname8 gl), [] + | pat::names -> pat,names in + rnames := !rnames @ [pat]; + tclTHEN (intros_pattern destopt [pat]) (peel_tac ra' names) gl + | (RecArg,(recvarname7,recvarname8)) :: ra' -> + let introtac,names = match names with + | [] -> + let id8 = fresh_id avoid8 recvarname8 gl in + let i = + if !Options.v7 then IntroAvoid avoid7 else IntroMustBe id8 + in + (* For translator *) + let id7 = fresh_id avoid7 (default_id gl + (match kind_of_term (pf_concl gl) with + | Prod (name,t,_) -> (name,None,t) + | LetIn (name,b,t,_) -> (name,Some b,t) + | _ -> assert false)) gl in + if Options.do_translate() & id7 <> id8 then force := true; + let id = if !Options.v7 then id7 else id8 in + rnames := !rnames @ [IntroIdentifier id]; + intro_gen i destopt false, [] + | pat::names -> + rnames := !rnames @ [pat]; + intros_pattern destopt [pat],names in + tclTHEN introtac (peel_tac ra' names) gl + | (OtherArg,_) :: ra' -> + let introtac,names = match names with + | [] -> + (* For translator *) + let id7 = fresh_id avoid7 (default_id gl + (match kind_of_term (pf_concl gl) with + | Prod (name,t,_) -> (name,None,t) + | LetIn (name,b,t,_) -> (name,Some b,t) + | _ -> assert false)) gl in + let id8 = fresh_id avoid8 (default_id gl + (match kind_of_term (pf_concl gl) with + | Prod (name,t,_) -> (name,None,t) + | LetIn (name,b,t,_) -> (name,Some b,t) + | _ -> assert false)) gl in + if Options.do_translate() & id7 <> id8 then force := true; + let id = if !Options.v7 then id7 else id8 in + let avoid = if !Options.v7 then avoid7 else avoid8 in + rnames := !rnames @ [IntroIdentifier id]; + intro_gen (IntroAvoid avoid) destopt false, [] + | pat::names -> + rnames := !rnames @ [pat]; + intros_pattern destopt [pat],names in + tclTHEN introtac (peel_tac ra' names) gl + | [] -> + check_unused_names names; + tclIDTAC gl + in + let intros_move lstatus = + let newlstatus = (* if some IH has taken place at the top of hyps *) + List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus in + intros_move newlstatus + in + tclTHENLIST [ peel_tac ra names; + intros_rmove rstatus; + intros_move lstatus ] gl + +(* - le recalcul de indtyp à chaque itération de atomize_one est pour ne pas + s'embêter à regarder si un letin_tac ne fait pas des + substitutions aussi sur l'argument voisin *) + +(* Marche pas... faut prendre en compte l'occurrence précise... *) + +let atomize_param_of_ind (indref,nparams) hyp0 gl = + let tmptyp0 = pf_get_hyp_typ gl hyp0 in + let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in + let prods, indtyp = decompose_prod typ0 in + let argl = snd (decompose_app indtyp) in + let params = list_firstn nparams argl in + (* le gl est important pour ne pas préévaluer *) + let rec atomize_one i avoid gl = + if i<>nparams then + let tmptyp0 = pf_get_hyp_typ gl hyp0 in + (* If argl <> [], we expect typ0 not to be quantified, in order to + avoid bound parameters... then we call pf_reduce_to_atomic_ind *) + let indtyp = pf_apply reduce_to_atomic_ref gl indref tmptyp0 in + let argl = snd (decompose_app indtyp) in + let c = List.nth argl (i-1) in + match kind_of_term c with + | Var id when not (List.exists (occur_var (pf_env gl) id) avoid) -> + atomize_one (i-1) ((mkVar id)::avoid) gl + | Var id -> + let x = fresh_id [] id gl in + tclTHEN + (letin_tac true (Name x) (mkVar id) allClauses) + (atomize_one (i-1) ((mkVar x)::avoid)) gl + | _ -> + let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) + Anonymous in + let x = fresh_id [] id gl in + tclTHEN + (letin_tac true (Name x) c allClauses) + (atomize_one (i-1) ((mkVar x)::avoid)) gl + else + tclIDTAC gl + in + atomize_one (List.length argl) params gl + +let find_atomic_param_of_ind nparams indtyp = + let argl = snd (decompose_app indtyp) in + let argv = Array.of_list argl in + let params = list_firstn nparams argl in + let indvars = ref Idset.empty in + for i = nparams to (Array.length argv)-1 do + match kind_of_term argv.(i) with + | Var id + when not (List.exists (occur_var (Global.env()) id) params) -> + indvars := Idset.add id !indvars + | _ -> () + done; + Idset.elements !indvars; + + + (* [cook_sign] builds the lists [indhyps] of hyps that must be + erased, the lists of hyps to be generalize [(hdeps,tdeps)] on the + goal together with the places [(lstatus,rstatus)] where to re-intro + them after induction. To know where to re-intro the dep hyp, we + remember the name of the hypothesis [lhyp] after which (if the dep + hyp is more recent than [hyp0]) or [rhyp] before which (if older + than [hyp0]) its equivalent must be moved when the induction has + been applied. Since computation of dependencies and [rhyp] is from + more ancient (on the right) to more recent hyp (on the left) but + the computation of [lhyp] progresses from the other way, [cook_hyp] + is in two passes (an alternative would have been to write an + higher-order algorithm). We strongly use references to reduce + the accumulation of arguments. + + To summarize, the situation looks like this + + Goal(n,x) -| H6:(Q n); x:A; H5:True; H4:(le O n); H3:(P n); H2:True; n:nat + Left Right + + Induction hypothesis is H4 ([hyp0]) + Variable parameters of (le O n) is the singleton list with "n" ([indvars]) + Part of [indvars] really in context is the same ([indhyps]) + The dependent hyps are H3 and H6 ([dephyps]) + For H3 the memorized places are H5 ([lhyp]) and H2 ([rhyp]) + because these names are among the hyp which are fixed through the induction + For H6 the neighbours are None ([lhyp]) and H5 ([rhyp]) + For H3, because on the right of H4, we remember rhyp (here H2) + For H6, because on the left of H4, we remember lhyp (here None) + For H4, we remember lhyp (here H5) + + The right neighbour is then translated into the left neighbour + because move_hyp tactic needs the name of the hyp _after_ which we + move the hyp to move. + + But, say in the 2nd subgoal of the hypotheses, the goal will be + + (m:nat)((P m)->(Q m)->(Goal m)) -> (P Sm)-> (Q Sm)-> (Goal Sm) + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ + both go where H4 was goes where goes where + H3 was H6 was + + We have to intro and move m and the recursive hyp first, but then + where to move H3 ??? Only the hyp on its right is relevant, but we + have to translate it into the name of the hyp on the left + + Note: this case where some hyp(s) in [dephyps] has(have) the same + left neighbour as [hyp0] is the only problematic case with right + neighbours. For the other cases (e.g. an hyp H1:(R n) between n and H2 + would have posed no problem. But for uniformity, we decided to use + the right hyp for all hyps on the right of H4. + + Others solutions are welcome *) + +exception Shunt of identifier option + +let cook_sign hyp0 indvars env = + (* First phase from L to R: get [indhyps], [decldep] and [statuslist] + for the hypotheses before (= more ancient than) hyp0 (see above) *) + let allindhyps = hyp0::indvars in + let indhyps = ref [] in + let decldeps = ref [] in + let ldeps = ref [] in + let rstatus = ref [] in + let lstatus = ref [] in + let before = ref true in + let seek_deps env (hyp,_,_ as decl) rhyp = + if hyp = hyp0 then begin + before:=false; + None (* fake value *) + end else if List.mem hyp indvars then begin + (* warning: hyp can still occur after induction *) + (* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *) + indhyps := hyp::!indhyps; + rhyp + end else + if (List.exists (fun id -> occur_var_in_decl env id decl) allindhyps + or List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) + !decldeps) + then begin + decldeps := decl::!decldeps; + if !before then + rstatus := (hyp,rhyp)::!rstatus + else + ldeps := hyp::!ldeps; (* status computed in 2nd phase *) + Some hyp end + else + Some hyp + in + let _ = fold_named_context seek_deps env ~init:None in + (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) + let compute_lstatus lhyp (hyp,_,_ as d) = + if hyp = hyp0 then raise (Shunt lhyp); + if List.mem hyp !ldeps then begin + lstatus := (hyp,lhyp)::!lstatus; + lhyp + end else + if List.mem hyp !indhyps then lhyp else (Some hyp) + in + try + let _ = fold_named_context_reverse compute_lstatus ~init:None env in + anomaly "hyp0 not found" + with Shunt lhyp0 -> + let statuslists = (!lstatus,List.rev !rstatus) in + (statuslists, lhyp0, !indhyps, !decldeps) + +let induction_tac varname typ ((elimc,lbindelimc),elimt) gl = + let c = mkVar varname in + let (wc,kONT) = startWalk gl in + let indclause = make_clenv_binding wc (c,typ) NoBindings in + let elimclause = + make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in + elimination_clause_scheme kONT elimclause indclause true gl + +let make_up_names7 n ind (old_style,cname) = + if old_style (* = V6.3 version of Induction on hypotheses *) + then + let recvarname = + if n=1 then + cname + else (* To force renumbering if there is only one *) + make_ident (string_of_id cname ) (Some 1) in + recvarname, add_prefix "Hrec" recvarname, [] + else + let is_hyp = atompart_of_id cname = "H" in + let hyprecname = + add_prefix "IH" (if is_hyp then Nametab.id_of_global ind else cname) in + let avoid = + if n=1 (* Only one recursive argument *) + or + (* Rem: no recursive argument (especially if Destruct) *) + n=0 (* & atompart_of_id cname <> "H" (* for 7.1 compatibility *)*) + then [] + else + (* Forbid to use cname, cname0, hyprecname and hyprecname0 *) + (* in order to get names such as f1, f2, ... *) + let avoid = + (make_ident (string_of_id cname) (Some 0)) ::(*here for 7.1 cmpat*) + (make_ident (string_of_id hyprecname) None) :: + (make_ident (string_of_id hyprecname) (Some 0)) :: [] in + if atompart_of_id cname <> "H" then + (make_ident (string_of_id cname) None) :: avoid + else avoid in + cname, hyprecname, avoid + +let make_base n id = + if n=0 or n=1 then id + else + (* This extends the name to accept new digits if it already ends with *) + (* digits *) + id_of_string (atompart_of_id (make_ident (string_of_id id) (Some 0))) + +let make_up_names8 n ind (_,cname) = + let is_hyp = atompart_of_id cname = "H" in + let base = string_of_id (make_base n cname) in + let hyprecname = + add_prefix "IH" + (make_base n (if is_hyp then Nametab.id_of_global ind else cname)) in + let avoid = + if n=1 (* Only one recursive argument *) or n=0 then [] + else + (* Forbid to use cname, cname0, hyprecname and hyprecname0 *) + (* in order to get names such as f1, f2, ... *) + let avoid = + (make_ident (string_of_id hyprecname) None) :: + (make_ident (string_of_id hyprecname) (Some 0)) :: [] in + if atompart_of_id cname <> "H" then + (make_ident base (Some 0)) :: (make_ident base None) :: avoid + else avoid in + id_of_string base, hyprecname, avoid + +let is_indhyp p n t = + let l, c = decompose_prod t in + let c,_ = decompose_app c in + let p = p + List.length l in + match kind_of_term c with + | Rel k when p < k & k <= p + n -> true + | _ -> false + +let chop_context n l = + let rec chop_aux acc = function + | n, (_,Some _,_ as h :: t) -> chop_aux (h::acc) (n, t) + | 0, l2 -> (List.rev acc, l2) + | n, (h::t) -> chop_aux (h::acc) (n-1, t) + | _, [] -> anomaly "chop_context" + in + chop_aux [] (n,l) + +let error_ind_scheme s = + let s = if s <> "" then s^" " else s in + error ("Cannot recognise "^s^"an induction schema") + +(* Check that the elimination scheme has a form similar to the + elimination schemes built by Coq *) +let compute_elim_signature elimt names_info = + let nparams = ref 0 in + let hyps,ccl = decompose_prod_assum elimt in + let n = List.length hyps in + if n = 0 then error_ind_scheme ""; + let f,l = decompose_app ccl in + let _,indbody,ind = List.hd hyps in + if indbody <> None then error "Cannot recognise an induction scheme"; + let nargs = List.length l in + let dep = (nargs >= 1 && list_last l = mkRel 1) in + let nrealargs = if dep then nargs-1 else nargs in + let args = if dep then list_firstn nrealargs l else l in + let realargs,hyps1 = chop_context nrealargs (List.tl hyps) in + if args <> extended_rel_list 1 realargs then + error_ind_scheme "the conclusion of"; + let indhd,indargs = decompose_app ind in + let indt = + try reference_of_constr indhd + with _ -> error "Cannot find the inductive type of the inductive schema" in + let nparams = List.length indargs - nrealargs in + let revparams, revhyps2 = chop_context nparams (List.rev hyps1) in + let rec check_elim npred = function + | (na,None,t)::l when isSort (snd (decompose_prod_assum t)) -> + check_elim (npred+1) l + | l -> + let is_pred n c = + let hd = fst (decompose_app c) in match kind_of_term hd with + | Rel q when n < q & q <= n+npred -> IndArg + | _ when hd = indhd -> RecArg + | _ -> OtherArg in + let rec check_branch p c = match kind_of_term c with + | Prod (_,t,c) -> is_pred p t :: check_branch (p+1) c + | LetIn (_,_,_,c) -> OtherArg :: check_branch (p+1) c +(* | App (f,_) when is_pred p f = IndArg -> []*) + | _ when is_pred p c = IndArg -> [] + | _ -> raise Exit in + let rec find_branches p = function + | (_,None,t)::brs -> + (match try Some (check_branch p t) with Exit -> None with + | Some l -> + let n7 = List.fold_left + (fun n b -> if b=IndArg then n+1 else n) 0 l in + let n8 = List.fold_left + (fun n b -> if b=RecArg then n+1 else n) 0 l in + let recvarname7, hyprecname7, avoid7 = make_up_names7 n7 indt names_info in + let recvarname8, hyprecname8, avoid8 = make_up_names8 n8 indt names_info in + let namesign = List.map + (fun b -> (b,if b=IndArg then (hyprecname7,hyprecname8) + else (recvarname7,recvarname8))) l in + ((avoid7,avoid8),namesign) :: find_branches (p+1) brs + | None -> error_ind_scheme "the branches of") + | (_,Some _,_)::_ -> error_ind_scheme "the branches of" + | [] -> + (* Check again conclusion *) + let ccl_arg_ok = is_pred (p + List.length realargs + 1) f = IndArg in + let ind_is_ok = + list_lastn nrealargs indargs = extended_rel_list 0 realargs in + if not (ccl_arg_ok & ind_is_ok) then + error "Cannot recognize the conclusion of an induction schema"; + [] in + find_branches 0 l in + nparams, indt, (Array.of_list (check_elim 0 revhyps2)) + +let find_elim_signature isrec style elim hyp0 gl = + let tmptyp0 = pf_get_hyp_typ gl hyp0 in + let (elimc,elimt) = match elim with + | None -> + let mind,_ = pf_reduce_to_quantified_ind gl tmptyp0 in + let s = elimination_sort_of_goal gl in + let elimc = + if isrec then Indrec.lookup_eliminator mind s + else pf_apply Indrec.make_case_gen gl mind s in + let elimt = pf_type_of gl elimc in + ((elimc, NoBindings), elimt) + | Some (elimc,lbind as e) -> + (e, pf_type_of gl elimc) in + let name_info = (style,hyp0) in + let nparams,indref,indsign = compute_elim_signature elimt name_info in + (elimc,elimt,nparams,indref,indsign) + +let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl = + (*test suivant sans doute inutile car refait par le letin_tac*) + if List.mem hyp0 (ids_of_named_context (Global.named_context())) then + errorlabstrm "induction" + (str "Cannot generalize a global variable"); + let elimc,elimt,nparams,indref,indsign = elim_info in + let tmptyp0 = pf_get_hyp_typ gl hyp0 in + let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in + let env = pf_env gl in + let indvars = find_atomic_param_of_ind nparams (snd (decompose_prod typ0)) in + let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in + let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in + let names = compute_induction_names (Array.length indsign) names in + (* For translator *) + let names' = Array.map ref (Array.make (Array.length indsign) []) in + let b = ref false in + b_rnames := (b,Array.to_list names')::!b_rnames; + let names = array_map2 (fun n n' -> (n,b,n')) names names' in + (* End translator *) + let dephyps = List.map (fun (id,_,_) -> id) deps in + let args = + List.fold_left + (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in + + (* Magistral effet de bord: si hyp0 a des arguments, ceux d'entre + eux qui ouvrent de nouveaux buts arrivent en premier dans la + liste des sous-buts du fait qu'ils sont le plus à gauche dans le + combinateur engendré par make_case_gen (un "Cases (hyp0 ?) of + ...") et il faut alors appliquer tclTHENLASTn; en revanche, + comme lookup_eliminator renvoie un combinateur de la forme + "ind_rec ... (hyp0 ?)", les buts correspondant à des arguments de + hyp0 sont maintenant à la fin et c'est tclTHENFIRSTn qui marche !!! *) + tclTHENLIST + [ if deps = [] then tclIDTAC else apply_type tmpcl args; + thin dephyps; + (if isrec then tclTHENFIRSTn else tclTHENLASTn) + (tclTHENLIST + [ induction_tac hyp0 typ0 (elimc,elimt); + thin [hyp0]; + tclTRY (thin indhyps) ]) + (array_map2 + (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names) + ] + gl + +let induction_with_atomization_of_ind_arg isrec elim names hyp0 gl = + let (elimc,elimt,nparams,indref,indsign as elim_info) = + find_elim_signature isrec false elim hyp0 gl in + tclTHEN + (atomize_param_of_ind (indref,nparams) hyp0) + (induction_from_context isrec elim_info hyp0 names) gl + +(* This is Induction since V7 ("natural" induction both in quantified + premisses and introduced ones) *) +let new_induct_gen isrec elim names c gl = + match kind_of_term c with + | Var id when not (mem_named_context id (Global.named_context())) -> + induction_with_atomization_of_ind_arg isrec elim names id gl + | _ -> + let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) + Anonymous in + let id = fresh_id [] x gl in + tclTHEN + (letin_tac true (Name id) c allClauses) + (induction_with_atomization_of_ind_arg isrec elim names id) gl + +let new_induct_destruct isrec c elim names = match c with + | ElimOnConstr c -> new_induct_gen isrec elim names c + | ElimOnAnonHyp n -> + tclTHEN (intros_until_n n) + (tclLAST_HYP (new_induct_gen isrec elim names)) + (* Identifier apart because id can be quantified in goal and not typable *) + | ElimOnIdent (_,id) -> + tclTHEN (tclTRY (intros_until_id id)) + (new_induct_gen isrec elim names (mkVar id)) + +let new_induct = new_induct_destruct true +let new_destruct = new_induct_destruct false + +(* The registered tactic, which calls the default elimination + * if no elimination constant is provided. *) + +(* Induction tactics *) + +(* This was Induction before 6.3 (induction only in quantified premisses) *) +let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim) +let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim) + +(* This was Induction in 6.3 (hybrid form) *) +let induction_from_context_old_style hyp b_ids gl = + let elim_info = find_elim_signature true true None hyp gl in + let x = induction_from_context true elim_info hyp (None,b_ids) gl in + (* For translator *) fst (List.hd !b_ids) := true; + x + +let simple_induct_id hyp b_ids = + if !Options.v7 then + tclORELSE (raw_induct hyp) (induction_from_context_old_style hyp b_ids) + else + raw_induct hyp +let simple_induct_nodep = raw_induct_nodep + +let simple_induct = function + | NamedHyp id,b_ids -> simple_induct_id id b_ids + | AnonHyp n,_ -> simple_induct_nodep n + +(* Destruction tactics *) + +let simple_destruct_id s = + (tclTHEN (intros_until_id s) (tclLAST_HYP simplest_case)) +let simple_destruct_nodep n = + (tclTHEN (intros_until_n n) (tclLAST_HYP simplest_case)) + +let simple_destruct = function + | NamedHyp id -> simple_destruct_id id + | AnonHyp n -> simple_destruct_nodep n + +(* + * Eliminations giving the type instead of the proof. + * These tactics use the default elimination constant and + * no substitutions at all. + * May be they should be integrated into Elim ... + *) + +let elim_scheme_type elim t gl = + let (wc,kONT) = startWalk gl in + let clause = mk_clenv_type_of wc elim in + match kind_of_term (last_arg (clenv_template clause).rebus) with + | Meta mv -> + let clause' = + (* t is inductive, then CUMUL or CONV is irrelevant *) + clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in + elim_res_pf kONT clause' true gl + | _ -> anomaly "elim_scheme_type" + +let elim_type t gl = + let (ind,t) = pf_reduce_to_atomic_ind gl t in + let elimc = Indrec.lookup_eliminator ind (elimination_sort_of_goal gl) in + elim_scheme_type elimc t gl + +let case_type t gl = + let (ind,t) = pf_reduce_to_atomic_ind gl t in + let env = pf_env gl in + let elimc = Indrec.make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in + elim_scheme_type elimc t gl + + +(* Some eliminations frequently used *) + +(* These elimination tactics are particularly adapted for sequent + calculus. They take a clause as argument, and yield the + elimination rule if the clause is of the form (Some id) and a + suitable introduction rule otherwise. They do not depend on + the name of the eliminated constant, so they can be also + used on ad-hoc disjunctions and conjunctions introduced by + the user. + -- Eduardo Gimenez (11/8/97) + + HH (29/5/99) replaces failures by specific error messages + *) + +let andE id gl = + let t = pf_get_hyp_typ gl id in + if is_conjunction (pf_hnf_constr gl t) then + (tclTHEN (simplest_elim (mkVar id)) (tclDO 2 intro)) gl + else + errorlabstrm "andE" + (str("Tactic andE expects "^(string_of_id id)^" is a conjunction.")) + +let dAnd cls = + onClauses + (function + | None -> simplest_split + | Some (id,_,_) -> andE id) + cls + +let orE id gl = + let t = pf_get_hyp_typ gl id in + if is_disjunction (pf_hnf_constr gl t) then + (tclTHEN (simplest_elim (mkVar id)) intro) gl + else + errorlabstrm "orE" + (str("Tactic orE expects "^(string_of_id id)^" is a disjunction.")) + +let dorE b cls = + onClauses + (function + | (Some (id,_,_)) -> orE id + | None -> (if b then right else left) NoBindings) + cls + +let impE id gl = + let t = pf_get_hyp_typ gl id in + if is_imp_term (pf_hnf_constr gl t) then + let (dom, _, rng) = destProd (pf_hnf_constr gl t) in + tclTHENLAST + (cut_intro rng) + (apply_term (mkVar id) [mkMeta (new_meta())]) gl + else + errorlabstrm "impE" + (str("Tactic impE expects "^(string_of_id id)^ + " is a an implication.")) + +let dImp cls = + onClauses + (function + | None -> intro + | Some (id,_,_) -> impE id) + cls + +(************************************************) +(* Tactics related with logic connectives *) +(************************************************) + +(* Reflexivity tactics *) + +let reflexivity gl = + match match_with_equation (pf_concl gl) with + | None -> error "The conclusion is not a substitutive equation" + | Some (hdcncl,args) -> one_constructor 1 NoBindings gl + +let intros_reflexivity = (tclTHEN intros reflexivity) + +(* Symmetry tactics *) + +(* This tactic first tries to apply a constant named sym_eq, where eq + is the name of the equality predicate. If this constant is not + defined and the conclusion is a=b, it solves the goal doing (Cut + b=a;Intro H;Case H;Constructor 1) *) + +let symmetry gl = + match match_with_equation (pf_concl gl) with + | None -> error "The conclusion is not a substitutive equation" + | Some (hdcncl,args) -> + let hdcncls = string_of_inductive hdcncl in + begin + try + (apply (pf_parse_const gl ("sym_"^hdcncls)) gl) + with _ -> + let symc = match args with + | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) + | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |]) + | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |]) + | _ -> assert false + in + tclTHENLAST (cut symc) + (tclTHENLIST + [ intro; + tclLAST_HYP simplest_case; + one_constructor 1 NoBindings ]) + gl + end + +let symmetry_in id gl = + let ctype = pf_type_of gl (mkVar id) in + let sign,t = decompose_prod_assum ctype in + match match_with_equation t with + | None -> (* Do not deal with setoids yet *) + error "The term provided does not end with an equation" + | Some (hdcncl,args) -> + let symccl = match args with + | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) + | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |]) + | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |]) + | _ -> assert false in + tclTHENS (cut (it_mkProd_or_LetIn symccl sign)) + [ intro_replacing id; + tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] + gl + +let intros_symmetry = + onClauses + (function + | None -> tclTHEN intros symmetry + | Some (id,_,_) -> symmetry_in id) + +(* Transitivity tactics *) + +(* This tactic first tries to apply a constant named trans_eq, where eq + is the name of the equality predicate. If this constant is not + defined and the conclusion is a=b, it solves the goal doing + Cut x1=x2; + [Cut x2=x3; [Intros e1 e2; Case e2;Assumption + | Idtac] + | Idtac] + --Eduardo (19/8/97) +*) + +let transitivity t gl = + match match_with_equation (pf_concl gl) with + | None -> error "The conclusion is not a substitutive equation" + | Some (hdcncl,args) -> + let hdcncls = string_of_inductive hdcncl in + begin + try + apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl + with _ -> + let eq1, eq2 = match args with + | [typ1;c1;typ2;c2] -> let typt = pf_type_of gl t in + ( mkApp(hdcncl, [| typ1; c1; typt ;t |]), + mkApp(hdcncl, [| typt; t; typ2; c2 |]) ) + | [typ;c1;c2] -> + ( mkApp (hdcncl, [| typ; c1; t |]), + mkApp (hdcncl, [| typ; t; c2 |]) ) + | [c1;c2] -> + ( mkApp (hdcncl, [| c1; t|]), + mkApp (hdcncl, [| t; c2 |]) ) + | _ -> assert false + in + tclTHENFIRST (cut eq2) + (tclTHENFIRST (cut eq1) + (tclTHENLIST + [ tclDO 2 intro; + tclLAST_HYP simplest_case; + assumption ])) gl + end + +let intros_transitivity n = tclTHEN intros (transitivity n) + +(* tactical to save as name a subproof such that the generalisation of + the current goal, abstracted with respect to the local signature, + is solved by tac *) + +let interpretable_as_section_decl d1 d2 = match d1,d2 with + | (_,Some _,_), (_,None,_) -> false + | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2 + | (_,None,t1), (_,_,t2) -> eq_constr t1 t2 + +let abstract_subproof name tac gls = + let env = Global.env() in + let current_sign = Global.named_context() + and global_sign = pf_hyps gls in + let sign,secsign = + List.fold_right + (fun (id,_,_ as d) (s1,s2) -> + if mem_named_context id current_sign & + interpretable_as_section_decl (Sign.lookup_named id current_sign) d + then (s1,add_named_decl d s2) + else (add_named_decl d s1,s2)) + global_sign (empty_named_context,empty_named_context) in + let na = next_global_ident_away false name (pf_ids_of_hyps gls) in + let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in + if occur_existential concl then + if !Options.v7 then error "Abstract cannot handle existentials" + else error "\"abstract\" cannot handle existentials"; + let lemme = + start_proof na (IsGlobal (Proof Lemma)) secsign concl (fun _ _ -> ()); + let _,(const,kind,_) = + try + by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); + let r = cook_proof () in + delete_current_proof (); r + with e when catchable_exception e -> + (delete_current_proof(); raise e) + in (* Faudrait un peu fonctionnaliser cela *) + let cd = Entries.DefinitionEntry const in + let sp = Declare.declare_internal_constant na (cd,IsProof Lemma) in + let newenv = Global.env() in + constr_of_reference (ConstRef (snd sp)) + in + exact_no_check + (applist (lemme, + List.rev (Array.to_list (instance_from_named_context sign)))) + gls + +let tclABSTRACT name_op tac gls = + let s = match name_op with + | Some s -> s + | None -> add_suffix (get_current_proof_name ()) "_subproof" + in + abstract_subproof s tac gls -- cgit v1.2.3