Dyck words

A Dyck word is a sequence consisting of an equal number n of symbols of two types such that for all prefixes one symbol occurs at least as many times as the other. If the symbols are ( and ) the latter restriction is equivalent to balanced brackets; if they are U = (1, 1) and D = (1, -1) the sequence is a lattice path from (0, 0) to (0, 2n) and the restriction requires the path to never go below the x-axis.

This file defines Dyck words and constructs their bijection with rooted binary trees, one consequence being that the number of Dyck words with length 2 * n is catalan n.

Main definitions

• DyckWord: a list of Us and Ds with as many Us as Ds and with every prefix having at least as many Us as Ds.
• DyckWord.semilength: semilength (half the length) of a Dyck word.
• DyckWord.firstReturn: for a nonempty word, the index of the D matching the initial U.

Main results

• DyckWord.equivTree: equivalence between Dyck words and rooted binary trees. See the docstrings of DyckWord.equivTreeToFun and DyckWord.equivTreeInvFun for details.
• DyckWord.equivTreesOfNumNodesEq: equivalence between Dyck words of length 2 * n and rooted binary trees with n internal nodes.
• DyckWord.card_dyckWord_semilength_eq_catalan: there are catalan n Dyck words of length 2 * n or semilength n.

Implementation notes

While any two-valued type could have been used for DyckStep, a new enumerated type is used here to emphasise that the definition of a Dyck word does not depend on that underlying type.

inductive DyckStep : Type

A DyckStep is either U or D, corresponding to ( and ) respectively.

• U: DyckStep
• D: DyckStep

instance instInhabitedDyckStep : Inhabited DyckStep

Equations

• instInhabitedDyckStep = { default := DyckStep.U }

instance instDecidableEqDyckStep : DecidableEq DyckStep

Equations

• instDecidableEqDyckStep x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

theorem DyckStep.dichotomy (s : DyckStep) : s = DyckStep.U ∨ s = DyckStep.D

Named in analogy to Bool.dichotomy.

theorem DyckWord.ext {x : DyckWord} {y : DyckWord} (toList : ↑x = ↑y) : x = y

theorem DyckWord.ext_iff {x : DyckWord} {y : DyckWord} : x = y ↔ ↑x = ↑y

structure DyckWord : Type

A Dyck word is a list of DyckSteps with as many Us as Ds and with every prefix having at least as many Us as Ds.

• toList : List DyckStep

  The underlying list

• count_U_eq_count_D : List.count DyckStep.U ↑self = List.count DyckStep.D ↑self

  There are as many Us as Ds

• count_D_le_count_U : ∀ (i : ℕ), List.count DyckStep.D (List.take i ↑self) ≤ List.count DyckStep.U (List.take i ↑self)

  Each prefix has as least as many Us as Ds

theorem DyckWord.count_U_eq_count_D (self : DyckWord) : List.count DyckStep.U ↑self = List.count DyckStep.D ↑self

There are as many Us as Ds

theorem DyckWord.count_D_le_count_U (self : DyckWord) (i : ℕ) : List.count DyckStep.D (List.take i ↑self) ≤ List.count DyckStep.U (List.take i ↑self)

Each prefix has as least as many Us as Ds

instance instDecidableEqDyckWord : DecidableEq DyckWord

Equations

• instDecidableEqDyckWord = decEqDyckWord✝

instance instCoeDyckWordListDyckStep : Coe DyckWord (List DyckStep)

Equations

• instCoeDyckWordListDyckStep = { coe := DyckWord.toList }

instance instAddDyckWord : Add DyckWord

Equations

• instAddDyckWord = { add := fun (p q : DyckWord) => { toList := ↑p ++ ↑q, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ } }

instance instZeroDyckWord : Zero DyckWord

Equations

• instZeroDyckWord = { zero := { toList := [], count_U_eq_count_D := instZeroDyckWord.proof_1, count_D_le_count_U := instZeroDyckWord.proof_2 } }

instance instAddCancelMonoidDyckWord : AddCancelMonoid DyckWord

Dyck words form an additive cancellative monoid under concatenation, with the empty word as 0.

Equations

• instAddCancelMonoidDyckWord = AddCancelMonoid.mk instAddCancelMonoidDyckWord.proof_7

theorem DyckWord.toList_eq_nil {p : DyckWord} : ↑p = [] ↔ p = 0

theorem DyckWord.toList_ne_nil {p : DyckWord} : ↑p ≠ [] ↔ p ≠ 0

instance DyckWord.instUniqueAddUnits : Unique (AddUnits DyckWord)

The only Dyck word that is an additive unit is the empty word.

Equations

• DyckWord.instUniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := DyckWord.instUniqueAddUnits.proof_1 }

theorem DyckWord.head_eq_U (p : DyckWord) (h : ↑p ≠ []) : (↑p).head h = DyckStep.U

The first element of a nonempty Dyck word is U.

