-- Parity of a sum of weights at most two: it is the parity of the number
-- of points of weight one
-- 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.Cardinal.SumParity
import NaturalSum
import Nat.Parity

def ones (V w : Set) : Set := { v ∈ V | w(v) = 1 }

theorem ones.subset (V w : Set)
  shows ones(V, w) ⊆ V
proof
  intros v hv
  have parts := ones.membership.forward with hv
  exact parts.left

theorem ones.insert_other (V w a : Set)
  requires other : w(a) ≠ 1
  shows ones(insert(a, V), w) = ones(V, w)
proof
  ext v
  constructor
  . intro hv
    have parts := ones.membership.forward with hv
    have split := insert.membership.forward with parts.left
    cases split with same | inV
    . exfalso
      rw same at parts
      exact other with parts.right
    . exact ones.membership.backward with ⟨inV, parts.right⟩
  . intro hv
    have parts := ones.membership.forward with hv
    have inserted : v ∈ insert(a, V)
      apply insert.membership.backward
      right
      exact parts.left
    exact ones.membership.backward with ⟨inserted, parts.right⟩

theorem ones.insert_one (V w a : Set)
  requires one : w(a) = 1
  shows ones(insert(a, V), w) = insert(a, ones(V, w))
proof
  ext v
  constructor
  . intro hv
    have parts := ones.membership.forward with hv
    have split := insert.membership.forward with parts.left
    apply insert.membership.backward
    cases split with same | inV
    . left
      exact same
    . right
      exact ones.membership.backward with ⟨inV, parts.right⟩
  . intro hv
    have split := insert.membership.forward with hv
    cases split with same | inOnes
    . rw same
      apply ones.membership.backward
      have inserted : a ∈ insert(a, V)
        apply insert.membership.backward
        left
        rfl
      exact ⟨inserted, one⟩
    . have parts := ones.membership.forward with inOnes
      have inserted : v ∈ insert(a, V)
        apply insert.membership.backward
        right
        exact parts.left
      exact ones.membership.backward with ⟨inserted, parts.right⟩

theorem Even.two
  shows Even(2)
proof
  have double := Even.double at 1
  have same : add(1, 1) = 2 by compute
  rwa same at double

theorem Even.add_two_iff (s : Nat)
  shows Even(s + 2) ↔ Even(s)
proof
  constructor
  . intro even
    have split := parity.exhaustive at s
    cases split with evenS | oddS
    . exact evenS
    . exfalso
      have odd := Odd.add_even with oddS, Even.two
      exact Odd.not_even with odd, even
  . intro even
    exact Even.add with even, Even.two

theorem Even.add_one_iff (s : Nat)
  shows Even(s + 1) ↔ Odd(s)
proof
  rw add.right_one
  exact Even.succ_iff

-- The sum of weights in {0, 1, 2} has the parity of the number of ones.
theorem natSum.parity_of_size (V w : Set, n : Nat)
  requires finite : Finite(V)
  requires size : cardinality(V) = n
  requires weights : ∀ v ∈ V, w(v) = 0 ∨ w(v) = 1 ∨ w(v) = 2
  shows Even(natSum(V, w)) ↔ Even(cardinality(ones(V, w)))
