Induction with more than one base case

Stream: new members

[Pedro Minicz]

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]

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]

docs#nat.two_step_induction