Ltac1 name of changing name of unused variable breaks tactic · Coq users

Hi, I have the following Ltac code where changing the name of a unused variable changes the behaviour of the tactic. Is this expected or a bug?

From Coq Require Export String.
Open Scope string_scope.

Tactic Notation "intro_test" "(" simple_intropattern(x) ")" :=
  let name := lazymatch goal with
              | |- let _ := (fun name => _) in _ => name
              end in
  simpl;
  let y := fresh name in
  intros y; revert y; intros x.

Tactic Notation "tac1" constr(name) "(" simple_intropattern(x) ")" :=
    intro_test ( x ).

Tactic Notation "tac2" constr(name2) "(" simple_intropattern(x) ")" :=
    intro_test ( x ).

Goal let f := (fun z => z = z) in forall x : nat, f x.
  (** Fails with Ltac variable name is bound to "a" which cannot be coerced to an identifier. *)
  Fail tac1 "a" ( y ).
  (** Succeeds. *)
  tac2 "a" ( y ).

MackieLoeffel (Jul 27 2020 at 13:45):

Sadly, based on my previous experience with Ltac1 I would not be too surprised if this is the expected behaviour...

Théo Winterhalter (Jul 27 2020 at 13:51):

MackieLoeffel (Jul 27 2020 at 13:54):

No, I don't think this is the case. If I only change the definition of intro_test, both tac1 and tac2 work.

Tactic Notation "intro_test2" "(" simple_intropattern(x) ")" :=
  simpl; intros x.

Tactic Notation "tac1" constr(name) "(" simple_intropattern(x) ")" :=
    intro_test2 ( x ).

Tactic Notation "tac2" constr(name2) "(" simple_intropattern(x) ")" :=
    intro_test2 ( x ).
Goal let f := (fun z => z = z) in forall x : nat, f x.
  (** Succeeds *)
  tac1 "a" ( y ).
  Undo.
  (** Succeeds. *)
  tac2 "a" ( y ).
Abort.

Pierre-Marie Pédrot (Jul 27 2020 at 13:54):

With tactic notations you can never be sure, this looks like what I would call "typical ltac behaviour"

Pierre-Marie Pédrot (Jul 27 2020 at 13:55):

Pierre-Marie Pédrot (Jul 27 2020 at 13:56):

so here the fact there is a clash between a bound variable name from the match pattern and the bound variable name from the notation is the root of the issue

Pierre-Marie Pédrot (Jul 27 2020 at 13:57):

so, even if this were deeemed a buggy behaviour, it'd likely be treated as WONTFIX

MackieLoeffel (Jul 27 2020 at 14:11):

Tej Chajed (Jul 29 2020 at 22:11):

For context, intro_test is in library code and tac1/tac2 are something in user code.
So I guess in Ltac1 the library code should use some complicated likely-to-be-fresh identifier instead of name to protect itself from the local bindings?

Tej Chajed (Jul 29 2020 at 22:13):

@Pierre-Marie Pédrot since all Ltac1 bugs now effectively get closed WONTFIX, it would be nice to start seeing Ltac2 solutions to these problems; here the pattern matching in intro_test seems quite hard to implement in Ltac2 (and preserving names is the entire point of this code, so it needs to do that)

Jason Gross (Jul 30 2020 at 07:07):

What if you return ident:(name) or fresh name from inside the lazymatch? Does that make it work as desired?

Jason Gross (Jul 30 2020 at 07:12):

And the pattern matching is not too hard in Ltac2: it's something like

match Constr.Unsafe.kind (Control.goal ()) with | Constr.Unsafe.LetIn _ v _ => match Constr.Unsafe.kind v with | Constr.Unsafe.Lambda n _ => Some (Binder.name n) | _ => None end | _ => None end

(I'm going from memory here, so probably got a bunch of names wrong)

Stream: Coq users

Topic: Ltac1 name of changing name of unused variable breaks tactic

MackieLoeffel (Jul 27 2020 at 13:43):