Hi everyone. I've been working on a library to derive instances of mathcomp classes for basic inductive types. The code lives here, and it is available as coq-deriving
on the extra-dev
OPAM repository. I was planning on cleaning the code releasing a first version soon, so I would be very interested in any feedback that you guys have!
You may be interested in the strongly related work by @Enrico Tassi : Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq.
I think @Arthur Azevedo de Amorim is aware of my work. His work covers less inductive types, IIRC, but is pure gallina, so zero external dependencies and zero maintenance cost (it's correct by typing). IMO it would be a nice companion to eqType for example.
Okay, my main interest for bringing this up was to get someone to compare the two, thank you. If I recall your talk on the subject correctly, then your work does not require the user to write recursors for nested inductive types, does it? (I guess whether coq-elpi is to be considered an external dependency depends on how quickly the port to HB becomes part of mathcomp master).
Until recently, Deriving could only handle non-mutual inductive definitions. I just added support for mutual inductives, which allows you to handle nested inductives as well (provided the user is willing to write their own recursors).
What is not very pretty about the library is the inference part, which reifies the recursor of a type. It uses a combination of Ltac, type classes and canonical structures, and it's been a bit challenging to maintain. It would be nice to see if this would be more natural to program in ELPI.
I have also found it challenging to simplify the generated terms for things like eq_op
. Doing it naively causes the performance to blow up quickly, and doing it faster is hard to maintain. I've managed to get the performance to acceptable levels for small types, and tolerable levels for larger types. But there is a lot of room for improvement.
Last updated: Oct 13 2024 at 01:02 UTC