-- Even and odd integers
-- 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.Int.Parity
import OrderMul

predicate IntegerEven (z : Set) := ∃ k ∈ ℤ, z = k + k
predicate IntegerOdd (z : Set) := ∃ k ∈ ℤ, z = k + k + 1

theorem IntegerEven.double (k : Integer)
  shows IntegerEven(k + k)
proof
  have member : k ∈ ℤ by settle with Integer
  exact ⟨k, member, rfl⟩

theorem IntegerOdd.double_add_one (k : Integer)
  shows IntegerOdd(k + k + 1)
proof
  have member : k ∈ ℤ by settle with Integer
  exact ⟨k, member, rfl⟩

theorem IntegerEven.integer (z : Set)
  requires even : IntegerEven(z)
  shows Integer(z)
proof
  obtain ⟨k, kMember, shape⟩ := even
  have kInteger : Integer(k) by typecheck
  rw shape
  exact integerAddValue.integer with *

theorem IntegerOdd.integer (z : Set)
  requires odd : IntegerOdd(z)
  shows Integer(z)
proof
  obtain ⟨k, kMember, shape⟩ := odd
  have kInteger : Integer(k) by typecheck
  have sum := integerAddValue.integer at k, k with *
  rw shape
  exact integerAddValue.integer at k + k, integerOne with *

theorem IntegerEven.zero
  shows IntegerEven(integerZero)
proof
  have doubled := IntegerEven.double at integerZero
  have shape : integerZero + integerZero = integerZero by ring
  rw shape at doubled
  exact doubled

theorem IntegerOdd.one
  shows IntegerOdd(integerOne)
proof
  have shaped := IntegerOdd.double_add_one at integerZero
  have shape : integerZero + integerZero + 1 = integerOne by ring
  rw shape at shaped
  exact shaped

theorem IntegerEven.neg (z : Integer)
  requires even : IntegerEven(z)
  shows IntegerEven(-z)
proof
  obtain ⟨k, kMember, shape⟩ := even
  have kInteger : Integer(k) by typecheck
  have negated : -z = (-k) + (-k)
    rw shape
    ring
  rw negated
  exact IntegerEven.double with *

theorem IntegerOdd.neg (z : Integer)
  requires odd : IntegerOdd(z)
  shows IntegerOdd(-z)
proof
  obtain ⟨k, kMember, shape⟩ := odd
  have kInteger : Integer(k) by typecheck
  have negated : -z = (-k - 1) + (-k - 1) + 1
    rw shape
    ring
  rw negated
  exact IntegerOdd.double_add_one with *

theorem IntegerEven.add (x y : Integer)
  requires first : IntegerEven(x)
  requires second : IntegerEven(y)
  shows IntegerEven(x + y)
proof
  obtain ⟨k, kMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have kInteger : Integer(k) by typecheck
  have mInteger : Integer(m) by typecheck
  have sum : x + y = (k + m) + (k + m)
    rw [xShape, yShape]
    ring
  rw sum
  exact IntegerEven.double with *

theorem IntegerOdd.add_even (x y : Integer)
  requires first : IntegerOdd(x)
  requires second : IntegerEven(y)
  shows IntegerOdd(x + y)
proof
  obtain ⟨k, kMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have kInteger : Integer(k) by typecheck
  have mInteger : Integer(m) by typecheck
  have sum : x + y = (k + m) + (k + m) + 1
    rw [xShape, yShape]
    ring
  rw sum
  exact IntegerOdd.double_add_one with *

theorem IntegerOdd.even_add (x y : Integer)
  requires first : IntegerEven(x)
  requires second : IntegerOdd(y)
  shows IntegerOdd(x + y)
proof
  have swapped := IntegerOdd.add_even with second, first
  have shape : y + x = x + y by ring
  rw shape at swapped
  exact swapped

theorem IntegerEven.add_odd_odd (x y : Integer)
  requires first : IntegerOdd(x)
  requires second : IntegerOdd(y)
  shows IntegerEven(x + y)
proof
  obtain ⟨k, kMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have kInteger : Integer(k) by typecheck
  have mInteger : Integer(m) by typecheck
  have sum : x + y = (k + m + 1) + (k + m + 1)
    rw [xShape, yShape]
    ring
  rw sum
  exact IntegerEven.double with *

theorem IntegerEven.sub (x y : Integer)
  requires first : IntegerEven(x)
  requires second : IntegerEven(y)
  shows IntegerEven(x - y)
proof
  have negated := IntegerEven.neg with second
  have sum := IntegerEven.add with first, negated
  have shape : x + (-y) = x - y by ring
  rw shape at sum
  exact sum

