How can I disambiguate notation? · Coq users

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:

It seems that add from SetOfℤ shadows the one from SetOfℚ, consequently the notation only works for Z.
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: Oct 13 2024 at 01:02 UTC