Stream: Coq users

Topic: Use `|-` in notation?


view this post on Zulip Ralf Jung (Oct 31 2023 at 17:42):

I am using the ASCII turnstile |- in a notation and now I realized that Ltac's match goal no longer works. Is there a way to pick the right level for my coq-level |- notation to avoid interfering with the parsing of ltac's match goal?

view this post on Zulip Pierre Roux (Oct 31 2023 at 17:55):

I would try a combination of Locate "|-" and Print Notation of the results to try to understand what can be done in terms of parsing levels.

view this post on Zulip Ralf Jung (Oct 31 2023 at 18:53):

sadly the ltac notation does not show up in Locate

view this post on Zulip Ralf Jung (Oct 31 2023 at 18:53):

it's probably hard-coded somewhere, no idea how to figure out its level

view this post on Zulip Ralf Jung (Oct 31 2023 at 18:53):

not sure if it's even a level thing, ltac should be its own non-terminal in the grammar, no?

view this post on Zulip Pierre Roux (Oct 31 2023 at 18:55):

Maybe Print Grammar, otherwise grep the mlg files in Coq sources?

view this post on Zulip Ralf Jung (Oct 31 2023 at 20:19):

I should probably first produce a minimal example, I realized there's more interactions here than I originally though

view this post on Zulip Paolo Giarrusso (Oct 31 2023 at 21:14):

Is this about https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/bi/ascii.v ? At bedrock we're still using |-- instead, possibly out of caution for this problem.

view this post on Zulip Ralf Jung (Oct 31 2023 at 22:37):

so this came up in the coq files for my class

view this post on Zulip Ralf Jung (Nov 01 2023 at 06:26):

yeah here is a reproducer

Reserved Notation "Gamma |- e : A" (at level 74, e, A at next level).

Goal True.
repeat match goal with
  [ H : _ = _ |- _ ] => clear H
end.

view this post on Zulip Ralf Jung (Nov 01 2023 at 06:26):

match goal with [ |- pattern ] still works, but the moment I add a hypothesis it breaks

view this post on Zulip Ralf Jung (Nov 01 2023 at 06:27):

Pierre Roux said:

Maybe Print Grammar, otherwise grep the mlg files in Coq sources?

Print Grammar says Error: Grammar not a defined object.

view this post on Zulip Ralf Jung (Nov 01 2023 at 06:27):

I have no idea what to look for in the mlg files...

view this post on Zulip Janno (Nov 01 2023 at 10:59):

It takes a while to get to the bottom of it but you can go via Print Grammar tactic and work you way towards the actual parsing rules which eventually end up revealing that the term to the right of : in H : .. is parsed at level 200. It seems that putting your notation at a level > 200 fixes match goal but I haven't tried actually using the notation for anything useful afterwards.

view this post on Zulip Erik Martin-Dorel (Nov 01 2023 at 11:17):

FWIW, if using a raw |- is not feasible, you could just as well use a UTF8 symbol:
Reserved Notation "Gamma ⊢ e : A" (at level 74, e, A at next level).

or to keep ASCII style, you could tweak the token in an MathComp-like fashion, adding a prefix apostrophe… not so nice, but YMMV:
Reserved Notation "Gamma '|- e : A" (at level 74, e, A at next level).

view this post on Zulip Ralf Jung (Nov 02 2023 at 13:55):

this is in a teaching context, so Im avoiding unicode since I dont want to deal with all the trouble of students having to set up their editors for unicode input

view this post on Zulip Ralf Jung (Nov 02 2023 at 13:56):

yeah alternative notations are possible (|-- also comes to mind), but not this year, since I realized this after we already introduced the notation :joy:

view this post on Zulip Ralf Jung (Nov 02 2023 at 14:03):

@Janno yeah everything breaks when I put it at level 201...

view this post on Zulip Ralf Jung (Nov 02 2023 at 14:04):

is there any way to add parentheses in the match goal that would resolve the ambiguity? I guess not, match goal relies on |- to not be in the follow set of constr and that's just fundamentally incompatible with the notation we want.


Last updated: Jun 13 2024 at 19:02 UTC