Stream: Coq users

Topic: Coercions inside tuples

Mikkel Milo (Jun 21 2021 at 13:11):

Hey there, I'm having an issue where coercions don't work inside tuples. Here's a minimal example where I make a coercion from nat to bool, and write a function from nat to bool * bool. However, the coercion mechanism doesn't seem to work inside the tuple. Is there a good reason why this shouldn't work? And is there a way to circumvent this?

Axiom nat_to_bool : nat -> bool.
Coercion nat_to_bool : nat >-> bool.

(* Works fine *)
Definition test1 (n : nat) : bool := n.

(* Doesn't work *)
(* Error:
  The term "(n, n)" has type "(nat * nat)%type" while it is expected to have type "(bool * bool)%type".
 *)
Fail Definition test2 (n : nat) : bool * bool := (n, n).

(* Works with annotations inside the tuple *)
Definition test3 (n : nat) : bool * bool := (n:bool, n:bool).


(* But doesn't work with annotations outside the tuple *)
(* Error:
  The term "(n, n)" has type "(nat * nat)%type" while it is expected to have type "(bool * bool)%type".
*)
Fail Definition test4 (n : nat) : bool * bool := (n, n) : bool * bool.

Guillaume Melquiond (Jun 21 2021 at 13:17):

Coercion lookup is triggered by typing errors. In your case, Coq has typed (n,n) as nat*nat. It then tries to unify it with bool*bool, which fails. So, it looks for a coercion from nat*nat to bool*bool, which does not exist.

Mikkel Milo (Jun 21 2021 at 13:20):

Is it possible to automatically derive coercions for products (if that makes any sense)? e.g. if I have coercions A >-> B and C >-> D I should also automatically (at least intuitively) have (A * C) >-> (B * D).

Bas Spitters (Jun 21 2021 at 13:22):

It would be possible with type class casts sec 4.5 here: https://arxiv.org/pdf/1106.3448.pdf
@Enrico Tassi will tell you that things will be much easier with unification hints

Gaëtan Gilbert (Jun 21 2021 at 13:25):

use a bidirectionality hint for tuples

Axiom nat_to_bool : nat -> bool.
Coercion nat_to_bool : nat >-> bool.

Arguments pair {_ _} & _ _.
Definition test (n : nat) : bool * bool := (n, n).

Gaëtan Gilbert (Jun 21 2021 at 13:25):

((a, b) being a notation for @pair _ _ a b)

Guillaume Melquiond (Jun 21 2021 at 13:29):

The bidirectionality hint only works at toplevel. For example, if you replace (n,n) by id(n,n), it will fail again.

Gaëtan Gilbert (Jun 21 2021 at 13:30):

then you'll need a hint for id too ;)

Mikkel Milo (Jun 21 2021 at 13:36):

Thanks! That's a very clever solution, and seems to do exactly what I need.

Last updated: Oct 03 2023 at 04:02 UTC