Stream: Coq users

Topic: Coercions inside tuples


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

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Jun 21 2021 at 13:25):

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

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

view this post on Zulip Gaëtan Gilbert (Jun 21 2021 at 13:30):

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

view this post on Zulip 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: Jan 27 2023 at 02:04 UTC