proof
  induction n generalizing V
  | zero =>
    intros V finite size weights
    have has := cardinality.correct with finite
    rw size at has
    have empty := HasCardinality.empty_of_zero at V with has
    have onesEmpty : ones(∅, w) = ∅
      apply Subset.antisymmetric
      . exact ones.subset at ∅, w
      . exact empty.subset at ones(∅, w)
    rw [empty, natSum.empty, onesEmpty]
    rw ← nat.zero
    rw cardinality.natural
    constructor
    . intro h
      exact h
    . intro h
      exact h
  | succ(k) using ih =>
    intros V finite size weights
    have has := cardinality.correct with finite
    rw size at has
    obtain ⟨a, ha⟩ := HasCardinality.exists_member with has
    have removed := cardinality.remove with finite, ha
    rw size at removed
    have smaller := Naturals.injective.succ with removed
    have restSize : cardinality(V ∖ {a}) = k
      symm
      exact smaller
    have restFinite := Finite.subset with finite, (difference.subset_left at V, {a})
    have restWeights : ∀ v ∈ V ∖ {a}, w(v) = 0 ∨ w(v) = 1 ∨ w(v) = 2
      intros v hv
      have parts := difference.singleton_membership.forward with hv
      exact weights with v, parts.left
    have rest := ih with V ∖ {a}, restFinite, restSize, restWeights
    have naturals : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ
      intros v hv
      have split := restWeights with v, hv
      cases split with zero | more
      . rw zero
        typecheck
      . cases more with one | two
        . rw one
          typecheck
        . rw two
          typecheck
    have fresh : ¬a ∈ V ∖ {a}
      intro inside
      have parts := difference.singleton_membership.forward with inside
      apply parts.right
      rfl
    have restore := insert.restore with ha
    have onesFinite := Finite.subset with restFinite, (ones.subset at V ∖ {a}, w)
    have onesFresh : ¬a ∈ ones(V ∖ {a}, w)
      intro inside
      exact fresh with (ones.subset at V ∖ {a}, w with a, inside)
    have split := weights with a, ha
    have sumNat := natSum.natural with restFinite, naturals
    have onesCorrect := cardinality.correct with onesFinite
    have onesNat := onesCorrect.left
    rw ← restore
    cases split with zero | more
    . have weightA : w(a) ∈ ℕ
        rw zero
        typecheck
      have inserted := natSum.insert with restFinite, naturals, weightA, fresh
      have other : w(a) ≠ 1
        rw zero
        exact zero.ne_one
      have onesSame := ones.insert_other at V ∖ {a}, w, a with other
      rw [inserted, onesSame, zero, add.right_unit]
      exact rest
    . cases more with one | two
      . have weightA : w(a) ∈ ℕ
          rw one
          typecheck
        have inserted := natSum.insert with restFinite, naturals, weightA, fresh
        have onesIns := ones.insert_one at V ∖ {a}, w, a with one
        have onesCard := cardinality.insert with onesFinite, onesFresh
        rw [inserted, onesIns, one, onesCard]
        have left := Even.add_one_iff at natSum(V ∖ {a}, w)
        have right := Even.succ_iff at cardinality(ones(V ∖ {a}, w))
        have oddSum := Odd.iff_not_even at natSum(V ∖ {a}, w)
        have oddOnes := Odd.iff_not_even at cardinality(ones(V ∖ {a}, w))
        constructor
        . intro h
          have oddS := left.forward with h
          have notEvenS := oddSum.forward with oddS
          have notEvenC : ¬Even(cardinality(ones(V ∖ {a}, w)))
            intro evenC
            exact notEvenS with (rest.backward with evenC)
          exact right.backward with (oddOnes.backward with notEvenC)
        . intro h
          have oddC := right.forward with h
          have notEvenC := oddOnes.forward with oddC
          have notEvenS : ¬Even(natSum(V ∖ {a}, w))
            intro evenS
            exact notEvenC with (rest.forward with evenS)
          exact left.backward with (oddSum.backward with notEvenS)
      . have weightA : w(a) ∈ ℕ
          rw two
          typecheck
        have inserted := natSum.insert with restFinite, naturals, weightA, fresh
        have other : w(a) ≠ 1
          rw two
          decide
        have onesSame := ones.insert_other at V ∖ {a}, w, a with other
        rw [inserted, onesSame, two]
        have shift := Even.add_two_iff at natSum(V ∖ {a}, w)
        constructor
        . intro h
          exact rest.forward with (shift.forward with h)
        . intro h
          exact shift.backward with (rest.backward with h)


-- The same for a finite set, with no size parameter.
theorem natSum.parity (V w : Set)
  requires finite : Finite(V)
  requires weights : ∀ v ∈ V, w(v) = 0 ∨ w(v) = 1 ∨ w(v) = 2
  shows Even(natSum(V, w)) ↔ Even(cardinality(ones(V, w)))
proof
  have correct := cardinality.correct with finite
  have natural := correct.left
  have size : cardinality(V) = cardinality(V) by rfl
  exact natSum.parity_of_size at V, w, cardinality(V)
    with natural, finite, size, weights