theorem IntegerEven.sub_odd_odd (x y : Integer)
  requires first : IntegerOdd(x)
  requires second : IntegerOdd(y)
  shows IntegerEven(x - y)
proof
  have negated := IntegerOdd.neg with second
  have sum := IntegerEven.add_odd_odd with first, negated
  have shape : x + (-y) = x - y by ring
  rw shape at sum
  exact sum

theorem IntegerEven.mul_left (x y : Integer)
  requires even : IntegerEven(x)
  shows IntegerEven(x * y)
proof
  obtain ⟨k, kMember, xShape⟩ := even
  have kInteger : Integer(k) by typecheck
  have product : x * y = (k * y) + (k * y)
    rw xShape
    ring
  rw product
  exact IntegerEven.double with *

theorem IntegerEven.mul_right (x y : Integer)
  requires even : IntegerEven(y)
  shows IntegerEven(x * y)
proof
  have swapped := IntegerEven.mul_left at y, x with even
  have shape : y * x = x * y by ring
  rw shape at swapped
  exact swapped

theorem IntegerOdd.mul (x y : Integer)
  requires first : IntegerOdd(x)
  requires second : IntegerOdd(y)
  shows IntegerOdd(x * y)
proof
  obtain ⟨k, kMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have kInteger : Integer(k) by typecheck
  have mInteger : Integer(m) by typecheck
  have product : x * y = (k * m + k * m + k + m) + (k * m + k * m + k + m) + 1
    rw [xShape, yShape]
    ring
  rw product
  exact IntegerOdd.double_add_one with *

theorem integerAddValue.double_ne_one (j : Integer)
  shows j + j ≠ 1
proof
  intro same
  have split := integerLe.cases_sign at j
  cases split with nonnegative | nonpositive
  . have cases := integerLe.cases with nonnegative
    cases cases with positive | zero
    . have one := integerLess.one_le_of_positive with positive
      have doubled := integerLe.add with one, one
      rw same at doubled
      have strict := integerLess.add_one at integerOne
      exact integerLe.not_less with doubled, strict
    . rw ← zero at same
      have shape : integerZero + integerZero = integerZero by ring
      rw shape at same
      have strict := integerLess.zero_one
      rw same at strict
      exact integerLess.irreflexive with strict
  . have doubled := integerLe.add with nonpositive, nonpositive
    rw same at doubled
    have shape : integerZero + integerZero = integerZero by ring
    rw shape at doubled
    have strict := integerLess.zero_one
    exact integerLe.not_less with doubled, strict

theorem IntegerOdd.not_even (z : Integer)
  requires odd : IntegerOdd(z)
  shows ¬IntegerEven(z)
proof
  intro even
  obtain ⟨k, kMember, oddShape⟩ := odd
  obtain ⟨m, mMember, evenShape⟩ := even
  have kInteger : Integer(k) by typecheck
  have mInteger : Integer(m) by typecheck
  have difference : (m - k) + (m - k) = 1
    linear_combination oddShape - evenShape
  have excluded := integerAddValue.double_ne_one at m - k
  exact excluded with difference

theorem IntegerEven.not_odd (z : Integer)
  requires even : IntegerEven(z)
  shows ¬IntegerOdd(z)
proof
  intro odd
  exact IntegerOdd.not_even with odd, even

theorem IntegerEven.ofNat (n : Nat)
  requires even : Even(n)
  shows IntegerEven(integerOfNat(n))
proof
  obtain ⟨k, kMember, shape⟩ := even
  have kNat := nat.omega.backward with kMember
  have sum := integerOfNat.add at k, k
  rw [shape, sum]
  exact IntegerEven.double with *

theorem IntegerOdd.ofNat (n : Nat)
  requires odd : Odd(n)
  shows IntegerOdd(integerOfNat(n))
proof
  obtain ⟨k, kMember, shape⟩ := odd
  have kNat := nat.omega.backward with kMember
  have step : succ(k + k) = (k + k) + 1 by ring
  have inner := integerOfNat.add at k, k
  have outer := integerOfNat.add at k + k, 1
  have one : integerOfNat(1) = 1
    unfold integerOne
    rfl
  rw [shape, step, outer, inner, one]
  exact IntegerOdd.double_add_one with *

theorem IntegerEven.negative_ofNat (n : Nat)
  requires even : Even(n)
  shows IntegerEven(integerNegativeOfNat(n))
proof
  have lifted := IntegerEven.ofNat with even
  have negated := IntegerEven.neg with lifted
  rw integerOfNat.neg at negated
  exact negated

