Stream: Coq users

Topic: ✔ Induction principle


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Li-yao (Oct 06 2022 at 01:26):

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

view this post on Zulip Li-yao (Oct 06 2022 at 01:27):

You can certainly prove such an induction principle.

view this post on Zulip 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

view this post on Zulip Notification Bot (Oct 06 2022 at 01:29):

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

view this post on Zulip 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.

view this post on Zulip 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: Jun 15 2024 at 08:01 UTC