## Stream: Coq users

### Topic: Coercion from (F A) to (F B)?

#### Yannick Zakowski (Oct 11 2020 at 09:31):

Hi everyone, I have a coercion question that is summed up in the following minimal example. Essentially the question reduces to: is there a trick to make it work without moving to giving explicit definition to `F A` and `F B` everywhere in the code base:

``````Section coercion.
Open Scope nat.
Parameter F : Set -> Set.
Parameter A B : Set.
Parameter c : F A -> F B.
Parameter g : F B -> nat.
(* I would like to be able to use [g] over a [F A] and have a coercion introduced *)
(* I cannot write:
Coercion c : F A >-> F B.
Because it wants classes on both sides.
*)
Section FOO.
(* I can do: *)
Notation FA := (F A).
Notation FB := (F B).
Coercion c : FA >-> FB.
(* But that doesn't work *)
Fail Goal forall (x : F A), 0 = g x.
End FOO.
Section BAR.
(* I can try to use definitions instead: *)
Definition FA := (F A).
Definition FB := (F B).
(* But then I cannot use c, I need to explicitly have FA and FB *)
Parameter c' : FA -> FB.
Coercion c' : FA >-> FB.
(* But not only that, I also need explicitly the argument typed as [FA] *)
Fail Goal forall (x : F A), 0 = g x.
(* And even worst, so does of course [g] *)
Fail Goal forall (x : FA), 0 = g x.
Parameter g' : FB -> nat.
(* So this one works, but that's too much side effects for my use case *)
Goal forall (x : FA), 0 = g' x.
End FOO.
(* Is there better? *)
End coercion.
``````

#### Paolo Giarrusso (Oct 11 2020 at 10:24):

The road ahead requires additional coercions from F A to FA. Those are not easy to write, but I think not impossible. That is, in one situation, I've done something similar using SubClass, after some effort decoding the manual : https://github.com/Blaisorblade/dot-iris/blob/master/theories/Dot/examples/hoas.v#L41

#### Paolo Giarrusso (Oct 11 2020 at 10:25):

but to be sure: Coercions are keyed exclusively on the _head_ constructor of the type, without any normalization.

#### Paolo Giarrusso (Oct 11 2020 at 10:26):

sadly, you’ll need quite a bit of the chapter on coercions, including identity coercions (https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html#identity-coercions) — SubClass is just sugar to declare identity coercions

#### Paolo Giarrusso (Oct 11 2020 at 10:28):

before that: the reason coercions `F A >-> FA` are hard to write is the “uniform inheritance condition” — basically, normal coercions are across (different) type constructors with the same parameters; when you violate the restriction, you need additional identity coercions.

#### Paolo Giarrusso (Oct 11 2020 at 10:31):

OTOH, chaining coercions is completely fine. It’s even efficient AFAICS, because Coq can compute the graph of coercions paths ahead of time and, I presume, compute its transitive closure.

#### Yannick Zakowski (Oct 11 2020 at 11:56):

Thanks for the snippet of code and the advice Paolo! I'll look into this in detail to judge if it's worth the trouble for my use case.

Last updated: Jun 23 2024 at 23:01 UTC