We have an internal library at BedRock called `deriving.v`

that we use to generate instances of stdpp classes like `Inhabited`

, `Finite`

, `Decision`

, `Countable`

, etc. Right now, it's not very extensible and supports a very limited set of types.

We're considering making it more re-usable and are wondering whether there are others who've implemented similar things who might be interested in coordinating efforts. (@Enrico Tassi: I know you have `coq-elpi/apps/derive`

for deriving equality tests and wondered whether that's a potential upstreaming target?)

Here's a small example of how the library currently works:

```
Module DerivingTest.
Variant t := A | B | C.
#[instance(eq_dec,countable)] Deriving t.
Goal forall x y : t, if bool_decide (x = y) then True else True.
Proof. by move => x y; case (bool_decide_reflect (x = y)). Qed.
Goal forall x y : t, encode x = encode y -> x = y.
Proof. by move => x y X; apply encode_inj in X. Qed.
Goal match Pos.compare (encode A) (encode B) with
| Eq => True
| Lt => True
| Gt => True
end.
Proof.
Succeed by vm_compute.
(* Even [simpl] normalizes this goal - that's nice! *)
by simpl; assert_True.
Qed.
End DerivingTest.
```

hmm, isn't the current closest thing in the MathComp world deriving? Very different approach, though.

if there is some technical reason for not upstreaming this into `coq-elpi`

(I guess it depends on stdpp?), then we would welcome a library like this into Coq-community (as long as it's under a license approved by OSI or considered a free software license by FSF). We collaboratively maintain a bunch of projects that are in Coq's CI, MathComp's CI, and in the Coq Platform.

Math-comp-wise, what Gordon mentioned and/or Enrico's https://drops.dagstuhl.de/opus/volltexte/2019/11084/pdf/LIPIcs-ITP-2019-29.pdf seem closer, but our generator is more limited

I've reworked derive very recently (for the CPP 2023 work) so that one can hook into it and break the dependencies. E.g. https://github.com/gares/elpi-derive-mathcomp (not released by lack of time) contains math-comp specific glue, so that coq-elpi (apps/derive actually) does not depend on MC. So the same would apply to stdpp, hopefully.

About upstreaming, I'm wondering if it is not the time for elpi/apps/derive to quit the nest and become a separate project. And that project would be welcoming all contributions. About style, one thing I found very handy is to define an AST which almost captures the inductives you can derive. The resulting code is much cleaner.

In any case I'm happy to help making "just one derive" (written in Elpi) a reality.

Thanks, Karl and Enrico, for the pointers and the support.

... coq-elpi (apps/derive actually) does not depend on MC. So the same would apply to stdpp, hopefully.

I took a closer look at `apps/derive`

. It seems like it's already pretty extensible? (In which case, the best strategy is probably for us to build `derive`

-compatible extensions, one for stdpp instances, one for our C++ logic, etc.)

I'm wondering if it is not the time for elpi/apps/derive to quit the nest...

That would be ideal! We're planning on revisiting our `deriving.v`

in the first few months of '23. We can start the porting even before `apps/derive`

becomes its own package. But targeting a standalone library would probably facilitate things.

Gordon Stewart has marked this topic as resolved.

The hope is that most of the code can be in derive (be it part of coq-elpi or not) and only the final "instance declaration" can live outside, and depend on the library it targets.

Yes, look at the derivations in `derive.std`

for example, they all hook into derive. I think I wrote some doc in the README, suggestions appreciated

@Gordon Stewart here the doc: https://github.com/LPCIC/coq-elpi/tree/master/apps/derive#writing-a-new-derivation

I did see those docs; thanks! @David Swasey and I started looking a bit more closely at `apps/derive`

this morning. I'm pretty confident we could adapt our existing derivations into your framework. At some point soon, we may have some additional questions and/or small change suggestions that would facilitate the ports. Though given the upcoming Christmas holiday, we probably won't make a huge amount of progress until January or so.

Great!

Following up, here's an initial version of our derive plugins: https://github.com/bedrocksystems/BRiCk/blob/master/theories/prelude/elpi/derive.v.

We currently support stdpp `EqDecision`

, `Inhabited`

, `Finite`

, `Countable`

, and some custom extensions related to bitsets.

Current known deficiencies:

- We support only "enum"-style types (e.g., variants with no-argument constructors).
- We generate custom
`Countable`

instances so that the encoding to positives computes properly; but the decoding function (positives to`T`

) is currently inefficient.

We noticed an issue in a test case at line https://github.com/bedrocksystems/BRiCk/blob/master/theories/prelude/elpi/derive.v#L44 (`derive`

gives error `Anomaly: Uncaught exception Failure("split dirpath")`

). I suspected this may be a `derive`

bug but haven't yet had time to investigate.

This is only when doing

```
#[only(finite)] derive
Variant T2 := A2 | B2 | C2.
```

The following works fine:

```
Variant T2 := A2 | B2 | C2.
#[only(finite)] derive T2.
```

This is all in:

```
coq-elpi 1.16.0 Elpi extension language for Coq
```

Gordon Stewart has marked this topic as unresolved.

great, I'll look at that ASAP!

Last updated: Jun 06 2023 at 22:01 UTC