Huỳnh Trần Khanh (Oct 06 2022 at 01:23): Huỳnh Trần Khanh (Oct 06 2022 at 01:23):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
Huỳnh Trần Khanh (Oct 06 2022 at 01:24):Is there an induction principle for lists that looks like assume P(l) is true, prove P(l ++ [x]) is true?
Huỳnh Trần Khanh (Oct 06 2022 at 01:25):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.
Li-yao (Oct 06 2022 at 01:26):Don't worry about CI. Beginner questions are always welcome here!
Li-yao (Oct 06 2022 at 01:27):You can certainly prove such an induction principle.
Li-yao (Oct 06 2022 at 01:28):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.
Li-yao (Oct 06 2022 at 01:29):You can see a bunch of list induction principles if you Require Import List and Search "_ind" list.
yiyuan-cao (Jun 28 2023 at 06:19):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 13 2024 at 01:02 UTC