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.
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