Library Combi.Combi.Dyckword: Dyck Words
Dyck Words
- for all prefix, the number of "(" is larger that the number of ")";
- the total number of "(" is equal to those of ")".
- 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_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
- 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
- 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.
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.
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.
#[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.
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).
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).
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.
[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.
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.
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.
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.
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.
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.
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.
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.
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.
Section BijBinTrees.
Fixpoint Dyck_of_bintree t :=
if t is BinNode l r then
[Dyck {{ (Dyck_of_bintree l) }} Dyck_of_bintree r]
else nil_Dyck.
Lemma bintree_of_Dyck_spec D :
{ t : bintree | Dyck_of_bintree t = D /\
forall t', Dyck_of_bintree t' = D -> t = t' }.
Definition bintree_of_Dyck D := proj1_sig (bintree_of_Dyck_spec D).
Lemma bintree_of_DyckK D : Dyck_of_bintree (bintree_of_Dyck D) = D.
Lemma bintree_of_nil_Dyck : bintree_of_Dyck nil_Dyck = BinLeaf.
Lemma bintree_of_join_Dyck D1 D2 :
bintree_of_Dyck ([Dyck {{ D1 }} D2]) =
BinNode (bintree_of_Dyck D1) (bintree_of_Dyck D2).
Theorem Dyck_of_bintreeK t : bintree_of_Dyck (Dyck_of_bintree t) = t.
Lemma size_Dyck_of_bintree t :
size (Dyck_of_bintree t) = (size_tree t).*2.
Lemma size_bintree_of_Dyck D :
(size_tree (bintree_of_Dyck D)).*2 = size D.
End BijBinTrees.
Fixpoint Dyck_of_bintree t :=
if t is BinNode l r then
[Dyck {{ (Dyck_of_bintree l) }} Dyck_of_bintree r]
else nil_Dyck.
Lemma bintree_of_Dyck_spec D :
{ t : bintree | Dyck_of_bintree t = D /\
forall t', Dyck_of_bintree t' = D -> t = t' }.
Definition bintree_of_Dyck D := proj1_sig (bintree_of_Dyck_spec D).
Lemma bintree_of_DyckK D : Dyck_of_bintree (bintree_of_Dyck D) = D.
Lemma bintree_of_nil_Dyck : bintree_of_Dyck nil_Dyck = BinLeaf.
Lemma bintree_of_join_Dyck D1 D2 :
bintree_of_Dyck ([Dyck {{ D1 }} D2]) =
BinNode (bintree_of_Dyck D1) (bintree_of_Dyck D2).
Theorem Dyck_of_bintreeK t : bintree_of_Dyck (Dyck_of_bintree t) = t.
Lemma size_Dyck_of_bintree t :
size (Dyck_of_bintree t) = (size_tree t).*2.
Lemma size_bintree_of_Dyck D :
(size_tree (bintree_of_Dyck D)).*2 = size D.
End BijBinTrees.
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.
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.
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).
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).
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}.
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}.