Laurent Théry (Feb 15 2022 at 23:12): 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?
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?)
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)
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.
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?
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?
Hmm it is being accepted as a coercion, but is probably not the coercion you are looking for.
Ali Caglayan (Feb 15 2022 at 23:34):I do believe this is the kind of problem the PR Jason pointed to will solve.
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
Ali Caglayan (Feb 15 2022 at 23:42):cc @Hugo Herbelin
Hugo Herbelin (Feb 16 2022 at 10:25):Looks indeed related to 11327.
Last updated: Oct 13 2024 at 01:02 UTC