## 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 `nat`s 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: Feb 04 2023 at 23:02 UTC