Stream: Coq users

Topic: Level of `==` notation

Paolo Giarrusso (Oct 12 2020 at 21:26):

What's the correct level and settings for the == notation, since that must be agreed upon globally (right?)
The most common levels seem:

Notation "x == y" := (equality x y) (at level 70, no associativity).

However, I've also seen

(* Coq.ZArith.Zdiv *)
Infix "==" := eqm (at level 70).
(* Coq.ZArith.Int. *)
Notation "x == y" := (i2z x = i2z y)
    (at level 70, y at next level, no associativity) : Int_scope.

Are those different levels, or just more or less explicit? If they are different, is that okay, or will that lead to conflicts if both are imported? I cannot reproduce conflicts, but it's hard to be sure:

Locate "==".
Require Import Coq.ZArith.Int.
Import Coq.ZArith.Int.Z_as_Int.
Open Scope Int_scope.
Locate "_ == _"%Int_scope. (* Still not found *)
Module Foo_Z_as_Int : Int := Coq.ZArith.Int.Z_as_Int.
Import Foo_Z_as_Int. (* Now we obtain the notation from the [Int] signature *)
Locate "_ == _"%Int_scope.
(*
Notation
"x == y" := eq (i2z x) (i2z y) : Int_scope (default interpretation)
*)
Require Import QArith.
Require Import Coq.QArith.Qcanon.
Locate "_ == _". (*
Notation
"x == y" := eq (i2z x) (i2z y) : Int_scope
"x == y" := Qeq x y : Q_scope (default interpretation)
 *)

Ana de Almeida Borges (Oct 13 2020 at 11:21):

If you define a notation that already exists at a level different from the defined one, Coq will complain and it will tell you which level it expected. For example:

Require Import QArith.
Require Import Coq.QArith.Qcanon.
Notation "a == b" := (eq a b) (at level 6, b at next level, no associativity).
(* Error: Notation "_ == _" is already defined at level 70 with arguments
constr at next level, constr at next level
while it is now required to be at level 7 with arguments constr
at next level, constr at next level. *)

If you remove the b at next level or the no associativity you get exactly the same result. If you write only

Notation "a == b" := (eq a b) (at level 70).

this is accepted, from which I conclude that it satisfies the same properties as the existing notation. I think the defaults here are for each constr to be at next level and for there to be no associativity. Indeed the following also produces an error:

Notation "a == b" := (eq a b) (at level 70, right associativity).
(* Error: Notation "_ == _" is already defined at level 70 with arguments
constr at next level, constr at next level
while it is now required to be at level 70 with arguments constr
at next level, constr at level 70. *)

I think the three examples you quoted behave exactly the same because the defaults in this case are the non associativity and the second argument at next level (in fact I believe the level of the arguments is completely determined by the kind of associativity and vice-versa).

Paolo Giarrusso (Oct 13 2020 at 12:52):

that's plausible, but defaults can also be inherited from existing notation; with an == in scope, you can even omit the level.

Paolo Giarrusso (Oct 13 2020 at 12:54):

but then I know which experiments are needed: define == at level 70 in one scope, then at level 70 with other settings in other scopes, and check compatibility.

Paolo Giarrusso (Oct 13 2020 at 12:55):

Also, double-check which settings must agree and which needn't (I assume the formats can differ, not sure about the rest; probably whatever goes into the grammar must agree).

Last updated: Sep 09 2024 at 04:02 UTC