theorem DyckWord.getLast_eq_D (p : DyckWord) (h : ↑p ≠ []) : (↑p).getLast h = DyckStep.D

The last element of a nonempty Dyck word is D.

theorem DyckWord.cons_tail_dropLast_concat {p : DyckWord} (h : p ≠ 0) : DyckStep.U :: (↑p).dropLast.tail ++ [DyckStep.D] = ↑p

def DyckWord.take (p : DyckWord) (i : ℕ) (hi : List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p)) : DyckWord

Prefix of a Dyck word as a Dyck word, given that the count of Us and Ds in it are equal.

Equations

• p.take i hi = { toList := List.take i ↑p, count_U_eq_count_D := hi, count_D_le_count_U := ⋯ }

def DyckWord.drop (p : DyckWord) (i : ℕ) (hi : List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p)) : DyckWord

Suffix of a Dyck word as a Dyck word, given that the count of Us and Ds in the prefix are equal.

Equations

• p.drop i hi = { toList := List.drop i ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }

def DyckWord.nest (p : DyckWord) : DyckWord

Nest p in one pair of brackets, i.e. x becomes (x).

Equations

• p.nest = { toList := [DyckStep.U] ++ ↑p ++ [DyckStep.D], count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }

@[simp]

theorem DyckWord.nest_ne_zero {p : DyckWord} : p.nest ≠ 0

def DyckWord.IsNested (p : DyckWord) : Prop

A property stating that p is nonempty and strictly positive in its interior, i.e. is of the form (x) with x a Dyck word.

Equations

• p.IsNested = (p ≠ 0 ∧ ∀ ⦃i : ℕ⦄, 0 < i → i < (↑p).length → List.count DyckStep.D (List.take i ↑p) < List.count DyckStep.U (List.take i ↑p))

theorem DyckWord.IsNested.nest {p : DyckWord} : p.nest.IsNested

def DyckWord.denest (p : DyckWord) (hn : p.IsNested) : DyckWord

Denest p, i.e. (x) becomes x, given that p.IsNested.

Equations

• p.denest hn = { toList := (↑p).dropLast.tail, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }

theorem DyckWord.nest_denest (p : DyckWord) (hn : p.IsNested) : (p.denest hn).nest = p

theorem DyckWord.denest_nest (p : DyckWord) : p.nest.denest ⋯ = p

def DyckWord.semilength (p : DyckWord) : ℕ

The semilength of a Dyck word is half of the number of DyckSteps in it, or equivalently its number of Us.

Equations

• p.semilength = List.count DyckStep.U ↑p

@[simp]

theorem DyckWord.semilength_zero : DyckWord.semilength 0 = 0

@[simp]

theorem DyckWord.semilength_add {p : DyckWord} {q : DyckWord} : (p + q).semilength = p.semilength + q.semilength

@[simp]

theorem DyckWord.semilength_nest {p : DyckWord} : p.nest.semilength = p.semilength + 1

theorem DyckWord.semilength_eq_count_D {p : DyckWord} : p.semilength = List.count DyckStep.D ↑p

@[simp]

theorem DyckWord.two_mul_semilength_eq_length {p : DyckWord} : 2 * p.semilength = (↑p).length

def DyckWord.firstReturn (p : DyckWord) : ℕ

p.firstReturn is 0 if p = 0 and the index of the D matching the initial U otherwise.

Equations

• p.firstReturn = List.findIdx (fun (i : ℕ) => decide (List.count DyckStep.U (List.take (i + 1) ↑p) = List.count DyckStep.D (List.take (i + 1) ↑p))) (List.range (↑p).length)

@[simp]

theorem DyckWord.firstReturn_zero : DyckWord.firstReturn 0 = 0

theorem DyckWord.firstReturn_pos {p : DyckWord} (h : p ≠ 0) : 0 < p.firstReturn

theorem DyckWord.firstReturn_lt_length {p : DyckWord} (h : p ≠ 0) : p.firstReturn < (↑p).length

theorem DyckWord.count_take_firstReturn_add_one {p : DyckWord} (h : p ≠ 0) : List.count DyckStep.U (List.take (p.firstReturn + 1) ↑p) = List.count DyckStep.D (List.take (p.firstReturn + 1) ↑p)

theorem DyckWord.count_D_lt_count_U_of_lt_firstReturn {p : DyckWord} {i : ℕ} (hi : i < p.firstReturn) : List.count DyckStep.D (List.take (i + 1) ↑p) < List.count DyckStep.U (List.take (i + 1) ↑p)

@[simp]

theorem DyckWord.firstReturn_add {p : DyckWord} {q : DyckWord} : (p + q).firstReturn = if p = 0 then q.firstReturn else p.firstReturn

@[simp]

theorem DyckWord.firstReturn_nest {p : DyckWord} : p.nest.firstReturn = (↑p).length + 1

