Stream: math-comp users

Topic: Decide Equality ?

Bas Spitters (Mar 09 2022 at 10:46):

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

Kazuhiko Sakaguchi (Mar 09 2022 at 10:51):

case: (x =P y)? (assuming the type of x and y is an eqType)

Kazuhiko Sakaguchi (Mar 09 2022 at 10:55):

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

Bas Spitters (Mar 09 2022 at 12:10):

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.

Enrico Tassi (Mar 09 2022 at 12:39):

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).

Christian Doczkal (Mar 09 2022 at 15:32):

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.

Karl Palmskog (Mar 09 2022 at 15:35):

isn't this what https://github.com/arthuraa/deriving is used for as well?

Bas Spitters (Mar 10 2022 at 13:48):

Thanks @Karl Palmskog Deriving actually works for choicetypes already.

Bas Spitters (Mar 10 2022 at 13:52):

@Arthur Azevedo de Amorim How stable is Deriving?
It looks like it needs a minor update to 8.15.

Karl Palmskog (Mar 10 2022 at 13:53):

@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

Bas Spitters (Mar 10 2022 at 14:02):

Great! then the readme and the opam just need to be updated:
https://github.com/arthuraa/deriving

Arthur Azevedo de Amorim (Mar 10 2022 at 15:07):

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