Zulip Chat Archive

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