Library Combi.Combi.Dyckword: Dyck Words

Dyck Words

A Dyck word is a word on the two letter alphabet "(" and ")" which is well parentesized. More formally
  • for all prefix, the number of "(" is larger that the number of ")";
  • the total number of "(" is equal to those of ")".
We encode those words using:
  • brace == a type with two values Open and Close and locally use the notations "{{" and "}}"
  • height w == the difference between the number of "{{" and "}}"
  • prefixes w == the list of all the prefix of w
  • w is a Dyck_prefix <=> for all prefix, the number of "{{" is larger than the number of "}}"
  • w is a Dyck_word <=> w is a Dyck word, that is a Dyck_prefix of height 0
  • Dyck == a Sigma-type for Dyck words. It is canonically a countType
  • [Dyck of s] == a Dyck word for the sequence s; the proof is canonically infered.
  • [Dyck of s by pf] == a Dyck word for the sequence s using the proof pf
  • [Dyck {{ D1 }} D2] == the term of type Dyck corresponding to the word "(D1)D2", assuming that D1 and D2 are of type Dyck
Dyck words are in bijection with binary trees:
  • Dyck_of_bintree t == the image of the binary tree t by the standard bijection from trees to Dyck words.
  • bintree_of_Dyck D == the converse bijection
The main result of this file is to show that the number of Dyck word is the so-called Catalan numbers defined below:
  • Catalan n == the n-th Catalan number 'C(n.*2, n) %/ n.+1
  • Dyck_hsz n == the set of tuple of half size n which are Dyck words
  • bal_hsz n == the set of tuple of half size n which are balanced words
We prove bijectively the equality with catalan binomial formula, using the rotation trick: there is a (n+1) to 1 map from balanced words to Dyck words.
  • minh w == the minimal height of prefixes of w
  • pfminh w == the first position where the minimal height is reached
  • Dyck_of_bal w == given a balanced word w returns the unique Dyck word D such that D) is a rotation of w)
  • bal_of_Dyck rt w == the word obtained by rotating w) by rt and removing the last letter.
  • bal_part n == the partition of balanced words given by the fiber of the Dyck_of_bal map. The main argument is to show that all the fibers have the same cardinality n+1.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import div ssralg ssrint ssrnum binomial.
Require Import tools combclass bintree.

Set Implicit Arguments.

Import Order.TTheory GRing.Theory Num.Theory.

Section PreimPartition.

Variables (T rT : finType) (f : T -> rT) (D : {set T}).

Lemma mem_preim_partition (B : {set T}) :
  B \in preim_partition f D ->
  exists x0 : T, (x0 \in B) /\ (B = D :&: f @^-1: [set f x0]).

Lemma imset_transversal_preim :
  f @: (transversal (preim_partition f D) D) = f @: D.

Lemma card_preim_partition : #|preim_partition f D| = #|f @: D|.

End PreimPartition.

Lemma card_preim_nth (m : nat) (T : eqType) (s : seq T) (P : pred T) (u : T):
  size s = m -> #|[set i : 'I_m | preim (nth u s) P i]| = count P s.

Braces and Dyck words

Inductive brace : Set := | Open : brace | Close : brace.

#[local] Notation "{{" := Open.
#[local] Notation "}}" := Close.

