Man, in the past few days I've been seeing topics about CI runners running out of resources. At the same time I want to ask a question

Is there an induction principle for lists that looks like assume P(l) is true, prove P(l ++ [x]) is true?

Apologies and thanks in advance. I'm not sure whether it's appropriate to ask a beginner question when you are busy maintaining your CI.

Don't worry about CI. Beginner questions are always welcome here!

You can certainly prove such an induction principle.

There is `rev_ind`

```
rev_ind:
forall [A : Type] (P : list A -> Prop),
P nil ->
(forall (x : A) (l : list A), P l -> P (l ++ x :: nil)) ->
forall l : list A, P l
```

Huỳnh Trần Khanh has marked this topic as resolved.

You can see a bunch of list induction principles if you `Require Import List`

and `Search "_ind" list`

.

Is there any resource available that provides a detailed explanation of how Coq generates induction principles for inductive data types? I am having difficulty understanding the generation of induction principles for inductively-defined propositions and indexed types and would like more precise information on the subject.

Last updated: Oct 01 2023 at 19:01 UTC