Examples

A cookbook of short, self-contained proofs of concept, each demonstrating one technique. Every code sample on these pages is run through a real rocq top at build time (see Rocq-Elpi), so what you read is guaranteed to actually work.

• Data bases stores data and shares it across commands and runs via a Db.

• Record expansion translates a term abstracted over a record into one abstracted over the record's components.

• Record to sigma desugars a record type into iterated sigma types.

• Fuzzer mutates a well-typed inductive type while preserving its well-typedness, mapping a term and calling the type checker deep inside it.

• Curry-Howard tactics builds simple tactics directly as proof terms, using Rocq's elaborator.

• Generalize abstracts a term over a subterm, like the generalize tactic.

• Closing terms with holes closes a term containing holes (evars) by replacing them with bound variables.

• Record import gives short names to a record instance's applied projections.

• Reduction surgery fine-tunes cbv to unfold only the constants coming from a given module.

• Open terms implements a replace-like tactic that works on terms with variables bound in the goal but not in the proof context.

• Reflexive tactic builds a reflexive tactic solving monoid equalities via reification and a Db of known monoids.

For adding builtin predicates (implemented in OCaml) to Elpi via a Rocq plugin, see Adding builtin predicates via an OCaml plugin.