Consider the self-contained example here: https://gist.github.com/vzaliva/9f616fcd49043f5ba390743d1574c4a0. Initially, I defined a type `mem_value_indt`

for which the default induction principle generated by Coq was inadequate. For instance, it did not consider `MVarray`

to be a recursive case. I addressed this with `mem_value_indt_induction`

, which I was able to prove successfully. Similarly, I defined the inductive predicate `mem_value_indt_eq`

for which I attempted to establish a custom induction principle, as I did earlier. However, the proof fails on "Qed" with the message, "Recursive definition of IH is ill-formed. Not enough abstractions in the definition." I never used custom induction principles before and have several questions: 1) Am I doing this right (for these types)? 2) If there is a way to associate my custom induction principle with data type so I do not need to specify it each time in `induction`

tactics. 3) Does the principle generated by`Scheme Induction`

differs from the one generated by default? 4) Perhaps providing a measure function to `fix`

tactics in the prove above will fix the error?

the error is because you need to intro at least `n`

after `fix f n`

One way to have Coq pick it up by default is to first tell Coq not to generate the bogus induction principle, and then proceed to name your custom one has Coq would have done.

@Théo Winterhalter how to tell it not to generate one? use `Variant`

instead of `Inductive`

and when define following `_ind`

naming convention?

```
Lemma foo : unit -> nat -> nat.
Proof.
fix f 2.
intros x;destruct x;intros n;exact 0. (* bad: destruct x before intros n *)
Fail Qed.
```

Vadim Zaliva said:

Théo Winterhalter how to tell it not to generate one? use

`Variant`

instead of`Inductive`

and when define following`_ind`

naming convention?

I'm guessing `Unset Elimination Schemes.`

https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:flag.Elimination-Schemes

`Variant`

would work, but also it doesn't allow you to have recursive types, so it only works when you don't care about induction.

@Gaëtan Gilbert if I modify my example to do `intros x y H; fix IH 3`

I am getting "Error: Not enough products."

Yes, `Unset Elimination Schemes.`

is the way to go. Basically, if the automatically generated induction principle for `foo`

is rubbish, the usual yoga is:

```
Unset Elimination Scheme.
Inductive foo … : … :=
…
.
Set Elimination Schemes.
Lemma foo_rec : … := … .
(* If you need other induction principles in other sorts, define foo_rect, foo_ind… accordingly *)
```

The `Scheme`

command, when used with non-mutual inductive types is afaik what Coq uses internally to generate the induction principle. In the case of mutual ones, it gives a bit more flexibility to define different version of mutual induction principles. It is too weak for nested inductive types, where you have to do things by hand (sadly).

@Gaëtan Gilbert also in `mem_value_indt_induction`

proof I used `fix IH 1`

before doing `intros x`

and it worked.

Vadim Zaliva said:

Gaëtan Gilbert if I modify my example to do

`intros x y H; fix IH 3`

I am getting "Error: Not enough products."

that's not how it should be, it should be `fix IH 3;intros x y H`

Vadim Zaliva said:

Gaëtan Gilbert also in

`mem_value_indt_induction`

proof I used`fix IH 1`

before doing`intros x`

and it worked.

you do `fix IH 1; destruct m`

with the goal `forall m, ...`

so `destruct m`

does the intro (equivalent to `intros m;destruct m`

)

@Gaëtan Gilbert thank you so much! it worked. Now I would love to understand why :)

Last updated: Oct 13 2024 at 01:02 UTC