-- Even and odd natural numbers, their dichotomy, and addition laws.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Nat.Parity
import Order
import Foundation

predicate Even (n : Set) := ∃ k ∈ ℕ, n = add(k, k)
predicate Odd (n : Set) := ∃ k ∈ ℕ, n = succ(add(k, k))

theorem Even.double (k : Nat)
  shows Even(add(k, k))
proof
  unfold Even
  refine ⟨k, nat.omega.forward at k with *, rfl⟩

theorem Even.zero
  shows Even(0)
proof
  have doubled := Even.double at 0 with *
  simpa [add] using doubled

theorem Even.natural (n : Set)
  requires even : Even(n)
  shows Nat(n)
proof
  rcases even with ⟨k, member, equality⟩
  have natural := nat.omega.backward with member
  rw equality
  typecheck

theorem Even.add (a b : Set)
  requires evenA : Even(a)
  requires evenB : Even(b)
  shows Even(add(a, b))
proof
  rcases evenA with ⟨k, hk, aEq⟩
  rcases evenB with ⟨m, hm, bEq⟩
  have kNat := nat.omega.backward with hk
  have mNat := nat.omega.backward with hm
  have sumNat : Nat(add(k, m)) by typecheck
  witness add(k, m)
  constructor
  . exact nat.omega.forward at add(k, m) with sumNat
  . rw [aEq, bEq]
    ring

-- Integer rounding excludes a half-integer witness for any double plus one.
theorem Even.not_successor_double (n : Nat)
  shows ¬Even(succ(add(n, n)))
proof
  intro even
  rcases even with ⟨k, member, equation⟩
  have natural := nat.omega.backward with member
  have low : k ≤ n by arith
  have high : succ(n) ≤ k by arith
  have impossible : k < k by arith
  exact Less.irreflexive with *, impossible

theorem Odd.double_successor (k : Nat)
  shows Odd(succ(add(k, k)))
proof
  unfold Odd
  refine ⟨k, nat.omega.forward at k with *, rfl⟩

theorem Odd.natural (n : Set)
  requires odd : Odd(n)
  shows Nat(n)
proof
  rcases odd with ⟨k, member, equality⟩
  have natural := nat.omega.backward with member
  rw equality
  typecheck

theorem Odd.not_even (n : Set)
  requires odd : Odd(n)
  shows ¬Even(n)
proof
  rcases odd with ⟨k, member, equality⟩
  have natural := nat.omega.backward with member
  rw equality
  exact Even.not_successor_double with *

theorem Even.not_odd (n : Set)
  requires even : Even(n)
  shows ¬Odd(n)
proof
  simp [Odd.not_even]

theorem Odd.succ_of_even (n : Set)
  requires even : Even(n)
  shows Odd(succ(n))
proof
  rcases even with ⟨k, member, equality⟩
  have natural := nat.omega.backward with member
  rw equality
  exact Odd.double_successor with *

theorem Even.succ_of_odd (n : Set)
  requires odd : Odd(n)
  shows Even(succ(n))
proof
  rcases odd with ⟨k, member, equality⟩
  have natural := nat.omega.backward with member
  have nextNat : Nat(succ(k)) by typecheck
  witness succ(k)
  constructor
  . exact nat.omega.forward at succ(k) with nextNat
  . rw equality
    ring

theorem parity.exhaustive (n : Nat)
  shows Even(n) ∨ Odd(n)
proof
  induction n
  | zero =>
    left
    exact Even.zero
  | succ(k) using ih =>
    cases ih with even | odd
    . right
      exact Odd.succ_of_even with even
    . left
      exact Even.succ_of_odd with odd

theorem Even.iff_not_odd (n : Nat)
  shows Even(n) ↔ ¬Odd(n)
proof
  simp [parity.exhaustive, Even.not_odd]

theorem Odd.iff_not_even (n : Nat)
  shows Odd(n) ↔ ¬Even(n)
proof
  simp [parity.exhaustive, Odd.not_even]

theorem Odd.add_even (a b : Set)
  requires oddA : Odd(a)
  requires evenB : Even(b)
  shows Odd(add(a, b))
proof
  rcases oddA with ⟨k, hk, aEq⟩
  rcases evenB with ⟨m, hm, bEq⟩
  have kNat := nat.omega.backward with hk
  have mNat := nat.omega.backward with hm
  have sumNat : Nat(add(k, m)) by typecheck
  witness add(k, m)
  constructor
  . exact nat.omega.forward at add(k, m) with sumNat
  . rw [aEq, bEq]
    ring

theorem Odd.add_odd (a b : Set)
  requires oddA : Odd(a)
  requires oddB : Odd(b)
  shows Even(add(a, b))
proof
  rcases oddA with ⟨k, hk, aEq⟩
  rcases oddB with ⟨m, hm, bEq⟩
  have kNat := nat.omega.backward with hk
  have mNat := nat.omega.backward with hm
  have sumNat : Nat(succ(add(k, m))) by typecheck
  witness succ(add(k, m))
  constructor
  . exact nat.omega.forward at succ(add(k, m)) with sumNat
  . rw [aEq, bEq]
    ring

theorem Odd.even_add (a b : Set)
  requires evenA : Even(a)
  requires oddB : Odd(b)
  shows Odd(add(a, b))
proof
  have swapped : add(a, b) = add(b, a) by ring
  rw swapped
  exact Odd.add_even with *

theorem Even.succ_iff (n : Nat)
  shows Even(succ(n)) ↔ Odd(n)
proof
  have alternatives := parity.exhaustive with *
  have fromEven := Odd.succ_of_even at n
  have fromOdd := Even.succ_of_odd at n
  have excluded := Odd.not_even at succ(n)
  tauto

theorem Odd.succ_iff (n : Nat)
  shows Odd(succ(n)) ↔ Even(n)
proof
  have alternatives := parity.exhaustive with *
  have fromEven := Odd.succ_of_even at n
  have fromOdd := Even.succ_of_odd at n
  have excluded := Even.not_odd at succ(n)
  tauto

theorem Odd.three
  shows Odd(3)
proof
  have result := Odd.double_successor at 1 with *
  simpa [add] using result

theorem Odd.five
  shows Odd(5)
proof
  have result := Odd.double_successor at 2 with *
  simpa [add] using result

theorem Even.not_three
  shows ¬Even(3)
proof
  exact Odd.not_even with Odd.three

theorem Even.not_five
  shows ¬Even(5)
proof
  exact Odd.not_even with Odd.five