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.
```

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.

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)`

.

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

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).
```

(`(a, b)`

being a notation for `@pair _ _ a b`

)

The bidirectionality hint only works at toplevel. For example, if you replace `(n,n)`

by `id(n,n)`

, it will fail again.

then you'll need a hint for `id`

too ;)

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

Last updated: Jun 16 2024 at 04:03 UTC