Stream: Coq users

Topic: notation confusion

view this post on Zulip Bhakti Shah (May 02 2023 at 21:31):

Hi! I'm having some issues understanding some caveats of notation levels in coq, and why certain terms are parsed a certain way.
I'm working with a lot of notation, and these are specifically the ones I'm having issues with (with some type information if that helps):

Notation "A ⟷ B" := (Compose A B)
  (left associativity, at level 40)
Notation "'Z'" := Z_Spider (no associativity, at level 1)
Reserved Notation "⊙ zx" (at level 0). (* level 0 has right associativity *)
Fixpoint color_swap {nIn nOut} (zx : ZX nIn nOut) : ZX nIn nOut :=
...
where "⊙ zx" := (color_swap zx).

Inductive ZX : nat -> nat -> Type :=
| ...
| Z_Spider n m (α : R) : ZX n m
| Cup  : ZX 2 0
| Cap : ZX 0 2
| Compose {n m o} (zx0 : ZX n m) (zx1 : ZX m o) : ZX n o.
| ...

Specifically I'm confused about why ⊙ is acting the following way:

Check ⊙ Z 0 0 0 ⟷ Z 0 0 0.
>>> ⊙ (Z 0 0 0 ⟷ Z 0 0 0) : ZX 0 0

Check ⊙ Cap ⟷ Cup.
>>> ⊙ (Cap) ⟷ Cup: ZX 0 0

Specifically, I'm unsure why ⊙ Z 0 0 0 ⟷ Z 0 0 0 is applying ⊙ to (Z 0 0 0 ⟷ Z 0 0 0) and not just the first Z 0 0 0 (like i believe it should be ⊙ (Z 0 0 0) ⟷ Z 0 0 0 or (⊙ Z 0 0 0) ⟷ Z 0 0 0 ). From what I understand, ⊙ is at level 0 and hence should bind the tightest, while ⟷ should be the "outermost" function. The binding with the second check is what makes more sense to me.

If I expand the notation Z to then try ⊙ Z_Spider 2 2 2 ⟷ Z_Spider 2 2 2, this doesn't actually parse.

I believe the discrepancy is probably because Z itself is notation, but I don't really understand why?

view this post on Zulip Paolo Giarrusso (May 02 2023 at 21:43):

you should specify the level for zx as well, that's what matters for parsing the "content" of your operator. Example:

Reserved Notation "⊢ Q" (at level 20, Q at level 200).

view this post on Zulip Paolo Giarrusso (May 02 2023 at 21:44):

Your current notation has a level for zx, but that's decided via undocumented heuristics

view this post on Zulip Paolo Giarrusso (May 02 2023 at 21:45):

Roughly, the semantics of my example is to add a production to "constr_20" that invokes "constr_200" to parse Q.

view this post on Zulip Paolo Giarrusso (May 02 2023 at 21:46):

(sorry for the formatting but I'm screen-typing from an iPad)

view this post on Zulip Bhakti Shah (May 02 2023 at 21:47):

I see, that actually makes a lot of sense
thank you so much!

Last updated: Oct 04 2023 at 23:01 UTC