Bug in the parser?

Using Coq
#1

The proof below fails with the error:

"Error: Syntax error: [tactic:red_expr] expected after 'eval' (in [tactic:constr_eval])."

In the example below, “eval” is sometimes parsed using my definition and sometimes not, in ways that I cannot predict.
Am I doing something wrong or is this a bug in the parser?

Set Default Proof Using "Type".
Ltac mytac k := rewrite (plus_O_n k). 
Definition eval2 := 2 .
Definition eval := 3.

Lemma test_mytac_eval: 0 + eval  = eval. 
Proof.
  assert(0 + eval = eval) by (rewrite plus_O_n; auto). 
  assert(0 + eval2 = eval2) by (mytac eval2; reflexivity). 
  mytac eval. reflexivity.
Qed.
#2

There are two languages: Gallina terms and Ltac tactics. (This is too simplistic, but it suffices to explain the issue here.) There exists an eval tactic, and you are defining an eval term. When Coq parses mytac eval, it expects a tactic and thus parses it as a tactic. Since mytac is a simple user-defined tactic (rather than something with custom grammar rules), it reads the argument as a tactic too, hence the error, since you are now passing the eval tactic as an argument to rewrite, which expects a term.

There are two ways to fix it.

  1. Make it clear that you meant the term rather than the tactic: mytac constr:(eval). (Conversely, ltac:(eval) can be used in the other direction.)

  2. Put a custom grammar rule for mytac: Tactic Notation "mytac" constr(k) := mytac k. (Conversely, tactic(k) can be used in the other direction.)

1 Like
#3

Thanks for the prompt explanation Silene. If I understand correctly, the tactic parser will first try to parse “eval” as a tactic and only if that fails will it consider “eval” as a term, which is why “myac eval2” parses correctly. I will pursue your suggestions.

Yours,
Barry

#4

I don’t think the parser will ever try to parse “eval” as a term in the case you are considering if you do not put an explicit constr:( ) around it. Unless of course you change the parser by using the Tactic Notation command suggested above.

#5

Indeed, now that I reread what I wrote, I see that my wording was making it confusing. I should have said that eval is parsed by the tactic-level parser (rather than saying that it is parsed as a tactic). Since eval has custom parsing rule for this parser, it is always parsed as a tactic (unless constr:() is used).

But for a plain identifier x with no custom parsing rules (e.g., eval2), Coq first looks whether x denotes an Ltac binder, then it looks whether it denotes a Gallina term, and finally it looks whether it denotes an Ltac toplevel tactic. (Hopefully, I did not get the order too wrong.) So, for mytac eval2, eval2 will denote the Gallina definition, even if you define an Ltac tactic with that name.

1 Like
#6

Right, what surprised me was that the argument of mytac could be either a tactic or a Gallina term. I had naively expected the tactic language to force a static choice between these possibilities but have now learnt that it is not so. I’m sure that there are good reasons for this, and can now work around the issue without much difficulty. Thanks again to you, and to Zimmi48.

Yours,
Barry