Definition bool_of_brace b := if b is {{ then true else false.
Definition brace_of_bool b := if b then {{ else }}.

Lemma bool_of_braceK : cancel bool_of_brace brace_of_bool.
Lemma brace_of_boolK : cancel brace_of_bool bool_of_brace.


Lemma size_count_braceE (w : seq brace) :
  size w = count_mem {{ w + count_mem }} w.

Import GRing.Theory Num.Theory.
Open Scope int_scope.
Open Scope ring_scope.

Height of a word

Section Defs.

Implicit Type n : nat.
Implicit Type u v w : seq brace.

Definition height w : int := Posz (count_mem {{ w) - Posz (count_mem }} w).

Lemma height_nil : height [::] = 0.

Lemma height_cons l v :
  height (l :: v) = (if l == {{ then 1 else -1) + height v.

Lemma height_rcons v l :
  height (rcons v l) = height v + (if l == {{ then 1 else -1).

Lemma height_cat u v : height (u ++ v) = height u + height v.

Definition height_simpl := (height_cons, height_rcons, height_cat, height_nil).

Lemma height_drop n u : height (drop n u) = height u - height (take n u).

Lemma height_rev u : height (rev u) = height u.

Lemma height_nseq n b :
  height (nseq n b) = Posz n * (if b == {{ then 1 else -1).

Definition prefixes w := [seq take n w | n <- iota 0 (size w).+1].

Lemma take_prefixes w i : take i w \in prefixes w.
Lemma mem_prefixesP w p : reflect (exists i, p = take i w) (p \in prefixes w).

Definitions

Definition Dyck_prefix :=
  [qualify a w : seq brace |
   all (fun p : seq brace => height p >= 0) (prefixes w)].
Definition Dyck_word :=
  [qualify a w : seq brace | (w \is a Dyck_prefix) && (height w == 0)].

Lemma Dyck_prefixP w :
  reflect (forall n, height (take n w) >= 0) (w \is a Dyck_prefix).

Lemma Dyck_wordP w :
  reflect
    ((forall n, height (take n w) >= 0) /\ (height w = 0))
    (w \is a Dyck_word).

Lemma height_take_leq (h : int) w :
  (forall n : nat, h <= height (take n w)) <->
  (forall n : nat, (n <= size w)%N -> h <= height (take n w)).

Lemma Dyck_word_OwC w :
  w \is a Dyck_word -> {{ :: w ++ [:: }}] \is a Dyck_word.

Lemma Dyck_word_cat w1 w2 :
  w1 \is a Dyck_word -> w2 \is a Dyck_word -> w1 ++ w2 \is a Dyck_word.
Lemma Dyck_word_flatten l :
  all (mem Dyck_word) l -> flatten l \is a Dyck_word.

Lemma Dyck_word_OwCw w1 w2 :
  w1 \is a Dyck_word -> w2 \is a Dyck_word ->
  {{ :: w1 ++ }} :: w2 \is a Dyck_word.

End Defs.

Sigma type for Dyck words

Section DyckType.

Record Dyck := DyckWord {dyckword :> seq brace;
                         is_dyckword :> dyckword \is a Dyck_word}.

Implicit Type D : Dyck.

Lemma DyckP D : (dyckword D) \is a Dyck_word.
Hint Resolve DyckP : core.

Definition dyck D mkD : Dyck :=
  mkD (let: DyckWord _ DP := D return dyckword D \is a Dyck_word in DP).

Lemma dyckE D : dyck (fun sP => @DyckWord D sP) = D.

Canonical nil_Dyck := (@DyckWord [::] is_true_true).
Canonical cat_Dyck D1 D2 := DyckWord (Dyck_word_cat D1 D2).
Canonical join_Dyck D1 D2 := DyckWord (Dyck_word_OwCw D1 D2).

End DyckType.

Notation "[ 'Dyck' 'of' s ]" := (dyck (fun sP => @DyckWord s sP))
  (at level 9, format "[ 'Dyck' 'of' s ]") : form_scope.

Notation "[ 'Dyck' 'of' s 'by' pf ]" := (@DyckWord s pf)
  (at level 9, format "[ 'Dyck' 'of' s 'by' pf ]") : form_scope.

Notation "[ 'Dyck' {{ D1 }} D2 ]" := (join_Dyck D1 D2)
  (at level 8, format "[ 'Dyck' {{ D1 }} D2 ]",
   D1 at next level) : form_scope.

Standard factorization of Dyck words

Section DyckFactor.

Implicit Type D : Dyck.

Lemma Dyck_cut_ex D :
  D != [Dyck of [::]] -> exists i, (i != 0)%N && (height (take i D) == 0).

Theorem factor_Dyck D :
  D != [Dyck of [::]] -> { DD : Dyck * Dyck | D = [Dyck {{ DD.1 }} DD.2] }.

Theorem join_Dyck_inj D1 D2 E1 E2 :
  [Dyck {{D1}}D2] = [Dyck {{E1}}E2] -> (D1, D2) = (E1, E2).

End DyckFactor.

Induction on Dyck words following the standard factorization

Section DyckSetInd.

Implicit Type D : Dyck.

Variable P : Dyck -> Type.
Hypotheses (Pnil : P nil_Dyck)
           (Pcons : forall D1 D2, P D1 -> P D2 -> P ([Dyck {{ D1 }} D2])).

Theorem Dyck_ind D : P D.

End DyckSetInd.

Examples of application of the induction principle

Lemma Dyck_size_even (D : Dyck) : ~~ odd (size D).

Lemma factor_Dyck_seq D :
  { DS : seq Dyck | D = foldr join_Dyck nil_Dyck DS }.

Lemma foldr_join_Dyck_inj : injective (foldr join_Dyck nil_Dyck).

Lemma size_foldr_join_Dyck DS :
  (size (foldr join_Dyck nil_Dyck DS) =
   sumn (map (size \o dyckword) DS) + 2 * size DS)%N.

Bijection with binary trees

Dyck and balanced words

Rotation map from balanced words to a Dyck words

Section BalToDyck.

Variable w : seq brace.

Definition minh :=
  - Posz (\max_(s <- prefixes w) (count_mem }} s - count_mem {{ s)).

Lemma minhE :
  minh = - Posz (\max_(i < (size w).+1)
                  (count_mem }} (take i w) - count_mem {{ (take i w))).

Lemma minhP : forall i : nat, height (take i w) >= minh.

Fact exists_minh : exists i : nat, height (take i w) == minh.
Definition pfminh := ex_minn exists_minh.

Lemma pfminhP : height (take pfminh w) = minh.

Lemma pfminh_size : (pfminh <= size w)%N.

Lemma pfminh_min :
  forall i : nat, (i < pfminh)%N -> height (take i w) > minh.

Lemma pfminhE n :
  (n <= size w)%N ->
  (forall i : nat, height (take i w) >= height (take n w)) ->
  (forall i : nat, (i < n)%N -> height (take i w) > height (take n w)) ->
  n = pfminh.

Hypothesis Hbal1 : height w = -1.

Lemma minh_neg : minh < 0.

Lemma pfminh_pos : (pfminh > 0)%N.

Lemma nth_pfminh : nth {{ w pfminh.-1 = }}.

Lemma last_rot_pfminh : last {{ (rot pfminh w) = }}.

Lemma rot_pfminhE :
  rcons (take (size w).-1 (rot pfminh w)) }} = rot pfminh w.

Theorem rot_is_Dyck : take (size w).-1 (rot pfminh w) \is a Dyck_word.

End BalToDyck.

Section DyckToBal.

Variables (w : seq brace) (rt : nat).
Hypothesis HDyck : w \is a Dyck_word.
Hypothesis Hrt: (rt <= (size w))%N.

Lemma rrw_bal1 : height (rot rt (rcons w }})) = -1.

Lemma pfminh_rrw :
  pfminh (rot rt (rcons w }})) = ((size w).+1 - rt)%N.

Lemma minh_rrw : minh (rot rt (rcons w }})) = - height (take rt w) - 1.

