Stream: math-comp users

Topic: finType and Variant


view this post on Zulip Karl Palmskog (May 02 2022 at 19:23):

@Alessandro Bruni the main difference between Inductive and Variant is just that you don't get any induction principle. There is no general way to create a finType from an arbitrary inductive type. You will have to use one of the finType Mixins in fintype.v or look at a library such as Deriving that has some automation for finType instance generation. But the properties required by your type are quite restrictive.

view this post on Zulip Karl Palmskog (May 02 2022 at 19:31):

in particular, I can't see that non-recursive constructors would automatically guarantee finType (consider a constructor that has a nat)

view this post on Zulip Paolo Giarrusso (May 02 2022 at 20:20):

... the question might make sense if the Variant is "just an enum" (like a | b | c)?

view this post on Zulip Karl Palmskog (May 02 2022 at 21:18):

in that case, regular FinMixin would work, but I'm sure Deriving has some magic for that case as well..

view this post on Zulip Karl Palmskog (May 02 2022 at 21:19):

someone ambitious could write a plugin in MetaCoq that introspects on the "just an enum" case and proves Finite.axiom I guess?

view this post on Zulip Paolo Giarrusso (May 02 2022 at 21:25):

Elpi seems to have a nicer learning curve, just from how many are using it in my team

view this post on Zulip Paolo Giarrusso (May 02 2022 at 21:28):

I think @Jasper Haag plans to write something like the stdpp version at some point, maybe we’d want to open source that (no promises?), and I’m sure he can share his experience learning it

view this post on Zulip Karl Palmskog (May 02 2022 at 21:33):

ah, you mean, generate Finite typeclass instance

view this post on Zulip Karl Palmskog (May 02 2022 at 21:35):

(and I hope open source means non-AGPL-like...)

view this post on Zulip Karl Palmskog (May 02 2022 at 21:37):

but regardless, packages and code examples like that are welcome in the opam archive and elsewhere (possibly in the Platform, eventually)

view this post on Zulip Paolo Giarrusso (May 03 2022 at 03:47):

(Our stdpp/iris contributions are under the respective BSD licenses)

view this post on Zulip Alessandro Bruni (May 03 2022 at 05:45):

Thanks for the answers! indeed, I meant Variant to be "just an enum" like @Paolo Giarrusso says. But in my case ordinal n works just as well

view this post on Zulip Jasper Haag (May 03 2022 at 17:23):

I'll second Paolo's suggestion to look into coq-elpi if you're interested in generating your own code in circumstances which are unsupported by existing infrastructure. At the moment we have an internal utility which is able to automatically generate definitions/lemmata/hints based on a "variant"-like enum from a C++ program. This utility is implemented entirely in elpi and it has been robust/extensible thus far.

@Paolo Giarrusso has separately done some work using Finite/Countable instances, and we'd like to link the two together in the future. While I don't anticipate us open-sourcing the C++-specific utilities in the near-term, I do believe it will be possible to extract and upstream the core infrastructure responsible for ingesting Variants+metadata and producing useful definitions/lemmata/hints/instances based on that.

view this post on Zulip Bas Spitters (Oct 19 2022 at 12:02):

@Paolo Giarrusso can one now derive countable instances for stdpp automatically using elpi?


Last updated: Feb 08 2023 at 08:02 UTC