diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 787 |
1 files changed, 402 insertions, 385 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 186b5c48..988d9f53 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - +open Compat open Pp open Util open Names @@ -25,9 +24,8 @@ open Libnames open Evd open Pfedit open Tacred -open Rawterm +open Glob_term open Tacmach -open Proof_trees open Proof_type open Logic open Evar_refiner @@ -61,6 +59,8 @@ let inj_with_occurrences e = (all_occurrences_expr,e) let dloc = dummy_loc +let typ_of = Retyping.get_type_of + (* Option for 8.2 compatibility *) open Goptions let dependent_propositions_elimination = ref true @@ -72,25 +72,15 @@ let use_dependent_propositions_elimination () = let _ = declare_bool_option { optsync = true; + optdepr = false; optname = "dependent-propositions-elimination tactic"; optkey = ["Dependent";"Propositions";"Elimination"]; optread = (fun () -> !dependent_propositions_elimination) ; optwrite = (fun b -> dependent_propositions_elimination := b) } -let apply_in_side_conditions_come_first = ref true - -let use_apply_in_side_conditions_come_first () = - !apply_in_side_conditions_come_first - && Flags.version_strictly_greater Flags.V8_2 - -let _ = - declare_bool_option - { optsync = true; - optname = "apply-in side-conditions coming first"; - optkey = ["Side";"Conditions";"First";"For";"apply";"in"]; - optread = (fun () -> !dependent_propositions_elimination) ; - optwrite = (fun b -> dependent_propositions_elimination := b) } - +let finish_evar_resolution env initial_sigma c = + snd (Pretyping.solve_remaining_evars true true solve_by_implicit_tactic + env initial_sigma c) (*********************************************) (* Tactics *) @@ -165,7 +155,6 @@ let internal_cut_rev_replace = internal_cut_rev_gen true (* Moving hypotheses *) let move_hyp = Tacmach.move_hyp -let order_hyps = Tacmach.order_hyps (* Renaming hypotheses *) let rename_hyp = Tacmach.rename_hyp @@ -285,9 +274,12 @@ let reduct_in_hyp redfun (id,where) gl = convert_hyp_no_check (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl +let revert_cast (redfun,kind as r) = + if kind = DEFAULTcast then (redfun,REVERTcast) else r + let reduct_option redfun = function | Some id -> reduct_in_hyp (fst redfun) id - | None -> reduct_in_concl redfun + | None -> reduct_in_concl (revert_cast redfun) (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb t env sigma c = @@ -323,35 +315,25 @@ let change chg c cls gl = cls gl (* Pour usage interne (le niveau User est pris en compte par reduce) *) -let try_red_in_concl = reduct_in_concl (try_red_product,DEFAULTcast) -let red_in_concl = reduct_in_concl (red_product,DEFAULTcast) +let try_red_in_concl = reduct_in_concl (try_red_product,REVERTcast) +let red_in_concl = reduct_in_concl (red_product,REVERTcast) let red_in_hyp = reduct_in_hyp red_product -let red_option = reduct_option (red_product,DEFAULTcast) -let hnf_in_concl = reduct_in_concl (hnf_constr,DEFAULTcast) +let red_option = reduct_option (red_product,REVERTcast) +let hnf_in_concl = reduct_in_concl (hnf_constr,REVERTcast) let hnf_in_hyp = reduct_in_hyp hnf_constr -let hnf_option = reduct_option (hnf_constr,DEFAULTcast) -let simpl_in_concl = reduct_in_concl (simpl,DEFAULTcast) +let hnf_option = reduct_option (hnf_constr,REVERTcast) +let simpl_in_concl = reduct_in_concl (simpl,REVERTcast) let simpl_in_hyp = reduct_in_hyp simpl -let simpl_option = reduct_option (simpl,DEFAULTcast) -let normalise_in_concl = reduct_in_concl (compute,DEFAULTcast) +let simpl_option = reduct_option (simpl,REVERTcast) +let normalise_in_concl = reduct_in_concl (compute,REVERTcast) let normalise_in_hyp = reduct_in_hyp compute -let normalise_option = reduct_option (compute,DEFAULTcast) +let normalise_option = reduct_option (compute,REVERTcast) 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_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast) 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. *) - -let checking_fun = function - (* Expansion is not necessarily well-typed: e.g. expansion of t into x is - not well-typed in [H:(P t); x:=t |- G] because x is defined after H *) - | Fold _ -> with_check - | Pattern _ -> with_check - | _ -> (fun x -> x) - (* The main reduction function *) let reduction_clause redexp cl = @@ -433,31 +415,34 @@ let find_intro_names ctxt gl = ctxt (pf_env gl , []) in List.rev res -let build_intro_tac id = function - | MoveToEnd true -> introduction id - | dest -> tclTHEN (introduction id) (move_hyp true id dest) +let build_intro_tac id dest tac = match dest with + | MoveToEnd true -> tclTHEN (introduction id) (tac id) + | dest -> tclTHENLIST [introduction id; move_hyp true id dest; tac id] -let rec intro_gen loc name_flag move_flag force_flag dep_flag gl = +let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl = match kind_of_term (pf_concl gl) with | Prod (name,t,u) when not dep_flag or (dependent (mkRel 1) u) -> - build_intro_tac (find_name loc (name,None,t) gl name_flag) move_flag gl + build_intro_tac (find_name loc (name,None,t) gl name_flag) move_flag tac gl | LetIn (name,b,t,u) when not dep_flag or (dependent (mkRel 1) u) -> - build_intro_tac (find_name loc (name,Some b,t) gl name_flag) move_flag + build_intro_tac (find_name loc (name,Some b,t) gl name_flag) move_flag tac gl | _ -> if not force_flag then raise (RefinerError IntroNeedsProduct); try tclTHEN try_red_in_concl - (intro_gen loc name_flag move_flag force_flag dep_flag) gl + (intro_then_gen loc name_flag move_flag force_flag dep_flag tac) gl with Redelimination -> user_err_loc(loc,"Intro",str "No product even after head-reduction.") +let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> tclIDTAC) let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) no_move true false let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false false +let intro_then = intro_then_gen dloc (IntroAvoid []) no_move false false let intro = intro_gen dloc (IntroAvoid []) no_move false false let introf = intro_gen dloc (IntroAvoid []) no_move true false let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false false -let introf_move_name destopt = intro_gen dloc (IntroAvoid []) destopt true false + +let intro_then_force = intro_then_gen dloc (IntroAvoid []) no_move true false (**** Multiple introduction tactics ****) @@ -469,8 +454,13 @@ let intros = tclREPEAT intro let intro_erasing id = tclTHEN (thin [id]) (introduction id) -let intro_forthcoming_gen loc name_flag move_flag dep_flag = - tclREPEAT (intro_gen loc name_flag move_flag false dep_flag) +let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac = + let rec aux ids = + tclORELSE0 + (intro_then_gen loc name_flag move_flag false dep_flag + (fun id -> aux (id::ids))) + (tac ids) in + aux [] let rec get_next_hyp_position id = function | [] -> error ("No such hypothesis: " ^ string_of_id id) @@ -517,8 +507,8 @@ let intro_move idopt hto = match idopt with | Some id -> intro_gen dloc (IntroMustBe id) hto true false 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_displayed env ccl id + | AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n + | NamedHyp id -> Detyping.lookup_name_as_displayed env ccl id let pf_lookup_hypothesis_as_renamed_gen red h gl = let env = pf_env gl in @@ -565,8 +555,13 @@ 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 tclCHECKVAR id gl = ignore (pf_get_hyp gl id); tclIDTAC gl + +let try_intros_until_id_check id = + tclORELSE (intros_until_id id) (tclCHECKVAR id) + let try_intros_until tac = function - | NamedHyp id -> tclTHEN (tclTRY (intros_until_id id)) (tac id) + | NamedHyp id -> tclTHEN (try_intros_until_id_check id) (tac id) | AnonHyp n -> tclTHEN (intros_until_n n) (onLastHypId tac) let rec intros_move = function @@ -583,17 +578,32 @@ let dependent_in_decl a (_,c,t) = (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) +let onOpenInductionArg tac = function + | ElimOnConstr cbl -> + tac cbl + | ElimOnAnonHyp n -> + tclTHEN + (intros_until_n n) + (onLastHyp (fun c -> tac (Evd.empty,(c,NoBindings)))) + | ElimOnIdent (_,id) -> + (* A quantified hypothesis *) + tclTHEN + (try_intros_until_id_check id) + (tac (Evd.empty,(mkVar id,NoBindings))) + let onInductionArg tac = function - | ElimOnConstr (c,lbindc as cbl) -> - if isVar c & lbindc = NoBindings then - tclTHEN (tclTRY (intros_until_id (destVar c))) (tac cbl) - else - tac cbl + | ElimOnConstr cbl -> + tac cbl | ElimOnAnonHyp n -> tclTHEN (intros_until_n n) (onLastHyp (fun c -> tac (c,NoBindings))) | ElimOnIdent (_,id) -> - (*Identifier apart because id can be quantified in goal and not typable*) - tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings)) + (* A quantified hypothesis *) + tclTHEN (try_intros_until_id_check id) (tac (mkVar id,NoBindings)) + +let map_induction_arg f = function + | ElimOnConstr (sigma,(c,bl)) -> ElimOnConstr (f (sigma,c),bl) + | ElimOnAnonHyp n -> ElimOnAnonHyp n + | ElimOnIdent id -> ElimOnIdent id (**************************) (* Refinement tactics *) @@ -615,9 +625,9 @@ let bring_hyps hyps = let resolve_classes gl = let env = pf_env gl and evd = project gl in - if evd = Evd.empty then tclIDTAC gl + if Evd.is_empty evd then tclIDTAC gl else - let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in + let evd' = Typeclasses.resolve_typeclasses env evd in (tclTHEN (tclEVARS evd') tclNORMEVAR) gl (**************************) @@ -723,24 +733,15 @@ let index_of_ind_arg t = | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let elim_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; - modulo_delta = empty_transparent_state; - resolve_evars = false; - use_evars_pattern_unification = true; -} - -let elimination_clause_scheme with_evars allow_K i elimclause indclause gl = +let elimination_clause_scheme with_evars ?(flags=elim_flags) i elimclause indclause gl = let indmv = (match kind_of_term (nth_arg i 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 ~flags:elim_flags indmv elimclause indclause in - res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags - gl + let elimclause' = clenv_fchain ~flags indmv elimclause indclause in + res_pf elimclause' ~with_evars:with_evars ~flags gl (* * Elimination tactic with bindings and using an arbitrary @@ -769,8 +770,8 @@ let general_elim_clause elimtac (c,lbindc) elim gl = let indclause = make_clenv_binding gl (c,t) lbindc in general_elim_clause_gen elimtac indclause elim gl -let general_elim with_evars c e ?(allow_K=true) = - general_elim_clause (elimination_clause_scheme with_evars allow_K) c e +let general_elim with_evars c e = + general_elim_clause (elimination_clause_scheme with_evars) c e (* Elimination tactic with bindings but using the default elimination * constant associated with the type. *) @@ -786,15 +787,15 @@ let default_elim with_evars (c,_ as cx) gl = let elim_in_context with_evars c = function | Some elim -> general_elim with_evars c {elimindex = Some (-1); elimbody = elim} - ~allow_K:true | None -> default_elim with_evars c let elim with_evars (c,lbindc as cx) elim = match kind_of_term c with | Var id when lbindc = NoBindings -> - tclTHEN (tclTRY (intros_until_id id)) + tclTHEN (try_intros_until_id_check id) (elim_in_context with_evars cx elim) - | _ -> elim_in_context with_evars cx elim + | _ -> + elim_in_context with_evars cx elim (* The simplest elimination tactic, with no substitutions at all. *) @@ -810,13 +811,13 @@ let simplest_elim c = default_elim false (c,NoBindings) (e.g. it could replace id:A->B->C by id:C, knowing A/\B) *) -let clenv_fchain_in id elim_flags mv elimclause hypclause = - try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause - with PretypeError (env,NoOccurrenceFound (op,_)) -> +let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause = + try clenv_fchain ~flags mv elimclause hypclause + with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> (* Set the hypothesis name in the message *) - raise (PretypeError (env,NoOccurrenceFound (op,Some id))) + raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) -let elimination_in_clause_scheme with_evars id i elimclause indclause gl = +let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl = let indmv = destMeta (nth_arg i elimclause.templval.rebus) in let hypmv = try match list_remove indmv (clenv_independent elimclause) with @@ -824,12 +825,11 @@ let elimination_in_clause_scheme with_evars id i elimclause indclause gl = | _ -> failwith "" with Failure _ -> errorlabstrm "elimination_clause" (str "The type of elimination clause is not well-formed.") in - let elimclause' = clenv_fchain indmv elimclause indclause in + let elimclause' = clenv_fchain ~flags indmv elimclause indclause in let hyp = mkVar id in let hyp_typ = pf_type_of gl hyp in let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in - let elimclause'' = - clenv_fchain_in id elim_flags hypmv elimclause' hypclause in + let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in if eq_constr hyp_typ new_hyp_typ then errorlabstrm "general_rewrite_in" @@ -855,8 +855,8 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl = let general_case_analysis with_evars (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 with_evars cx) + tclTHEN (try_intros_until_id_check id) + (general_case_analysis_in_context with_evars cx) | _ -> general_case_analysis_in_context with_evars cx @@ -871,6 +871,7 @@ type conjunction_status = let make_projection sigma params cstr sign elim i n c = let elim = match elim with | NotADefinedRecordUseScheme elim -> + (* bugs: goes from right to left when i increases! *) let (na,b,t) = List.nth cstr.cs_args i in let b = match b with None -> mkRel (i+1) | Some b -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in @@ -885,6 +886,7 @@ let make_projection sigma params cstr sign elim i n c = else None | DefinedRecord l -> + (* goes from left to right when i increases! *) match List.nth l i with | Some proj -> let t = Typeops.type_of_constant (Global.env()) proj in @@ -919,7 +921,7 @@ let descend_in_conjunctions tac exit c gl = | Some (p,pt) -> tclTHENS (internal_cut id pt) - [refine_no_check p; + [refine p; (* Might be ill-typed due to forbidden elimination. *) tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl) n) gl | None -> @@ -961,9 +963,9 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> if with_destruct then descend_in_conjunctions - try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl + try_main_apply (fun _ -> Loc.raise loc exn) c gl else - Stdpp.raise_with_loc loc exn + Loc.raise loc exn in try_red_apply thm_ty0 in try_main_apply with_destruct c gl0 @@ -1023,8 +1025,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl = let apply_in_once sidecond_first with_delta with_destruct with_evars id (loc,(d,lbind)) gl0 = - let flags = - if with_delta then default_unify_flags else default_no_delta_unify_flags in + let flags = if with_delta then elim_flags else elim_no_delta_flags in let t' = pf_get_hyp_typ gl0 id in let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in let rec aux with_destruct c gl = @@ -1119,7 +1120,7 @@ let clear_wildcards ids = try with_check (Tacmach.thin_no_check [id]) gl with ClearDependencyError (id,err) -> (* Intercept standard [thin] error message *) - Stdpp.raise_with_loc loc + Loc.raise loc (error_clear_dependency (pf_env gl) (id_of_string "_") err)) ids @@ -1137,11 +1138,14 @@ let rec intros_clearing = function (* Modifying/Adding an hypothesis *) let specialize mopt (c,lbind) g = - let term = - if lbind = NoBindings then c + let tac, term = + if lbind = NoBindings then + let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in + tclEVARS evd, nf_evar evd c else let clause = make_clenv_binding g (c,pf_type_of g c) lbind in - let clause = clenv_unify_meta_types clause in + let flags = { default_unify_flags with resolve_evars = true } in + let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_stack clause.evd (clenv_value clause) in let nargs = List.length tstack in let tstack = match mopt with @@ -1158,16 +1162,18 @@ let specialize mopt (c,lbind) g = errorlabstrm "" (str "Cannot infer an instance for " ++ pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ str "."); - term + tclEVARS clause.evd, term in match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with | Var id when List.mem id (pf_ids_of_hyps g) -> - tclTHENFIRST + tclTHEN tac + (tclTHENFIRST (fun g -> internal_cut_replace id (pf_type_of g term) g) - (exact_no_check term) g - | _ -> tclTHENLAST - (fun g -> cut (pf_type_of g term) g) - (exact_no_check term) g + (exact_no_check term)) g + | _ -> tclTHEN tac + (tclTHENLAST + (fun g -> cut (pf_type_of g term) g) + (exact_no_check term)) g (* Keeping only a few hypotheses *) @@ -1245,12 +1251,20 @@ let simplest_split = split NoBindings (* Decomposing introductions *) (*****************************) +(* Rewriting function for rewriting one hypothesis at the time *) let forward_general_multi_rewrite = ref (fun _ -> failwith "general_multi_rewrite undefined") +(* Rewriting function for substitution (x=t) everywhere at the same time *) +let forward_subst_one = + ref (fun _ -> failwith "subst_one undefined") + let register_general_multi_rewrite f = forward_general_multi_rewrite := f +let register_subst_one f = + forward_subst_one := f + let error_unexpected_extra_pattern loc nb pat = let s1,s2,s3 = match pat with | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no" @@ -1284,6 +1298,8 @@ let intro_or_and_pattern loc b ll l' tac id gl = let rewrite_hyp l2r id gl = let rew_on l2r = !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in + let subst_on l2r x rhs = + !forward_subst_one true x (id,rhs,l2r) in let clear_var_and_eq c = tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in @@ -1291,9 +1307,9 @@ let rewrite_hyp l2r id gl = match match_with_equality_type t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then - tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq lhs) gl + subst_on l2r (destVar lhs) rhs gl else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then - tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq rhs) gl + subst_on l2r (destVar rhs) lhs gl else tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl | Some (hdcncl,[c]) -> @@ -1315,57 +1331,65 @@ let rec explicit_intro_names = function | [] -> [] +let wild_id = id_of_string "_tmp" + +let rec list_mem_assoc_right id = function + | [] -> false + | (x,id')::l -> id = id' || list_mem_assoc_right id l + +let check_thin_clash_then id thin avoid tac = + if list_mem_assoc_right id thin then + let newid = next_ident_away (add_suffix id "'") avoid in + let thin = + List.map (on_snd (fun id' -> if id = id' then newid else id')) thin in + tclTHEN (rename_hyp [id,newid]) (tac thin) + else + tac thin + (* 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 b avoid thin destopt = function +let rec intros_patterns b avoid ids thin destopt tac = function | (loc, IntroWildcard) :: l -> - tclTHEN - (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) - no_move true false) - (onLastHypId (fun id -> - tclORELSE - (tclTHEN (clear [id]) (intros_patterns b avoid thin destopt l)) - (intros_patterns b avoid ((loc,id)::thin) destopt l))) + intro_then_gen loc (IntroBasedOn(wild_id,avoid@explicit_intro_names l)) + no_move true false + (fun id -> intros_patterns b avoid ids ((loc,id)::thin) destopt tac l) | (loc, IntroIdentifier id) :: l -> - tclTHEN - (intro_gen loc (IntroMustBe id) destopt true false) - (intros_patterns b avoid thin destopt l) + check_thin_clash_then id thin avoid (fun thin -> + intro_then_gen loc (IntroMustBe id) destopt true false + (fun id -> intros_patterns b avoid (id::ids) thin destopt tac l)) | (loc, IntroAnonymous) :: l -> - tclTHEN - (intro_gen loc (IntroAvoid (avoid@explicit_intro_names l)) - destopt true false) - (intros_patterns b avoid thin destopt l) + intro_then_gen loc (IntroAvoid (avoid@explicit_intro_names l)) + destopt true false + (fun id -> intros_patterns b avoid (id::ids) thin destopt tac l) | (loc, IntroFresh id) :: l -> - tclTHEN - (intro_gen loc (IntroBasedOn (id, avoid@explicit_intro_names l)) - destopt true false) - (intros_patterns b avoid thin destopt l) + (* todo: avoid thinned names to interfere with generation of fresh name *) + intro_then_gen loc (IntroBasedOn (id, avoid@explicit_intro_names l)) + destopt true false + (fun id -> intros_patterns b avoid (id::ids) thin destopt tac l) | (loc, IntroForthcoming onlydeps) :: l -> - tclTHEN - (intro_forthcoming_gen loc (IntroAvoid (avoid@explicit_intro_names l)) - destopt onlydeps) - (intros_patterns b avoid thin destopt l) + intro_forthcoming_then_gen loc (IntroAvoid (avoid@explicit_intro_names l)) + destopt onlydeps + (fun ids -> intros_patterns b avoid ids thin destopt tac l) | (loc, IntroOrAndPattern ll) :: l' -> - tclTHEN - introf - (onLastHypId - (intro_or_and_pattern loc b ll l' - (intros_patterns b avoid thin destopt))) + intro_then_force + (intro_or_and_pattern loc b ll l' + (intros_patterns b avoid ids thin destopt tac)) | (loc, IntroRewrite l2r) :: l -> - tclTHEN - (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) - no_move true false) - (onLastHypId (fun id -> + intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l)) + no_move true false + (fun id -> tclTHENLAST (* Skip the side conditions of the rewriting step *) (rewrite_hyp l2r id) - (intros_patterns b avoid thin destopt l))) - | [] -> clear_wildcards thin + (intros_patterns b avoid ids thin destopt tac l)) + | [] -> tac ids thin -let intros_pattern = intros_patterns false [] [] +let intros_pattern destopt = + intros_patterns false [] [] [] destopt (fun _ -> clear_wildcards) -let intro_pattern destopt pat = intros_patterns false [] [] destopt [dloc,pat] +let intro_pattern destopt pat = + intros_pattern destopt [dloc,pat] let intro_patterns = function | [] -> tclREPEAT intro @@ -1390,7 +1414,7 @@ let prepare_intros s ipat gl = match ipat with | IntroOrAndPattern ll -> make_id s gl, onLastHypId (intro_or_and_pattern loc true ll [] - (intros_patterns true [] [] no_move)) + (intros_patterns true [] [] [] no_move (fun _ -> clear_wildcards))) | IntroForthcoming _ -> user_err_loc (loc,"",str "Introduction pattern for one hypothesis expected") @@ -1400,7 +1424,8 @@ let ipat_of_name = function let allow_replace c gl = function (* A rather arbitrary condition... *) | Some (_, IntroIdentifier id) -> - fst (decompose_app ((strip_lam_assum c))) = mkVar id + let c = fst (decompose_app ((strip_lam_assum c))) in + isVar c && destVar c = id | _ -> false @@ -1422,7 +1447,8 @@ let as_tac id ipat = match ipat with | Some (loc,IntroRewrite l2r) -> !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl | Some (loc,IntroOrAndPattern ll) -> - intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) + intro_or_and_pattern loc true ll [] + (intros_patterns true [] [] [] no_move (fun _ -> clear_wildcards)) id | Some (loc, (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | @@ -1484,7 +1510,7 @@ let generalize_goal gl i ((occs,c,b),na) cl = let decls,cl = decompose_prod_n_assum i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in - let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in + let cl' = subst_closed_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in mkProd_or_LetIn (na,b,t) cl' @@ -1659,14 +1685,48 @@ let letin_tac with_eq name c occs gl = (* Implementation without generalisation: abbrev will be lost in hyps in *) (* in the extracted proof *) -let letin_abstract id c (occs,check_occs) gl = +let default_matching_flags sigma = { + modulo_conv_on_closed_terms = Some empty_transparent_state; + use_metas_eagerly_in_conv_on_closed_terms = false; + modulo_delta = empty_transparent_state; + modulo_delta_types = full_transparent_state; + check_applied_meta_types = true; + resolve_evars = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = false; + frozen_evars = + fold_undefined (fun evk _ evars -> ExistentialSet.add evk evars) + sigma ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; + modulo_betaiota = false; + modulo_eta = false; + allow_K_in_toplevel_higher_order_unification = false +} + +let make_pattern_test env sigma0 (sigma,c) = + let flags = default_matching_flags sigma0 in + let matching_fun t = + try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t) + with _ -> raise NotUnifiable in + let merge_fun c1 c2 = + match c1, c2 with + | Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) -> + raise NotUnifiable + | _ -> c1 in + { match_fun = matching_fun; merge_fun = merge_fun; + testing_state = None; last_found = None }, + (fun test -> match test.testing_state with + | None -> finish_evar_resolution env sigma0 (sigma,c) + | Some (sigma,_) -> nf_evar sigma c) + +let letin_abstract id c (test,out) (occs,check_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 = (all_occurrences,InHyp) & d = newdecl then + let newdecl = subst_closed_term_occ_decl_modulo occ test d in + if occ = (all_occurrences,InHyp) & eq_named_declaration d newdecl then if check_occs & not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls @@ -1675,19 +1735,21 @@ let letin_abstract id c (occs,check_occs) gl = 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 + | Some occ -> + subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in let lastlhyp = if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in - (depdecls,lastlhyp,ccl) + (depdecls,lastlhyp,ccl,out test) -let letin_tac_gen with_eq name c ty occs gl = +let letin_tac_gen with_eq name (sigmac,c) test ty occs gl = let id = - let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in + let t = match ty with Some t -> t | None -> typ_of (pf_env gl) sigmac c in + let x = id_of_name_using_hdchar (Global.env()) t 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 = match ty with Some t -> t | None -> pf_type_of gl c in + let (depdecls,lastlhyp,ccl,c) = letin_abstract id c test occs gl in + let t = match ty with Some t -> t | None -> pf_apply typ_of gl c in let newcl,eq_tac = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with @@ -1711,8 +1773,15 @@ let letin_tac_gen with_eq name c ty occs gl = tclMAP convert_hyp_no_check depdecls; eq_tac ] gl -let letin_tac with_eq name c ty occs = - letin_tac_gen with_eq name c ty (occs,true) +let make_eq_test c = (make_eq_test c,fun _ -> c) + +let letin_tac with_eq name c ty occs gl = + letin_tac_gen with_eq name (project gl,c) (make_eq_test c) ty (occs,true) gl + +let letin_pat_tac with_eq name c ty occs gl = + letin_tac_gen with_eq name c + (make_pattern_test (pf_env gl) (project gl) c) + ty (occs,true) gl (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *) let forward usetac ipat c gl = @@ -1755,6 +1824,9 @@ let unfold_all x gl = if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else tclIDTAC gl +(* Either unfold and clear if defined or simply clear if not a definition *) +let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id]) + (*****************************) (* High-level induction *) (*****************************) @@ -1797,16 +1869,6 @@ let check_unused_names names = (str"Unused introduction " ++ str (plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc pr_intro_pattern names) -let rec first_name_buggy avoid gl (loc,pat) = match pat with - | IntroOrAndPattern [] -> no_move - | IntroOrAndPattern ([]::l) -> - first_name_buggy avoid gl (loc,IntroOrAndPattern l) - | IntroOrAndPattern ((p::_)::_) -> first_name_buggy avoid gl p - | IntroWildcard -> no_move - | IntroRewrite _ -> no_move - | IntroIdentifier id -> MoveAfter id - | IntroAnonymous | IntroFresh _ | IntroForthcoming _ -> (* buggy *) no_move - let rec consume_pattern avoid id isdep gl = function | [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), []) | (loc,IntroAnonymous)::names -> @@ -1822,7 +1884,8 @@ let rec consume_pattern avoid id isdep gl = function ((loc,IntroIdentifier (fresh_id avoid id' gl)), names) | pat::names -> (pat,names) -let re_intro_dependent_hypotheses (lstatus,rstatus) tophyp = +let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) = + let tophyp = match tophyp with None -> MoveToEnd true | Some hyp -> MoveAfter hyp in let newlstatus = (* if some IH has taken place at the top of hyps *) List.map (function (hyp,MoveToEnd true) -> (hyp,tophyp) | x -> x) lstatus in @@ -1832,20 +1895,46 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) tophyp = let update destopt tophyp = if destopt = no_move then tophyp else destopt -let safe_dest_intros_patterns avoid dest pat gl = - try intros_patterns true avoid [] dest pat gl +let safe_dest_intros_patterns avoid thin dest pat tac gl = + try intros_patterns true avoid [] thin dest tac pat gl with UserError ("move_hyp",_) -> - (* May happen if the lemma has dependent arguments that has resolved - only after cook_sign is called, e.g. as in + (* May happen if the lemma has dependent arguments that are resolved + only after cook_sign is called, e.g. as in "destruct dec" in context "dec:forall x, {x=0}+{x<>0}; a:A |- if dec a then True else False" - for argument a of dec which will be found only lately *) - intros_patterns true avoid [] no_move pat gl + where argument a of dec will be found only lately *) + intros_patterns true avoid [] [] no_move tac pat gl type elim_arg_kind = RecArg | IndArg | OtherArg -let induct_discharge destopt avoid' tac (avoid,ra) names gl = +type recarg_position = + | AfterFixedPosition of identifier option (* None = top of context *) + +let update_dest (recargdests,tophyp as dests) = function + | [] -> dests + | hyp::_ -> + (match recargdests with + | AfterFixedPosition None -> AfterFixedPosition (Some hyp) + | x -> x), + (match tophyp with None -> Some hyp | x -> x) + +let get_recarg_dest (recargdests,tophyp) = + match recargdests with + | AfterFixedPosition None -> MoveToEnd true + | AfterFixedPosition (Some id) -> MoveAfter id + +(* Current policy re-introduces recursive arguments of destructed + variable at the place of the original variable while induction + hypothesese are introduced at the top of the context. Since in the + general case of an inductive scheme, the induction hypotheses can + arrive just after the recursive arguments (e.g. as in "forall + t1:tree, P t1 -> forall t2:tree, P t2 -> P (node t1 t2)", we need + to update the position for t2 after "P t1" is introduced if ever t2 + had to be introduced at the top of the context). +*) + +let induct_discharge dests avoid' tac (avoid,ra) names gl = let avoid = avoid @ avoid' in - let rec peel_tac ra names tophyp gl = + let rec peel_tac ra dests names thin gl = match ra with | (RecArg,deprec,recvarname) :: (IndArg,depind,hyprecname) :: ra' -> @@ -1855,37 +1944,33 @@ let induct_discharge destopt avoid' tac (avoid,ra) names gl = (pat, [dloc, IntroIdentifier id']) | _ -> consume_pattern avoid recvarname deprec gl names in let hyprec,names = consume_pattern avoid hyprecname depind gl names in - (* IH stays at top: we need to update tophyp *) - (* This is buggy for intro-or-patterns with different first hypnames *) - (* Would need to pass peel_tac as a continuation of intros_patterns *) - (* (or to have hypotheses classified by blocks...) *) - let newtophyp = - if tophyp=no_move then first_name_buggy avoid gl hyprec else tophyp - in - tclTHENLIST - [ safe_dest_intros_patterns avoid (update destopt tophyp) [recpat]; - safe_dest_intros_patterns avoid no_move [hyprec]; - peel_tac ra' names newtophyp] gl + let dest = get_recarg_dest dests in + safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin -> + safe_dest_intros_patterns avoid thin no_move [hyprec] (fun ids' thin -> + peel_tac ra' (update_dest dests ids') names thin)) + gl | (IndArg,dep,hyprecname) :: ra' -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid hyprecname dep gl names in - tclTHEN (safe_dest_intros_patterns avoid (update destopt tophyp) [pat]) - (peel_tac ra' names tophyp) gl + safe_dest_intros_patterns avoid thin no_move [pat] (fun ids thin -> + peel_tac ra' (update_dest dests ids) names thin) gl | (RecArg,dep,recvarname) :: ra' -> let pat,names = consume_pattern avoid recvarname dep gl names in - tclTHEN (safe_dest_intros_patterns avoid (update destopt tophyp) [pat]) - (peel_tac ra' names tophyp) gl + let dest = get_recarg_dest dests in + safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin -> + peel_tac ra' dests names thin) gl | (OtherArg,_,_) :: ra' -> let pat,names = match names with | [] -> (dloc, IntroAnonymous), [] | pat::names -> pat,names in - tclTHEN (safe_dest_intros_patterns avoid (update destopt tophyp) [pat]) - (peel_tac ra' names tophyp) gl + let dest = get_recarg_dest dests in + safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin -> + peel_tac ra' dests names thin) gl | [] -> check_unused_names names; - tac tophyp gl + tclTHEN (clear_wildcards thin) (tac dests) gl in - peel_tac ra names no_move gl + peel_tac ra dests names [] 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 @@ -2063,8 +2148,13 @@ let cook_sign hyp0_opt indvars env = fold_named_context_reverse compute_lstatus ~init:(MoveToEnd true) env in raise (Shunt (MoveToEnd true)) (* ?? FIXME *) with Shunt lhyp0 -> + let lhyp0 = match lhyp0 with + | MoveToEnd true -> None + | MoveAfter hyp -> Some hyp + | _ -> assert false in let statuslists = (!lstatus,List.rev !rstatus) in - (statuslists, (if hyp0_opt=None then MoveToEnd true else lhyp0), + let recargdests = AfterFixedPosition (if hyp0_opt=None then None else lhyp0) in + (statuslists, (recargdests,None), !indhyps, !decldeps) @@ -2167,23 +2257,6 @@ let make_up_names n ind_opt cname = 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 recognize "^s^"an induction scheme.") @@ -2194,8 +2267,6 @@ let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl) let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq") let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl") -let coq_block = lazy (Coqlib.coq_constant "tactics" ["Program";"Equality"] "block") - let mkEq t x y = mkApp (Lazy.force coq_eq, [| refresh_universes_strict t; x; y |]) @@ -2218,8 +2289,6 @@ let lift_togethern n l = l ([], n) in l' -let lift_together l = lift_togethern 0 l - let lift_list l = List.map (lift 1) l let ids_of_constr ?(all=false) vars c = @@ -2267,11 +2336,11 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = in (* Abstract by equalitites *) let eqs = lift_togethern 1 eqs in (* lift together and past genarg *) - let abseqs = it_mkProd_or_LetIn ~init:(lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in + let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in (* Abstract by the "generalized" hypothesis. *) let genarg = mkProd_or_LetIn (Name id, body, c) abseqs in (* Abstract by the extension of the context *) - let genctyp = it_mkProd_or_LetIn ~init:genarg ctx in + let genctyp = it_mkProd_or_LetIn genarg ctx in (* The goal will become this product. *) let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in (* Apply the old arguments giving the proper instantiation of the hyp *) @@ -2282,17 +2351,6 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls = let appeqs = mkApp (instc, Array.of_list refls) in (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *) mkApp (appeqs, abshypt) - -let deps_of_var id env = - Environ.fold_named_context - (fun _ (n,b,t) (acc : Idset.t) -> - if Option.cata (occur_var env id) false b || occur_var env id t then - Idset.add n acc - else acc) - env ~init:Idset.empty - -let idset_of_list = - List.fold_left (fun s x -> Idset.add x s) Idset.empty let hyps_of_vars env sign nogen hyps = if Idset.is_empty hyps then [] @@ -2311,6 +2369,23 @@ let hyps_of_vars env sign nogen hyps = sign in lh +exception Seen + +let linear vars args = + let seen = ref vars in + try + Array.iter (fun i -> + let rels = ids_of_constr ~all:true Idset.empty i in + let seen' = + Idset.fold (fun id acc -> + if Idset.mem id acc then raise Seen + else Idset.add id acc) + rels !seen + in seen := seen') + args; + true + with Seen -> false + let is_defined_variable env id = pi2 (lookup_named id env) <> None @@ -2337,6 +2412,7 @@ let abstract_args gl generalize_vars dep id defined f args = in let argty = pf_type_of gl arg in let argty = refresh_universes_strict argty in + let ty = refresh_universes_strict ty in let lenctx = List.length ctx in let liftargty = lift lenctx argty in let leq = constr_cmp Reduction.CUMUL liftargty ty in @@ -2364,23 +2440,19 @@ let abstract_args gl generalize_vars dep id defined f args = nongenvars, Idset.union argvars vars, env) in let f', args' = decompose_indapp f args in - let parvars = ids_of_constr ~all:true Idset.empty f' in - let seen = ref parvars in let dogen, f', args' = - let find i x = not (isVar x) || - let v = destVar x in - if is_defined_variable env v || Idset.mem v !seen then true - else (seen := Idset.add v !seen; false) - in - match array_find_i find args' with - | None -> false, f', args' - | Some nonvar -> - let before, after = array_chop nonvar args' in - true, mkApp (f', before), after + let parvars = ids_of_constr ~all:true Idset.empty f' in + if not (linear parvars args') then true, f, args + else + match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with + | None -> false, f', args' + | Some nonvar -> + let before, after = array_chop nonvar args' in + true, mkApp (f', before), after in if dogen then - let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],!seen,Idset.empty,env) args' + let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = + Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,Idset.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -2389,7 +2461,7 @@ let abstract_args gl generalize_vars dep id defined f args = hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars else [] in - let body, c' = if defined then Some c', Retyping.get_type_of ctxenv Evd.empty c' else None, c' in + let body, c' = if defined then Some c', typ_of ctxenv Evd.empty c' else None, c' in Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls, dep, succ (List.length ctx), vars) else None @@ -2429,20 +2501,20 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl = let specialize_eqs id gl = let env = pf_env gl in let ty = pf_get_hyp_typ gl id in - let evars = ref (create_evar_defs (project gl)) in + let evars = ref (project gl) in let unif env evars c1 c2 = Evarconv.e_conv env evars c2 c1 in let rec aux in_eqs ctx acc ty = match kind_of_term ty with | Prod (na, t, b) -> (match kind_of_term t with - | App (eq, [| eqty; x; y |]) when in_eqs && eq_constr eq (Lazy.force coq_eq) -> + | App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) -> let c = if noccur_between 1 (List.length ctx) x then y else x in let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when in_eqs && eq_constr heq (Lazy.force coq_heq) -> + | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) -> let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in @@ -2454,10 +2526,8 @@ let specialize_eqs id gl = else let e = e_new_evar evars (push_rel_context ctx env) t in aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) - | App (f, args) when eq_constr f (Lazy.force coq_block) && not in_eqs -> - aux true ctx acc args.(1) | t -> acc, in_eqs, ctx, ty - in + in let acc, worked, ctx, ty = aux false [] (mkVar id) ty in let ctx' = nf_rel_context_evar !evars ctx in let ctx'' = List.map (fun (n,b,t as decl) -> @@ -2485,33 +2555,6 @@ 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 = @@ -2671,83 +2714,62 @@ let compute_elim_sig ?elimc elimt = let compute_scheme_signature scheme names_info ind_type_guess = 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 scheme." - | None -> (* Non standard scheme *) - 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+scheme.npredicates -> IndArg - | _ when hd = ind_type_guess & not scheme.farg_in_concl -> RecArg - | _ -> OtherArg in - let rec check_branch p c = - match kind_of_term c with - | Prod (_,t,c) -> - (is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c - | LetIn (_,_,_,c) -> - (OtherArg, dependent (mkRel 1) c) :: 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,dep) -> - (b,dep,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 - Array.of_list (find_branches 0 (List.rev scheme.branches)) - - | Some ( _,None,ind) -> (* Standard scheme from an inductive type *) - let indhd,indargs = decompose_app ind 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+scheme.npredicates -> 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, dependent (mkRel 1) c) :: check_branch (p+1) c - | LetIn (_,_,_,c) -> - (OtherArg, dependent (mkRel 1) c) :: 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,dep) -> - (b,dep,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_ind_scheme "the conclusion of"; - [] - in - Array.of_list (find_branches 0 (List.rev scheme.branches)) + let cond, check_concl = + match scheme.indarg with + | Some (_,Some _,_) -> + error "Strange letin, cannot recognize an induction scheme." + | None -> (* Non standard scheme *) + let cond hd = eq_constr hd ind_type_guess && not scheme.farg_in_concl + in (cond, fun _ _ -> ()) + | Some ( _,None,ind) -> (* Standard scheme from an inductive type *) + let indhd,indargs = decompose_app ind in + let cond hd = eq_constr hd indhd in + let check_concl is_pred p = + (* Check again conclusion *) + let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in + let ind_is_ok = + list_equal eq_constr + (list_lastn scheme.nargs indargs) + (extended_rel_list 0 scheme.args) in + if not (ccl_arg_ok & ind_is_ok) then + error_ind_scheme "the conclusion of" + in (cond, check_concl) + 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+scheme.npredicates -> IndArg + | _ when cond hd -> RecArg + | _ -> OtherArg + in + let rec check_branch p c = + match kind_of_term c with + | Prod (_,t,c) -> + (is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c + | LetIn (_,_,_,c) -> + (OtherArg, dependent (mkRel 1) c) :: 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,dep) -> + (b,dep,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_concl is_pred p; [] + in + Array.of_list (find_branches 0 (List.rev scheme.branches)) (* Check that the elimination scheme has a form similar to the elimination schemes built by Coq. Schemes may have the standard @@ -2885,7 +2907,7 @@ let induction_tac_felim with_evars indvars nparams elim gl = (* elimclause' is built from elimclause by instanciating all args and params. *) let elimclause' = recolle_clenv nparams indvars elimclause gl in (* one last resolution (useless?) *) - let resolved = clenv_unique_resolver true elimclause' gl in + let resolved = clenv_unique_resolver ~flags:elim_flags elimclause' gl in clenv_refine with_evars resolved gl (* Apply induction "in place" replacing the hypothesis on which @@ -2895,7 +2917,9 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t let isrec, elim, indsign = get_eliminator elim gl in let names = compute_induction_names (Array.length indsign) names in (if isrec then tclTHENFIRSTn else tclTHENLASTn) - (tclTHEN (induct_tac elim) (tclTRY (thin indhyps))) + (tclTHEN + (induct_tac elim) + (tclMAP (fun id -> tclTRY (expand_hyp id)) (List.rev indhyps))) (array_map2 (induct_discharge destopt avoid tac) indsign names) gl (* Apply induction "in place" taking into account dependent @@ -2979,7 +3003,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl = let elimclause = make_clenv_binding gl (mkCast (elimc,DEFAULTcast,elimt),elimt) lbindelimc in - elimination_clause_scheme with_evars true i elimclause indclause gl + elimination_clause_scheme with_evars i elimclause indclause gl let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names inhyps gl = @@ -3017,14 +3041,6 @@ let induction_without_atomization isrec with_evars elim names lid gl = then error "Not the right number of induction arguments." else induction_from_context_l with_evars elim_info lid names gl -let enforce_eq_name id gl = function - | (b,(loc,IntroAnonymous)) -> - (b,(loc,IntroIdentifier (fresh_id [id] (add_prefix "Heq" id) gl))) - | (b,(loc,IntroFresh heq_base)) -> - (b,(loc,IntroIdentifier (fresh_id [id] heq_base gl))) - | x -> - x - let has_selected_occurrences = function | None -> false | Some cls -> @@ -3054,7 +3070,7 @@ let clear_unselected_context id inhyps cls gl = thin ids gl | None -> tclIDTAC gl -let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl = +let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls gl = let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in @@ -3067,14 +3083,17 @@ let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl = (induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind) inhyps) gl | _ -> - let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) + let x = id_of_name_using_hdchar (Global.env()) (typ_of (pf_env gl) sigma c) Anonymous in let id = fresh_id [] x gl in (* We need the equality name now *) let with_eq = Option.map (fun eq -> (false,eq)) eqname in (* TODO: if ind has predicate parameters, use JMeq instead of eq *) tclTHEN - (letin_tac_gen with_eq (Name id) c None (Option.default allHypsAndConcl cls,false)) + (* Warning: letin is buggy when c is not of inductive type *) + (letin_tac_gen with_eq (Name id) (sigma,c) + (make_pattern_test (pf_env gl) (project gl) (sigma,c)) + None (Option.default allHypsAndConcl cls,false)) (induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind) inhyps) gl @@ -3131,7 +3150,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) if List.length lc = 1 && not (is_functional_induction elim gl) then (* standard induction *) - onInductionArg + onOpenInductionArg (fun c -> new_induct_gen isrec with_evars elim names c cls) (List.hd lc) gl else begin @@ -3143,6 +3162,8 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = str "Example: induction x1 x2 x3 using my_scheme."); if cls <> None then error "'in' clause not supported here."; + let lc = List.map + (map_induction_arg (pf_apply finish_evar_resolution gl)) lc in if List.length lc = 1 then (* Hook to recover standard induction on non-standard induction schemes *) (* will be removable when is_functional_induction will be more clever *) @@ -3150,8 +3171,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = (fun (c,lbind) -> if lbind <> NoBindings then error "'with' clause not supported here."; - new_induct_gen_l isrec with_evars elim names [c]) - (List.hd lc) gl + new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc) gl else let newlc = List.map (fun x -> @@ -3179,11 +3199,8 @@ let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls) (* Induction tactics *) (* This was Induction before 6.3 (induction only in quantified premisses) *) -let raw_induct s = tclTHEN (intros_until_id s) (onLastHyp simplest_elim) -let raw_induct_nodep n = tclTHEN (intros_until_n n) (onLastHyp simplest_elim) - -let simple_induct_id hyp = raw_induct hyp -let simple_induct_nodep = raw_induct_nodep +let simple_induct_id s = tclTHEN (intros_until_id s) (onLastHyp simplest_elim) +let simple_induct_nodep n = tclTHEN (intros_until_n n) (onLastHyp simplest_elim) let simple_induct = function | NamedHyp id -> simple_induct_id id @@ -3213,9 +3230,9 @@ let elim_scheme_type elim t gl = | Meta mv -> let clause' = (* t is inductive, then CUMUL or CONV is irrelevant *) - clenv_unify true Reduction.CUMUL t + clenv_unify ~flags:elim_flags Reduction.CUMUL t (clenv_meta_type clause mv) clause in - res_pf clause' ~allow_K:true gl + res_pf clause' ~flags:elim_flags gl | _ -> anomaly "elim_scheme_type" let elim_type t gl = @@ -3472,7 +3489,7 @@ let abstract_subproof id tac gl = let const = Pfedit.build_constant_by_tactic id secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in - let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in + let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in exact_no_check (applist (lem,List.rev (Array.to_list (instance_from_named_context sign)))) gl @@ -3501,8 +3518,9 @@ let admit_as_an_axiom gl = let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = - let cd = Entries.ParameterEntry (concl,false) in - let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in + let cd = + Entries.ParameterEntry (Pfedit.get_used_variables(),concl,None) in + let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in exact_no_check @@ -3517,7 +3535,6 @@ let unify ?(state=full_transparent_state) x y gl = modulo_delta = state; modulo_conv_on_closed_terms = Some state} in - let evd = w_unify false (pf_env gl) Reduction.CONV - ~flags x y (Evd.create_evar_defs (project gl)) + let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y in tclEVARS evd gl with _ -> tclFAIL 0 (str"Not unifiable") gl |