Ezra elias kilty Cooper (Apr 13 2023 at 03:10): Ezra elias kilty Cooper (Apr 13 2023 at 03:10):After an upgrade to Coq 8.16, This innocuous line, unfold set_In at 2 gives me Error: Syntax error: [occs_nums] expected after 'at' (in [occs]). The docs seem to suggest that this notation should work, and I scanned the release notes for a reference to this notation, to no avail. I'm guessing I might need to import something in order to use decimal numerals, but I tried a few things like Coq.Init.Decimal which didn't improve the situation.
How do I use at in an unfold tactic?
Notification Bot (Apr 13 2023 at 03:54):A message was moved here from #Coq users > Thinking of making a new proof editing UI by Ezra elias kilty Cooper.
Paolo Giarrusso (Apr 13 2023 at 06:53):Can you minimize the example? My suspicion is that the notation still works but you're importing some module that breaks it accidentally (it's far too easy)
Ezra elias kilty Cooper (Apr 15 2023 at 00:54):That sounds promising—I'll come back with a minimal example, thanks.
Ezra elias kilty Cooper (Apr 15 2023 at 06:27):OK, here is my minimal example. The defined tactic notation containing "2" interferes with the unfold ... at 2 notation, which I wouldn't really expect.
Tactic Notation "foo" "bar" "2" := idtac.
Lemma dilemma:
forall x y z, plus (plus x y) z = plus x (plus y z).
Proof.
unfold plus at 2.
fold plus.
Require Import Lia.
intros; lia.
Qed.
I do not really need to use this "clever" tactic notation with a 2, so I'll just work around it. Thanks for the suggestion, Paolo!
Paolo Giarrusso (Apr 15 2023 at 07:37):Oh cool it helped and thank you for the example! I knew notations could extend Coq's lexer and change the meaning of "existing" syntax, but I hadn't run into it yet with Tactic Notations!
Last updated: Oct 04 2023 at 22:01 UTC