Stream: Coq users

Topic: ✔ proof for induction on nats with two base cases

cdepillabout (Nov 19 2021 at 04:46):

I've been reading through Software Foundations, and in the very last section of https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html, the author says that induction on nats with two base cases could be defined like this:

Fixpoint nat_ind_2
         (P : nat -> Prop)
         (PO : P 0)
         (P1 : P 1)
         (PSS : forall m : nat, P m -> P (S (S m)))
         (n : nat) : P n :=
  match n with
  | 0 => PO
  | 1 => P1
  | (S (S k)) => PSS k (nat_ind_2 P PO P1 PSS k)
  end.

The author then says that proving nat_ind_2 as a lemma is much less straight-forward.

What would it look like to prove this as a lemma? I've tried a bunch of different things, but I can't seem to make any headway.

Li-yao (Nov 19 2021 at 06:52):

Either strong induction, or regular induction with an induction hypothesis which is about two consecutive numbers ((P n -> P (S (S n)) /\ (P (S n) -> P (S (S (S n)))))

cdepillabout (Nov 22 2021 at 06:03):

Thanks a lot for the suggestions. I looked up strong induction, and I was able to prove both strong induction, and then my nat_ind_2 function using strong induction!

Notification Bot (Nov 27 2021 at 04:45):

cdepillabout has marked this topic as resolved.

Last updated: Sep 30 2023 at 07:01 UTC