theorem IntegerOdd.negative_ofNat (n : Nat)
  requires odd : Odd(n)
  shows IntegerOdd(integerNegativeOfNat(n))
proof
  have lifted := IntegerOdd.ofNat with odd
  have negated := IntegerOdd.neg with lifted
  rw integerOfNat.neg at negated
  exact negated

theorem IntegerParity.exhaustive (z : Integer)
  shows IntegerEven(z) ∨ IntegerOdd(z)
proof
  obtain ⟨n, nNat, sign⟩ := Integer.signed_natural at z with *
  have split := parity.exhaustive at n
  cases sign with positive | negative
  . rw positive
    cases split with even | odd
    . left
      exact IntegerEven.ofNat with even
    . right
      exact IntegerOdd.ofNat with odd
  . rw negative
    cases split with even | odd
    . left
      exact IntegerEven.negative_ofNat with even
    . right
      exact IntegerOdd.negative_ofNat with odd

theorem IntegerEven.iff_not_odd (z : Integer)
  shows IntegerEven(z) ↔ ¬IntegerOdd(z)
proof
  constructor
  . intro even
    exact IntegerEven.not_odd with even
  . intro notOdd
    have split := IntegerParity.exhaustive at z
    cases split with even | odd
    . exact even
    . exfalso
      exact notOdd with odd

theorem IntegerOdd.iff_not_even (z : Integer)
  shows IntegerOdd(z) ↔ ¬IntegerEven(z)
proof
  constructor
  . intro odd
    exact IntegerOdd.not_even with odd
  . intro notEven
    have split := IntegerParity.exhaustive at z
    cases split with even | odd
    . exfalso
      exact notEven with even
    . exact odd

theorem IntegerEven.ofNat_iff (n : Nat)
  shows IntegerEven(integerOfNat(n)) ↔ Even(n)
proof
  constructor
  . intro even
    have split := parity.exhaustive at n
    cases split with natEven | natOdd
    . exact natEven
    . have odd := IntegerOdd.ofNat with natOdd
      exfalso
      exact IntegerOdd.not_even with odd, even
  . intro even
    exact IntegerEven.ofNat with even

theorem IntegerOdd.ofNat_iff (n : Nat)
  shows IntegerOdd(integerOfNat(n)) ↔ Odd(n)
proof
  constructor
  . intro odd
    have split := parity.exhaustive at n
    cases split with natEven | natOdd
    . have even := IntegerEven.ofNat with natEven
      exfalso
      exact IntegerEven.not_odd with even, odd
    . exact natOdd
  . intro odd
    exact IntegerOdd.ofNat with odd

theorem IntegerEven.add_one_iff (z : Integer)
  shows IntegerEven(z + 1) ↔ IntegerOdd(z)
proof
  constructor
  . intro even
    have split := IntegerParity.exhaustive at z
    cases split with zEven | zOdd
    . have one := IntegerOdd.one
      have odd := IntegerOdd.even_add with zEven, one
      exfalso
      exact IntegerOdd.not_even with odd, even
    . exact zOdd
  . intro odd
    have one := IntegerOdd.one
    exact IntegerEven.add_odd_odd with odd, one

theorem IntegerOdd.add_one_iff (z : Integer)
  shows IntegerOdd(z + 1) ↔ IntegerEven(z)
proof
  constructor
  . intro odd
    have split := IntegerParity.exhaustive at z
    cases split with zEven | zOdd
    . exact zEven
    . have one := IntegerOdd.one
      have even := IntegerEven.add_odd_odd with zOdd, one
      exfalso
      exact IntegerEven.not_odd with even, odd
  . intro even
    have one := IntegerOdd.one
    exact IntegerOdd.even_add with even, one

theorem IntegerEven.mul_self_iff (z : Integer)
  shows IntegerEven(z * z) ↔ IntegerEven(z)
proof
  constructor
  . intro even
    have split := IntegerParity.exhaustive at z
    cases split with zEven | zOdd
    . exact zEven
    . have odd := IntegerOdd.mul with zOdd, zOdd
      exfalso
      exact IntegerOdd.not_even with odd, even
  . intro even
    exact IntegerEven.mul_left with even

theorem IntegerEven.neg_iff (z : Integer)
  shows IntegerEven(-z) ↔ IntegerEven(z)
proof
  constructor
  . intro even
    have negated := IntegerEven.neg with even
    have restore : -(-z) = z by ring
    rw restore at negated
    exact negated
  . intro even
    exact IntegerEven.neg with even