End DyckToBal.

Close Scope ring_scope.

Catalan numbers

Definition Catalan n := 'C(n.*2, n) %/ n.+1.

Definition Dyck_hsz n : {set n.*2.-tuple brace} :=
  [set w : n.*2.-tuple brace | tval w \is a Dyck_word].
Definition bal_hsz n : {set n.*2.-tuple brace} :=
  [set w : n.*2.-tuple brace | height w == 0].

Theorem card_bintreesz_dyck n : #|bintreesz n| = #|Dyck_hsz n|.

Lemma count_mem_height0 n (w : n.*2.-tuple brace) b :
  height w = 0 -> count_mem b w = n.

Lemma card_bal_hsz n : #|bal_hsz n| = 'C(n.*2, n).

The rotation bijection

Section DyckWordRotationBijection.

Variable n : nat.
Implicit Types u v w D : n.*2.-tuple brace.

Fact size_UnDn : size (nseq n {{ ++ nseq n }}) == n.*2.
Definition UnDn := Tuple size_UnDn.

Lemma UnDn_Dyck : tval UnDn \is a Dyck_word.

Fact size_UDn : size (flatten (nseq n [:: {{; }}])) == n.*2.
Definition UDn := Tuple size_UDn.

Lemma UDn_Dyck : tval UDn \is a Dyck_word.

Fact size_Dyck_of_bal w :
  size (take (size w) (rot (pfminh (rcons w }})) (rcons w }}))) == n.*2.
Definition Dyck_of_bal w := Tuple (size_Dyck_of_bal w).

Lemma Dyck_of_balP w : height w = 0 -> tval (Dyck_of_bal w) \is a Dyck_word.

Lemma Dyck_of_Dyck_hsz D : tval D \is a Dyck_word -> Dyck_of_bal D = D.

Fact size_bal_of_Dyck rt w :
  size (take (size w) (rotr rt (rcons w }}))) == n.*2.
Definition bal_of_Dyck rt w := Tuple (size_bal_of_Dyck rt w).

Lemma bal_of_DyckP rt w :
  (rt <= size w)%N ->
  nth {{ (rcons w }}) (size w - rt) = }} ->
  height w = 0 -> height (bal_of_Dyck rt w) = 0.

Lemma rcons_bal_of_Dyck w k :
  (k <= size w)%N ->
  nth {{ (rcons w }}) (size w - k) = }} ->
  rcons (bal_of_Dyck k w) }} = rotr k (rcons w }}).

Lemma bal_of_DyckK D rt :
  (rt <= size D)%N ->
  nth {{ (rcons D }}) (size D - rt) = }} ->
  tval D \is a Dyck_word ->
  Dyck_of_bal (bal_of_Dyck rt D) = D.

Lemma Dyck_of_balK w :
  height w = 0 -> w = bal_of_Dyck (pfminh (rcons w }})) (Dyck_of_bal w).

Lemma preim_Dyck_of_balE D :
  tval D \is a Dyck_word ->
  (bal_hsz n) :&: (Dyck_of_bal @^-1: [set D]) =
  [ set bal_of_Dyck (nat_of_ord rt) D |
    rt : 'I_((size D).+1) & nth {{ (rcons D }}) (size D - rt) == }} ].

Lemma card_preim_Dyck_of_bal D :
  tval D \is a Dyck_word ->
  #|(bal_hsz n) :&: (Dyck_of_bal @^-1: [set D])| = n.+1.

End DyckWordRotationBijection.

Arguments Dyck_of_bal {n}.
Arguments bal_of_Dyck {n}.

Main theorem for catalan numbers

Theorem card_bal_Dyck_hsz n : #|bal_hsz n| = #|Dyck_hsz n| * n.+1.

Lemma div_central_binomial n : n.+1 %| 'C(n.*2, n).

Theorem card_Dyck_hsz n : #|Dyck_hsz n| = Catalan n.

Theorem Catalan_binE n : Catalan_bin n = Catalan n.