Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Reverse coercions


view this post on Zulip Cyril Cohen (Feb 15 2022 at 09:41):

I would like to implement what I discussed here: https://coq.discourse.group/t/generalizing-coercions-to-infer-typeclass-arguments/1241/4?u=cohencyril and tried to impulse one day here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Reverse.20coercions

view this post on Zulip Cyril Cohen (Feb 15 2022 at 09:52):

@Enrico Tassi

view this post on Zulip Enrico Tassi (Feb 15 2022 at 09:53):

Hello, is this the same thing as https://arxiv.org/abs/1103.3320

view this post on Zulip Cyril Cohen (Feb 15 2022 at 09:54):

Can we meet in breakout room 2 and talk about it?

view this post on Zulip Cyril Cohen (Feb 15 2022 at 09:54):

Did you implement it in Matita ?

view this post on Zulip Enrico Tassi (Feb 15 2022 at 09:54):

ok for room two

view this post on Zulip Enrico Tassi (Feb 15 2022 at 10:17):

Hacking session on this topic tomorrow at 10:20 AM

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2022 at 10:52):

Great @Enrico Tassi , you mind updating the schedule in the wiki too?

view this post on Zulip Cyril Cohen (Feb 16 2022 at 09:26):

FYI We are starting hacking coercions in room 1

view this post on Zulip Enrico Tassi (Feb 16 2022 at 10:50):

https://github.com/coq/coq/pull/15693

view this post on Zulip Cyril Cohen (Feb 16 2022 at 13:24):

We resumed working with @Enrico Tassi. We noticed a failure in mathcomp when trying out the PR when replacing the old def of {poly R} by a simpler one.

view this post on Zulip Cyril Cohen (Feb 16 2022 at 13:24):

We are in Room 1

view this post on Zulip Cyril Cohen (Feb 16 2022 at 13:26):

The problem was that we immediately encounter an occurrence of predArgType >-> Type <-< ringType

view this post on Zulip Cyril Cohen (Feb 16 2022 at 13:29):

The solution for now is to deal only with types which have coercions either to Sortclass or Funclass

view this post on Zulip Jason Gross (Feb 16 2022 at 20:42):

What are reverse coercions? / what's the idea?

view this post on Zulip Ali Caglayan (Feb 16 2022 at 20:57):

@Jason Gross Here is the original discussion

view this post on Zulip Ali Caglayan (Feb 16 2022 at 20:57):

https://coq.discourse.group/t/generalizing-coercions-to-infer-typeclass-arguments/1241/4?u=cohencyril

view this post on Zulip Enrico Tassi (Feb 16 2022 at 21:13):

The paper I wrote a long ago is in topic. We did open a draft pr with a few examples.

view this post on Zulip Jason Gross (Feb 16 2022 at 21:45):

Thanks! And sorry, I missed the earlier messages. I guess I should narrow streams more to see the context.

view this post on Zulip Enrico Tassi (Feb 17 2022 at 13:56):

We did push a bunch of commits cleaning up a lot and kind of implementing the search for a common point to which the inferred and expected type can be coerced, on coercion path must be reversible (although the check for reversibility is still dummy).


Last updated: Jan 29 2023 at 14:02 UTC