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