Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jan 07 2022 at 17:37):

_ = _ :> _ is a notation

view this post on Zulip Gaëtan Gilbert (Jan 07 2022 at 17:38):

don't know what mathcomp does

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Ana de Almeida Borges (Jan 07 2022 at 18:04):

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

view this post on Zulip Ana de Almeida Borges (Jan 07 2022 at 18:07):

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

view this post on Zulip Cyril Cohen (Jan 07 2022 at 18:09):

Ana de Almeida Borges said:

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

see my previous message.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC