Overloading notation for different types in Coq
I would like to be able to define the same Coq notation for different inductive definitions and differentiate notation based on the types of their arguments.
Here's a minimal example:
Inductive type : Type :=
| TBool : type.
Inductive term1 : Type :=
| tvar1 : term1.
Inductive term2 : Type :=
| tvar2 : term2.
Definition context := nat -> (option type).
Reserved Notation "G '⊢' t '::' T" (at level 40, t at level 59).
Inductive typing1 : context -> term1 -> type -> Prop :=
| T_Var1 : forall G T,
G ⊢ tvar1 :: T
where "G '⊢' t1 '::' T" := (typing1 G t1 T)
with typing2 : context -> term2 -> type -> Prop :=
| T_Var2 : forall G T,
G ⊢ tvar2 :: T
where "G '⊢' t2 '::' T" := (typing2 G t2 T).
As you can see, there is a mutual inductance definition, which I would use the same notation for different types of terms ( term1
and term2
).
An error occurred while trying to compile this The term "tvar1" has type "term1" while it is expected to have type "term2".
.
Is there a way to make this work?
+3
source to share
1 answer
I wrote the Coq mailing list and got a response from Gaëtan Gilbert that solved my problem using typeclasses:
Inductive type : Type :=
| TBool : type.
Inductive term1 : Type :=
| tvar1 : term1.
Inductive term2 : Type :=
| tvar2 : term2.
Definition context := nat -> (option type).
Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.
Notation "G '⊢' t '::' T" := (vdash G t T) (at level 40, t at level 59).
Inductive typing1 : VDash context term1 type :=
| T_Var1 : forall G T,
G ⊢ tvar1 :: T
with typing2 : VDash context term2 type :=
| T_Var2 : forall G T,
G ⊢ tvar2 :: T.
+2
source to share