def DyckWord.insidePart (p : DyckWord) : DyckWord

The left part of the Dyck word decomposition, inside the U, D pair that firstReturn refers to. insidePart 0 = 0.

Equations

• p.insidePart = if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯

def DyckWord.outsidePart (p : DyckWord) : DyckWord

The right part of the Dyck word decomposition, outside the U, D pair that firstReturn refers to. outsidePart 0 = 0.

Equations

• p.outsidePart = if h : p = 0 then 0 else p.drop (p.firstReturn + 1) ⋯

@[simp]

theorem DyckWord.insidePart_zero : DyckWord.insidePart 0 = 0

@[simp]

theorem DyckWord.outsidePart_zero : DyckWord.outsidePart 0 = 0

@[simp]

theorem DyckWord.insidePart_add {p : DyckWord} {q : DyckWord} (h : p ≠ 0) : (p + q).insidePart = p.insidePart

@[simp]

theorem DyckWord.outsidePart_add {p : DyckWord} {q : DyckWord} (h : p ≠ 0) : (p + q).outsidePart = p.outsidePart + q

@[simp]

theorem DyckWord.insidePart_nest {p : DyckWord} : p.nest.insidePart = p

@[simp]

theorem DyckWord.outsidePart_nest {p : DyckWord} : p.nest.outsidePart = 0

@[simp]

theorem DyckWord.nest_insidePart_add_outsidePart {p : DyckWord} (h : p ≠ 0) : p.insidePart.nest + p.outsidePart = p

theorem DyckWord.semilength_insidePart_add_semilength_outsidePart_add_one {p : DyckWord} (h : p ≠ 0) : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength

theorem DyckWord.semilength_insidePart_lt {p : DyckWord} (h : p ≠ 0) : p.insidePart.semilength < p.semilength

theorem DyckWord.semilength_outsidePart_lt {p : DyckWord} (h : p ≠ 0) : p.outsidePart.semilength < p.semilength

instance DyckWord.instPreorder : Preorder DyckWord

Equations

• DyckWord.instPreorder = Preorder.mk DyckWord.instPreorder.proof_1 DyckWord.instPreorder.proof_2 DyckWord.instPreorder.proof_3

@[irreducible]

theorem DyckWord.le_add_self (p : DyckWord) (q : DyckWord) : q ≤ p + q

theorem DyckWord.zero_le (p : DyckWord) : 0 ≤ p

theorem DyckWord.infix_of_le {p : DyckWord} {q : DyckWord} (h : p ≤ q) : ↑p <:+: ↑q

theorem DyckWord.le_of_suffix {p : DyckWord} {q : DyckWord} (h : ↑p <:+ ↑q) : p ≤ q

instance DyckWord.instPartialOrder : PartialOrder DyckWord

Partial order on Dyck words: p ≤ q if a (possibly empty) sequence of insidePart and outsidePart operations can turn q into p.

Equations

• DyckWord.instPartialOrder = PartialOrder.mk DyckWord.instPartialOrder.proof_1

theorem DyckWord.pos_iff_ne_zero {p : DyckWord} : 0 < p ↔ p ≠ 0

theorem DyckWord.monotone_semilength : Monotone DyckWord.semilength

theorem DyckWord.strictMono_semilength : StrictMono DyckWord.semilength

def DyckWord.equivTree : DyckWord ≃ Tree Unit

Equivalence between Dyck words and rooted binary trees.

Equations

• DyckWord.equivTree = { toFun := DyckWord.equivTreeToFun, invFun := DyckWord.equivTreeInvFun, left_inv := DyckWord.equivTree_left_inv, right_inv := DyckWord.equivTree_right_inv }

@[irreducible]

theorem DyckWord.semilength_eq_numNodes_equivTree (p : DyckWord) : p.semilength = (DyckWord.equivTree p).numNodes

def DyckWord.equivTreesOfNumNodesEq (n : ℕ) : { p : DyckWord // p.semilength = n } ≃ { x : Tree Unit // x ∈ Tree.treesOfNumNodesEq n }

Equivalence between Dyck words of semilength n and rooted binary trees with n internal nodes.

Equations

• One or more equations did not get rendered due to their size.

instance DyckWord.instFintypeSubtypeEqNatSemilength {n : ℕ} : Fintype { p : DyckWord // p.semilength = n }

Equations

• DyckWord.instFintypeSubtypeEqNatSemilength = Fintype.ofEquiv { x : Tree Unit // x ∈ Tree.treesOfNumNodesEq n } (DyckWord.equivTreesOfNumNodesEq n).symm

theorem DyckWord.card_dyckWord_semilength_eq_catalan (n : ℕ) : Fintype.card { p : DyckWord // p.semilength = n } = catalan n

There are catalan n Dyck words of semilength n (or length 2 * n).

def Mathlib.Meta.Positivity.evalDyckWordFirstReturn : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: p.firstReturn is positive if p is nonzero.