## Stream: new members

### Topic: Induction with more than one base case

#### Pedro Minicz (Oct 05 2020 at 23:38):

I believe I've asked this here before, but I can't find the thread. How can I do induction on nat (or, if possible, any type) with more than one base case. For example, below, it would be nice to be able two base cases 0 and 1.

import tactic

open nat

def half : ℕ → ℕ
| 0       := 0
| 1       := 0
| (x + 2) := half x + 1

-- Not a problem with pattern matching
lemma half_lt : ∀ x, half x < x + 1
| 0       := one_pos
| 1       := two_pos
| (x + 2) := succ_lt_succ (lt.step (half_lt x))

example (x : ℕ) : half x < x + 1 :=
begin
-- This proof is kind of ugly.
apply nat.strong_induction_on x, clear x,
intros x ih,
rcases x with _|_|x,
{ exact one_pos },
{ exact two_pos },
{ specialize ih x (lt.step (lt.base x)),
apply succ_lt_succ,
calc half x < x + 1 : ih
...         < x + 2 : lt.base (x + 1) }
end


#### Kyle Miller (Oct 06 2020 at 00:05):

It seems like you have a pretty good pattern there with rcases. Here's a slight variation:

example (x : ℕ) : half x < x + 1 :=
begin
refine x.strong_induction_on (λ n ih, _),
rcases n with _|_|n,
{ exact one_pos },
{ exact two_pos },
{ exact succ_lt_succ (lt.step (ih n (by linarith : n < n + 2))) },
end


#### Chris Wong (Oct 07 2020 at 22:58):

docs#nat.two_step_induction

Last updated: Dec 20 2023 at 11:08 UTC