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??

https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.decide-equality

`case: (x =P y)`

? (assuming the type of `x`

and `y`

is an `eqType`

)

Many `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:

https://github.com/arthuraa/deriving

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