Stream: Coq users

Topic: Coercion with implicit arguments


view this post on Zulip Dennis H (Apr 10 2023 at 12:46):

Is it possible to define a Coercion with implicit parameters? For example, I have the following

Definition arrow_mor {C : category} (f : arrow C) := pr2 f.

Definition mor_to_arrow_ob {C : category} {x y : C} (f : x --> y) : arrow C :=
    (make_dirprod x y,, f).

and I would like to make both of these coercions (the domain of arrow_mor is also dependent on the parameter f). Would something like this be possible?

view this post on Zulip Raul (Apr 11 2023 at 22:25):

I can't help but to ask it again in hopes somebody knows it :sweat_smile: .
Most of my inductive types have parameters, which must be taken in account in the coercions.

view this post on Zulip Pierre Roux (Apr 11 2023 at 22:36):

I'm not sure to understand what's the issue. What happens if you replace Definition with Coercion?

view this post on Zulip Raul (Apr 12 2023 at 09:03):

On of the coercions where I have problems is this one

Inductive signed T :=
  | sign : 'Z_2 -> T -> signed T.
Coercion emb := fun T => (sign T 0%R) : T >-> signed T.

Gives the error

Error: Syntax error: '.' expected after [gallina_ext] (in [vernac_aux]).

In contrast, the following works fine

Variable n : nat.

Class ary_Connective {A : Connectives} := {
    ca : @Connective A;
    eqc_arity : n = @sk_arity skeleton
}.

Coercion ca : ary_Connective >-> Connective.

I suppose in the first case I can't hide the parameter, but in the second I can.

view this post on Zulip Pierre Roux (Apr 12 2023 at 09:07):

You should probably read the doc of coercion in the refman: https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html
In particular, the _ >-> _ syntax expects coercion classes which should be constants or local variables, as coercion only work on the head symbol.

view this post on Zulip Raul (Apr 12 2023 at 09:18):

Then 'ary_Connective' is constant as a dependent type?
Is it possible to have a coercion going out of "the identity functor"?

Do you have any recommendation about the type-theoretical/whatever nature of Coercions and Canonical commands?
I don't understand how they work.
(of all the questions I would rather say this is the more important, I don't really need to solve the others right now)

view this post on Zulip Pierre Roux (Apr 12 2023 at 09:59):

Well, coercion are pretty dumb, they are very syntactical and only activated on the head constant of the type (with the special cases of funclass and sortclass).

view this post on Zulip Paolo Giarrusso (Apr 12 2023 at 16:53):

So, you can't have coercions from the "identity functor", but you can write an identity function and have a coercion from uses of that function

view this post on Zulip Paolo Giarrusso (Apr 12 2023 at 16:54):

If type-theoretically = after type inference/elaboration, coercions are functions and Canonical things are constants/definitions. If you're asking how they're used in inference, the manual has the rules

view this post on Zulip Paolo Giarrusso (Apr 12 2023 at 16:54):

And "canonical structures for the working mathematician" IIRC has a good introduction


Last updated: Jun 20 2024 at 11:02 UTC