Overloading operators in Coq notations

Question

I'd like to create notations for several kinds of judgements, for example for a typing and subtyping relation:

Reserved Notation "Г '⊢' t '∈' T" (at level 40).
Reserved Notation "Г '⊢' T '<:' U" (at level 40).

Inductive typing_relation : context -> term -> type -> Prop := ...
where "Γ '⊢' t '∈' T" := (typing_relation Γ t T).

Inductive subtyping_relation : context -> type -> type -> Prop := ...
where "Г '⊢' T '<:' U" := (subtyping_relation Γ T U).

As I understand, Coq will not allow this because the ⊢ operator is overloaded in those definitions.

How could I make Coq infer the definition of an overloaded operator (in this case, ⊢) based on the types of its arguments (e.g. term vs type) (and/or based on the other operators that are part of the notation, e.g. ∈ vs <:)?

(Note that using different symbols would not be an option, because my Coq program defines several typing and subtyping relations.)

EDIT: Here is a minimal example:

Inductive type : Type :=
  | TBool : type.

Inductive term : Type :=
  | tvar : nat -> term.

Definition context := nat -> (option type).

Reserved Notation "G '⊢' t '∈' T" (at level 40).

Inductive typing_relation : context -> term -> type -> Prop :=
 | T_Var : forall G x T,
      G x = Some T ->
      G ⊢ tvar x ∈ T
 where "G '⊢' t '∈' T" := (typing_relation G t T).

Reserved Notation "G '⊢' T '<:' U" (at level 40).

Inductive subtype_relation : context -> type -> type -> Prop :=
  | S_Refl : forall G T,
      G ⊢ T <: T
  where "G '⊢' T '<:' U" := (subtype_relation G T U).

This results in the error:

Syntax error: '<:' or '∈' expected after [constr:operconstr level 200] (in [constr:operconstr]).

What error message do you get? Also, a minimal reproducible example would be nice. — Anton Trunov

Anton Trunov Anton Trunov · Accepted Answer · 2017-05-03T16:47:12

The reason is that you cannot use <: like that, because <: is already defined as Coq's typecast notation. It acts as if it was defined like so

Reserved Notation "t <: T" (at level 100, right associativity).

The situation is analogous to the one described in The Coq Reference Manual (§12.1.3):

In the last case though, there is a conflict with the notation for type casts. This last notation, as shown by the command Print Grammar constr. is at level 100. To avoid x : A being parsed as a type cast, it is necessary to put x at a level below 100, typically 99.

Here is a possible solution for your situation:

Reserved Notation "G '⊢' t '∈' T" (at level 40, t at level 99).
Reserved Notation "G '⊢' T '<:' U" (at level 40, T at level 99).

Overloading operators in Coq notations

1 Answers