Documentation

Mathlib.Combinatorics.Enumerative.DyckWord

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 #

Main results #

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 :

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

Instances For
    Equations
    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 :

    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.

    Instances For

      There are as many Us as Ds

      Each prefix has as least as many Us as Ds

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

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

      Equations
      theorem DyckWord.toList_eq_nil {p : DyckWord} :
      p = [] p = 0
      theorem DyckWord.toList_ne_nil {p : DyckWord} :
      p [] p 0

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

      Equations
      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

      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 := }
      Instances For

        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 := }
        Instances For

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

          Equations
          Instances For
            @[simp]
            theorem DyckWord.nest_ne_zero {p : DyckWord} :
            p.nest 0

            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
            Instances For
              theorem DyckWord.IsNested.nest {p : DyckWord} :
              p.nest.IsNested
              def DyckWord.denest (p : DyckWord) (hn : p.IsNested) :

              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 := }
              Instances For
                theorem DyckWord.nest_denest (p : DyckWord) (hn : p.IsNested) :
                (p.denest hn).nest = p
                theorem DyckWord.denest_nest (p : DyckWord) :
                p.nest.denest = p

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

                Equations
                Instances For
                  @[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
                  @[simp]
                  theorem DyckWord.two_mul_semilength_eq_length {p : DyckWord} :
                  2 * p.semilength = (↑p).length

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

                  Equations
                  Instances For
                    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)
                    @[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

                    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
                    Instances For

                      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)
                      Instances For
                        @[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
                        @[irreducible]
                        theorem DyckWord.le_add_self (p : DyckWord) (q : DyckWord) :
                        q p + q
                        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

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

                        Equations

                        Equivalence between Dyck words and rooted binary trees.

                        Equations
                        Instances For
                          @[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.
                          Instances For
                            instance DyckWord.instFintypeSubtypeEqNatSemilength {n : } :
                            Fintype { p : DyckWord // p.semilength = n }
                            Equations

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

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

                            Instances For