Search code examples
coqinduction

Turn off automatic induction principle in Coq

I have defined a nested inductive data type and have defined a custom inductive principle for it. However, automated tactics from a library I'm using (specifically, DBLib for de Bruijn indices) expects induction is on the usual inductive principle. Since I never intend to use the originally-generated inductive principle, is there any way to either replace the automatically-generated principle? Or, if not, is there a way to temporarily turn off this automatic generation?

Solution

  • You can do it using Elimination Schemes option. For instance,

    Unset Elimination Schemes.
Inductive nat_tree : Set :=
| NNode' : nat -> list nat_tree -> nat_tree.
Set Elimination Schemes.

    In addition, if you had a simpler (non-recursive) inductive type, you could have used the Variant keyword to make Coq not generate the induction principles:

    Variant foo : Type := Foo.