-- Parity of products, powers, and remainders modulo two
-- 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.ParityLemmas
import Parity
import PowLemmas
import Division

theorem Even.two_mul (k : Nat)
  shows Even(2 * k)
proof
  have doubled := mul.two_left at k
  rw doubled
  exact Even.double with *

theorem Even.mul_two (k : Nat)
  shows Even(k * 2)
proof
  have swap := mul.commutative at 2, k with *
  rw swap
  exact Even.two_mul with *

theorem Even.iff_two_mul (n : Nat)
  shows Even(n) ↔ ∃ k, Nat(k) ∧ n = 2 * k
proof
  constructor
  . intro even
    obtain ⟨k, kMember, equation⟩ := even
    have kNat := nat.omega.backward with kMember
    witness k
    rw equation
    ring
  . intro shape
    obtain ⟨k, kNat, equation⟩ := shape
    rw equation
    exact Even.two_mul with *

theorem Odd.iff_two_mul_add_one (n : Nat)
  shows Odd(n) ↔ ∃ k, Nat(k) ∧ n = 2 * k + 1
proof
  constructor
  . intro odd
    obtain ⟨k, kMember, equation⟩ := odd
    have kNat := nat.omega.backward with kMember
    witness k
    rw equation
    ring
  . intro shape
    obtain ⟨k, kNat, equation⟩ := shape
    have doubled := mul.two_left at k
    have step : 2 * k + 1 = succ(k + k) by ring
    rw [equation, step]
    exact Odd.double_successor with *

theorem Odd.one
  shows Odd(1)
proof
  have doubled := Odd.double_successor at 0
  simpa [add] using doubled

theorem Even.not_one
  shows ¬Even(1)
proof
  have one := Odd.one
  exact Odd.not_even with one

theorem Odd.add_one_iff (n : Nat)
  shows Odd(n + 1) ↔ Even(n)
proof
  have shape := add.right_one at n
  rw shape
  exact Odd.succ_iff with *

theorem Odd.positive (n : Nat)
  requires odd : Odd(n)
  shows 0 < n
proof
  obtain ⟨k, kMember, equation⟩ := odd
  have kNat := nat.omega.backward with kMember
  rw equation
  have step : succ(k + k) = k + k + 1 by ring
  rw step
  linarith

theorem Even.mul_left (a b : Nat)
  requires even : Even(a)
  shows Even(a * b)
proof
  obtain ⟨k, kNat, equation⟩ := Even.iff_two_mul.forward with even
  apply Even.iff_two_mul.backward
  witness k * b
  rw equation
  ring

theorem Even.mul_right (a b : Nat)
  requires even : Even(b)
  shows Even(a * b)
proof
  have swap := mul.commutative at b, a with *
  rw swap
  exact Even.mul_left with even

theorem Odd.mul (a b : Nat)
  requires first : Odd(a)
  requires second : Odd(b)
  shows Odd(a * b)
proof
  obtain ⟨k, kNat, aShape⟩ := Odd.iff_two_mul_add_one.forward with first
  obtain ⟨m, mNat, bShape⟩ := Odd.iff_two_mul_add_one.forward with second
  apply Odd.iff_two_mul_add_one.backward
  witness 2 * k * m + k + m
  rw [aShape, bShape]
  ring

theorem Even.of_mul (a b : Nat)
  requires even : Even(a * b)
  shows Even(a) ∨ Even(b)
proof
  have aSplit := parity.exhaustive at a
  cases aSplit with aEven | aOdd
  . left
    exact aEven
  . have bSplit := parity.exhaustive at b
    cases bSplit with bEven | bOdd
    . right
      exact bEven
    . have odd := Odd.mul with aOdd, bOdd
      exfalso
      exact Odd.not_even with odd, even

theorem Odd.of_mul (a b : Nat)
  requires odd : Odd(a * b)
  shows Odd(a) ∧ Odd(b)
proof
  have aSplit := parity.exhaustive at a
  have bSplit := parity.exhaustive at b
  constructor
  . cases aSplit with aEven | aOdd
    . have even := Even.mul_left at a, b with aEven
      exfalso
      exact Even.not_odd with even, odd
    . exact aOdd
  . cases bSplit with bEven | bOdd
    . have even := Even.mul_right at a, b with bEven
      exfalso
      exact Even.not_odd with even, odd
    . exact bOdd

theorem Even.mul_self_iff (n : Nat)
  shows Even(n * n) ↔ Even(n)
proof
  constructor
  . intro even
    have split := Even.of_mul with even
    cases split with first | second
    . exact first
    . exact second
  . intro even
    exact Even.mul_left with even

theorem Odd.mul_self_iff (n : Nat)
  shows Odd(n * n) ↔ Odd(n)
proof
  constructor
  . intro odd
    have both := Odd.of_mul with odd
    exact both.left
  . intro odd
    exact Odd.mul with odd, odd

theorem Even.pow (a n : Nat)
  requires even : Even(a)
  shows Even(a ^ (n + 1))
proof
  have powNat := pow.closed at a, n
  rw pow.add_one
  exact Even.mul_left with even

theorem Odd.pow (a n : Nat)
  requires odd : Odd(a)
  shows Odd(a ^ n)
