Odd residues mod 8

Stream: new members

[Michael Stoll]

For some reason, I need a statement like the following.

lemma mod8_odd (b : ℤ) : 0 ≤ b ∧ b < 8 ∧ odd b → b = 1 ∨ b = 3 ∨ b = 5 ∨ b = 7 := ...

I have constructed the following proof.

begin
  intro hh, rcases hh with ⟨ hlb, hub, hodd ⟩,
  by_cases hx : b = 0,
    simp only [hx, int.even_zero, not_true, int.odd_iff_not_even] at hodd, tauto,
  have hx' : 0 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 1 ≤ b, from hx', clear hx',
  by_cases hx : b = 1, tauto,
  have hx' : 1 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 2 ≤ b, from hx', clear hx',
  by_cases hx : b = 2,
    simp only [hx, not_true, int.even_bit0, int.odd_iff_not_even] at hodd, tauto,
  have hx' : 2 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 3 ≤ b, from hx', clear hx',
  by_cases hx : b = 3, tauto,
  have hx' : 3 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 4 ≤ b, from hx', clear hx',
  by_cases hx : b = 4,
    simp only [hx, not_true, int.even_bit0, int.odd_iff_not_even] at hodd, tauto,
  have hx' : 4 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 5 ≤ b, from hx', clear hx',
  by_cases hx : b = 5, tauto,
  have hx' : 5 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 6 ≤ b, from hx', clear hx',
  by_cases hx : b = 6,
    simp only [hx, not_true, int.even_bit0, int.odd_iff_not_even] at hodd, tauto,
  have hx' : 6 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 7 ≤ b, from hx', clear hx',
  by_cases hx : b = 7, tauto,
  have hx' : 7 < b, from lt_of_le_of_ne hlb (ne.symm hx), clear hlb hx,
  have hlb : 8 ≤ b, from hx', clear hx',
  exfalso,
  exact not_lt_of_le hlb hub,
end

It works, but is sort of ugly. Is there a more elegant way of doing this?

[Heather Macbeth]

A quick version:

import data.int.parity
import tactic.fin_cases

lemma mod8_odd (b : ℤ) : 0 ≤ b ∧ b < 8 ∧ odd b → b = 1 ∨ b = 3 ∨ b = 5 ∨ b = 7 :=
begin
  rintros ⟨h₁, h₂, h₃⟩,
  lift b to ℕ using h₁,
  have : b < 8 := by exact_mod_cast h₂,
  have h₂' : b ∈ finset.range 8 := by simpa using this,
  lift b to finset.range 8 using h₂',
  fin_cases b;
  try { simpa using h₃ }; simp,
end

[Heather Macbeth]

The tactic fin_cases is doing the heavy lifting here: the two lift exhibit the number of possibilities for b as coming from a finite set, then fin_cases makes a separate goal for each of this finite set of possibilities, and then simp deals with each of those cases.