even_odd.lean

-- Proof by induction that every natural number is either even or odd.
--
-- I did this after seeing the statement "showing every number is even or odd
-- is easier in binary than in unary, as binary is just unary partitioned by
-- evenness". <https://twitter.com/TaliaRinger/status/1261465453282512896>
--
-- I believe it, but the hidden part of the work is showing that they're the
-- natural numbers and defining addition and multiplication on them.

def is_even (n : ℕ) : Prop := ∃ k, 2 * k = n

def is_odd (n : ℕ) : Prop := ∃ k, 2 * k + 1 = n

def zero_even : is_even 0 := exists.intro 0 (by simp)

lemma even_succ (n : ℕ) (hne : is_even n) : is_odd (n + 1) :=
  exists.elim hne (λ k h2k,
    exists.intro k (show 2 * k + 1 = n + 1, by rw [h2k]))

lemma odd_succ (n : ℕ) (hno : is_odd n) : is_even (n + 1) :=
  exists.elim hno (λ k h2k,
    exists.intro (k + 1)
      (show 2 * (k + 1) = n + 1,
        from calc
          2 * (k + 1) = 2 * k + 2 : by refl
          ... = (2 * k + 1) + 1 : by rw []
          ... = n + 1 : by rw h2k))

-- Every number is either even or odd.
def even_or_odd (n : ℕ) : is_even n ∨ is_odd n :=
begin
  induction n,
  case nat.zero {left, exact zero_even},
  case nat.succ : p hp {
    cases hp,
    right, exact even_succ p hp,
    left, exact odd_succ p hp },
end

open nat

-- Verbose proof, with many steps written out.
def even_or_odd_explicit (n : ℕ) : is_even n ∨ is_odd n :=
begin
  induction n,
  -- Base case.
  case zero : {
    have : 2 * 0 = 0,            by simp,
    have : ∃ k, 2 * k = 0,       by exact exists.intro 0 this,
    have : is_even 0,            by exact this,
    show is_even 0 ∨ is_odd 0,   by { left, assumption }
  },
  -- Induction step.
  case succ : p hp {
    cases hp,
    case or.inl {
      have : is_even p,                         by assumption,
      have : is_odd (succ p),                   by exact even_succ p hp,
      show is_even (succ p) ∨ is_odd (succ p),  by { right, assumption }
    },
    case or.inr {
      -- the other case: p is odd. mirror image of the above, but terse
      left, exact odd_succ p hp
    }
  }
end