Operator Overloading in Coq Notation
I would like to create records for several kinds of judgments, for example for the input and subtyping relationship:
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 it, Coq will not allow this because the operator is โข
overloaded in these definitions.
How can I get Coq to infer the definition of an overloaded operator (in this case โข
) based on the types of its arguments (like term
vs type
) (and / or based on other operators that are part of the notation, like โ
vs <:
)?
(Note that using different characters would not be an option because my Coq program defines multiple input and subtyping relationships.)
EDIT: Here's 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 an error:
Syntax error: '<:' or 'โ' expected after [constr:operconstr level 200] (in [constr:operconstr]).
source to share
The reason is that you cannot use <:
like this because it is <:
already defined as Coq typecast notation . It acts as if it were defined like this
Reserved Notation "t <: T" (at level 100, right associativity).
The situation is similar to the situation described in the Coq Reference Guide ( ยง12.1.3 ):
In the latter case, however, there is a conflict with the type designation. This last notation shown by the command
Print Grammar constr.
is at level 100. To avoid parsingx : A
as type casting, you need to put itx
below 100, usually 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).
source to share