## Stream: Coq users

### Topic: How can I disambiguate notation?

#### Ignat Insarov (Jun 18 2021 at 22:50):

Example:

From Coq Require Import ZArith.
From Coq Require Import QArith.
Check 1%Q < 3.
Check 1%Z < 3.

Error: The term "1%Z" has type "Z" while it is expected to have type "Q".

Is there a way to use the notation for both types?

#### Alexander Gryzlov (Jun 18 2021 at 23:27):

You can delimit the scope to the whole expression, i.e. Check (1 < 3)%Z.

#### Ignat Insarov (Jun 19 2021 at 07:14):

Thank you Alexander. This works. However, I am having trouble with this more complicated case:

From Coq Require Import ZArith.
From Coq Require Import QArith.
From Coq Require Import QArith.QOrderedType.
From Coq Require Import MSets.MSets.

Module SetOfℚ := Make (Q_as_OT). Import SetOfℚ.
Module SetOfℤ := Make (Z_as_OT). Import SetOfℤ.
Notation "{ x }" := (add x empty).
Check ({ 1 })%Z.
Check ({ 1 })%Q.
Notation "{ x ; y ; .. ; z }" := (add x (add y .. (add z empty) .. )).
Check ({ 1 })%Z.
Check ({ 1 })%Q.
Check ({ 1; 2 })%Z.
Check ({ 1; 2 })%Q.

There are several problems here:

1. It seems that add from SetOfℤ shadows the one from SetOfℚ, consequently the notation only works for Z.
2. After I define the notation with the ellipsis, the notation for a singleton set stops working.

My desire is to have an ergonomic way to work with sets of ℤ and ℚ simultaneously. How can I achieve that?

#### Ignat Insarov (Jun 19 2021 at 07:45):

This is my next iteration:

Open Scope Q.
Module SetOfℚ := Make (Q_as_OT). Import SetOfℚ.
Notation "{ x }" := (add x empty): Q_scope.
Notation "{ x ; y ; .. ; z }" := (add x (add y .. (add z empty) .. )): Q_scope.
Close Scope Q.

Open Scope Z.
Module SetOfℤ := Make (Z_as_OT). Import SetOfℤ.
Notation "{ x }" := (add x empty): Z_scope.
Notation "{ x ; y ; .. ; z }" := (add x (add y .. (add z empty) .. )): Z_scope.
Close Scope Z.

Check {1; 2}%Z.
Check {1; 2}%Q.

_(Unfortunately, the notation for singletons still does not work, for reason unknown to me.)_

I suppose this is as good as it gets. I wish I could make add and empty polymorphic, so that this notation were also magically polymorphic, but I do not know how.

#### Théo Winterhalter (Jun 19 2021 at 08:41):

Scopes only apply to notations. For definitions you will need to qualify them. Use Locate add. to see how to qualify in your context.

#### Emilio Jesús Gallego Arias (Jun 19 2021 at 13:08):

math-comp does provide a generic notation for rings, also, algebraic structures are formulated so setoids are not required

#### Emilio Jesús Gallego Arias (Jun 19 2021 at 13:09):

similarly for order and lattice structures, tho for sets of such elements, you need to use the finmap library

#### Emilio Jesús Gallego Arias (Jun 19 2021 at 13:09):

as done in multinomials

Last updated: Apr 14 2024 at 11:02 UTC