Computation of the number of distinct colorings

Evaluating the number of distinct colorings with the #eval command is generally slow. Here, we define a function computeNumDistinctColorings for fast computation of the number of distinct colorings, along with a proof of its correctness: computeNumDistinctColorings_eq_numDistinctColorings.

We prove some auxiliary results about arrays.

We define a function visitCycle that takes a permutation f : Fin n → Fin n, an element x : Fin n, and an array of length n. It returns an identical array except that it is set to true at all indices belonging to the same cycle of the permutation f as x. It first stores x as the final element, then repeatedly sets the array at index x to true and updates x := f x until x equals final.

We define a function computeNumCyclesOfPerm that takes a permutation f : Fin n → Fin n and computes its number of cycles. It first creates a boolean array of size n initialized to false, then iterates through values n - 1, n - 2, ..., 0. For each value, it checks if the array is already set to true at its index. If so, it proceeds to the next value. Otherwise, it increments the number of cycles, sets the array to true at all indices in the same cycle as the current value using visitCycle, and proceeds to the next value.

We define a function computeNumDistinctColorings for fast computation of the number of distinct colorings. It requires a bijection X → Fin n to reduce the problem of computing the number of distinct colorings of X with colors in Y under the group action of G on X to the problem of computing the number of distinct colorings of Fin n with colors in Y under the induced group action of G on Fin n. It uses computeNumCyclesOfPerm to compute the number of cycles of elements in the group. The proof computeNumDistinctColorings_eq_numDistinctColorings establishes its correctness using Pólya’s enumeration theorem.

@[simp]

theorem ArrayAuxiliary.setD_getElem!_eq {X : Type u} [Inhabited X] {array : Array X} (i : Fin array.size) (v : X) : (array.setD (↑i) v)[↑i]! = v

Setting an array at index i to a value v and then retrieving the value at index i results in v.

theorem ArrayAuxiliary.setD_getElem!_eq_of_getElem!_eq {X : Type u} [Inhabited X] {array : Array X} (i : Fin array.size) {j : Fin array.size} {v : X} (h : array[↑j]! = v) : (array.setD (↑i) v)[↑j]! = v

If an array has value v at index i, then after setting the value at some index to v, the value at index i remains v.

theorem ArrayAuxiliary.setD_getElem!_eq_of_not_SameCycle {X : Type u} [Inhabited X] {array : Array X} {i j : Fin array.size} (v : X) {f : Equiv.Perm (Fin array.size)} (h : ¬f.SameCycle i j) : (array.setD (↑i) v)[↑j]! = array[↑j]!

If i and j are not in the same cycle of a permutation, then they are distinct, and setting the value at index i does not affect the value at index j.

@[irreducible]

def ComputationNumberOfCycles.visitCycleAux {n : ℕ} {f : Equiv.Perm (Fin n)} {final x : Fin n} (visited : Array Bool) (htermination : ∃ (m : ℕ), (f ^ (m + 1)) x = final) : Array Bool

Auxiliary function for visitCycle. It sets the array visited to true at indices {x, f x, f² x, ..., f⁻¹ final}. To ensure termination, it requires a proof that iterating f on x eventually results in final. The proof visitCycleAux_spec establishes the correctness of this function.

Equations

• ComputationNumberOfCycles.visitCycleAux visited htermination = if h : f x = final then visited.set! (↑x) true else ComputationNumberOfCycles.visitCycleAux (visited.set! (↑x) true) ⋯

theorem ComputationNumberOfCycles.visitCycleAux_get!_true_of_get!_true {visited : Array Bool} {f : Equiv.Perm (Fin visited.size)} {final x y : Fin visited.size} (hf : ∃ (m : ℕ), (f ^ (m + 1)) x = final) (hy : visited.get! ↑y = true) : (ComputationNumberOfCycles.visitCycleAux visited hf).get! ↑y = true

visitCycleAux visited _ returns an array that is true at all indices where visited is true.

