Stream: Coq users

Topic: notation confusion

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?

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

Paolo Giarrusso (May 02 2023 at 21:44):

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

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.

Paolo Giarrusso (May 02 2023 at 21:46):

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

Bhakti Shah (May 02 2023 at 21:47):

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

Last updated: Jun 20 2024 at 12:02 UTC