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: Oct 13 2024 at 01:02 UTC