## Stream: Coq users

### Topic: Coercions and "_ = _ :> _"

#### Ana de Almeida Borges (Jan 07 2022 at 17:33):

Consider the following example:

``````Variables (A B : Type) (B_of_A : A -> B).
Coercion B_of_A : A >-> B.
Goal forall (a : A), a = a :> B.
(*
============================
forall a : A, a = a
*)
``````

Why does the `:> B` disappear? Sanity check:

``````Set Printing Coercions.
(*
============================
forall a : A, B_of_A a = B_of_A a
*)
Unset Printing Coercions.
Abort.
``````

so the coercion is there.

In the following example the `:>` doesn't disappear:

``````From mathcomp Require Import ssrint.

Open Scope ring_scope.
Goal forall (n : nat), n = n :> int.
(*
============================
forall n : nat, n = n :> int
*)
``````

However now a different strange thing happens: `Set Printing Coercions` doesn't do anything:

``````Set Printing Coercions.
(*
============================
forall n : nat, n = n :> int
*)
Unset Printing Notations.
(*
============================
forall n : nat, eq (Posz n) (Posz n)
*)
Abort.
``````

Is any of this behaviors possibly a bug?

#### Gaëtan Gilbert (Jan 07 2022 at 17:37):

`_ = _ :> _` is a notation

#### Gaëtan Gilbert (Jan 07 2022 at 17:38):

don't know what mathcomp does

#### Li-yao (Jan 07 2022 at 17:42):

It's not a bug. There can be more than one notation for the same expression, and when printing, one notation has to be chosen.

#### Ana de Almeida Borges (Jan 07 2022 at 17:56):

Sure, but why does the choice change in these two examples? Or do you think that mathcomp redefines the notation? Shouldn't the supposed redefinition also change the behavior of the `B_of_A` example? (It doesn't change if done after importing mathcomp stuff).

#### Cyril Cohen (Jan 07 2022 at 17:58):

In mathcomp, in order to disambiguate `n = m :> nat` and `n = m :> int` when `n` and `m` are in `nat` and a coercion to `int` is potentially triggered, we force the printing of the ternary form explicitly:
https://github.com/math-comp/math-comp/blob/bd9431c4926e10c39da8a20374dd2050120fab32/mathcomp/algebra/ssrint.v#L70

#### Cyril Cohen (Jan 07 2022 at 18:01):

(the `'in' 't'` hack comes from the time it was not possible to register several printing rules for the same notation format in Coq, so we use a combination of two strings `in` and `t` that render to `int` when glued together at printing time, you can ignore this hack, which we should replace by now-legitimate Coq code, I believe)

#### Ana de Almeida Borges (Jan 07 2022 at 18:04):

Ok, I admit I did not see that coming, thanks.

#### Ana de Almeida Borges (Jan 07 2022 at 18:07):

Why `'in' 't'` instead of `'int'`?

#### Cyril Cohen (Jan 07 2022 at 18:09):

Ana de Almeida Borges said:

Why `'in' 't'` instead of `'int'`?

see my previous message.

#### Ana de Almeida Borges (Jan 07 2022 at 18:11):

So we couldn't have `int` as both a token in a notation and the name of a type?

#### Paolo Giarrusso (Jan 07 2022 at 20:05):

to be clearer regarding `a = a :> B`: that disappears because that’s just a notation for `@eq B a a`, unlike the math-comp notations (and I’d expect it to be a parsing-only notation).

#### Cyril Cohen (Jan 07 2022 at 22:18):

Ana de Almeida Borges said:

So we couldn't have `int` as both a token in a notation and the name of a type?

No, that's a different problem, Coq would not make it a token. It's just the left over of a missing feature that has been added since then.
I removed it in math-comp/math-comp#834

Last updated: Sep 23 2023 at 07:01 UTC