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.

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))))`

)

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!

cdepillabout has marked this topic as resolved.

Last updated: Jun 15 2024 at 08:01 UTC