proof
  induction n
  | zero =>
    rw pow.zero
    exact Odd.one
  | succ(k) using ih =>
    have powNat := pow.closed at a, k
    rw pow.succ
    exact Odd.mul with odd, ih

theorem Even.of_pow (a n : Nat)
  requires even : Even(a ^ n)
  shows Even(a)
proof
  have split := parity.exhaustive at a
  cases split with aEven | aOdd
  . exact aEven
  . have odd := Odd.pow at a, n with aOdd
    exfalso
    exact Odd.not_even with odd, even

theorem Even.of_add_even (a b : Nat)
  requires sum : Even(a + b)
  requires even : Even(a)
  shows Even(b)
proof
  have split := parity.exhaustive at b
  cases split with bEven | bOdd
  . exact bEven
  . have odd := Odd.even_add at a, b with even, bOdd
    exfalso
    exact Odd.not_even with odd, sum

theorem Odd.of_add_even_odd (a b : Nat)
  requires sum : Even(a + b)
  requires odd : Odd(a)
  shows Odd(b)
proof
  have split := parity.exhaustive at b
  cases split with bEven | bOdd
  . have sumOdd := Odd.add_even at a, b with odd, bEven
    exfalso
    exact Odd.not_even with sumOdd, sum
  . exact bOdd

theorem Odd.of_add_odd_even (a b : Nat)
  requires sum : Odd(a + b)
  requires even : Even(a)
  shows Odd(b)
proof
  have split := parity.exhaustive at b
  cases split with bEven | bOdd
  . have sumEven := Even.add at a, b with even, bEven
    exfalso
    exact Even.not_odd with sumEven, sum
  . exact bOdd

theorem Even.of_add_odd_odd (a b : Nat)
  requires sum : Odd(a + b)
  requires odd : Odd(a)
  shows Even(b)
proof
  have split := parity.exhaustive at b
  cases split with bEven | bOdd
  . exact bEven
  . have sumEven := Odd.add_odd at a, b with odd, bOdd
    exfalso
    exact Even.not_odd with sumEven, sum

theorem Even.add_iff (a b : Nat)
  shows Even(a + b) ↔ (Even(a) ↔ Even(b))
proof
  have aSplit := parity.exhaustive at a
  constructor
  . intro sum
    constructor
    . intro aEven
      exact Even.of_add_even with sum, aEven
    . intro bEven
      have swap := add.commutative at b, a with *
      rw swap at sum
      exact Even.of_add_even at b, a with sum, bEven
  . intro same
    cases aSplit with aEven | aOdd
    . have bEven := same.forward with aEven
      exact Even.add with aEven, bEven
    . have bOdd : Odd(b)
        have split := parity.exhaustive at b
        cases split with bEven | odd
        . have aEven := same.backward with bEven
          exfalso
          exact Odd.not_even with aOdd, aEven
        . exact odd
      exact Odd.add_odd with aOdd, bOdd

theorem Even.mod_two (n : Nat)
  shows Even(n) ↔ n % 2 = 0
proof
  have two : 2 ≠ 0
    intro zero
    have impossible : 0 < 2 by linarith
    rw zero at impossible
    exact Less.irreflexive with impossible
  have division := mod.division at 2, n with two
  rcases division with ⟨equation, bound⟩
  obtain ⟨q, qNat, shape⟩ := equation
  have modNat := mod.natural at 2, n
  have remainder : n % 2 = 0 ∨ n % 2 = 1
    have small : n % 2 ≤ 1 by linarith
    have split := LessEqual.cases with small
    cases split with strict | one
    . left
      have zero : n % 2 ≤ 0 by linarith
      exact LessEqual.eq_zero with zero
    . right
      exact one
  constructor
  . intro even
    cases remainder with zero | one
    . exact zero
    . rw one at shape
      have odd : Odd(n)
        apply Odd.iff_two_mul_add_one.backward
        witness q
        exact shape
      exfalso
      exact Odd.not_even with odd, even
  . intro zero
    rw zero at shape
    apply Even.iff_two_mul.backward
    witness q
    have unit := add.right_unit at 2 * q
    rw unit at shape
    exact shape

theorem Odd.mod_two (n : Nat)
  shows Odd(n) ↔ n % 2 = 1
proof
  have two : 2 ≠ 0
    intro zero
    have impossible : 0 < 2 by linarith
    rw zero at impossible
    exact Less.irreflexive with impossible
  have modNat := mod.natural at 2, n
  have bound := mod.less at n, 2 with two
  constructor
  . intro odd
    have notEven := Odd.not_even with odd
    have nonzero : n % 2 ≠ 0
      intro zero
      have even := Even.mod_two.backward with zero
      exact notEven with even
    have positive := Less.positive_of_ne_zero with nonzero
    have upper : n % 2 ≤ 1 by linarith
    have lower : 1 ≤ n % 2 by linarith
    exact LessEqual.antisymmetric with upper, lower
  . intro one
    have split := parity.exhaustive at n
    cases split with even | odd
    . have zero := Even.mod_two.forward with even
      rw zero at one
      have impossible : 0 < 1 by linarith
      rw ← one at impossible
      exfalso
      exact Less.irreflexive with impossible
    . exact odd