3

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

1 Answer 1

2

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).
2
  • This change made the above code compile. However, I am not able to actually use the notation. The following code: Definition t1 G t T := G ⊢ t ∈ T. results in the error Syntax error: '<:' expected after [constr:operconstr level 99] (in [constr:operconstr]).
    – amaurremi
    May 3, 2017 at 17:47
  • 1
    Coq is using an LL1 parser, so you need to modify all the notations that start with the same token. I updated the answer. May 3, 2017 at 18:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.