Library Combi.Combi.skewtab: Skew Tableaux
Skew tableau and skew yamanouchi words:
- is_skew_yam inn out y == y ++ y0 is Yamanouchi of evaluation out for any y0 of evaluation inn.
- skew_dominate s u v == the row u dominate the row v when shifted by s.
- is_skew_tableau inn t == t is a skew tableau with inner shape t.
- skew_reshape inn out s == reshape the sequence s by the skew shape out/inn.
- filter_leqX_tab n t == keeps only the entries greater than n in t.
- join_tab t st == join the tableau t with the skew tableau st. this gives a tableau if the inner shape of st is the shape of t and the entries of t are smaller than the entries of st.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import tools partition skewpart Yamanouchi ordtype tableau std stdtab.
Set Implicit Arguments.
Import Order.Theory.
From mathcomp Require Import all_ssreflect.
Require Import tools partition skewpart Yamanouchi ordtype tableau std stdtab.
Set Implicit Arguments.
Import Order.Theory.
Open Scope N.
Open Scope Combi.
Definition is_skew_yam innev outev sy :=
(forall y, is_yam_of_eval innev y -> is_yam_of_eval outev (sy ++ y)).
Lemma skew_yam_nil sh : is_skew_yam sh sh [::].
Lemma skew_nil_yamE eval y : is_yam_of_eval eval y -> is_skew_yam [::] eval y.
Lemma skew_yam_cat sha shb shc y z :
is_skew_yam sha shb y -> is_skew_yam shb shc z -> is_skew_yam sha shc (z ++ y).
Lemma is_skew_yamE innev outev z y0 :
is_yam_of_eval innev y0 ->
is_yam_of_eval outev (z ++ y0) ->
is_skew_yam innev outev z.
Lemma is_part_skew_yam sha shb y :
is_part sha -> is_skew_yam sha shb y -> is_part shb.
Lemma skew_yam_catrK sha shb shc y z :
is_part sha ->
is_skew_yam sha shb y ->
is_skew_yam sha shc (z ++ y) ->
is_skew_yam shb shc z.
Lemma skew_yam_consK sha shc i y :
is_part sha -> is_skew_yam sha shc (i :: y) ->
is_skew_yam sha (decr_nth shc i) y.
Lemma skew_yam_catK sha shc y z :
is_part sha -> is_skew_yam sha shc (y ++ z) ->
{ shb | is_skew_yam sha shb z & is_skew_yam shb shc y }.
Lemma skew_yam_included sha shb y :
is_part sha -> is_skew_yam sha shb y -> included sha shb.
Open Scope Combi.
Definition is_skew_yam innev outev sy :=
(forall y, is_yam_of_eval innev y -> is_yam_of_eval outev (sy ++ y)).
Lemma skew_yam_nil sh : is_skew_yam sh sh [::].
Lemma skew_nil_yamE eval y : is_yam_of_eval eval y -> is_skew_yam [::] eval y.
Lemma skew_yam_cat sha shb shc y z :
is_skew_yam sha shb y -> is_skew_yam shb shc z -> is_skew_yam sha shc (z ++ y).
Lemma is_skew_yamE innev outev z y0 :
is_yam_of_eval innev y0 ->
is_yam_of_eval outev (z ++ y0) ->
is_skew_yam innev outev z.
Lemma is_part_skew_yam sha shb y :
is_part sha -> is_skew_yam sha shb y -> is_part shb.
Lemma skew_yam_catrK sha shb shc y z :
is_part sha ->
is_skew_yam sha shb y ->
is_skew_yam sha shc (z ++ y) ->
is_skew_yam shb shc z.
Lemma skew_yam_consK sha shc i y :
is_part sha -> is_skew_yam sha shc (i :: y) ->
is_skew_yam sha (decr_nth shc i) y.
Lemma skew_yam_catK sha shc y z :
is_part sha -> is_skew_yam sha shc (y ++ z) ->
{ shb | is_skew_yam sha shb z & is_skew_yam shb shc y }.
Lemma skew_yam_included sha shb y :
is_part sha -> is_skew_yam sha shb y -> included sha shb.
Section Dominate.
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type u v : seq T.
Definition skew_dominate sh u v := dominate (drop sh u) v.
Lemma skew_dominate0 : skew_dominate 0 =2 (@dominate _ T).
Lemma skew_dominate_take n sh u v :
skew_dominate sh u (take n v) -> skew_dominate sh u v.
Lemma skew_dominate_no_overlap sh u v :
size u <= sh -> skew_dominate sh u v.
Lemma skew_dominate_consl sh l u v :
skew_dominate sh u v -> skew_dominate sh.+1 (l :: u) v.
Lemma skew_dominate_cut sh u v :
skew_dominate sh u v = skew_dominate sh u (take (size u - sh) v).
Fixpoint is_skew_tableau inner t :=
if t is t0 :: t'
then [&& head 0 inner + size t0 != 0,
is_row t0,
skew_dominate ((head 0 inner) - (head 0 (behead inner)))
(head [::] t') t0 & is_skew_tableau (behead inner) t']
else inner == [::].
Lemma is_skew_tableauP inner t :
reflect
[/\ size inner <= size t,
forall i, i < size t -> nth 0 inner i + size (nth [::] t i) != 0,
forall i, is_row (nth [::] t i) &
forall i, skew_dominate ((nth 0 inner i) - (nth 0 inner i.+1))
(nth [::] t i.+1) (nth [::] t i)]
(is_skew_tableau inner t).
Lemma is_skew_tableau0 : is_skew_tableau [::] =1 is_tableau.
Lemma is_skew_tableau_pad0 inner t :
is_skew_tableau inner t = is_skew_tableau (pad 0 (size t) inner) t.
Definition skew_reshape (inner outer : seq nat) (s : seq T) :=
rev (reshape (rev (outer / inner)) s).
Lemma size_skew_reshape inner outer s :
size (skew_reshape inner outer s) = size outer.
Lemma shape_skew_reshape inner outer s :
included inner outer ->
size s = sumn (outer / inner) ->
shape (skew_reshape inner outer s) = outer / inner.
Lemma to_word_skew_reshape inner outer s :
included inner outer ->
size s = sumn (outer / inner) ->
to_word (skew_reshape inner outer s) = s.
Lemma skew_reshapeK inner t :
size inner <= size t ->
skew_reshape inner (outer_shape inner (shape t)) (to_word t) = t.
Lemma row_hb_strip inner t :
is_part inner ->
is_skew_tableau inner t -> is_row (to_word t) ->
hb_strip inner (outer_shape inner (shape t)).
Lemma hb_strip_rowE inner outer u :
is_part inner -> is_part outer ->
is_row u -> size u = sumn (outer / inner) ->
included inner outer &&
is_skew_tableau inner (skew_reshape inner outer u) =
hb_strip inner outer.
End Dominate.
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type u v : seq T.
Definition skew_dominate sh u v := dominate (drop sh u) v.
Lemma skew_dominate0 : skew_dominate 0 =2 (@dominate _ T).
Lemma skew_dominate_take n sh u v :
skew_dominate sh u (take n v) -> skew_dominate sh u v.
Lemma skew_dominate_no_overlap sh u v :
size u <= sh -> skew_dominate sh u v.
Lemma skew_dominate_consl sh l u v :
skew_dominate sh u v -> skew_dominate sh.+1 (l :: u) v.
Lemma skew_dominate_cut sh u v :
skew_dominate sh u v = skew_dominate sh u (take (size u - sh) v).
Fixpoint is_skew_tableau inner t :=
if t is t0 :: t'
then [&& head 0 inner + size t0 != 0,
is_row t0,
skew_dominate ((head 0 inner) - (head 0 (behead inner)))
(head [::] t') t0 & is_skew_tableau (behead inner) t']
else inner == [::].
Lemma is_skew_tableauP inner t :
reflect
[/\ size inner <= size t,
forall i, i < size t -> nth 0 inner i + size (nth [::] t i) != 0,
forall i, is_row (nth [::] t i) &
forall i, skew_dominate ((nth 0 inner i) - (nth 0 inner i.+1))
(nth [::] t i.+1) (nth [::] t i)]
(is_skew_tableau inner t).
Lemma is_skew_tableau0 : is_skew_tableau [::] =1 is_tableau.
Lemma is_skew_tableau_pad0 inner t :
is_skew_tableau inner t = is_skew_tableau (pad 0 (size t) inner) t.
Definition skew_reshape (inner outer : seq nat) (s : seq T) :=
rev (reshape (rev (outer / inner)) s).
Lemma size_skew_reshape inner outer s :
size (skew_reshape inner outer s) = size outer.
Lemma shape_skew_reshape inner outer s :
included inner outer ->
size s = sumn (outer / inner) ->
shape (skew_reshape inner outer s) = outer / inner.
Lemma to_word_skew_reshape inner outer s :
included inner outer ->
size s = sumn (outer / inner) ->
to_word (skew_reshape inner outer s) = s.
Lemma skew_reshapeK inner t :
size inner <= size t ->
skew_reshape inner (outer_shape inner (shape t)) (to_word t) = t.
Lemma row_hb_strip inner t :
is_part inner ->
is_skew_tableau inner t -> is_row (to_word t) ->
hb_strip inner (outer_shape inner (shape t)).
Lemma hb_strip_rowE inner outer u :
is_part inner -> is_part outer ->
is_row u -> size u = sumn (outer / inner) ->
included inner outer &&
is_skew_tableau inner (skew_reshape inner outer u) =
hb_strip inner outer.
End Dominate.
Section FilterLeqGeq.
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type l : T.
Implicit Type r w : seq T.
Implicit Type t : seq (seq T).
Lemma filter_le_dominate n r1 r0 :
is_row r0 -> is_row r1 -> dominate r1 r0 ->
skew_dominate ((count (>%O n) r0) - (count (>%O n) r1))
(filter (<=%O n) r1) (filter (<=%O n) r0).
Definition filter_le_tab n :=
[fun t : (seq (seq T)) => [seq [seq x <- i | (n <= x)%O] | i <- t]].
Lemma is_skew_tableau_filter_le_tmp n t :
is_tableau t -> is_skew_tableau
(shape ([seq [seq x <- i | (x < n)%O] | i <- t]))
(filter_le_tab n t).
Lemma filter_gt_first_row0 n r t :
is_tableau t ->
dominate (head [::] t) r ->
[seq x <- r | (x < n)%O] = [::] ->
[seq [seq x <- i | (n <= x)%O] | i <- t] = t.
Lemma filter_le_first_row0 n r t :
is_tableau t ->
dominate (head [::] t) r ->
[seq x <- r | (x < n)%O] = [::] ->
[seq [seq x <- i | (x < n)%O] | i <- t] = nseq (size t) [::].
Lemma included_shape_filter_gt c (t : seq (seq T)) :
is_tableau t -> included (shape (filter_gt_tab c t)) (shape t).
Lemma shape_inner_filter_le n t :
is_tableau t ->
shape ([seq [seq x <- i | (x < n)%O] | i <- t]) =
pad 0 (size t) (shape (filter_gt_tab n t)).
Lemma is_skew_tableau_filter_le n t:
is_tableau t ->
is_skew_tableau (shape (filter_gt_tab n t)) (filter_le_tab n t).
Definition join_tab s t :=
[seq pr.1 ++ pr.2 | pr <- zip (pad [::] (size t) s) t].
Lemma size_join_tab s t :
size s <= size t ->
size_tab (join_tab s t) = size_tab s + size_tab t.
Lemma shape_join_tab s t :
shape (join_tab s t) =
([seq pr.1 + pr.2 | pr <- zip (pad 0 (size t) (shape s)) (shape t)])%N.
Lemma perm_join_tab s t :
size s <= size t ->
perm_eq (to_word (join_tab s t)) (to_word s ++ to_word t).
Lemma join_tab_filter n t :
is_tableau t -> join_tab (filter_gt_tab n t) (filter_le_tab n t) = t.
Lemma all_allLtn_cat (s0 s1 s : seq T) :
all (allLtn (s0 ++ s1)) s -> all (allLtn s0) s /\ all (allLtn s1) s.
Lemma shape_join_tab_skew_reshape t sh w :
included (shape t) sh ->
size w = sumn (sh / (shape t)) ->
shape (join_tab t (skew_reshape (shape t) sh w)) = sh.
Lemma join_tab_skew s t :
all (allLtn (to_word s)) (to_word t) ->
is_tableau s -> is_skew_tableau (shape s) t ->
is_tableau (join_tab s t).
End FilterLeqGeq.
Variables (disp : unit) (T : inhOrderType disp).
Implicit Type l : T.
Implicit Type r w : seq T.
Implicit Type t : seq (seq T).
Lemma filter_le_dominate n r1 r0 :
is_row r0 -> is_row r1 -> dominate r1 r0 ->
skew_dominate ((count (>%O n) r0) - (count (>%O n) r1))
(filter (<=%O n) r1) (filter (<=%O n) r0).
Definition filter_le_tab n :=
[fun t : (seq (seq T)) => [seq [seq x <- i | (n <= x)%O] | i <- t]].
Lemma is_skew_tableau_filter_le_tmp n t :
is_tableau t -> is_skew_tableau
(shape ([seq [seq x <- i | (x < n)%O] | i <- t]))
(filter_le_tab n t).
Lemma filter_gt_first_row0 n r t :
is_tableau t ->
dominate (head [::] t) r ->
[seq x <- r | (x < n)%O] = [::] ->
[seq [seq x <- i | (n <= x)%O] | i <- t] = t.
Lemma filter_le_first_row0 n r t :
is_tableau t ->
dominate (head [::] t) r ->
[seq x <- r | (x < n)%O] = [::] ->
[seq [seq x <- i | (x < n)%O] | i <- t] = nseq (size t) [::].
Lemma included_shape_filter_gt c (t : seq (seq T)) :
is_tableau t -> included (shape (filter_gt_tab c t)) (shape t).
Lemma shape_inner_filter_le n t :
is_tableau t ->
shape ([seq [seq x <- i | (x < n)%O] | i <- t]) =
pad 0 (size t) (shape (filter_gt_tab n t)).
Lemma is_skew_tableau_filter_le n t:
is_tableau t ->
is_skew_tableau (shape (filter_gt_tab n t)) (filter_le_tab n t).
Definition join_tab s t :=
[seq pr.1 ++ pr.2 | pr <- zip (pad [::] (size t) s) t].
Lemma size_join_tab s t :
size s <= size t ->
size_tab (join_tab s t) = size_tab s + size_tab t.
Lemma shape_join_tab s t :
shape (join_tab s t) =
([seq pr.1 + pr.2 | pr <- zip (pad 0 (size t) (shape s)) (shape t)])%N.
Lemma perm_join_tab s t :
size s <= size t ->
perm_eq (to_word (join_tab s t)) (to_word s ++ to_word t).
Lemma join_tab_filter n t :
is_tableau t -> join_tab (filter_gt_tab n t) (filter_le_tab n t) = t.
Lemma all_allLtn_cat (s0 s1 s : seq T) :
all (allLtn (s0 ++ s1)) s -> all (allLtn s0) s /\ all (allLtn s1) s.
Lemma shape_join_tab_skew_reshape t sh w :
included (shape t) sh ->
size w = sumn (sh / (shape t)) ->
shape (join_tab t (skew_reshape (shape t) sh w)) = sh.
Lemma join_tab_skew s t :
all (allLtn (to_word s)) (to_word t) ->
is_tableau s -> is_skew_tableau (shape s) t ->
is_tableau (join_tab s t).
End FilterLeqGeq.
Section EqInvSkewTab.
Lemma eq_inv_skew_dominate
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 v1 : seq T1) (u2 v2 : seq T2) s :
eq_inv (u1 ++ v1) (u2 ++ v2) ->
size u1 = size u2 ->
skew_dominate s u1 v1 -> skew_dominate s u2 v2.
Lemma eq_inv_is_skew_tableau_reshape_size
inner outer
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 : seq T1) (u2 : seq T2) :
size inner = size outer ->
eq_inv u1 u2 -> size u1 = sumn (outer / inner) ->
is_skew_tableau inner (skew_reshape inner outer u1) ->
is_skew_tableau inner (skew_reshape inner outer u2).
Lemma is_skew_tableau_skew_reshape_pad0 inner outer
(d : unit) (T : inhOrderType d) (u : seq T) :
is_skew_tableau inner (skew_reshape inner outer u) =
is_skew_tableau ((pad 0 (size outer)) inner)
(skew_reshape ((pad 0 (size outer)) inner) outer u).
Theorem eq_inv_is_skew_tableau_reshape
inner outer
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 : seq T1) (u2 : seq T2) :
size inner <= size outer ->
eq_inv u1 u2 ->
size u1 = sumn (outer / inner) ->
is_skew_tableau inner (skew_reshape inner outer u1) ->
is_skew_tableau inner (skew_reshape inner outer u2).
Theorem is_skew_tableau_reshape_std inner outer
(d : unit) (T : inhOrderType d) (u : seq T) :
size inner <= size outer ->
size u = sumn (outer / inner) ->
is_skew_tableau inner (skew_reshape inner outer u) =
is_skew_tableau inner (skew_reshape inner outer (std u)).
Theorem is_tableau_reshape_std sh
(d : unit) (T : inhOrderType d) (u : seq T) :
size u = sumn sh ->
is_tableau (skew_reshape [::] sh u) =
is_tableau (skew_reshape [::] sh (std u)).
Theorem is_tableau_std (d : unit) (T : inhOrderType d) (t : seq (seq T)) :
is_tableau t = is_tableau (skew_reshape [::] (shape t) (std (to_word t))).
End EqInvSkewTab.
Lemma eq_inv_skew_dominate
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 v1 : seq T1) (u2 v2 : seq T2) s :
eq_inv (u1 ++ v1) (u2 ++ v2) ->
size u1 = size u2 ->
skew_dominate s u1 v1 -> skew_dominate s u2 v2.
Lemma eq_inv_is_skew_tableau_reshape_size
inner outer
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 : seq T1) (u2 : seq T2) :
size inner = size outer ->
eq_inv u1 u2 -> size u1 = sumn (outer / inner) ->
is_skew_tableau inner (skew_reshape inner outer u1) ->
is_skew_tableau inner (skew_reshape inner outer u2).
Lemma is_skew_tableau_skew_reshape_pad0 inner outer
(d : unit) (T : inhOrderType d) (u : seq T) :
is_skew_tableau inner (skew_reshape inner outer u) =
is_skew_tableau ((pad 0 (size outer)) inner)
(skew_reshape ((pad 0 (size outer)) inner) outer u).
Theorem eq_inv_is_skew_tableau_reshape
inner outer
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 : seq T1) (u2 : seq T2) :
size inner <= size outer ->
eq_inv u1 u2 ->
size u1 = sumn (outer / inner) ->
is_skew_tableau inner (skew_reshape inner outer u1) ->
is_skew_tableau inner (skew_reshape inner outer u2).
Theorem is_skew_tableau_reshape_std inner outer
(d : unit) (T : inhOrderType d) (u : seq T) :
size inner <= size outer ->
size u = sumn (outer / inner) ->
is_skew_tableau inner (skew_reshape inner outer u) =
is_skew_tableau inner (skew_reshape inner outer (std u)).
Theorem is_tableau_reshape_std sh
(d : unit) (T : inhOrderType d) (u : seq T) :
size u = sumn sh ->
is_tableau (skew_reshape [::] sh u) =
is_tableau (skew_reshape [::] sh (std u)).
Theorem is_tableau_std (d : unit) (T : inhOrderType d) (t : seq (seq T)) :
is_tableau t = is_tableau (skew_reshape [::] (shape t) (std (to_word t))).
End EqInvSkewTab.