The Deriving library builds instances of basic MathComp classes for inductive
data types with little boilerplate, akin to Haskell's deriving functionality.
To define an eqType instance for a type foo, just write:
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrnat eqtype.
From deriving Require Import deriving.
Inductive foo := Foo1 of nat | Foo2 of foo & nat.
(* foo_rect is the recursor automatically generated by Coq *)
Definition foo_indDef := [indDef for foo_rect].
Canonical foo_indType := IndType foo foo_indDef.
Definition foo_hasDecEq := [derive hasDecEq for foo].
HB.instance Definition _ := foo_hasDecEq.
Besides simple definitions such as the one above, Deriving can handle the following features:
-
Types with uniform parameters (e.g.
list). -
Mutually inductive types (by using the recursor generated by
Combined Schemecommand). -
Nested inductive types (if you write your own recursor).
Check the tests/ directory for detailed examples.
The following features are still not supported:
-
Types with non-uniform parameters (e.g.
Vector.t). -
Constructors with dependent types (e.g.
C : forall n : nat, P n -> T). -
Coinductive types.
Besides eqType, there are predefined generic instances for choiceType,
countType, finType and orderType. To use them, you must ensure that every
non-recursive argument of the type is also an instance of the class;
otherwise, you'll get an ugly, uninformative error message. For finType, you
must additionally ensure that the type does not have recursive occurrences.
You can also define instances for your own classes inside of Coq, without
resorting to OCaml code. This feature is not documented yet, but you can refer
to the definition of the instances provided by Deriving in
theories/instances. Or drop me a line!
Coq does not generate induction principles for record types by default. If you want to derive an instance for a record type, you need to generate the induction principle by hand:
Record foo := (* ... *)
Scheme foo_rect := Induction for foo Sort Type.
Check the tests for an example.
It is useful for instances of certain classes to have good reduction behavior
(e.g. eqType). By default, Deriving attempts to simplify the derived
instances as much as possible, to make them more similar to hand-written code.
However, this process can be too slow for large definitions, so it can be
disabled with the nored flag:
Definition large_type_hasDecEq : Equality.mixin_of large_type.
Proof. exact [derive nored hasDecEq for large_type]. Qed.
In such cases, it is a good idea to keep the instance opaque (e.g. defined with
Qed) to avoid slowdown.
-
Coq 8.17 -- 8.18
-
coq-mathcomp-ssreflect2.0.0
Deriving can be installed through the
released repository:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-derivingAlternatively, you can compile Deriving from source:
make && make installIf you want to cite Deriving, you can refer to its Zenodo page.