diff options
| -rw-r--r-- | dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh | 5 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 158 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13413.v | 20 | ||||
| -rw-r--r-- | test-suite/success/forward.v | 4 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 12 |
6 files changed, 122 insertions, 83 deletions
diff --git a/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh new file mode 100644 index 0000000000..4c8cdbbb45 --- /dev/null +++ b/dev/ci/user-overlays/13512-herbelin-master+fix13413-apply-on-intro-pattern-fresh-names.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then + + overlay perennial https://github.com/herbelin/perennial master+adapt13512-fresness-names-apply-in-introduction-pattern + +fi diff --git a/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst new file mode 100644 index 0000000000..aaacb2aadf --- /dev/null +++ b/doc/changelog/04-tactics/13512-master+fix13413-apply-on-intro-pattern-fresh-names.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Possible collision between a user-level name and an internal name when + using the :n:`%` introduction pattern + (`#13512 <https://github.com/coq/coq/pull/13512>`_, + fixes `#13413 <https://github.com/coq/coq/issues/13413>`_, + by Hugo Herbelin). diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b40bdbc25e..f72764945c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1299,7 +1299,7 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = +let clenv_refine_in ?err with_evars targetid replace sigma0 clenv tac = let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in let clenv = Clenv.update_clenv_evd clenv evd in @@ -1310,11 +1310,10 @@ let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = let new_hyp_prf = clenv_value clenv in let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in - let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas evd)) (Tacticals.New.tclTHENLAST - (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac) + (assert_after_then_gen ?err replace naming new_hyp_typ tac) exact_tac) (********************************************) (* Elimination tactics *) @@ -1365,7 +1364,7 @@ let elimination_in_clause_scheme env sigma with_evars ~flags if EConstr.eq_constr sigma hyp_typ new_hyp_typ then user_err ~hdr:"general_rewrite_in" (str "Nothing to rewrite in " ++ Id.print id ++ str"."); - clenv_refine_in with_evars id id sigma elimclause'' + clenv_refine_in with_evars id true sigma elimclause'' (fun id -> Proofview.tclUNIT ()) (* @@ -1814,6 +1813,7 @@ let apply_in_once ?(respect_opaque = false) with_delta let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (make_annot Anonymous Sorts.Relevant,t')) naming gl in + let replace = Id.equal id targetid in let rec aux ?err idstoclear with_destruct c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1826,7 +1826,7 @@ let apply_in_once ?(respect_opaque = false) with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in ?err with_evars targetid id sigma clause + clenv_refine_in ?err with_evars targetid replace sigma clause (fun id -> replace_error_option err ( apply_clear_request clear_flag false c <*> @@ -2324,26 +2324,31 @@ let rewrite_hyp_then with_evars thin l2r id tac = tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin)) end -let prepare_naming ?loc = function - | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) - | IntroAnonymous -> NamingAvoid Id.Set.empty - | IntroFresh id -> NamingBasedOn (id, Id.Set.empty) - -let rec explicit_intro_names = let open CAst in function -| {v=IntroForthcoming _} :: l -> explicit_intro_names l -| {v=IntroNaming (IntroIdentifier id)} :: l -> Id.Set.add id (explicit_intro_names l) +let rec collect_intro_names = let open CAst in function +| {v=IntroForthcoming _} :: l -> collect_intro_names l +| {v=IntroNaming (IntroIdentifier id)} :: l -> + let ids1, ids2 = collect_intro_names l in Id.Set.add id ids1, ids2 | {v=IntroAction (IntroOrAndPattern l)} :: l' -> let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in - let fold accu l = Id.Set.union accu (explicit_intro_names (l@l')) in - List.fold_left fold Id.Set.empty ll + let fold (ids1',ids2') l = + let ids1, ids2 = collect_intro_names (l@l') in + Id.Set.union ids1 ids1', Id.Set.union ids2 ids2' in + List.fold_left fold (Id.Set.empty,Id.Set.empty) ll | {v=IntroAction (IntroInjection l)} :: l' -> - explicit_intro_names (l@l') + collect_intro_names (l@l') | {v=IntroAction (IntroApplyOn (c,pat))} :: l' -> - explicit_intro_names (pat::l') -| {v=(IntroNaming (IntroAnonymous | IntroFresh _) + collect_intro_names (pat::l') +| {v=IntroNaming (IntroFresh id)} :: l -> + let ids1, ids2 = collect_intro_names l in ids1, Id.Set.add id ids2 +| {v=(IntroNaming IntroAnonymous | IntroAction (IntroWildcard | IntroRewrite _))} :: l -> - explicit_intro_names l -| [] -> Id.Set.empty + collect_intro_names l +| [] -> Id.Set.empty, Id.Set.empty + +let explicit_intro_names l = fst (collect_intro_names l) + +let explicit_all_intro_names l = + let ids1,ids2 = collect_intro_names l in Id.Set.union ids1 ids2 let rec check_name_unicity env ok seen = let open CAst in function | {v=IntroForthcoming _} :: l -> check_name_unicity env ok seen l @@ -2368,30 +2373,33 @@ let rec check_name_unicity env ok seen = let open CAst in function check_name_unicity env ok seen l | [] -> () -let wild_id = Id.of_string "_tmp" +let fresh_wild ids = + let rec aux s = + if Id.Set.exists (fun id -> String.is_prefix s (Id.to_string id)) ids + then aux (s ^ "'") + else Id.of_string s in + aux "_H" -let rec list_mem_assoc_right id = function - | [] -> false - | {CAst.v=id'}::l -> Id.equal 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 CAst.(map (fun id' -> if Id.equal id id' then newid else id')) thin in - Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin) - else - tac thin +let make_naming ?loc avoid l = function + | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) + | IntroAnonymous -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l)) + | IntroFresh id -> NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l)) -let make_tmp_naming avoid l = function +let rec make_naming_action avoid l = function (* In theory, we could use a tmp id like "wild_id" for all actions but we prefer to avoid it to avoid this kind of "ugly" names *) - (* Alternatively, we could have called check_thin_clash_then on - IntroAnonymous, but at the cost of a "renaming"; Note that in the - case of IntroFresh, we should use check_thin_clash_then anyway to - prevent the case of an IntroFresh precisely using the wild_id *) - | IntroWildcard -> NamingBasedOn (wild_id, Id.Set.union avoid (explicit_intro_names l)) - | pat -> NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) + | IntroWildcard -> + NamingBasedOn (fresh_wild (Id.Set.union avoid (explicit_all_intro_names l)), Id.Set.empty) + | IntroApplyOn (_,{CAst.v=pat;loc}) -> make_naming_pattern avoid ?loc l pat + | (IntroOrAndPattern _ | IntroInjection _ | IntroRewrite _) as pat -> + NamingAvoid(Id.Set.union avoid (explicit_intro_names ((CAst.make @@ IntroAction pat)::l))) + +and make_naming_pattern ?loc avoid l = function + | IntroNaming pat -> make_naming ?loc avoid l pat + | IntroAction pat -> make_naming_action avoid l pat + | IntroForthcoming _ -> NamingAvoid (Id.Set.union avoid (explicit_intro_names l)) + +let prepare_naming ?loc pat = make_naming ?loc Id.Set.empty [] pat let fit_bound n = function | None -> true @@ -2430,38 +2438,21 @@ let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac = [CAst.make @@ IntroNaming IntroAnonymous] | {CAst.loc;v=pat} :: l -> if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else + let naming = make_naming_pattern avoid l pat in match pat with | IntroForthcoming onlydeps -> - intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt onlydeps bound n + intro_forthcoming_then_gen naming destopt onlydeps bound n (fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound (n+List.length ids) tac l) | IntroAction pat -> - intro_then_gen (make_tmp_naming avoid l pat) - destopt true false + intro_then_gen naming destopt true false (intro_pattern_action ?loc with_evars pat thin destopt (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0 (fun ids thin -> intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l))) | IntroNaming pat -> - intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l - - (* Pi-introduction rule, used backwards *) -and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l = - match pat with - | IntroIdentifier id -> - check_thin_clash_then id thin avoid (fun thin -> - intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)) - | IntroAnonymous -> - intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) - | IntroFresh id -> - (* todo: avoid thinned names to interfere with generation of fresh name *) - intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) - destopt true false - (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) + intro_then_gen naming destopt true false + (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound (n+1) tac l) and intro_pattern_action ?loc with_evars pat thin destopt tac id = match pat with @@ -2474,24 +2465,16 @@ and intro_pattern_action ?loc with_evars pat thin destopt tac id = | IntroRewrite l2r -> rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None []) | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) -> - let naming,tac_ipat = - prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in - let doclear = - if naming = NamingMustBe (CAst.make ?loc id) then - Proofview.tclUNIT () (* apply_in_once do a replacement *) - else - clear [id] in - let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) - in + let naming = NamingMustBe (CAst.make ?loc id) in + let tac_ipat = prepare_action ?loc with_evars destopt pat in + let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f) - (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) + (fun id -> Tacticals.New.tclTHENLIST [tac_ipat id; tac thin None []]) -and prepare_intros ?loc with_evars dft destopt = function +and prepare_action ?loc with_evars destopt = function | IntroNaming ipat -> - prepare_naming ?loc ipat, - (fun id -> move_hyp id destopt) + (fun _ -> Proofview.tclUNIT ()) | IntroAction ipat -> - prepare_naming ?loc dft, (let tac thin bound = intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in @@ -2528,9 +2511,19 @@ let intros_patterns with_evars = function (* Forward reasoning *) (**************************) -let prepare_intros_opt with_evars dft destopt = function - | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ()) - | Some {CAst.loc;v=ipat} -> prepare_intros ?loc with_evars dft destopt ipat +let prepare_intros_opt with_evars dft destopt ipat = + let naming, loc, ipat = match ipat with + | None -> + let pat = IntroNaming dft in make_naming_pattern Id.Set.empty [] pat, None, pat + | Some {CAst.loc;v=(IntroNaming pat as ipat)} -> + (* "apply ... in H as id" needs to use id and H is kept iff id<>H *) + prepare_naming ?loc pat, loc, ipat + | Some {CAst.loc;v=(IntroAction pat as ipat)} -> + (* "apply ... in H as pat" reuses H so that old H is always cleared *) + (match dft with IntroIdentifier _ -> prepare_naming ?loc dft | _ -> make_naming_action Id.Set.empty [] pat), + loc, ipat + | Some {CAst.loc;v=(IntroForthcoming _)} -> assert false in + naming, prepare_action ?loc with_evars destopt ipat let ipat_of_name = function | Anonymous -> None @@ -3045,8 +3038,7 @@ let specialize (c,lbind) ipat = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> (* Like assert (id:=id args) but with the concept of specialization *) - let naming,tac = - prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in + let naming,tac = prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in let repl = do_replace (Some id) naming in Tacticals.New.tclTHENFIRST (assert_before_then_gen repl naming typ tac) @@ -3059,10 +3051,10 @@ let specialize (c,lbind) ipat = (* TODO: add intro to be more homogeneous. It will break scripts but will be easy to fix *) (Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term)) - | Some {CAst.loc;v=ipat} -> + | Some _ as ipat -> (* Like pose proof with extra support for "with" bindings *) (* even though the "with" bindings forces full application *) - let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in + let naming, tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in Tacticals.New.tclTHENFIRST (assert_before_then_gen false naming typ tac) (exact_no_check term) diff --git a/test-suite/bugs/closed/bug_13413.v b/test-suite/bugs/closed/bug_13413.v new file mode 100644 index 0000000000..b4414a6a1d --- /dev/null +++ b/test-suite/bugs/closed/bug_13413.v @@ -0,0 +1,20 @@ +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?H%H H0. +exact H1. +Qed. + +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H J%H H0. +exact J. +Qed. + +Set Mangle Names. +Goal forall (A B : Prop) (H : A -> B), A -> A -> B. +intros A B H ?%H _0. +assumption. +Qed. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v index 4e36dec15b..62c788e910 100644 --- a/test-suite/success/forward.v +++ b/test-suite/success/forward.v @@ -27,3 +27,7 @@ Fail match goal with |- (?f ?a) => idtac end. (* should be beta-iota reduced *) 2:match goal with _: (?f ?a) |- _ => idtac end. (* should not be beta-iota reduced *) Abort. +Goal nat. +assert nat as J%S by exact 0. +exact J. +Qed. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index d37ad9f528..b8fbff05c6 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -152,3 +152,15 @@ Definition d := ltac:(intro x; exact (x*x)). Definition d' : nat -> _ := ltac:(intros;exact 0). End Evar. + +Module Wildcard. + +(* We check that the wildcard internal name does not interfere with + user fresh names (currently the prefix is "_H") *) + +Goal nat -> bool -> nat -> bool. +intros _ ?_H ?_H. +exact _H. +Qed. + +End Wildcard. |