This Coq library allows you to transform an inductive definition to another inductive definition, by providing a constructor transformer tactic. It can be used to generate boilerplate lemmas for backward and forward reasoning, and to generate inductive types with many similar cases.
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-idt
- coq (8.12-8.13)
- coq-metacoq-template (>= 1.0~beta2+8.12)
A set of more complicated applications can be found in the Coq formalization of oblivious algebraic data types.
- Generate lemmas about multi-parallel-reduction for backward reasoning: theories/lang_oadt/mpared.v
- Generate inversion lemmas about the typing and kinding relations for forward reasoning: theories/lang_oadt/inversion.v
- Generate the indistinguishability relation with mostly boring congruence cases: theories/lang_oadt/indistinguishable.v
- Generate an equivalent small-step semantics with the evaluation context rule (and the nonstandard "leaky" context rule) "expanded": theories/lang_oadt/step_alt.v
- Generate an equivalent intermediate semantics that admits a stronger induction principle: theories/lang_oadt/reveal.v