theorem ComputationNumberOfCycles.visitCycleAux_spec {i : ℕ} {visited : Array Bool} {f : Equiv.Perm (Fin visited.size)} {final x : Fin visited.size} (hi : (f ^ (i + 1)) x = final) (hi' : ∀ l < i, (f ^ (l + 1)) x ≠ final) : (∀ l < i + 1, (ComputationNumberOfCycles.visitCycleAux visited ⋯).get! ↑((f ^ l) x) = true) ∧ (∀ (y : Fin visited.size), ¬f.SameCycle final y → (ComputationNumberOfCycles.visitCycleAux visited ⋯).get! ↑y = visited.get! ↑y) ∧ (ComputationNumberOfCycles.visitCycleAux visited ⋯).size = visited.size

visitCycleAux visited _ returns an array identical to visited at all indices not in the same cycle as x, and set to true at all indices in {x, f x, f² x, ..., fⁱ x} = {x, f x, f² x, ..., f⁻¹ final}. It has the same size as visited.

def ComputationNumberOfCycles.visitCycle {n : ℕ} (f : Equiv.Perm (Fin n)) (x : Fin n) (visited : Array Bool) : Array Bool

A function that sets the array visited to true at indices in the same cycle of permutation f as x. The proof visitCycle_spec establishes its correctness.

Equations

• ComputationNumberOfCycles.visitCycle f x visited = ComputationNumberOfCycles.visitCycleAux visited ⋯

theorem ComputationNumberOfCycles.visitCycle_spec {visited : Array Bool} (f : Equiv.Perm (Fin visited.size)) (x : Fin visited.size) : (∀ (y : Fin visited.size), f.SameCycle x y → (ComputationNumberOfCycles.visitCycle f x visited).get! ↑y = true) ∧ (∀ (y : Fin visited.size), ¬f.SameCycle x y → (ComputationNumberOfCycles.visitCycle f x visited).get! ↑y = visited.get! ↑y) ∧ (ComputationNumberOfCycles.visitCycle f x visited).size = visited.size

visitCycle f x visited returns an array identical to visited, except that it is set to true at all indices that belong to the same cycle of the permutation f as x.

def ComputationNumberOfCycles.computeNumCyclesOfPermAux {n i : ℕ} (f : Equiv.Perm (Fin n)) (visited : Array Bool) (count : ℕ) (hi : i ≤ n) : ℕ

Auxiliary function for computeNumCyclesOfPerm. Returns count incremented by the number of cycles of f that contain a value in {m ∈ {0, ..., i - 1} | visited[m] = false}. The proof computeNumCyclesOfPermAux_exists_representatives establishes its correctness.

Equations

• One or more equations did not get rendered due to their size.
• ComputationNumberOfCycles.computeNumCyclesOfPermAux f visited count hi_2 = count

theorem ComputationNumberOfCycles.computeNumCyclesOfPermAux_exists_representatives {i : ℕ} {visited : Array Bool} {f : Equiv.Perm (Fin visited.size)} (count : ℕ) (hi : i ≤ visited.size) (h1 : ∀ (x : Fin visited.size), ↑x ≥ i → ∀ (y : Fin visited.size), f.SameCycle x y → visited.get! ↑y = true) (h2 : ∀ (x : Fin visited.size), visited.get! ↑x = true → ∃ (y : Fin visited.size), ↑y ≥ i ∧ f.SameCycle x y) (h3 : ∃ (s : Finset (Fin visited.size)), (∀ x ∈ s, ↑x ≥ i) ∧ (∀ x ∈ s, ∀ y ∈ s, f.SameCycle x y → x = y) ∧ (∀ (x : Fin visited.size), ↑x ≥ i → ∃ y ∈ s, f.SameCycle x y) ∧ count = s.card) : ∃ (s : Finset (Fin visited.size)), (∀ x ∈ s, ∀ y ∈ s, f.SameCycle x y → x = y) ∧ (∀ (x : Fin visited.size), ∃ y ∈ s, f.SameCycle x y) ∧ ComputationNumberOfCycles.computeNumCyclesOfPermAux f visited count hi = s.card

computeNumCyclesOfPermAux takes a permutation f, an array visited that is set to true at indices in the same cycle of f as some element in {i, ..., n - 1}, and a number count representing the cardinality of some set of representatives of those cycles of f containing some element in {i, ..., n - 1}. It computes the cardinality of some set of representatives of cycles of f.

def ComputationNumberOfCycles.computeNumCyclesOfPerm {n : ℕ} (f : Equiv.Perm (Fin n)) : ℕ

Computes the number of cycles of a permutation f : Fin n → Fin n. The proof computeNumCyclesOfPerm_eq_numCyclesOfPerm establishes its correctness.

Equations

• ComputationNumberOfCycles.computeNumCyclesOfPerm f = ComputationNumberOfCycles.computeNumCyclesOfPermAux f (mkArray n false) 0 ⋯

theorem ComputationNumberOfCycles.computeNumCyclesOfPerm_exists_representatives {n : ℕ} (f : Equiv.Perm (Fin n)) : ∃ (s : Finset (Fin n)), (∀ x ∈ s, ∀ y ∈ s, f.SameCycle x y → x = y) ∧ (∀ (x : Fin n), ∃ y ∈ s, f.SameCycle x y) ∧ ComputationNumberOfCycles.computeNumCyclesOfPerm f = s.card

computeNumCyclesOfPerm f computes the cardinality of some set of representatives of cycles of f, which is a set containing exactly one element from each cycle of f.

theorem ComputationNumberOfCycles.computeNumCyclesOfPerm_eq_numCyclesOfPerm {n : ℕ} (f : Equiv.Perm (Fin n)) : ComputationNumberOfCycles.computeNumCyclesOfPerm f = CyclesOfPermutation.numCyclesOfPerm f

computeNumCyclesOfPerm f computes the number of cycles of the permutation f.

def ComputationNumberOfDistinctColorings.computeNumDistinctColorings (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype Y] [Fintype G] [enum : FinEnum X] : ℕ

Computes the number of distinct colorings of X with colors in Y under the group action of G on X. The proof computeNumDistinctColorings_eq_numDistinctColorings establishes its correctness.

Equations

• ComputationNumberOfDistinctColorings.computeNumDistinctColorings X Y G = (∑ g : G, Fintype.card Y ^ ComputationNumberOfCycles.computeNumCyclesOfPerm (MulAction.toPerm g)) / Fintype.card G

@[simp]

theorem ComputationNumberOfDistinctColorings.computeNumDistinctColorings_eq_numDistinctColorings (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype Y] [Fintype G] [enum : FinEnum X] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] [(g : G) → Fintype ↑(MulAction.fixedBy (Fin (FinEnum.card X) → Y) g)] : ComputationNumberOfDistinctColorings.computeNumDistinctColorings X Y G = DistinctColorings.numDistinctColorings X Y G

computeNumDistinctColorings X Y G computes the number of distinct colorings of X with colors in Y under the group action of G on X.