Search code examples
coq

Notations in Coq

I want to use the notations to represent the predicate test as follows:

Variable A B : Type.

Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
    a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.

However, the Coq has an error: enter image description here

Why this notation cannot be accepted in Coq?

Solution

  • The notation is accepted, it's actually that Coq is incorrectly parsing your use of the notation within the definition of test1. To correctly parse this notation you need to adjust the parsing levels of its terms. You can do that with a reserved notation, since these where clauses for notation within an inductive don't support the syntax for configuring the notation:

    Variable A B : Type.

Reserved Notation "c1 '\' st '||' c2 '\' st'" (at level 40, st at next level, c2 at next level, no associativity).

Inductive test : A -> B -> A -> B -> Prop :=
| test1 : forall a1 a2 b1 b2,
    a1 \ b1 || a2 \ b2
where "c1 '\' st '||' c2 '\' st'" := (test c1 st c2 st')
.

    I don't have a good intuition for what parsing levels work well (40 is somewhat arbitrary above), so the best advice I can give is to experiment and if it's parsed incorrectly somewhere then try adjusting the level.