diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 30 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 3 | ||||
| -rw-r--r-- | pretyping/namegen.ml | 22 | ||||
| -rw-r--r-- | pretyping/namegen.mli | 5 | ||||
| -rw-r--r-- | proofs/logic.ml | 11 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 77 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
9 files changed, 99 insertions, 58 deletions
@@ -657,9 +657,9 @@ Other tactics clears (resp. reverts) H and all the hypotheses that depend on H. - Ltac's pattern-matching now supports matching metavariables that depend on variables bound upwards in the pattern. -- Case analysis on schemes in Type containing Proposition now produces - "H"-based names (important source of incompatibility that can be - repaired by using option "Unset Standard Proposition Elimination Names"). +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. Tactic definitions diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f6ca611a3..5e853784e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -446,21 +446,6 @@ let find_coinductive env sigma c = (* find appropriate names for pattern variables. Useful in the Case and Inversion (case_then_using et case_nodep_then_using) tactics. *) -let h_based_elimination_names = ref false - -let use_h_based_elimination_names () = - !h_based_elimination_names (* && Flags.version_strictly_greater Flags.V8_4 *) - -open Goptions - -let _ = declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of \"H\"-based proposition names in elimination tactics"; - optkey = ["Standard";"Proposition";"Elimination";"Names"]; - optread = (fun () -> !h_based_elimination_names); - optwrite = (:=) h_based_elimination_names } - let is_predicate_explicitly_dep env pred arsign = let rec srec env pval arsign = let pv' = whd_betadeltaiota env Evd.empty pval in @@ -489,9 +474,6 @@ let is_predicate_explicitly_dep env pred arsign = From Coq > 8.2, using or not the the effective dependency of the predicate is parametrable! *) - if use_h_based_elimination_names () then - dependent (mkRel 1) t - else begin match na with | Anonymous -> false | Name _ -> true @@ -505,13 +487,11 @@ let is_elim_predicate_explicitly_dependent env pred indf = let arsign,_ = get_arity env indf in is_predicate_explicitly_dep env pred arsign -let set_names preprocess_names env n brty = +let set_names env n brty = let (ctxt,cl) = decompose_prod_n_assum n brty in - let ctxt = - if use_h_based_elimination_names () then preprocess_names ctxt else ctxt in Namegen.it_mkProd_or_LetIn_name env cl ctxt -let set_pattern_names preprocess_names env ind brv = +let set_pattern_names env ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map @@ -519,9 +499,9 @@ let set_pattern_names preprocess_names env ind brv = rel_context_length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in - Array.map2 (set_names preprocess_names env) arities brv + Array.map2 (set_names env) arities brv -let type_case_branches_with_names preprocess_names env indspec p c = +let type_case_branches_with_names env indspec p c = let (ind,args) = indspec in let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in @@ -531,7 +511,7 @@ let type_case_branches_with_names preprocess_names env indspec p c = let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env p (ind,params) then - (set_pattern_names preprocess_names env (fst ind) lbrty, conclty) + (set_pattern_names env (fst ind) lbrty, conclty) else (lbrty, conclty) (* Type of Case predicates *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 5583eff4d..1561cf97b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -156,8 +156,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - (rel_context -> rel_context) -> env -> pinductive * constr list -> constr -> - constr -> types array * types + env -> pinductive * constr list -> constr -> constr -> types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 8b9e6e633..16ba03ad7 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -367,3 +367,25 @@ let rename_bound_vars_as_displayed avoid env c = | _ -> c in rename avoid env c + +(**********************************************************************) +(* "H"-based naming strategy introduced June 2014 for hypotheses in + Prop produced by case/elim/destruct/induction, in place of the + strategy that was using the first letter of the type, leading to + inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar + types *) + +let h_based_elimination_names = ref false + +let use_h_based_elimination_names () = + !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4 + +open Goptions + +let _ = declare_bool_option + { optsync = true; + optdepr = false; + optname = "use of \"H\"-based proposition names in elimination tactics"; + optkey = ["Standard";"Proposition";"Elimination";"Names"]; + optread = (fun () -> !h_based_elimination_names); + optwrite = (:=) h_based_elimination_names } diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index cb2891996..88ce43f8e 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -95,3 +95,8 @@ val compute_displayed_let_name_in : renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list val rename_bound_vars_as_displayed : Id.t list -> Name.t list -> types -> types + +(**********************************************************************) +(* Naming strategy for arguments in Prop when eliminating inductive types *) + +val use_h_based_elimination_names : unit -> bool diff --git a/proofs/logic.ml b/proofs/logic.ml index e1cbe4af0..59de85901 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -314,14 +314,6 @@ let rename_hyp id1 id2 sign = (**********************************************************************) -let name_prop_vars env sigma ctxt = - List.map2 (fun (na,b,t as d) s -> - if na = Anonymous && s = prop_sort then - let s = match Namegen.head_name t with Some id -> string_of_id id | None -> "" in - (Name (add_suffix Namegen.default_prop_ident s),b,t) - else - d) - ctxt (sorts_of_context env sigma ctxt) (************************************************************************) (************************************************************************) @@ -526,8 +518,7 @@ and mk_casegoals sigma goal goalacc p c = let indspec = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals") in - let (lbrty,conclty) = - type_case_branches_with_names (name_prop_vars env sigma) env indspec p c in + let (lbrty,conclty) = type_case_branches_with_names env indspec p c in (acc'',lbrty,conclty,sigma,p',c') diff --git a/tactics/equality.ml b/tactics/equality.ml index 2c21f9809..a23ae4e82 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -337,7 +337,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d Proofview.V82.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) - {elimindex = None; elimbody = (elim,NoBindings)} + {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} end let adjust_rewriting_direction args lft2rgt = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3b1cf6575..442f0a3cb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -829,7 +829,44 @@ let index_of_ind_arg t = | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty, bindings) indclause gl = +let enforce_prop_bound_names rename tac = + match rename with + | Some (isrec,nn) when Namegen.use_h_based_elimination_names () -> + (* Rename dependent arguments in Prop with name "H" *) + (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *) + (* elim or induction with schemes built by Indrec.build_induction_scheme *) + let rec aux env sigma i t = + if i = 0 then t else match kind_of_term t with + | Prod (Name _ as na,t,t') -> + let very_standard = true in + let na = + if Retyping.get_sort_family_of env sigma t = InProp then + (* "very_standard" says that we should have "H" names only, but + this would break compatibility even more... *) + let s = match Namegen.head_name t with + | Some id when not very_standard -> string_of_id id + | _ -> "" in + Name (add_suffix Namegen.default_prop_ident s) + else + na in + mkProd (na,t,aux (push_rel (na,None,t) env) sigma (i-1) t') + | Prod (Anonymous,t,t') -> + mkProd (Anonymous,t,aux (push_rel (Anonymous,None,t) env) sigma (i-1) t') + | LetIn (na,c,t,t') -> + mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t') + | _ -> print_int i; Pp.msg (print_constr t); assert false in + let rename_branch i gl = + let env = pf_env gl in + let sigma = project gl in + let t = pf_concl gl in + change_concl (aux env sigma i t) gl in + (if isrec then tclTHENFIRSTn else tclTHENLASTn) + tac + (Array.map rename_branch nn) + | _ -> + tac + +let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause gl = let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in let indmv = (match kind_of_term (nth_arg i elimclause.templval.rebus) with @@ -838,7 +875,7 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty, (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - Proofview.V82.of_tactic (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags) gl + enforce_prop_bound_names rename (Proofview.V82.of_tactic (Clenvtac.res_pf elimclause' ~with_evars:with_evars ~flags)) gl (* * Elimination tactic with bindings and using an arbitrary @@ -850,6 +887,7 @@ let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i (elim, elimty, type eliminator = { elimindex : int option; (* None = find it automatically *) + elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : constr with_bindings } @@ -858,12 +896,12 @@ let general_elim_clause_gen elimtac indclause elim gl = let elimt = pf_type_of gl elimc in let i = match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in - elimtac i (elimc, elimt, lbindelimc) indclause gl + elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause gl let general_elim with_evars (c, lbindc) elim gl = - let elimtac = elimination_clause_scheme with_evars 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 elimtac = elimination_clause_scheme with_evars in let indclause = pf_apply make_clenv_binding gl (c, t) lbindc in general_elim_clause_gen elimtac indclause elim gl @@ -879,7 +917,8 @@ let general_case_analysis_in_context with_evars (c,lbindc) gl = pf_apply build_case_analysis_scheme_default gl mind sort in tclTHEN (tclEVARS sigma) (general_elim with_evars (c,lbindc) - {elimindex = None; elimbody = (elim,NoBindings)}) gl + {elimindex = None; elimbody = (elim,NoBindings); + elimrename = Some (false, constructors_nrealdecls (fst mind))}) gl let general_case_analysis with_evars (c,lbindc as cx) = match kind_of_term c with @@ -907,7 +946,8 @@ let find_eliminator c gl = let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in if is_record ind <> None then raise IsRecord; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in - evd, {elimindex = None; elimbody = (c,NoBindings)} + evd, {elimindex = None; elimbody = (c,NoBindings); + elimrename = Some (true, constructors_nrealdecls ind)} let default_elim with_evars (c,_ as cx) = Proofview.tclORELSE @@ -926,7 +966,9 @@ let default_elim with_evars (c,_ as cx) = let elim_in_context with_evars c = function | Some elim -> - Proofview.V82.tactic (general_elim with_evars c {elimindex = Some (-1); elimbody = elim}) + Proofview.V82.tactic + (general_elim with_evars c {elimindex = Some (-1); elimbody = elim; + elimrename = None}) | None -> default_elim with_evars c let elim with_evars (c,lbindc as cx) elim = @@ -957,7 +999,7 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = (* Set the hypothesis name in the message *) raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) -let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i (elim, elimty, bindings) indclause gl = +let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause gl = let elimclause = make_clenv_binding (pf_env gl) (project gl) (elim, elimty) bindings in let indmv = destMeta (nth_arg i elimclause.templval.rebus) in let hypmv = @@ -978,9 +1020,9 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i (elim, e clenv_refine_in with_evars id elimclause'' gl let general_elim_clause with_evars flags id c e = - let elim gl = match id with - | None -> elimination_clause_scheme with_evars ~flags gl - | Some id -> elimination_in_clause_scheme with_evars ~flags id gl + let elim = match id with + | None -> elimination_clause_scheme with_evars ~flags + | Some id -> elimination_in_clause_scheme with_evars ~flags id in Proofview.V82.tactic (fun gl -> general_elim_clause_gen elim c e gl) @@ -3052,7 +3094,7 @@ let find_induction_type isrec elim hyp0 gl = let scheme = compute_elim_sig ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature scheme hyp0 ind_guess in - let elim = ({elimindex = Some(-1); elimbody = elimc},elimt) in + let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in evd, scheme, ElimUsing (elim,indsign) in evd,(Option.get scheme.indref,scheme.nparams, elim) @@ -3077,8 +3119,9 @@ let get_eliminator elim gl = match elim with Proofview.Goal.sigma gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec id gl in - let _, (l, _) = compute_elim_signature elims id in - evd, isrec, ({elimindex = None; elimbody = elimc}, elimt), l + let _, (l, s) = compute_elim_signature elims id in + let branchlengthes = List.map (fun (_,b,c) -> assert (b=None); pi1 (decompose_prod_letin c)) (List.rev s.branches) in + evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l (* Instantiate all meta variables of elimclause using lid, some elts of lid are parameters (first ones), the other are @@ -3219,18 +3262,18 @@ let induction_from_context_l with_evars elim_info lid names = (* FIXME: Tester ca avec un principe dependant et non-dependant *) induction_tac_felim with_evars realindvars scheme.nparams elim ]) in - let elim = ElimUsing (({elimindex = Some scheme.index; elimbody = Option.get scheme.elimc}, scheme.elimt), indsign) in + let elim = ElimUsing (({elimindex = Some scheme.index; elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in apply_induction_in_context None elim (hyp0::indvars) names induct_tac (* Unification between ((elimc:elimt) ?i ?j ?k ?l ... ?m) and the hypothesis on which the induction is made *) let induction_tac with_evars elim (varname,lbind) typ gl = - let ({elimindex=i;elimbody=(elimc,lbindelimc)},elimt) = elim in + let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in let indclause = pf_apply make_clenv_binding gl (mkVar varname,typ) lbind in let i = match i with None -> index_of_ind_arg elimt | Some i -> i in let elimc = mkCast (elimc, DEFAULTcast, elimt) in - elimination_clause_scheme with_evars i (elimc, elimt, lbindelimc) indclause gl + elimination_clause_scheme with_evars rename i (elimc, elimt, lbindelimc) indclause gl let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names inhyps = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7d88b7a90..20b974a82 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -241,6 +241,7 @@ val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme (** elim principle with the index of its inductive arg *) type eliminator = { elimindex : int option; (** None = find it automatically *) + elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : constr with_bindings } |