Stream: Coq users

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


view this post on Zulip MackieLoeffel (Jul 27 2020 at 13:43):

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 ).

view this post on Zulip 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...

view this post on Zulip Théo Winterhalter (Jul 27 2020 at 13:51):

It might be that name is a reserved keyword?

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 13:55):

Ltac relies on complex heuristics to decide what the user thought she wanted

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip MackieLoeffel (Jul 27 2020 at 14:11):

Thanks for the explanation!

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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)


Last updated: Feb 04 2023 at 23:02 UTC