COUNTING: Count words of order n in the free magma (Lemma 1.3) (teor…

…th#146) * Copy `Combinatorics.Enumerative.Catalan` for counting words in the free magma * Update blueprint
b-mehta · Sep 30, 2024 · 8f7a77f · 8f7a77f
1 parent 20bc7ca
commit 8f7a77f
Show file tree

Hide file tree

Showing 4 changed files with 92 additions and 5 deletions.
diff --git a/blueprint/src/chapter/intro.tex b/blueprint/src/chapter/intro.tex
@@ -27,10 +27,10 @@ \chapter{Basic theory of magmas}
   \item etc.
 \end{itemize}
 
-\begin{lemma}  For a finite alphabet $X$, the number of words of order $n$ is $C_n |X|^{n+1}$, where $C_n$ is the $n^{\mathrm{th}}$ Catalan number and $X$ is the cardinality of $X$.
+\begin{lemma} \leanok \lean{FreeMagma.elementsOfNumNodesEq_card_eq_catalan_mul_pow} For a finite alphabet $X$, the number of words of order $n$ is $C_n |X|^{n+1}$, where $C_n$ is the $n^{\mathrm{th}}$ Catalan number and $X$ is the cardinality of $X$.
 \end{lemma}
 
-\begin{proof} Follows from standard properties of Catalan numbers.
+\begin{proof} \leanok Follows from standard properties of Catalan numbers.
 \end{proof}
 
 The first few Catalan numbers are
@@ -108,7 +108,7 @@ \chapter{Basic theory of magmas}
 
 The sequence $D_n$ is
 $$ 1, 1, 2, 4, 11, 32, 117, \dots$$
-(\href{https://oeis.org/A103293}{OEIS A103293}), and the sequence in Lemma \ref{law-count-sym} is 
+(\href{https://oeis.org/A103293}{OEIS A103293}), and the sequence in Lemma \ref{law-count-sym} is
 $$ 2, 5, 41, 364, 4294, 57882, 888440, \dots$$
 
 We can also identify all laws of the form $w \formaleq w$ with the trivial law $0 \formaleq 0$.  The number of such laws of total order $n$ is zero if $n$ is odd, and $C_{n/2} B_{n/2+1}$ if $n$ is even.  We conclude:

diff --git a/equational_theories.lean b/equational_theories.lean
@@ -3,4 +3,5 @@ import equational_theories.Subgraph
 import equational_theories.AllEquations
 import equational_theories.InfModel
 import equational_theories.Generated
+import equational_theories.Counting
 import equational_theories.SmallMagmas
diff --git a/equational_theories/Counting.lean b/equational_theories/Counting.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2022 Julian Kuelshammer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+import equational_theories.FreeMagma
+import Mathlib.Combinatorics.Enumerative.Catalan
+
+variable {X : Type*}
+
+namespace FreeMagma
+
+def order : FreeMagma X → ℕ
+  | Lf _ => 0
+  | a ⋆ b => order a + order b + 1
+
+@[simp]
+lemma order_leaf (a : X) : (Lf a).order = 0 := rfl
+
+@[simp]
+lemma order_fork (a b : FreeMagma X) : (a ⋆ b).order = a.order + b.order + 1 := rfl
+
+-- Compare to `Tree.pairwiseNode`
+abbrev pairwiseFork (a b : Finset (FreeMagma X)) : Finset (FreeMagma X) :=
+  (a ×ˢ b).map ⟨fun ⟨x, y⟩ ↦ x ⋆ y, fun ⟨a, b⟩ ⟨c, d⟩ ↦ by simp⟩
+
+variable (X) [Fintype X] [DecidableEq X]
+
+-- Compare to `Tree.treesOfNumNodesEq`
+def elementsOfNumNodesEq : ℕ → Finset (FreeMagma X)
+  | 0 => Finset.univ.map ⟨Lf, fun a b h ↦ by simpa using h⟩
+  | n + 1 =>
+    (Finset.antidiagonal n).attach.biUnion fun ijh =>
+      pairwiseFork (elementsOfNumNodesEq ijh.1.1) (elementsOfNumNodesEq ijh.1.2)
+  -- Porting note: Add this to satisfy the linter.
+  decreasing_by
+    · simp_wf; have := Finset.antidiagonal.fst_le ijh.2; omega
+    · simp_wf; have := Finset.antidiagonal.snd_le ijh.2; omega
+
+-- Compare to `Tree.treesOfNumNodesEq_zero`
+@[simp]
+theorem elementsOfNumNodesEq_zero : elementsOfNumNodesEq X 0 =
+    Finset.univ.map ⟨Lf, fun a b h ↦ by simpa using h⟩ := by rw [elementsOfNumNodesEq]
+
+-- Compare to `Tree.treesOfNumNodesEq_succ`
+theorem elementsOfNumNodesEq_succ {n : ℕ} : elementsOfNumNodesEq X (n + 1) =
+    (Finset.antidiagonal n).biUnion fun ijh => pairwiseFork (elementsOfNumNodesEq X ijh.1)
+      (elementsOfNumNodesEq X ijh.2) := by
+  rw [elementsOfNumNodesEq]
+  ext
+  simp
+
+-- Compare to `Tree.mem_treesOfNumNodesEq`
+@[simp]
+theorem mem_elementsOfNumNodesEq {x : FreeMagma X} {n : ℕ} :
+    x ∈ elementsOfNumNodesEq X n ↔ order x = n := by
+  induction x generalizing n <;> cases n
+  · simp
+  · simp [elementsOfNumNodesEq_succ]
+  · simp
+  · simp [elementsOfNumNodesEq_succ, *]
+
+-- Compare to `Tree.treesOfNumNodesEq_card_eq_catalan`
+theorem elementsOfNumNodesEq_card_eq_catalan_mul_pow (n : ℕ) :
+    (elementsOfNumNodesEq X n).card = catalan n * (Fintype.card X) ^ (n + 1) := by
+  induction' n using Nat.case_strong_induction_on with n ih
+  · simp
+  rw [elementsOfNumNodesEq_succ, Finset.card_biUnion, catalan_succ', Finset.sum_mul]
+  · apply Finset.sum_congr rfl
+    rintro ⟨i, j⟩ h
+    rw [Finset.card_map, Finset.card_product, ih _ (Finset.antidiagonal.fst_le h),
+      ih _ (Finset.antidiagonal.snd_le h)]
+    rw [← Finset.mem_antidiagonal.1 h]
+    ring
+  · simp_rw [Finset.disjoint_left]
+    rintro ⟨i, j⟩ _ ⟨i', j'⟩ _
+    intros h a
+    cases' a with a l r
+    · intro h; simp at h
+    · intro h1 h2
+      apply h
+      trans (order l, order r)
+      · simp at h1; simp [h1]
+      · simp at h2; simp [h2]
+
+
+end FreeMagma
diff --git a/equational_theories/FreeMagma.lean b/equational_theories/FreeMagma.lean
@@ -7,6 +7,7 @@ universe v
 inductive FreeMagma (α : Type u)
   | Leaf : α → FreeMagma α
   | Fork : FreeMagma α → FreeMagma α → FreeMagma α
+  deriving DecidableEq
 
 instance (α : Type u) : Magma (FreeMagma α) where
   op := FreeMagma.Fork
@@ -16,8 +17,7 @@ infixl:65 " ⋆ " => FreeMagma.Fork
 @[simp]
 theorem FreeMagma_op_eq_fork (α : Type u) (a b : FreeMagma α) : a ∘ b = a ⋆ b := rfl
 
-@[match_pattern]
-def Lf {α : Type u} : (α → FreeMagma α) := FreeMagma.Leaf
+notation "Lf" => FreeMagma.Leaf
 
 def fmapFreeMagma {α : Type u} {β : Type v} (f : α → β) : FreeMagma α → FreeMagma β
   | Lf a => FreeMagma.Leaf (f a)