CODEWITHSUNDEEP
coq
Bodo
Bodo

Reputation: 3

Overloading operators in Coq via typeclasses and notation scopes: Is there anything special about the '+' and '*' symbols?

I would like to create infix notations for (overloaded) operations. I apply the - to my knowledge - standard two-step approach in Coq:

  1. Typeclass used for actual operator overloading (e.g. overload add operation)
  2. Notation scope used for definition of operator symbol (e.g. infix notation '+')

This approach seems to work fine. E.g. overloading of the '-' symbol (which is used at least once in the predefined notation scope nat_scope) poses no problems. However, the '+' and '*' symbols (also used in the predefined notation scope nat_scope) lead to erros in certain circumstances. Is there anything special about the '+' and '*' symbols in Coq that has to be considered when adding them to a new notation scope?

Example

Let's model classical sets as predicates, i.e. as functions of type A->Prop:

Definition pred1 (a:nat) := a=1. (* pred1 corresponds to {1} *)
Definition pred2 (a:nat) := a=1 \/ a=2. (* pred2 corresponds to {1,2} *)

Union (addition) is modelled as the overloaded operation pred_add via the typeclass PredAdd and corresponding typeclass instances. For the sake of simplicity only the typeclass instance add_elem (addition of elements to sets) is provided:

Class PredAdd (X Y Z: Type) := {pred_add: X->Y->Z->Prop}.
Instance add_elem {A:Type}: PredAdd (A->Prop) (A) (A) := {
  pred_add (P:A->Prop) (a:A) (x:A) := P x \/ x=a
}.

The infix notation '+' is used for the operation pred_add:

  Declare Scope mypred_scope.
  Notation "x + y" := (pred_add x y)  (at level 50, left associativity): mypred_scope.
  Open Scope mypred_scope.

Now, let's use the test case {1} + 2 = {1,2} to see what works and what does not work.

Operator overloading and infix notation '+' seem to work fine (at first glance):

Example ex1: (pred_add pred1 2) 1. unfold pred_add, pred1; simpl; auto. Qed.
Example ex2: forall (p1 p2:nat->Prop) (x:nat),
  p1 = pred1 + 2 -> p2 = pred2 -> p1 x=p2 x.
  unfold pred_add, pred1, pred2; intros; subst; auto.
Qed.

However, the application of notation '+' fails in certain cases. E.g. in the following case:

Fail Example ex2: (pred1 + 2) 2.

we get the error message:

The command has indeed failed with message: The term "pred1" has type "nat -> Prop" while it is expected to have type "Type".

Interestingly, the outcome seems to depend on the particular choice of the notation symbol. The same example works fine with e.g. the symbol '-':

Notation "x - y" := (pred_add x y)  (at level 50, left associativity): mypred_scope.
Example ex3: (pred1 - 2) 2.  unfold pred_add, pred1; simpl; auto. Qed.

but fails with the notation symbol '*':

Notation "x * y" := (pred_add x y)  (at level 40, left associativity): mypred_scope.
Fail Example ex4: (pred1 * 2) 2.

The command has indeed failed with message: The term "pred1" has type "nat -> Prop" while it is expected to have type "Type".

(The symbols '-' and '*' may be a confusing choice for an add operation. But this lets us keep the example short and simple.)

Platform

Tested on Coq version: 8.15.2

Upvotes: 0

Views: 136

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33389

+ and * are also overloaded as sum and product types in type_scope, which is automatically open on the right of :, taking precedence over the open mypred_scope. This is why the error messages say that a Type is expected. Hence on the right of : you have to reopen mypred_scope.

Delimit Scope mypred_scope with mypred.
Example ex2: (pred1 + 2)%mypred 2.

Upvotes: 1

Related Questions