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.


Last updated: Jan 31 2023 at 14:03 UTC