nat_parity.lean

inductive vector (α : Type) : ℕ → Type
| nil {} : vector 0
| cons {n : ℕ} : α → vector n → vector (nat.succ n)

def x := vector.cons "1" (vector.cons "2" (vector.cons "3" vector.nil))
#check x
#check (⟨3, x⟩ : Σn, vector string n)

#check nat.le_refl
#check nat.le_refl 10
#check nat.lt_succ_of_le (nat.le_refl 10)

def nat_is_inf₁ : ∀(n : ℕ), ∃m, n < m :=
  λn, ⟨n + 1, nat.lt_succ_of_le (nat.le_refl n)⟩

def nat_is_inf₂ : ∀(n : ℕ), ∃m, n < m :=
  λn, nat.rec_on n
    ⟨1, nat.lt_succ_of_le (nat.le_refl 0)⟩
    (λn h, Exists.cases_on h (λ m p, ⟨nat.succ m, nat.succ_le_succ p⟩))

theorem nat_is_inf₃ : ∀(n : ℕ), ∃m, n < m :=
begin
  intro n,
  existsi n + 1,
  apply nat.lt_succ_of_le (nat.le_refl n),
  done
end

theorem nat_is_inf₄ : ∀(n : ℕ), ∃m, n < m :=
begin
  intro n,
  induction n,
    case nat.zero {
      existsi 1,
      apply nat.lt_succ_of_le (nat.le_refl 0)
    },
    case nat.succ : n h {
      cases h with m p,
      existsi nat.succ m,
      apply nat.succ_le_succ p
    },
  done
end



def is_even (n : ℕ) := ∃m, m + m = n
def is_odd (n : ℕ) := ∃m, nat.succ (m + m) = n

lemma zero_is_even : is_even 0 :=
begin existsi 0, reflexivity end

lemma odd_after_even (n : ℕ) : is_even n → is_odd (nat.succ n) :=
begin
  intro h, cases h with m p,
  existsi m, rewrite p
end

lemma even_after_odd (n : ℕ) : is_odd n → is_even (nat.succ n) :=
begin
  intro h, cases h with m p,
  existsi nat.succ m,
  rewrite nat.add_succ,
  rewrite <- p, simp, done
end

theorem nat_parity : ∀n, is_even n ∨ is_odd n :=
begin
  intro n,
  induction n,
    case nat.zero { apply or.inl zero_is_even },
    case nat.succ : n h {
      cases h,
        case or.inl { right, apply odd_after_even n h },
        case or.inr { left, apply even_after_odd n h },
    }
end

variable n : nat
variable m : nat
variable p : nat.succ (m + m) = n
#check p
#check nat.add_succ m m
#check eq.trans (nat.add_comm _ _) (eq.trans (nat.add_succ m m) p)
#check eq.trans (nat.add_comm (nat.succ m) m) (eq.trans (nat.add_succ m m) p)


def zero_is_even₂ : is_even 0 := ⟨0, refl 0⟩
def odd_after_even₂ (n : ℕ) (n_is_even : is_even n) : is_odd (nat.succ n) :=
  Exists.cases_on n_is_even (λm p, ⟨m, congr_arg nat.succ p⟩)
def even_after_odd₂ (n : ℕ) (n_is_odd : is_odd n) : is_even (nat.succ n) :=
  Exists.cases_on n_is_odd (λm p, ⟨nat.succ m,
    congr_arg nat.succ
      (eq.trans
        (nat.add_comm (nat.succ m) m)
        (eq.trans (nat.add_succ m m) p))⟩)


def odd_after_even₃ (n : ℕ) (n_is_even : is_even n) : is_odd (nat.succ n) :=
  let ⟨m, p⟩ := n_is_even
  in ⟨m, congr_arg nat.succ p⟩

def even_after_odd₃ (n : ℕ) (n_is_odd : is_odd n) : is_even (nat.succ n) :=
  let ⟨m, p⟩ := n_is_odd in ⟨
    nat.succ m,
    congr_arg nat.succ
      (eq.trans
        (nat.add_comm (nat.succ m) m)
        (eq.trans (nat.add_succ m m) p))
  ⟩

def nat_parity₂ (n : ℕ) : is_even n ∨ is_odd n :=
  nat.rec_on n
    (or.inl zero_is_even₂)
    (λn h, or.cases_on h
      (λn_is_even, or.inr (odd_after_even₃ n n_is_even))
      (λn_is_odd, or.inl (even_after_odd₃ n n_is_odd)))

def nat_parity₃ (n : ℕ) : is_even n ∨ is_odd n :=
  nat.rec_on n
    (or.inl zero_is_even₂)
    (λn h, match h with
      | or.inl n_is_even := or.inr (odd_after_even₃ n n_is_even)
      | or.inr n_is_odd := or.inl (even_after_odd₃ n n_is_odd)
    end)