diff options
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 1791 |
1 files changed, 1143 insertions, 648 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2ba09e52..1d97dc4f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml,v 1.162.2.7 2005/07/13 16:18:57 herbelin Exp $ *) +(* $Id: tactics.ml 8701 2006-04-12 08:07:35Z courtieu $ *) open Pp open Util @@ -31,6 +31,7 @@ open Proof_type open Logic open Evar_refiner open Clenv +open Clenvtac open Refiner open Tacticals open Hipattern @@ -39,6 +40,8 @@ open Nametab open Genarg open Tacexpr open Decl_kinds +open Evarutil +open Indrec exception Bound @@ -47,7 +50,7 @@ let rec nb_prod x = match kind_of_term c with Prod(_,_,t) -> count (n+1) t | LetIn(_,a,_,t) -> count n (subst1 a t) - | Cast(c,_) -> count n c + | Cast(c,_,_) -> count n c | _ -> n in count 0 x @@ -141,28 +144,24 @@ type tactic_reduction = env -> evar_map -> constr -> constr 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_concl (redfun,sty) gl = + convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl -let reduct_in_hyp redfun (id,_,(where,where')) gl = +let reduct_in_hyp redfun (id,_,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 + | Some id -> reduct_in_hyp (fst redfun) id | None -> reduct_in_concl redfun (* The following tactic determines whether the reduction @@ -182,10 +181,13 @@ let change_and_check cv_pb t env sigma c = (* 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) + | Some occl -> contextually false occl (change_and_check Reduction.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_in_concl occl t = + reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast) + +let change_in_hyp occl t = + reduct_in_hyp (change_on_subterm Reduction.CONV t occl) let change_option occl t = function Some id -> change_in_hyp occl t id @@ -200,22 +202,23 @@ let change occl c cls = 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_concl = reduct_in_concl (red_product,DEFAULTcast) 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 red_option = reduct_option (red_product,DEFAULTcast) +let hnf_in_concl = reduct_in_concl (hnf_constr,DEFAULTcast) 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 hnf_option = reduct_option (hnf_constr,DEFAULTcast) +let simpl_in_concl = reduct_in_concl (nf,DEFAULTcast) let simpl_in_hyp = reduct_in_hyp nf -let simpl_option = reduct_option nf -let normalise_in_concl = reduct_in_concl compute +let simpl_option = reduct_option (nf,DEFAULTcast) +let normalise_in_concl = reduct_in_concl (compute,DEFAULTcast) 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) +let normalise_option = reduct_option (compute,DEFAULTcast) +let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast) +let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,DEFAULTcast) +let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) +let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast) +let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast) (* A function which reduces accordingly to a reduction expression, as the command Eval does. *) @@ -228,7 +231,7 @@ let needs_check = function let reduce redexp cl goal = (if needs_check redexp then with_check else (fun x -> x)) - (redin_combinator (reduction_of_redexp redexp) cl) + (redin_combinator (Redexpr.reduction_of_red_expr redexp) cl) goal (* Unfolding occurrences of a constant *) @@ -300,6 +303,8 @@ let intro_force force_flag = intro_gen (IntroAvoid []) None force_flag let intro = intro_force false let introf = intro_force true +let intro_avoiding l = intro_gen (IntroAvoid l) None false + let introf_move_name destopt = intro_gen (IntroAvoid []) destopt true (* For backwards compatibility *) @@ -313,7 +318,7 @@ let rec intros_using = function let intros = tclREPEAT (intro_force false) -let intro_erasing id = tclTHEN (thin [id]) (intro_using id) +let intro_erasing id = tclTHEN (thin [id]) (introduction id) let intros_replacing ids gls = let rec introrec = function @@ -341,7 +346,9 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl = 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) + aux + ((fst (Redexpr.reduction_of_red_expr (Red true))) + env (project gl) ccl) | x -> x in try aux (pf_concl gl) @@ -428,7 +435,7 @@ let rec intros_rmove = function * of the type of a term. *) let apply_type hdcty argl gl = - refine (applist (mkCast (mkMeta (new_meta()),hdcty),argl)) gl + refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl let apply_term hdc argl gl = refine (applist (hdc,argl)) gl @@ -438,39 +445,33 @@ let bring_hyps hyps = else (fun gl -> let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in - let f = mkCast (mkMeta (new_meta()),newcl) in + let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, 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 thm_ty0 = nf_betaiota (pf_type_of gl 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 clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in + Clenvtac.res_pf clause gl + with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn -> let red_thm = - try red_product (w_env wc) (w_Underlying wc) thm_ty + try red_product (pf_env gl) (project gl) thm_ty with (Redelimination | UserError _) -> raise exn in try_apply red_thm in try try_apply thm_ty0 - with (RefinerError _|UserError _|Failure _) -> + with (Pretype_errors.PretypeError _|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 clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in + Clenvtac.res_pf clause gl let apply c = apply_with_bindings (c,NoBindings) @@ -481,9 +482,8 @@ let apply_list = function (* 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 + let clause = mk_clenv_type_of gl c in + res_pf clause gl (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -502,6 +502,10 @@ let apply_without_reduce c gl = end. *) +(**************************) +(* Cut tactics *) +(**************************) + 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 @@ -511,24 +515,6 @@ let cut_and_apply c gl = (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 _ -> @@ -541,14 +527,13 @@ let cut c 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 + +let cut_replacing id t tac = + tclTHENS (cut t) + [tclORELSE (intro_replacing id) - (tclORELSE (intro_erasing id) - (intro_using id))) + (tclORELSE (intro_erasing id) (intro_using id)); + tac (refine_no_check (mkVar id)) ] let cut_in_parallel l = let rec prec = function @@ -557,226 +542,6 @@ let cut_in_parallel l = 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 in_every_hyp cls = (cls.onhyps = None) - -(* -(* 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 occ = [] & d = newdecl then - if not (in_every_hyp 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 = Evarutil.refresh_universes (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 *) (********************************************************************) @@ -838,9 +603,8 @@ let rec intros_clearing = function (* 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 clause = make_clenv_binding g (c,pf_type_of g c) lbind in + let (thd,tstack) = whd_stack (clenv_value clause) in let nargs = List.length tstack in let cut_pf = applist(thd, @@ -848,10 +612,25 @@ let new_hyp mopt (c,lbind) g = | Some m -> if m < nargs then list_firstn m tstack else tstack | None -> tstack) in - (tclTHENLAST (tclTHEN (kONT clause.hook) + (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.env)) (cut (pf_type_of g cut_pf))) ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g +(* Keeping only a few hypotheses *) + +let keep hyps gl = + let env = Global.env() in + let ccl = pf_concl gl in + let cl,_ = + fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> + if List.mem hyp hyps + or List.exists (occur_var_in_decl env hyp) keep + or occur_var env hyp ccl + then (clear,decl::keep) + else (hyp::clear,keep)) + ~init:([],[]) (pf_env gl) + in thin cl gl + (************************) (* Introduction tactics *) (************************) @@ -860,8 +639,7 @@ 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 + Array.length (snd (Global.lookup_inductive mind)).mind_consnames 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 @@ -872,7 +650,8 @@ let constructor_tac boundopt i lbind gl = 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 + (tclTHENLIST + [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl let one_constructor i = constructor_tac None i @@ -903,33 +682,26 @@ 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 + | App (f,cl) -> + array_last cl | _ -> anomaly "last_arg" -let elimination_clause_scheme kONT elimclause indclause allow_K gl = +let elimination_clause_scheme allow_K elimclause indclause gl = let indmv = - (match kind_of_term (last_arg (clenv_template elimclause).rebus) with + (match kind_of_term (last_arg elimclause.templval.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 + res_pf elimclause' ~allow_K: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) + clenv_type (make_clenv_binding wc (c,t) lbind) (* * Elimination tactic with bindings and using an arbitrary @@ -939,41 +711,30 @@ let type_clenv_binding wc (c,t) lbind = * 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 general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl = 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 + let indclause = make_clenv_binding gl (c,t) lbindc in + let elimt = pf_type_of gl elimc in + let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in + elimtac elimclause indclause gl + +let general_elim c e ?(allow_K=true) = + general_elim_clause (elimination_clause_scheme allow_K) c e (* 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 (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + lookup_eliminator ind (elimination_sort_of_goal gl) + +let default_elim (c,_ as cx) gl = + general_elim cx (find_eliminator c gl,NoBindings) gl + +let elim_in_context c = function + | Some elim -> general_elim c elim ~allow_K:true + | None -> default_elim c let elim (c,lbindc as cx) elim = match kind_of_term c with @@ -987,7 +748,7 @@ let simplest_elim c = default_elim (c,NoBindings) (* Elimination in hypothesis *) -let elimination_in_clause_scheme kONT id elimclause indclause = +let elimination_in_clause_scheme id elimclause indclause gl = let (hypmv,indmv) = match clenv_independent elimclause with [k1;k2] -> (k1,k2) @@ -995,43 +756,31 @@ let elimination_in_clause_scheme kONT id elimclause indclause = (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 hyp_typ = pf_type_of gl hyp in let hypclause = - mk_clenv_from_n elimclause'.hook (Some 0) (hyp, hyp_typ) in + mk_clenv_from_n gl (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 + let new_hyp_prf = clenv_value elimclause'' in + let new_hyp_typ = clenv_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 + (tclEVARS (evars_of elimclause''.env)) + (cut_replacing id new_hyp_typ + (fun x gls -> refine_no_check new_hyp_prf gls)) gl + +let general_elim_in id = + general_elim_clause (elimination_in_clause_scheme id) (* 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 + let case = + if occur_term c (pf_concl gl) then make_case_dep else make_case_gen in + let elim = pf_apply case gl mind sort in general_elim (c,lbindc) (elim,NoBindings) gl let general_case_analysis (c,lbindc as cx) = @@ -1051,23 +800,295 @@ let simplest_case c = general_case_analysis (c,NoBindings) 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 +let rec explicit_intro_names = function +| (IntroWildcard | IntroAnonymous) :: l -> explicit_intro_names l +| IntroIdentifier id :: l -> id :: explicit_intro_names l +| IntroOrAndPattern ll :: l' -> + List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll) +| [] -> [] + + (* We delay thinning until the completion of the whole intros tactic + to ensure that dependent hypotheses are cleared in the right + dependency order (see bug #1000); we use fresh names, not used in + the tactic, for the hyps to clear *) +let rec intros_patterns avoid thin destopt = function + | IntroWildcard :: l -> + tclTHEN + (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true) + (onLastHyp (fun id -> + tclORELSE + (tclTHEN (clear [id]) (intros_patterns avoid thin destopt l)) + (intros_patterns avoid (id::thin) destopt l))) + | IntroIdentifier id :: l -> + tclTHEN + (intro_gen (IntroMustBe id) destopt true) + (intros_patterns avoid thin destopt l) + | IntroAnonymous :: l -> + tclTHEN + (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) destopt true) + (intros_patterns avoid thin destopt l) + | IntroOrAndPattern ll :: l' -> + tclTHEN + introf (tclTHENS (tclTHEN case_last clear_last) - (List.map (intros_pattern destopt) l)) + (List.map (fun l -> intros_patterns avoid thin destopt (l@l')) ll)) + | [] -> clear thin + +let intros_pattern = intros_patterns [] [] -and intros_pattern destopt l = tclMAP (intro_pattern destopt) l +let intro_pattern destopt pat = intros_patterns [] [] destopt [pat] let intro_patterns = function | [] -> tclREPEAT intro | l -> intros_pattern None l +(**************************) +(* Other cut tactics *) +(**************************) + +let hid = id_of_string "H" +let xid = id_of_string "X" + +let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid) + +let prepare_intros s ipat gl = match ipat with + | IntroAnonymous -> make_id s gl, tclIDTAC + | IntroWildcard -> let id = make_id s gl in id, thin [id] + | IntroIdentifier id -> id, tclIDTAC + | IntroOrAndPattern ll -> make_id s gl, + (tclTHENS + (tclTHEN case_last clear_last) + (List.map (intros_pattern None) ll)) + +let ipat_of_name = function + | Anonymous -> IntroAnonymous + | Name id -> IntroIdentifier id + +let assert_as first ipat c gl = + match kind_of_term (hnf_type_of gl c) with + | Sort s -> + let id,tac = prepare_intros s ipat gl in + tclTHENS ((if first then internal_cut else internal_cut_rev) id c) + (if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl + | _ -> error "Not a proposition or a type" + +let assert_tac first na = assert_as first (ipat_of_name na) +let true_cut = assert_tac true + +(**************************) +(* 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 in_every_hyp cls = (cls.onhyps=None) + +(* +(* 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 occ = [] & d = newdecl then + if not (in_every_hyp 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 occ = [] & d = newdecl then + if not (in_every_hyp 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 = refresh_universes (pf_type_of gl c) in + let newcl = mkNamedLetIn id c t ccl in + tclTHENLIST + [ convert_concl_no_check newcl DEFAULTcast; + intro_gen (IntroMustBe id) lastlhyp true; + if with_eq then tclIDTAC else thin_body [id]; + tclMAP convert_hyp_no_check depdecls ] gl + +(* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) +let forward usetac ipat c gl = + match usetac with + | None -> + let t = refresh_universes (pf_type_of gl c) in + tclTHENS (assert_as true ipat t) [exact_no_check c; tclIDTAC] gl + | Some tac -> + tclTHENS (assert_as true ipat c) [tac; tclIDTAC] gl + +(*****************************) +(* High-level induction *) +(*****************************) + (* * A "natural" induction tactic * @@ -1100,20 +1121,12 @@ let intro_patterns = function *) -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) + msg_warning + (str"Unused introduction pattern" ++ str s ++ + str": " ++ prlist_with_sep spc pr_intro_pattern names) let rec first_name_buggy = function | IntroOrAndPattern [] -> None @@ -1121,100 +1134,48 @@ let rec first_name_buggy = function | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p | IntroWildcard -> None | IntroIdentifier id -> Some id + | IntroAnonymous -> assert false + +let consume_pattern avoid id gl = function + | [] -> (IntroIdentifier (fresh_id avoid id gl), []) + | IntroAnonymous::names -> + let avoid = avoid@explicit_intro_names names in + (IntroIdentifier (fresh_id avoid id gl), names) + | pat::names -> (pat,names) 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 induct_discharge statuslists destopt avoid' (avoid,ra) names gl = + let avoid = avoid @ 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, []) + | (RecArg,recvarname) :: + (IndArg,hyprecname) :: ra' -> + let recpat,names = match names with | [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 + let id = next_ident_away (add_prefix "IH" id) avoid in + (pat, [IntroIdentifier id]) + | _ -> consume_pattern avoid recvarname gl names in + let hyprec,names = consume_pattern avoid hyprecname gl 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]; + [ intros_patterns avoid [] destopt [recpat]; + intros_patterns avoid [] None [hyprec]; peel_tac ra' names ] gl - | (IndArg,(hyprecname7,hyprecname8)) :: ra' -> + | (IndArg,hyprecname) :: 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) - | _ -> raise (RefinerError IntroNeedsProduct))) 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 + let pat,names = consume_pattern avoid hyprecname gl names in + tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl + | (RecArg,recvarname) :: ra' -> + let pat,names = consume_pattern avoid recvarname gl names in + tclTHEN (intros_patterns avoid [] destopt [pat]) (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) - | _ -> raise (RefinerError IntroNeedsProduct))) 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) - | _ -> raise (RefinerError IntroNeedsProduct))) 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 + let pat,names = match names with + | [] -> IntroAnonymous, [] + | pat::names -> pat,names in + tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl | [] -> check_unused_names names; tclIDTAC gl @@ -1335,11 +1296,25 @@ let find_atomic_param_of_ind nparams indtyp = 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 *) + Others solutions are welcome + + PC 9 fev 06: Adapted to accept multi argument principle with no + main arg hyp. hyp0 is now optional, meaning that it is possible + that there is no main induction hypotheses. In this case, we + consider the last "parameter" (in [indvars]) as the limit between + "left" and "right", BUT it must be included in indhyps. + + Other solutions are still welcome + +*) exception Shunt of identifier option -let cook_sign hyp0 indvars env = +let cook_sign hyp0_opt indvars_init env = + let hyp0,indvars = + match hyp0_opt with + | None -> List.hd (List.rev indvars_init) , indvars_init + | Some h -> h,indvars_init in (* 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 @@ -1352,6 +1327,9 @@ let cook_sign hyp0 indvars env = let seek_deps env (hyp,_,_ as decl) rhyp = if hyp = hyp0 then begin before:=false; + (* If there was no main induction hypotheses, then hyp is one of + indvars too, so add it to indhyps. *) + (if hyp0_opt=None then indhyps := hyp::!indhyps); None (* fake value *) end else if List.mem hyp indvars then begin (* warning: hyp can still occur after induction *) @@ -1374,7 +1352,7 @@ let cook_sign hyp0 indvars env = 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) = + let compute_lstatus lhyp (hyp,_,_) = if hyp = hyp0 then raise (Shunt lhyp); if List.mem hyp !ldeps then begin lstatus := (hyp,lhyp)::!lstatus; @@ -1384,49 +1362,89 @@ let cook_sign hyp0 indvars env = in try let _ = fold_named_context_reverse compute_lstatus ~init:None env in - anomaly "hyp0 not found" +(* anomaly "hyp0 not found" *) + raise (Shunt (None)) (* ?? FIXME *) with Shunt lhyp0 -> let statuslists = (!lstatus,List.rev !rstatus) in - (statuslists, lhyp0, !indhyps, !decldeps) + (statuslists, (if hyp0_opt=None then None else lhyp0) , !indhyps, !decldeps) -let induction_tac varname typ ((elimc,lbindelimc),elimt) gl = + +(* + The general form of an induction principle is the following: + + forall prm1 prm2 ... prmp, (induction parameters) + forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates) + branch1, branch2, ... , branchr, (branches of the principle) + forall (x1:Ti_1) (x2:Ti_2) ... (xni:Ti_ni), (induction arguments) + (HI: I prm1..prmp x1...xni) (optional main induction arg) + -> (Qi x1...xni HI (f prm1...prmp x1...xni)).(conclusion) + ^^ ^^^^^^^^^^^^^^^^^^^^^^^^ + optional optional argument added if + even if HI principle generated by functional + present above induction, only if HI does not exist + [indarg] [farg] + + HI is not present when the induction principle does not come directly from an + inductive type (like when it is generated by functional induction for + example). HI is present otherwise BUT may not appear in the conclusion + (dependent principle). HI and (f...) cannot be both present. + + Principles taken from functional induction have the final (f...).*) + +(* [rel_contexts] and [rel_declaration] actually contain triples, and + lists are actually in reverse order to fit [compose_prod]. *) +type elim_scheme = { + elimc: (Term.constr * constr Rawterm.bindings) option; + elimt: types; + indref: global_reference option; + params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (* number of parameters *) + predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (* Number of predicates *) + branches: rel_context; (* branchr,...,branch1 *) + nbranches: int; (* Number of branches *) + args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (* number of arguments *) + indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) + if HI is in premisses, None otherwise *) + concl: types; (* Qi x1...xni HI (f...), HI and (f...) + are optional and mutually exclusive *) + indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) + farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) +} + +let empty_scheme = + { + elimc = None; + elimt = mkProp; + indref = None; + params = []; + nparams = 0; + predicates = []; + npredicates = 0; + branches = []; + nbranches = 0; + args = []; + nargs = 0; + indarg = None; + concl = mkProp; + indarg_in_concl = false; + farg_in_concl = false; + } + + +(* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the + hypothesis on which the induction is made *) +let induction_tac varname typ scheme (*(elimc,lbindelimc),elimt*) gl = + let elimc,lbindelimc = + match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in + let elimt = scheme.elimt in let c = mkVar varname in - let (wc,kONT) = startWalk gl in - let indclause = make_clenv_binding wc (c,typ) NoBindings in + let indclause = make_clenv_binding gl (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 + make_clenv_binding gl + (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in + elimination_clause_scheme true elimclause indclause gl let make_base n id = if n=0 or n=1 then id @@ -1435,12 +1453,19 @@ let make_base n id = (* digits *) id_of_string (atompart_of_id (make_ident (string_of_id id) (Some 0))) -let make_up_names8 n ind (_,cname) = +(* Builds tw different names from an optional inductive type and a + number, also deals with a list of names to avoid. If the inductive + type is None, then hyprecname is HIi where i is a number. *) +let make_up_names n ind_opt 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 base_ind = + if is_hyp then + match ind_opt with + | None -> id_of_string "" + | Some ind_id -> Nametab.id_of_global ind_id + else cname in + let hyprecname = add_prefix "IH" (make_base n base_ind) in let avoid = if n=1 (* Only one recursive argument *) or n=0 then [] else @@ -1475,109 +1500,432 @@ let error_ind_scheme s = let s = if s <> "" then s^" " else s in error ("Cannot recognise "^s^"an induction schema") + + + +let occur_rel n c = + let res = not (noccurn n c) in + res + +let list_filter_firsts f l = + let rec list_filter_firsts_aux f acc l = + match l with + | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l' + | _ -> acc,l + in + list_filter_firsts_aux f [] l + +let count_rels_from n c = + let rels = free_rels c in + let cpt,rg = ref 0, ref n in + while Intset.mem !rg rels do + cpt:= !cpt+1; rg:= !rg+1; + done; + !cpt + +let count_nonfree_rels_from n c = + let rels = free_rels c in + if Intset.exists (fun x -> x >= n) rels then + let cpt,rg = ref 0, ref n in + while not (Intset.mem !rg rels) do + cpt:= !cpt+1; rg:= !rg+1; + done; + !cpt + else raise Not_found + + +(* cuts a list in two parts, first of size n. Size must be greater than n *) +let cut_list n l = + let rec cut_list_aux acc n l = + if n<=0 then acc,l + else match l with + | [] -> assert false + | e::l' -> cut_list_aux (acc@[e]) (n-1) l' in + let res = cut_list_aux [] n l in + res + + +(* This functions splits the products of the induction scheme [elimt] in three + parts: + - branches, easily detectable (they are not referred by rels in the subterm) + - what was found before branches (acc1) that is: parameters and predicates + - what was found after branches (acc3) that is: args and indarg if any + if there is no branch, we try to fill in acc3 with args/indargs. + We also return the conclusion. +*) +let decompose_paramspred_branch_args elimt = + let rec cut_noccur elimt acc2 : rel_context * rel_context * types = + match kind_of_term elimt with + | Prod(nme,tpe,elimt') -> + let hd_tpe,_ = decompose_app (snd (decompose_prod_assum tpe)) in + if not (occur_rel 1 elimt') && isRel hd_tpe + then cut_noccur elimt' ((nme,None,tpe)::acc2) + else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl + | App(_, _) | Rel _ -> acc2 , [] , elimt + | _ -> error "cannot recognise an induction schema" in + let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types = + match kind_of_term elimt with + | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1) + | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl + | App(_, _) | Rel _ -> acc1,[],[],elimt + | _ -> error "cannot recognise an induction schema" in + let acc1, acc2 , acc3, ccl = cut_occur elimt [] in + (* Particular treatment when dealing with a dependent empty type elim scheme: + if there is no branch, then acc1 contains all hyps which is wrong (acc1 + should contain parameters and predicate only). This happens for an empty + type (See for example Empty_set_ind, as False would actually be ok). Then + we must find the predicate of the conclusion to separate params_pred from + args. We suppose there is only one predicate here. *) + if List.length acc2 <> 0 then acc1, acc2 , acc3, ccl + else + let hyps,ccl = decompose_prod_assum elimt in + let hd_ccl_pred,_ = decompose_app ccl in + match kind_of_term hd_ccl_pred with + | Rel i -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl + | _ -> error "cannot recognize an induction schema" + + + +let exchange_hd_app subst_hd t = + let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args) + + +exception NoLastArg +exception NoLastArgCcl + +(* Builds an elim_scheme frome its type and calling form (const+binding) We + first separate branches. We obtain branches, hyps before (params + preds), + hyps after (args <+ indarg if present>) and conclusion. Then we proceed as + follows: + + - separate parameters and predicates in params_preds. For that we build: + forall (x1:Ti_1)(xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY x1...xni HI/farg + ^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^ + optional opt + Free rels appearing in this term are parameters (branches should not + appear, and the only predicate would have been Qi but we replaced it by + DUMMY). We guess this heuristic catches all params. TODO: generalize to + the case where args are merged with branches (?) and/or where several + predicates are cited in the conclusion. + + - finish to fill in the elim_scheme: indarg/farg/args and finally indref. *) +let compute_elim_sig ?elimc elimt = + let params_preds,branches,args_indargs,conclusion = + decompose_paramspred_branch_args elimt in + + let ccl = exchange_hd_app (mkVar (id_of_string "__QI_DUMMY__")) conclusion in + let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in + let nparams = Intset.cardinal (free_rels concl_with_args) in + let preds,params = cut_list (List.length params_preds - nparams) params_preds in + + (* A first approximation, further anlysis will tweak it *) + let res = ref { empty_scheme with + (* This fields are ok: *) + elimc = elimc; elimt = elimt; concl = conclusion; + predicates = preds; npredicates = List.length preds; + branches = branches; nbranches = List.length branches; + farg_in_concl = (try isApp (last_arg ccl) with _ -> false); + params = params; nparams = nparams; + (* all other fields are unsure at this point. Including these:*) + args = args_indargs; nargs = List.length args_indargs; } in + try + (* Order of tests below is important. Each of them exits if successful. *) + (* 1- First see if (f x...) is in the conclusion. *) + if !res.farg_in_concl + then begin + res := { !res with + indarg = None; + indarg_in_concl = false; farg_in_concl = true }; + raise Exit + end; + (* 2- If no args_indargs (=!res.nargs at this point) then no indarg *) + if !res.nargs=0 then raise Exit; + (* 3- Look at last arg: is it the indarg? *) + ignore ( + match List.hd args_indargs with + | hiname,Some _,hi -> error "cannot recognize an induction schema" + | hiname,None,hi -> + let hi_ind, hi_args = decompose_app hi in + let hi_is_ind = (* hi est d'un type inductif *) + match kind_of_term hi_ind with | Ind (mind,_) -> true | _ -> false in + let hi_args_enough = (* hi a le bon nbre d'arguments *) + List.length hi_args = List.length params + !res.nargs -1 in + (* FIXME: Ces deux tests ne sont pas suffisants. *) + if not (hi_is_ind & hi_args_enough) then raise Exit (* No indarg *) + else (* Last arg is the indarg *) + res := {!res with + indarg = Some (List.hd !res.args); + indarg_in_concl = occur_rel 1 ccl; + args = List.tl !res.args; nargs = !res.nargs - 1; + }; + raise Exit); + raise Exit(* exit anyway *) + with Exit -> (* Ending by computing indrev: *) + match !res.indarg with + | None -> !res (* No indref *) + | Some ( _,Some _,_) -> error "Cannot recognise an induction scheme" + | Some ( _,None,ind) -> + let indhd,indargs = decompose_app ind in + try {!res with indref = Some (global_of_constr indhd) } + with _ -> error "Cannot find the inductive type of the inductive 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 = + elimination schemes built by Coq. Schemes may have the standard + form computed from an inductive type OR (feb. 2006) a non standard + form. That is: with no main induction argument and with an optional + extra final argument of the form (f x y ...) in the conclusion. In + the non standard case, naming of generated hypos is slightly + different. *) +let compute_elim_signature elimc elimt names_info = + let scheme = compute_elim_sig ~elimc:elimc elimt in + let f,l = decompose_app scheme.concl in + (* Vérifier que les arguments de Qi sont bien les xi. *) + match scheme.indarg with + | Some (_,Some _,_) -> error "strange letin, cannot recognize an induction schema" + | None -> (* Non standard scheme *) + let npred = List.length scheme.predicates in + 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 + | _ -> 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 + | _ when is_pred p c = IndArg -> [] + | _ -> raise Exit in + let rec find_branches p lbrch = + match lbrch with + | (_,None,t)::brs -> + (try + let lchck_brch = check_branch p t in + let n = List.fold_left + (fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in + let recvarname, hyprecname, avoid = + make_up_names n scheme.indref names_info in + let namesign = + List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname)) + lchck_brch in + (avoid,namesign) :: find_branches (p+1) brs + with Exit-> error_ind_scheme "the branches of") + | (_,Some _,_)::_ -> error_ind_scheme "the branches of" + | [] -> [] in + let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in + indsign,scheme + + | Some ( _,None,ind) -> (* Standard scheme from an inductive type *) + let indhd,indargs = decompose_app ind in + let npred = List.length scheme.predicates in + 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 + | _ when is_pred p c = IndArg -> [] + | _ -> raise Exit in + let rec find_branches p lbrch = + match lbrch with + | (_,None,t)::brs -> + (try + let lchck_brch = check_branch p t in + let n = List.fold_left + (fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in + let recvarname, hyprecname, avoid = + make_up_names n scheme.indref names_info in + let namesign = + List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname)) + lchck_brch in + (avoid,namesign) :: find_branches (p+1) brs + with Exit -> error_ind_scheme "the branches of") + | (_,Some _,_)::_ -> error_ind_scheme "the branches of" + | [] -> + (* Check again conclusion *) + + let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in + let ind_is_ok = + list_lastn scheme.nargs indargs + = extended_rel_list 0 scheme.args in + if not (ccl_arg_ok & ind_is_ok) then + error "Cannot recognize the conclusion of an induction schema"; + [] + in + let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in + indsign,scheme + + +let find_elim_signature isrec 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 + if isrec then lookup_eliminator mind s + else pf_apply 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 indsign,elim_scheme = compute_elim_signature elimc elimt hyp0 in + (indsign,elim_scheme) + + +let mapi f l = + let rec mapi_aux f i l = + match l with + | [] -> [] + | e::l' -> f e i :: mapi_aux f (i+1) l' in + mapi_aux f 0 l + + +(* Instanciate all meta variables of elimclause using lid, some elts + of lid are parameters (first ones), the other are + arguments. Returns the clause obtained. *) +let recolle_clenv scheme lid elimclause gl = + let _,arr = destApp elimclause.templval.rebus in + let lindmv = + Array.map + (fun x -> + match kind_of_term x with + | Meta mv -> mv + | _ -> errorlabstrm "elimination_clause" + (str "The type of elimination clause is not well-formed")) + arr in + let nmv = Array.length lindmv in + let lidparams,lidargs = cut_list (scheme.nparams) lid in + let nidargs = List.length lidargs in + (* parameters correspond to first elts of lid. *) + let clauses_params = + mapi (fun id i -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i)) lidparams in + (* arguments correspond to last elts of lid. *) + let clauses_args = + mapi + (fun id i -> mkVar id , pf_get_hyp_typ gl id , lindmv.(nmv-nidargs+i)) + lidargs in + let clause_indarg = + match scheme.indarg with + | None -> [] + | Some (x,_,typx) -> [] + in + let clauses = clauses_params@clauses_args@clause_indarg in + (* iteration of clenv_fchain with all infos we have. *) + List.fold_right + (fun e acc -> + let x,y,i = e in + (* from_n (Some 0) means that x should be taken "as is" without + trying to unify (which would lead to trying to apply it to + evars if y is a product). *) + let indclause = mk_clenv_from_n gl (Some 0) (x,y) in + let elimclause' = clenv_fchain i acc indclause in + elimclause') + (List.rev clauses) + elimclause + + +(* Unification of the goal and the principle applied to meta variables: + (elimc ?i ?j ?k...?l). This solves partly meta variables (and may + produce new ones). Then refine with the resulting term with holes. +*) +let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl = + let elimt = scheme.elimt in + let elimc,lbindelimc = + match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in + (* elimclause contains this: (elimc ?i ?j ?k...?l) *) + let elimclause = + make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in + (* elimclause' is built from elimclause by instanciating all args and params. *) + let elimclause' = recolle_clenv scheme indvars elimclause gl in + (* one last resolution (useless?) *) + let resolved = clenv_unique_resolver true elimclause' gl in + clenv_refine resolved gl + +(* Induction with several induction arguments, main differences with + induction_from_context is that there is no main induction argument, + so we chose one to be the positioning reference. On the other hand, + all args and params must be given, so we help a bit the unifier by + making the "pattern" by hand before calling induction_tac_felim + FIXME: REUNIF AVEC induction_tac_felim? *) +let induction_from_context_l isrec elim_info lid names gl = + let indsign,scheme = elim_info in + (* number of all args, counting farg and indarg if present. *) + let nargs_indarg_farg = scheme.nargs + + (if scheme.farg_in_concl then 1 else 0) + + (if scheme.indarg <> None then 1 else 0) in + (* Number of given induction args must be exact. *) + if List.length lid <> nargs_indarg_farg + scheme.nparams then + error "not the right number of arguments given to induction scheme"; + let env = pf_env gl in + (* hyp0 is used for re-introducing hyps at the right place afterward. + We chose the first element of the list of variables on which to + induct. It is probably the first of them appearing in the + context. *) + let hyp0,indvars,lid_params = + match lid with + | [] -> anomaly "induction_from_context_l" + | e::l -> + let nargs_without_first = nargs_indarg_farg - 1 in + let ivs,lp = cut_list nargs_without_first l in + e, ivs, lp in + let statlists,lhyp0,indhyps,deps = cook_sign None (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 + let dephyps = List.map (fun (id,_,_) -> id) deps in + let deps_cstr = + List.fold_left (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in + (* terms to patternify we must patternify indarg or farg if present in concl *) + let lid_in_pattern = + if scheme.indarg <> None & not scheme.indarg_in_concl then List.rev indvars + else List.rev (hyp0::indvars) in + let lidcstr = List.map (fun x -> mkVar x) lid_in_pattern in + let realindvars = (* hyp0 is a real induction arg if it is not the + farg in the conclusion of the induction scheme *) + List.rev ((if scheme.farg_in_concl then indvars else hyp0::indvars) @ lid_params) in + (* Magistral effet de bord: comme dans induction_from_context. *) + tclTHENLIST + [ + (* Generalize dependent hyps (but not args) *) + if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr; + thin dephyps; (* clear dependent hyps *) + (* pattern to make the predicate appear. *) + reduce (Pattern (List.map (fun e -> ([],e)) lidcstr)) onConcl; + (* FIXME: Tester ca avec un principe dependant et non-dependant *) + (if isrec then tclTHENFIRSTn else tclTHENLASTn) + (tclTHENLIST [ + (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all + possible holes using arguments given by the user (but the + functional one). *) + induction_tac_felim realindvars scheme; + tclTRY (thin (List.rev (indhyps))); + ]) + (array_map2 + (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names) + ] + gl + + -let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl = +let induction_from_context isrec elim_info hyp0 names 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 indsign,scheme = elim_info in + + let indref = match scheme.indref with | None -> assert false | Some x -> x 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 indvars = find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in + (* induction_from_context_l isrec elim_info (hyp0::List.rev indvars) names gl *) + let statlists,lhyp0,indhyps,deps = cook_sign (Some 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 = + let deps_cstr = List.fold_left (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in @@ -1590,11 +1938,11 @@ let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl = "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; + [ if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr; thin dephyps; (if isrec then tclTHENFIRSTn else tclTHENLASTn) (tclTHENLIST - [ induction_tac hyp0 typ0 (elimc,elimt); + [ induction_tac hyp0 typ0 scheme (*scheme.elimc,scheme.elimt*); thin [hyp0]; tclTRY (thin indhyps) ]) (array_map2 @@ -1602,15 +1950,38 @@ let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl = ] gl + + +exception TryNewInduct of exn + 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 + let (indsign,scheme as elim_info) = find_elim_signature isrec elim hyp0 gl in + if scheme.indarg = None then (* This is not a standard induction scheme (the + argument is probably a parameter) So try the + more general induction mechanism. *) + induction_from_context_l isrec elim_info [hyp0] names gl + else + let indref = match scheme.indref with | None -> assert false | Some x -> x in + tclTHEN + (atomize_param_of_ind (indref,scheme.nparams) hyp0) + (induction_from_context isrec elim_info hyp0 names) gl + +(* Induction on a list of induction arguments. Analyse the elim + scheme (which is mandatory for multiple ind args), check that all + parameters and arguments are given (mandatory too). *) +let induction_without_atomization isrec elim names lid gl = + let (indsign,scheme as elim_info) = + find_elim_signature isrec elim (List.hd lid) gl in + let awaited_nargs = + scheme.nparams + scheme.nargs + + (if scheme.farg_in_concl then 1 else 0) + + (if scheme.indarg <> None then 1 else 0) + in + let nlid = List.length lid in + if nlid <> awaited_nargs + then error "Not the right number of induction arguments" + else induction_from_context_l isrec elim_info lid 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())) -> @@ -1623,18 +1994,119 @@ let new_induct_gen isrec elim names c gl = (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)) +(* The two following functions should already exist, but found nowhere *) +(* Unfolds x by its definition everywhere *) +let unfold_body x gl = + let hyps = pf_hyps gl in + let xval = + match Sign.lookup_named x hyps with + (_,Some xval,_) -> xval + | _ -> errorlabstrm "unfold_body" + (pr_id x ++ str" is not a defined hypothesis") in + let aft = afterHyp x gl in + let hl = List.fold_right (fun (y,yval,_) cl -> (y,[],InHyp) :: cl) aft [] in + let xvar = mkVar x in + let rfun _ _ c = replace_term xvar xval c in + tclTHENLIST + [tclMAP (fun h -> reduct_in_hyp rfun h) hl; + reduct_in_concl (rfun,DEFAULTcast)] gl + +(* Unfolds x by its definition everywhere and clear x. This may raise + an error if x is not defined. *) +let unfold_all x gl = + let (_,xval,_) = pf_get_hyp gl x in + (* If x has a body, simply replace x with body and clear x *) + if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl + else tclIDTAC gl + + +(* Induction on a list of arguments. First make induction arguments + atomic (using letins), then do induction. The specificity here is + that all arguments and parameters of the scheme are given + (mandatory for the moment), so we don't need to deal with + parameters of the inductive type as in new_induct_gen. *) +let new_induct_gen_l isrec elim names lc gl = + let newlc = ref [] in + let letids = ref [] in + let rec atomize_list l gl = + match l with + | [] -> tclIDTAC gl + | c::l' -> + match kind_of_term c with + | Var id when not (mem_named_context id (Global.named_context())) -> + let _ = newlc:= id::!newlc in + atomize_list l' gl + + | _ -> + let x = + id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in + + let id = fresh_id [] x gl in + let newl' = List.map (replace_term c (mkVar id)) l' in + let _ = newlc:=id::!newlc in + let _ = letids:=id::!letids in + tclTHEN + (letin_tac true (Name id) c allClauses) + (atomize_list newl') gl in + tclTHENLIST + [ + (atomize_list lc); + (fun gl' -> (* recompute each time to have the new value of newlc *) + induction_without_atomization isrec elim names !newlc gl') ; + (* after induction, try to unfold all letins created by atomize_list + FIXME: unfold_all does not exist anywhere else? *) + (fun gl' -> (* recompute each time to have the new value of letids *) + tclMAP (fun x -> tclTRY (unfold_all x)) !letids gl') + ] + gl -let new_induct = new_induct_destruct true -let new_destruct = new_induct_destruct false + +let induct_destruct_l isrec lc elim names = + (* Several induction hyps: induction scheme is mandatory *) + let _ = + if elim = None + then + error ("Induction scheme must be given when several induction hypothesis.\n" + ^ "Example: induction x1 x2 x3 using my_scheme.") in + let newlc = + List.map + (fun x -> + match x with (* FIXME: should we deal with ElimOnIdent? *) + | ElimOnConstr x -> x + | _ -> error "don't know where to find some argument") + lc in + new_induct_gen_l isrec elim names newlc + + +(* Induction either over a term, over a quantified premisse, or over + several quantified premisses (like with functional induction + principles). + TODO: really unify induction with one and induction with several + args *) +let induct_destruct isrec lc elim names = + assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) + if List.length lc = 1 then (* induction on one arg: use old mechanism *) + try + let c = List.hd lc in + 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)) + with (* If this fails, try with new mechanism but if it fails too, + then the exception is the first one. *) + | x -> (try induct_destruct_l isrec lc elim names with _ -> raise x) + else induct_destruct_l isrec lc elim names + + + + +let new_induct = induct_destruct true +let new_destruct = induct_destruct false (* The registered tactic, which calls the default elimination * if no elimination constant is provided. *) @@ -1645,23 +2117,12 @@ let new_destruct = new_induct_destruct false 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_id hyp = 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 + | NamedHyp id -> simple_induct_id id + | AnonHyp n -> simple_induct_nodep n (* Destruction tactics *) @@ -1682,25 +2143,25 @@ let simple_destruct = function *) 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 + let clause = mk_clenv_type_of gl elim in + match kind_of_term (last_arg clause.templval.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 + clenv_unify true Reduction.CUMUL t + (clenv_meta_type clause mv) clause in + res_pf clause' ~allow_K: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 + let elimc = 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 + let elimc = make_case_gen env (project gl) ind (elimination_sort_of_goal gl) in elim_scheme_type elimc t gl @@ -1773,9 +2234,12 @@ let dImp cls = (* Reflexivity tactics *) +let setoid_reflexivity = ref (fun _ -> assert false) +let register_setoid_reflexivity f = setoid_reflexivity := f + let reflexivity gl = match match_with_equation (pf_concl gl) with - | None -> error "The conclusion is not a substitutive equation" + | None -> !setoid_reflexivity gl | Some (hdcncl,args) -> one_constructor 1 NoBindings gl let intros_reflexivity = (tclTHEN intros reflexivity) @@ -1787,9 +2251,12 @@ let intros_reflexivity = (tclTHEN intros reflexivity) defined and the conclusion is a=b, it solves the goal doing (Cut b=a;Intro H;Case H;Constructor 1) *) +let setoid_symmetry = ref (fun _ -> assert false) +let register_setoid_symmetry f = setoid_symmetry := f + let symmetry gl = match match_with_equation (pf_concl gl) with - | None -> error "The conclusion is not a substitutive equation" + | None -> !setoid_symmetry gl | Some (hdcncl,args) -> let hdcncls = string_of_inductive hdcncl in begin @@ -1810,12 +2277,14 @@ let symmetry gl = gl end +let setoid_symmetry_in = ref (fun _ _ -> assert false) +let register_setoid_symmetry_in f = setoid_symmetry_in := f + 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" + | None -> !setoid_symmetry_in id gl | Some (hdcncl,args) -> let symccl = match args with | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) @@ -1845,9 +2314,12 @@ let intros_symmetry = --Eduardo (19/8/97) *) +let setoid_transitivity = ref (fun _ _ -> assert false) +let register_setoid_transitivity f = setoid_transitivity := f + let transitivity t gl = match match_with_equation (pf_concl gl) with - | None -> error "The conclusion is not a substitutive equation" + | None -> !setoid_transitivity t gl | Some (hdcncl,args) -> let hdcncls = string_of_inductive hdcncl in begin @@ -1886,7 +2358,6 @@ let interpretable_as_section_decl d1 d2 = match d1,d2 with | (_,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 = @@ -1894,16 +2365,15 @@ let abstract_subproof name tac gls = (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) + then (s1,push_named_context_val d s2) else (add_named_decl d s1,s2)) - global_sign (empty_named_context,empty_named_context) in + global_sign (empty_named_context,empty_named_context_val) 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"; + error "\"abstract\" cannot handle existentials"; let lemme = - start_proof na (IsGlobal (Proof Lemma)) secsign concl (fun _ _ -> ()); + start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ()); let _,(const,kind,_) = try by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); @@ -1913,9 +2383,8 @@ let abstract_subproof name tac gls = (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)) + let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in + constr_of_global (ConstRef con) in exact_no_check (applist (lemme, @@ -1928,3 +2397,29 @@ let tclABSTRACT name_op tac gls = | None -> add_suffix (get_current_proof_name ()) "_subproof" in abstract_subproof s tac gls + + +let admit_as_an_axiom gls = + 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 name = add_suffix (get_current_proof_name ()) "_admitted" 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 error "\"admit\" cannot handle existentials"; + let axiom = + let cd = Entries.ParameterEntry concl in + let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in + constr_of_global (ConstRef con) + in + exact_no_check + (applist (axiom, + List.rev (Array.to_list (instance_from_named_context sign)))) + gls |