Library Combi.Combi.tableau: Young Tableaux
Young Tableaux over an ordtype
- is_row r == r is sorted
- dominate u v == u dominate v, that is v is longer than u and the i-th letter of u is strictly larger than the i-th letter of v. this is an order relation on seq T.
- is_tableau t == t of type (seq (seq T)) is a tableau that is a sequence of non empty rows which is sorted for the dominate order.
- get_tab t (r, c) == the element of t of coordinate (r, c), or inhabitant T if (r, c) is not is the tableau
- to_word t == the row reading of the tableau t
- size_tab t == the size (number of boxes) of t
- filter_gtnX_tab n t == the sub-tableau of t formed by the element smaller
than n.
- tabsh_reading sh w == w is the row reading of a tableau of shape sh
- is_tab_of_shape sh t == t is a tableau of shape sh.
- tabsh sh == a sigma-type for the predicate is_tab_of_shape sh where sh is a partition of d (type 'P_d). This is canonically a subFinType.
- tabrowconst pf == if pf is a proof that size sh <= n.+1 then construct the tableau (of type tabsh sh) whose i-th row contains only i's as elements of 'I_n.+1.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import tools partition ordtype sorted.
Set Implicit Arguments.
Open Scope N.
Import Order.Theory.
From mathcomp Require Import all_ssreflect.
Require Import tools partition ordtype sorted.
Set Implicit Arguments.
Open Scope N.
Import Order.Theory.
Section Rows.
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type l : T.
Implicit Type r : seq T.
Notation is_row := (sorted <=%O).
Definition is_row1P Z r := sortedP Z (e := <=%O) (s := r).
Definition is_rowP Z r := sorted2P Z (@le_trans _ T) (@le_refl _ T) r.
Definition is_row_cons := sorted_cons (@le_refl _ T).
Definition is_row_consK := sorted_consK (T := T) (R := <=%O).
Definition is_row_rcons := sorted_rcons (T := T) (R := <=%O).
Definition is_row_rconsK := sorted_rconsK (T := T) (R := <=%O).
Definition is_row_last := sorted_last (@le_refl _ T).
Definition is_row_take := take_sorted (T := T) (leT := <=%O).
Definition is_row_drop := drop_sorted (T := T) (leT := <=%O).
Definition is_row_cat2 := cat_sorted2 (T := T) (leT := <=%O).
Definition head_leq_last_row :=
head_leq_last_sorted (@le_trans _ T) (@le_refl _ T).
Lemma row_lt_by_pos Z r p q:
is_row r -> p < size r -> q < size r ->
(nth Z r p < nth Z r q)%O -> p < q.
End Rows.
Notation is_row := (sorted <=%O).
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type l : T.
Implicit Type r : seq T.
Notation is_row := (sorted <=%O).
Definition is_row1P Z r := sortedP Z (e := <=%O) (s := r).
Definition is_rowP Z r := sorted2P Z (@le_trans _ T) (@le_refl _ T) r.
Definition is_row_cons := sorted_cons (@le_refl _ T).
Definition is_row_consK := sorted_consK (T := T) (R := <=%O).
Definition is_row_rcons := sorted_rcons (T := T) (R := <=%O).
Definition is_row_rconsK := sorted_rconsK (T := T) (R := <=%O).
Definition is_row_last := sorted_last (@le_refl _ T).
Definition is_row_take := take_sorted (T := T) (leT := <=%O).
Definition is_row_drop := drop_sorted (T := T) (leT := <=%O).
Definition is_row_cat2 := cat_sorted2 (T := T) (leT := <=%O).
Definition head_leq_last_row :=
head_leq_last_sorted (@le_trans _ T) (@le_refl _ T).
Lemma row_lt_by_pos Z r p q:
is_row r -> p < size r -> q < size r ->
(nth Z r p < nth Z r q)%O -> p < q.
End Rows.
Notation is_row := (sorted <=%O).
Section Dominate.
Context {disp : unit} {T : inhOrderType disp}.
Implicit Type l : T.
Implicit Type r u v : seq T.
Implicit Type t : seq (seq T).
Lemma in_shape_tab_size t i j :
in_shape (shape t) (i, j) -> i < size t.
Lemma in_shape_tab i j t :
in_shape (shape t) (i, j) -> j < size (nth [::] t i).
Lemma is_row_set_nth l r pos :
is_row r -> (l < nth l r pos)%O ->
(forall n : nat, (l < nth l r n)%O -> pos <= n) ->
is_row (set_nth l r pos l).
Fixpoint dominate_rec u v :=
if u is u0 :: u' then
if v is v0 :: v' then (u0 > v0)%O && (dominate_rec u' v')
else false
else true.
Definition dominate u v :=
(size u <= size v) &&
(all (fun i => nth inh u i > nth inh v i)%O (iota 0 (size u))).
Lemma dominate_recE : dominate =2 dominate_rec.
Lemma dominateP u v :
reflect (size u <= size v /\
forall i, i < size u -> (nth inh u i > nth inh v i)%O)
(dominate u v).
Lemma dominate_trans : transitive dominate.
Definition dominate_rev_trans := rev_trans dominate_trans.
Lemma dominate_rcons v u l : dominate u v -> dominate u (rcons v l).
Lemma dominate_take v u n : dominate u (take n v) -> dominate u v.
Lemma dominate_cut u v w:
size u <= size v -> dominate u (v ++ w) -> dominate u v.
Lemma dominate_head u v :
u != [::] -> dominate u v -> (head inh v < head inh u)%O.
Lemma dominate_tl a u b v :
dominate (a :: u) (b :: v) -> dominate u v.
End Dominate.
Arguments dominate_trans {disp T}.
Arguments dominate_rev_trans {disp T}.
Context {disp : unit} {T : inhOrderType disp}.
Implicit Type l : T.
Implicit Type r u v : seq T.
Implicit Type t : seq (seq T).
Lemma in_shape_tab_size t i j :
in_shape (shape t) (i, j) -> i < size t.
Lemma in_shape_tab i j t :
in_shape (shape t) (i, j) -> j < size (nth [::] t i).
Lemma is_row_set_nth l r pos :
is_row r -> (l < nth l r pos)%O ->
(forall n : nat, (l < nth l r n)%O -> pos <= n) ->
is_row (set_nth l r pos l).
Fixpoint dominate_rec u v :=
if u is u0 :: u' then
if v is v0 :: v' then (u0 > v0)%O && (dominate_rec u' v')
else false
else true.
Definition dominate u v :=
(size u <= size v) &&
(all (fun i => nth inh u i > nth inh v i)%O (iota 0 (size u))).
Lemma dominate_recE : dominate =2 dominate_rec.
Lemma dominateP u v :
reflect (size u <= size v /\
forall i, i < size u -> (nth inh u i > nth inh v i)%O)
(dominate u v).
Lemma dominate_trans : transitive dominate.
Definition dominate_rev_trans := rev_trans dominate_trans.
Lemma dominate_rcons v u l : dominate u v -> dominate u (rcons v l).
Lemma dominate_take v u n : dominate u (take n v) -> dominate u v.
Lemma dominate_cut u v w:
size u <= size v -> dominate u (v ++ w) -> dominate u v.
Lemma dominate_head u v :
u != [::] -> dominate u v -> (head inh v < head inh u)%O.
Lemma dominate_tl a u b v :
dominate (a :: u) (b :: v) -> dominate u v.
End Dominate.
Arguments dominate_trans {disp T}.
Arguments dominate_rev_trans {disp T}.
Section Tableau.
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type l : T.
Implicit Type r w : seq T.
Implicit Type t : seq (seq T).
Fixpoint is_tableau t :=
if t is t0 :: t'
then [&& (t0 != [::]), is_row t0, dominate (head [::] t') t0 & is_tableau t']
else true.
Definition get_tab t (rc : nat * nat) := nth inh (nth [::] t rc.1) rc.2.
Definition to_word t := flatten (rev t).
Lemma is_tableauP t :
reflect
[/\ forall i, i < size t -> (nth [::] t i) != [::],
forall i, is_row (nth [::] t i) &
forall i j, i < j -> dominate (nth [::] t j) (nth [::] t i)]
(is_tableau t).
Lemma get_tab_default t rc :
~~ in_shape (shape t) rc -> get_tab t rc = inh.
Lemma to_word_cons r t : to_word (r :: t) = to_word t ++ r.
Lemma to_word_rcons r t : to_word (rcons t r) = r ++ to_word t.
Lemma mem_to_word t rc :
in_shape (shape t) rc -> get_tab t rc \in (to_word t).
Lemma to_wordK t : rev (reshape (rev (shape t)) (to_word t)) = t.
Lemma tableau_is_row r t : is_tableau (r :: t) -> is_row r.
Lemma is_tableau_rconsK t (tn : seq T) :
is_tableau (rcons t tn) -> is_tableau t.
Lemma is_tableau_catl t1 t2 :
is_tableau (t1 ++ t2) -> is_tableau t1.
Lemma is_tableau_catr t1 t2 :
is_tableau (t1 ++ t2) -> is_tableau t2.
Lemma is_part_sht t : is_tableau t -> is_part (shape t).
Lemma tab_eqP p q :
is_tableau p -> is_tableau q ->
reflect (forall i, nth [::] p i = nth [::] q i) (p == q).
Lemma is_tableau_sorted_dominate t :
is_tableau t =
[&& is_part (shape t),
all (sorted <=%O) t &
sorted (fun (r s : seq T) => dominate s r) t].
Lemma is_tableau_getP t :
reflect
[/\ is_part (shape t),
(forall (r c : nat), in_shape (shape t) (r, c.+1) ->
(get_tab t (r, c) <= get_tab t (r, c.+1))%O) &
(forall (r c : nat), in_shape (shape t) (r.+1, c) ->
(get_tab t (r, c) < get_tab t (r.+1, c))%O)]
(is_tableau t).
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type l : T.
Implicit Type r w : seq T.
Implicit Type t : seq (seq T).
Fixpoint is_tableau t :=
if t is t0 :: t'
then [&& (t0 != [::]), is_row t0, dominate (head [::] t') t0 & is_tableau t']
else true.
Definition get_tab t (rc : nat * nat) := nth inh (nth [::] t rc.1) rc.2.
Definition to_word t := flatten (rev t).
Lemma is_tableauP t :
reflect
[/\ forall i, i < size t -> (nth [::] t i) != [::],
forall i, is_row (nth [::] t i) &
forall i j, i < j -> dominate (nth [::] t j) (nth [::] t i)]
(is_tableau t).
Lemma get_tab_default t rc :
~~ in_shape (shape t) rc -> get_tab t rc = inh.
Lemma to_word_cons r t : to_word (r :: t) = to_word t ++ r.
Lemma to_word_rcons r t : to_word (rcons t r) = r ++ to_word t.
Lemma mem_to_word t rc :
in_shape (shape t) rc -> get_tab t rc \in (to_word t).
Lemma to_wordK t : rev (reshape (rev (shape t)) (to_word t)) = t.
Lemma tableau_is_row r t : is_tableau (r :: t) -> is_row r.
Lemma is_tableau_rconsK t (tn : seq T) :
is_tableau (rcons t tn) -> is_tableau t.
Lemma is_tableau_catl t1 t2 :
is_tableau (t1 ++ t2) -> is_tableau t1.
Lemma is_tableau_catr t1 t2 :
is_tableau (t1 ++ t2) -> is_tableau t2.
Lemma is_part_sht t : is_tableau t -> is_part (shape t).
Lemma tab_eqP p q :
is_tableau p -> is_tableau q ->
reflect (forall i, nth [::] p i = nth [::] q i) (p == q).
Lemma is_tableau_sorted_dominate t :
is_tableau t =
[&& is_part (shape t),
all (sorted <=%O) t &
sorted (fun (r s : seq T) => dominate s r) t].
Lemma is_tableau_getP t :
reflect
[/\ is_part (shape t),
(forall (r c : nat), in_shape (shape t) (r, c.+1) ->
(get_tab t (r, c) <= get_tab t (r, c.+1))%O) &
(forall (r c : nat), in_shape (shape t) (r.+1, c) ->
(get_tab t (r, c) < get_tab t (r.+1, c))%O)]
(is_tableau t).
Lemma row_dominate (u v : seq T) :
is_row (u ++ v) -> dominate u v -> u = [::].
Lemma filter_gt_row r n :
is_row r -> filter (>%O n) r = take (count (>%O n) r) r.
Lemma filter_le_row n r :
is_row r -> filter (<=%O n) r = drop (count (>%O n) r) r.
Lemma count_gt_dominate r1 r0 n :
dominate r1 r0 -> (count (>%O n) r1) <= (count (>%O n) r0).
Lemma filter_gt_dominate r1 r0 n :
is_row r0 -> is_row r1 -> dominate r1 r0 ->
dominate (filter (>%O n) r1) (filter (>%O n) r0).
Definition filter_gt_tab n :=
[fun t : (seq (seq T)) => filter (fun r => r != [::])
[seq [seq x <- i | (n > x)%O] | i <- t]].
Lemma to_word_filter_nnil t : to_word (filter (fun r => r != [::]) t) = to_word t.
Lemma filter_to_word t p : filter p (to_word t) = to_word (map (filter p) t).
Lemma head_filter_gt_tab n t :
is_tableau t ->
head [::] (filter_gt_tab n t) = [seq x <- head [::] t | (x < n)%O].
Lemma is_tableau_filter_gt t n :
is_tableau t -> is_tableau (filter_gt_tab n t).
is_row (u ++ v) -> dominate u v -> u = [::].
Lemma filter_gt_row r n :
is_row r -> filter (>%O n) r = take (count (>%O n) r) r.
Lemma filter_le_row n r :
is_row r -> filter (<=%O n) r = drop (count (>%O n) r) r.
Lemma count_gt_dominate r1 r0 n :
dominate r1 r0 -> (count (>%O n) r1) <= (count (>%O n) r0).
Lemma filter_gt_dominate r1 r0 n :
is_row r0 -> is_row r1 -> dominate r1 r0 ->
dominate (filter (>%O n) r1) (filter (>%O n) r0).
Definition filter_gt_tab n :=
[fun t : (seq (seq T)) => filter (fun r => r != [::])
[seq [seq x <- i | (n > x)%O] | i <- t]].
Lemma to_word_filter_nnil t : to_word (filter (fun r => r != [::]) t) = to_word t.
Lemma filter_to_word t p : filter p (to_word t) = to_word (map (filter p) t).
Lemma head_filter_gt_tab n t :
is_tableau t ->
head [::] (filter_gt_tab n t) = [seq x <- head [::] t | (x < n)%O].
Lemma is_tableau_filter_gt t n :
is_tableau t -> is_tableau (filter_gt_tab n t).
Definition size_tab t := sumn (shape t).
Lemma tab0 t : is_tableau t -> size_tab t = 0 -> t = [::].
Lemma size_to_word t : size (to_word t) = size_tab t.
End Tableau.
Lemma tab0 t : is_tableau t -> size_tab t = 0 -> t = [::].
Lemma size_to_word t : size (to_word t) = size_tab t.
End Tableau.
Section TableauReading.
Variables (disp : unit) (A : inhOrderType disp).
Definition tabsh_reading (sh : seq nat) (w : seq A) :=
(size w == sumn sh) && (is_tableau (rev (reshape (rev sh) w))).
Lemma tabsh_readingP (sh : seq nat) (w : seq A) :
reflect
(exists tab, [/\ is_tableau tab, shape tab = sh & to_word tab = w])
(tabsh_reading sh w).
End TableauReading.
Variables (disp : unit) (A : inhOrderType disp).
Definition tabsh_reading (sh : seq nat) (w : seq A) :=
(size w == sumn sh) && (is_tableau (rev (reshape (rev sh) w))).
Lemma tabsh_readingP (sh : seq nat) (w : seq A) :
reflect
(exists tab, [/\ is_tableau tab, shape tab = sh & to_word tab = w])
(tabsh_reading sh w).
End TableauReading.
Section FinType.
Context {disp : unit} {T : inhFinOrderType disp}.
Variables (d : nat) (sh : 'P_d).
Definition is_tab_of_shape (sh : seq nat) :=
[pred t : seq (seq T) | (is_tableau t) && (shape t == sh) ].
Structure tabsh : predArgType :=
TabSh {tabshval :> seq (seq T); _ : is_tab_of_shape sh tabshval}.
Implicit Type (t : tabsh).
Lemma tabshP t : is_tableau t.
Lemma shape_tabsh t : shape t = sh.
Lemma tabsh_to_wordK t : rev (reshape (rev sh) (to_word (val t))) = t.
Let tabsh_enum :
seq tabsh := pmap insub
[seq rev (reshape (rev sh) (val w)) | w in {:d.-tuple T}].
Lemma finite_tabsh : Finite.axiom tabsh_enum.
Lemma to_word_enum_tabsh :
perm_eq
[seq to_word (tabshval t) | t : tabsh]
[seq x <- [seq (i : seq _) | i : d.-tuple T] | tabsh_reading sh x].
End FinType.
Notation "'tabsh[' T ']' mu" :=
(tabsh (T := T : inhFinOrderType _) mu) (at level 10).
#[export] Hint Resolve tabshP : core.
Context {disp : unit} {T : inhFinOrderType disp}.
Variables (d : nat) (sh : 'P_d).
Definition is_tab_of_shape (sh : seq nat) :=
[pred t : seq (seq T) | (is_tableau t) && (shape t == sh) ].
Structure tabsh : predArgType :=
TabSh {tabshval :> seq (seq T); _ : is_tab_of_shape sh tabshval}.
Implicit Type (t : tabsh).
Lemma tabshP t : is_tableau t.
Lemma shape_tabsh t : shape t = sh.
Lemma tabsh_to_wordK t : rev (reshape (rev sh) (to_word (val t))) = t.
Let tabsh_enum :
seq tabsh := pmap insub
[seq rev (reshape (rev sh) (val w)) | w in {:d.-tuple T}].
Lemma finite_tabsh : Finite.axiom tabsh_enum.
Lemma to_word_enum_tabsh :
perm_eq
[seq to_word (tabshval t) | t : tabsh]
[seq x <- [seq (i : seq _) | i : d.-tuple T] | tabsh_reading sh x].
End FinType.
Notation "'tabsh[' T ']' mu" :=
(tabsh (T := T : inhFinOrderType _) mu) (at level 10).
#[export] Hint Resolve tabshP : core.
TODO : Generalise to any finite order using Order.enum_val when released
Section OrdTableau.
Variable n : nat.
Variables (d : nat) (sh : 'P_d).
Implicit Type (t : tabsh['I_n.+1] sh).
Lemma all_ltn_nth_tabsh t (i : nat) :
all (fun x : 'I_n.+1 => (i <= x)%O) (nth [::] t i).
Lemma size_tabsh t : size t <= n.+1.
Hypothesis Hszs : size sh <= n.+1.
Lemma tabrowconst_subproof :
is_tab_of_shape
sh (take (size sh) [tuple nseq (nth 0 sh (i : 'I_n.+1)) i | i < n.+1]).
Definition tabrowconst := TabSh (tabrowconst_subproof).
End OrdTableau.
Variable n : nat.
Variables (d : nat) (sh : 'P_d).
Implicit Type (t : tabsh['I_n.+1] sh).
Lemma all_ltn_nth_tabsh t (i : nat) :
all (fun x : 'I_n.+1 => (i <= x)%O) (nth [::] t i).
Lemma size_tabsh t : size t <= n.+1.
Hypothesis Hszs : size sh <= n.+1.
Lemma tabrowconst_subproof :
is_tab_of_shape
sh (take (size sh) [tuple nseq (nth 0 sh (i : 'I_n.+1)) i | i < n.+1]).
Definition tabrowconst := TabSh (tabrowconst_subproof).
End OrdTableau.
Section IncrMap.
Context (disp1 disp2 : unit)
(T1 : inhOrderType disp1)
(T2 : inhOrderType disp2).
Variable F : T1 -> T2.
Lemma shape_map_tab (t : seq (seq T1)) :
shape [seq map F r | r <- t] = shape t.
Lemma get_map_tab (t : seq (seq T1)) rc :
in_shape (shape t) rc ->
get_tab [seq [seq F i | i <- r0] | r0 <- t] rc = F (get_tab t rc).
Lemma to_word_map_tab (t : seq (seq T1)) :
to_word [seq map F r | r <- t] = map F (to_word t).
Lemma incr_tab (t : seq (seq T1)) :
{in (to_word t) &, {homo F : x y / (x < y)%O}} ->
(is_tableau t) = (is_tableau [seq map F r | r <- t]).
End IncrMap.
Context (disp1 disp2 : unit)
(T1 : inhOrderType disp1)
(T2 : inhOrderType disp2).
Variable F : T1 -> T2.
Lemma shape_map_tab (t : seq (seq T1)) :
shape [seq map F r | r <- t] = shape t.
Lemma get_map_tab (t : seq (seq T1)) rc :
in_shape (shape t) rc ->
get_tab [seq [seq F i | i <- r0] | r0 <- t] rc = F (get_tab t rc).
Lemma to_word_map_tab (t : seq (seq T1)) :
to_word [seq map F r | r <- t] = map F (to_word t).
Lemma incr_tab (t : seq (seq T1)) :
{in (to_word t) &, {homo F : x y / (x < y)%O}} ->
(is_tableau t) = (is_tableau [seq map F r | r <- t]).
End IncrMap.