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.
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
but to be sure: Coercions are keyed exclusively on the _head_ constructor of the type, without any normalization.
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
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.
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.
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 04 2023 at 19:01 UTC