Is a tactic like Decide Equality available for math-comp? One could imagine extending it to automatically proof that a type is a choice type. Perhaps using elpi??
case: (x =P y)? (assuming the type of
y is an
eqType instances in MathComp are defined by hand, but if you wish to automatically derive them, see: https://doi.org/10.4230/LIPIcs.ITP.2019.29
Thanks! I knew I'd seen this idea somewhere. @Enrico Tassi would it be hard to generate a choiceType structure for these types?
I haven't looked at the list of supported types in detail, but I think most of them will also have a (canonical) choice type structure.
I'm sorry but I've not thought about it. Going trough the GenTree API seems the easiest path (but gives you equality tests which are uglier than the ones you would otherwise get, I mean computationally very different).
I can confirm that
GenTree is what you want to use if you need a
choiceType or indeed
countType instance. I've done this whenever I needed to define some (deeply embedded) syntax and then needed (finite) sets of terms.
isn't this what https://github.com/arthuraa/deriving is used for as well?
Thanks @Karl Palmskog Deriving actually works for choicetypes already.
@Arthur Azevedo de Amorim How stable is Deriving?
It looks like it needs a minor update to 8.15.
@Bas Spitters it's in the Platform for 8.15, so it should work: https://github.com/coq/platform/blob/2022.01.0/doc/README~8.15~beta1.md#coq-platform-2022010-with-coq-8150-extended-level
Great! then the readme and the opam just need to be updated:
Thanks for the heads-up, @Bas Spitters . Deriving has been pretty stable since 0.1.0 came out. I intend to continue maintaining it for the foreseeable future.
Last updated: Jan 29 2023 at 19:02 UTC