Stream: Coq users

Topic: Coercion and Funclass


view this post on Zulip Laurent Théry (Feb 15 2022 at 23:12):

I have the following definitions

Parameter bt : nat -> Type.
Parameter ct : nat -> Type -> Type.
Parameter ap : forall {m} {A} (b : bt m), (ct m A) -> (ct m A).
Parameter e : forall m, ct m bool.
Parameter v : bt 1.

so writing

Check ap v (e 1).

is ok. Now I would like to turn ap into a coercion so to be able to just write v (e 1).
I have tried

Coercion ap : bt >-> Funclass

but there is a problem of uniform inheritance. I've tried with Identity Coercion but without any success. Is there a way to make ap a coercion accepted by Coq?

view this post on Zulip Jason Gross (Feb 15 2022 at 23:15):

Does it work if you put {A} after (b : bt m) in the type of ap? (Is that acceptable?)

view this post on Zulip Jason Gross (Feb 15 2022 at 23:16):

(Note that you may have to write v _ (e 1) then, see also https://github.com/coq/coq/pull/11327)

view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:16):

@Laurent Théry It is still an accepted coercion, but Coq just complains about it. AFAIK Coq complains about a lot of sensible coercions. If the warning is annoying you can always disable it specifically before and after the problematic command.

view this post on Zulip Laurent Théry (Feb 15 2022 at 23:20):

Yes by moving A I can write v _ (e 1) but is there a way to make A implicit?

view this post on Zulip Laurent Théry (Feb 15 2022 at 23:27):

@Ali Caglayan do you mean

Parameter ap : forall {m} {A} (b : bt m), (ct m A) -> (ct m A).
Coercion ap : bt >-> Funclass.

should work even if there is a warning?


view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:33):

Hmm it is being accepted as a coercion, but is probably not the coercion you are looking for.

view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:34):

I do believe this is the kind of problem the PR Jason pointed to will solve.

view this post on Zulip Laurent Théry (Feb 15 2022 at 23:41):

@Ali Caglayan something weird happens, v (e 1) is not accepted but now

Check ap v (e 1).

returns

bool v (e 1)
     : ct 1 bool

!!!
I agree this should be related to 11327

view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:42):

cc @Hugo Herbelin

view this post on Zulip Hugo Herbelin (Feb 16 2022 at 10:25):

Looks indeed related to 11327.


Last updated: Jan 29 2023 at 01:02 UTC