Grace/Cumulus/Cardinal/Parity.g17

Open in Workbench Download source

Imports

NaturalSum · Pigeonhole · Nat.ParityLemmas

Declarations

Source

1-- Finite sets as a parity algebra: symmetric difference is the sum, and a set2-- is read as a vector over the two-element field.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Cardinal.Parity9import NaturalSum10import Pigeonhole11import Nat.ParityLemmas1213-- Symmetric difference and its notation △ come from Set.Algebra; the parity14-- law Even(a + b) ↔ (Even(a) ↔ Even(b)) is Even.add_iff of ParityLemmas.1516-- Parity of a finite set: the sum over the two-element field of its indicator.17predicate EvenSet (A : Set) := Even(cardinality(A))1819theorem EvenSet.empty20  shows EvenSet(∅)21proof22  unfold EvenSet23  rw cardinality.empty24  exact Even.zero2526-- |A △ B| ≡ |A| + |B| (mod 2): each of A △ B, A, B is the disjoint union27-- of two of the three sets A ∖ B, B ∖ A, and A ∩ B.28theorem EvenSet.symmetricDifference (A B : Set)29  requires first : Finite(A)30  requires second : Finite(B)31  shows EvenSet(A △ B) ↔ (EvenSet(A) ↔ EvenSet(B))32proof33  have finiteAB : Finite(A ∖ B) := Finite.difference with first34  have finiteBA : Finite(B ∖ A) := Finite.difference with second35  have finiteMeet : Finite(A ∩ B) :=36    Finite.subset with first, intersection.subset_left37  have sumSym :38      cardinality(A △ B) = cardinality(A ∖ B) + cardinality(B ∖ A)39    have apart : Disjoint(A ∖ B, B ∖ A) :=40      Disjoint.of_subset_right with (Disjoint.difference_left at A, B),41        difference.subset_left42    unfold symmetricDifference43    exact cardinality.union_disjoint with finiteAB, finiteBA, apart44  have sumA : cardinality(A) = cardinality(A ∖ B) + cardinality(A ∩ B)45    have apart : Disjoint(A ∖ B, A ∩ B) :=46      Disjoint.of_subset_right with (Disjoint.difference_left at A, B),47        intersection.subset_right48    have union := cardinality.union_disjoint with finiteAB, finiteMeet, apart49    rwa difference.union2_intersection at union50  have sumB : cardinality(B) = cardinality(B ∖ A) + cardinality(A ∩ B)51    have apart : Disjoint(B ∖ A, A ∩ B) :=52      Disjoint.of_subset_right with (Disjoint.difference_left at B, A),53        intersection.subset_left54    have union := cardinality.union_disjoint with finiteBA, finiteMeet, apart55    rw [intersection.commutative, difference.union2_intersection] at union56    rwa intersection.commutative57  unfold EvenSet58  rw [sumSym, sumA, sumB]59  simp [Even.add_iff]6061theorem EvenSet.union_disjoint (A B : Set)62  requires first : Finite(A)63  requires second : Finite(B)64  requires apart : Disjoint(A, B)65  shows EvenSet(A ∪ B) ↔ (EvenSet(A) ↔ EvenSet(B))66proof67  unfold EvenSet68  rw cardinality.union_disjoint with first, second, apart69  exact Even.add_iff7071-- The parity of an intersection is the dot product of the two indicators.72def dot (A B : Set) : Set := cardinality(A ∩ B)7374theorem dot.commutative (A B : Set)75  shows dot(A, B) = dot(B, A)76proof77  unfold dot78  rw intersection.commutative7980-- Bilinearity of the dot product modulo two: intersection with C distributes81-- over △, so this is the parity law for A ∩ C and B ∩ C.82theorem dot.symmetricDifference (A B C : Set)83  requires first : Finite(A)84  requires second : Finite(B)85  requires third : Finite(C)86  shows Even(dot(A △ B, C)) ↔ (Even(dot(A, C)) ↔ Even(dot(B, C)))87proof88  have finiteAC : Finite(A ∩ C) :=89    Finite.subset with first, intersection.subset_left90  have finiteBC : Finite(B ∩ C) :=91    Finite.subset with second, intersection.subset_left92  unfold dot93  rw symmetricDifference.intersection_distrib_right94  exact EvenSet.symmetricDifference with finiteAC, finiteBC95