-- Finite sets as a parity algebra: symmetric difference is the sum, and a set
-- is read as a vector over the two-element field.
-- 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.Parity
import NaturalSum
import Pigeonhole
import Nat.ParityLemmas

-- Symmetric difference and its notation △ come from Set.Algebra; the parity
-- law Even(a + b) ↔ (Even(a) ↔ Even(b)) is Even.add_iff of ParityLemmas.

-- Parity of a finite set: the sum over the two-element field of its indicator.
predicate EvenSet (A : Set) := Even(cardinality(A))

theorem EvenSet.empty
  shows EvenSet(∅)
proof
  unfold EvenSet
  rw cardinality.empty
  exact Even.zero

-- |A △ B| ≡ |A| + |B| (mod 2): each of A △ B, A, B is the disjoint union
-- of two of the three sets A ∖ B, B ∖ A, and A ∩ B.
theorem EvenSet.symmetricDifference (A B : Set)
  requires first : Finite(A)
  requires second : Finite(B)
  shows EvenSet(A △ B) ↔ (EvenSet(A) ↔ EvenSet(B))
proof
  have finiteAB : Finite(A ∖ B) := Finite.difference with first
  have finiteBA : Finite(B ∖ A) := Finite.difference with second
  have finiteMeet : Finite(A ∩ B) :=
    Finite.subset with first, intersection.subset_left
  have sumSym :
      cardinality(A △ B) = cardinality(A ∖ B) + cardinality(B ∖ A)
    have apart : Disjoint(A ∖ B, B ∖ A) :=
      Disjoint.of_subset_right with (Disjoint.difference_left at A, B),
        difference.subset_left
    unfold symmetricDifference
    exact cardinality.union_disjoint with finiteAB, finiteBA, apart
  have sumA : cardinality(A) = cardinality(A ∖ B) + cardinality(A ∩ B)
    have apart : Disjoint(A ∖ B, A ∩ B) :=
      Disjoint.of_subset_right with (Disjoint.difference_left at A, B),
        intersection.subset_right
    have union := cardinality.union_disjoint with finiteAB, finiteMeet, apart
    rwa difference.union2_intersection at union
  have sumB : cardinality(B) = cardinality(B ∖ A) + cardinality(A ∩ B)
    have apart : Disjoint(B ∖ A, A ∩ B) :=
      Disjoint.of_subset_right with (Disjoint.difference_left at B, A),
        intersection.subset_left
    have union := cardinality.union_disjoint with finiteBA, finiteMeet, apart
    rw [intersection.commutative, difference.union2_intersection] at union
    rwa intersection.commutative
  unfold EvenSet
  rw [sumSym, sumA, sumB]
  simp [Even.add_iff]

theorem EvenSet.union_disjoint (A B : Set)
  requires first : Finite(A)
  requires second : Finite(B)
  requires apart : Disjoint(A, B)
  shows EvenSet(A ∪ B) ↔ (EvenSet(A) ↔ EvenSet(B))
proof
  unfold EvenSet
  rw cardinality.union_disjoint with first, second, apart
  exact Even.add_iff

-- The parity of an intersection is the dot product of the two indicators.
def dot (A B : Set) : Set := cardinality(A ∩ B)

theorem dot.commutative (A B : Set)
  shows dot(A, B) = dot(B, A)
proof
  unfold dot
  rw intersection.commutative

-- Bilinearity of the dot product modulo two: intersection with C distributes
-- over △, so this is the parity law for A ∩ C and B ∩ C.
theorem dot.symmetricDifference (A B C : Set)
  requires first : Finite(A)
  requires second : Finite(B)
  requires third : Finite(C)
  shows Even(dot(A △ B, C)) ↔ (Even(dot(A, C)) ↔ Even(dot(B, C)))
proof
  have finiteAC : Finite(A ∩ C) :=
    Finite.subset with first, intersection.subset_left
  have finiteBC : Finite(B ∩ C) :=
    Finite.subset with second, intersection.subset_left
  unfold dot
  rw symmetricDifference.intersection_distrib_right
  exact EvenSet.symmetricDifference with finiteAC, finiteBC