Stream: Coq users

Topic: Terms as Coercions


view this post on Zulip Gregory Malecha (Dec 07 2022 at 14:43):

Is it possible to use a term (and not a definition) as a coercion? I have an interface like:

Module M.
Record t : Set := mk { is_const : bool ; frac : Qp }.
Notation c := (mk false).
Notation m := (mk true).
End M.

And I want to declare

Coercion (M.mk false) : Qp >-> M.t.

I can make a definition for M.mk false but then syntactic pattern matching does not work.

view this post on Zulip Gaëtan Gilbert (Dec 07 2022 at 14:44):

it is not possible

view this post on Zulip Gregory Malecha (Dec 07 2022 at 15:27):

How difficult would it be to implement something like that?

view this post on Zulip Gaëtan Gilbert (Dec 07 2022 at 15:34):

I think we generally don't like to store data as terms rather than in a constant, because then we have to deal with questions about universes in a adhoc way, the term doesn't get checked by the kernel etc
maybe we could have a way to make coercions as "to be reduced when inserted"?
also omitting such coercions when printing (regardless of if they're registered as terms or if they're reduced when inserted) would be difficult and probably not worth the effort

view this post on Zulip Gregory Malecha (Dec 07 2022 at 18:01):

having a way to reduce coercions when they are inserted would solve my problem. Personally, I don't care if the coercion is printed, and it seems reasonable to have different behavior if the coercion is a term or unfolded upon insertion

view this post on Zulip Gregory Malecha (Dec 07 2022 at 18:01):

thanks for your feedback

view this post on Zulip Paolo Giarrusso (Dec 08 2022 at 04:24):

"Arguments your_def /." might be a decent approximation: "your_def" would be unfolded by simpl/cbn :-)

view this post on Zulip Cyril Cohen (Jan 13 2023 at 09:20):

Recently I've been advocating for a variation of Arguments def / for which unfolding is performed eagerly (a bit like eta is after some tactics).

view this post on Zulip Paolo Giarrusso (Jan 13 2023 at 09:50):

would def be autounfolded in definitions that use it after elaboration? (Unfolded and beta-reduced I guess, without touching other redexes)


Last updated: Mar 28 2024 at 11:01 UTC