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: Apr 20 2024 at 05:01 UTC