cases on mod 3

Stream: new members

[Thomas Browning]

Is there a better way to prove this?

example {n : ℕ} : (n % 3 = 0) ∨ (n % 3 = 1) ∨ (n % 3 = 2) :=
begin
  induction n with n hn,
  exact or.inl (nat.zero_mod 3),
  rw [nat.succ_eq_add_one, nat.add_mod],
  cases hn with hn hn,
  { rw hn,
    exact or.inr (or.inl rfl) },
  cases hn with hn hn,
  { rw hn,
    exact or.inr (or.inr rfl) },
  { rw hn,
    exact or.inl rfl },
end

[Yevhenii Diomidov]

Some purely local optimizations:

example {n : ℕ} : (n % 3 = 0) ∨ (n % 3 = 1) ∨ (n % 3 = 2) :=
begin
  induction n with n hn,
  exact or.inl (nat.zero_mod 3),
  rw [nat.succ_eq_add_one, nat.add_mod],
  rcases hn with hn | hn | hn;
    { rw hn, tauto },
end

[Ruben Van de Velde]

example {n : ℕ} : (n % 3 = 0) ∨ (n % 3 = 1) ∨ (n % 3 = 2) :=
begin
  have : n % 3 < 3 := nat.mod_lt n zero_lt_three,
  interval_cases n % 3; tauto,
end

[Thomas Browning]

Thanks, that's exactly what I was looking for (and also thanks Yevhenii, I didn't know about the | notation)

[Yevhenii Diomidov]

Just for the sake of completeness, here is a term mode proof based on mod_two_eq_zero_or_one:

example {n : ℕ} : (n % 3 = 0) ∨ (n % 3 = 1) ∨ (n % 3 = 2) :=
match n % 3, @nat.mod_lt n 3 dec_trivial with
| 0,   _ := or.inl rfl
| 1,   _ := or.inr $ or.inl rfl
| 2,   _ := or.inr $ or.inr rfl
| k+3, h := absurd h dec_trivial
end