Plugin Projects in Template Coq

This is a list of potential plugins one could write using Template Coq. Feel free to add links to finished or ongoing projects, or add potential projects yourself.

• Induction principles

• Induction principles for mutual inductive types

• Induction principles for simple nested inductive types only mentioning prod, option and list

• Induction principles for nested inductive types

• Equality deciders (similar to Scheme Equality)

• Finiteness proofs

• Countability (/enumerability) proofs

• Selectors/discriminators (e.g. is_nil : forall A, list A -> bool and is_cons, or more advanced versions like inv_cons : forall A, list A -> option (A * list A)); also projectors extracting fields when the corresponding discriminator holds (e.g. cons_hd : forall A (l : list A), is_cons l -> A); a proof of concept for generating disciminators with metacoq is there

• Lenses & Prisms, extending https://github.com/gmalecha/coq-lens, for instance with proofs

• Subterm relations (similar to Derive Subterm in Equations)

• Show instances, i.e. Show A := show : A -> string

• Sized instances, i.e. Sized A := size : A -> nat/ord

• Quickchick Generators instances ?

• Haskell-style deriving of Functor, Monad, Applicative

• Haskell-style deriving of an ordering relation, e.g. Ord

• Polynomial representations of inductive types

• Record-based (Negative) presentation of indexed coinductive types (discussion on zulip)

• Graph relations for functions, similar to what Equations does or similar to what is asked for here

• Generating functions from inductive functional relations (+ case-tree data ?)