Library Combi.LRrule.Schensted: The Robinson-Schensted correspondence
The Robinson-Schensted correspondence
- inspred r l i == l bump the i letter of r
- bump r l == l bump when inserted in r
- mininspred r l == the position of the letter bumped by l
- inspos r l == the position of the letter bumped by l defined recursively
- insmin r l == the insertion of l in r defined using mininspred
- insrow r l == the insertion of l in r defined resursively
- ins r l == the insertion of l in r defined using inspos
- Sch w == Schented algorithm applied to w
- subseqrow s w == s is a nondeceasing subsequence of w
- subseqrow_n s w n == s is a nondeceasing subsequence of w of size n
- Corollary size_ndec_Sch : subseqrow s w -> (size s) <= size (Sch w).
- Corollary exist_size_Sch w : exists s : seq T, subseqrow_n s w (size (Sch w)).
- bumped r l == the letter bumped by l when inserted in r, l itself if there is no bumping
- bumprow r l == bump l in r of type (option T) * (seq T)
- instab t l == insert the letter l in the tableau t
- RS w == the insertion tableau (P-symbol) of w. It is a tableau as stated in Theorem is_tableau_RS.
- invbump b s == b has been bumped by s that is head b s < b
- invbumprow b s == the inverse bumping of b in the row s. The result is a pair (r, l) such that bumprow r l give back (some b, s). This is lemma bumprowinvK.
- invins b s == the r in (r, l) := invbumprow b s
- invbumped b s the l in (r, l) := invbumprow b s.
- instabnrow t l == a pair (s, n) where s is the result of the insertion of l in t and n is the index of the row where the insertion stopped. As stated in Lemma instabnrowE s = instab t l.
- invinstabnrow s n == the inverse insertion, that the pair (t, l) such that
instabnrow t l = (s, n). This is Theorem invinstabnrowK. See also
Theorem instabnrowinvK.
- RSmap w == the Robinson-Schensted map where the recording tableau is returned as a Yamanouchi word.
- is_RSpair (P, Q) == P is a tableau, Q is a Yammanouchi word and the shape of P is equal to the evaluation of Q.
- RSmapinv tab yam == the Robinson-Schensted inverse map of the pair (tab, yam)
- RSmapinv2 p == the uncurrying of RSmapinv.
- Theorem RSmapK stated as RSmapinv2 (RSmap w) = w.
- and Theorem RSmapinv2K as RSmap (RSmapinv2 pair) = pair.
- Theorem perm_RS w : perm_eq w (to_word (RS w)).
- rspair T == a sigma type for RS pair with tableau in type T.
- RSbij w == the rspair T associated to w : seq T
- RSbijinv p == the seq T associated to p : rspair T
- RSclass t == the list of word w having t as RS tableau. This is stated in Lemma RSclassE which says w \in RSclass tab = (RS w == tab).
- is_RStabpair (P, Q) == P and Q are two tableau of the same shape, and Q is standard.
- rstabpair T == a sigma type for is_RStabpair.
- RStabmap w == the RS map applied to w is is a RS pair as stated in
Theorem RStabmap_spec.
- RStab w == the RS map applied to w as a rstabpair T.
- RStabinv pair == the word w associated to a rstabpair
From HB Require Import structures.
From mathcomp Require Import all_boot order.
From mathcomp Require Import perm fingroup.
Require Import tools partition Yamanouchi ordtype subseq tableau std stdtab.
Set Implicit Arguments.
Open Scope N.
Import Order.Theory.
Section NonEmpty.
Context disp (T : inhOrderType disp).
From mathcomp Require Import all_boot order.
From mathcomp Require Import perm fingroup.
Require Import tools partition Yamanouchi ordtype subseq tableau std stdtab.
Set Implicit Arguments.
Open Scope N.
Import Order.Theory.
Section NonEmpty.
Context disp (T : inhOrderType disp).
Section Insert.
Variable Row : seq T.
Hypothesis HRow : is_row Row.
Variable l : T.
Definition inspred i := (l < nth l Row i)%O.
Definition bump := (l < (last l Row))%O.
Lemma notbump : ~~bump = (l >= (last l Row))%O.
Lemma transf : bump -> (l < (nth l Row (size Row).-1))%O.
Lemma inspred_any_bump i : inspred i -> bump.
Definition mininspred : nat :=
if ltP l (last l Row) is Order.LtlNotGe Hlast
then ex_minn (ex_intro inspred (size Row).-1 (transf Hlast))
else size Row.
Definition insmin := set_nth l Row mininspred l.
Lemma bump_mininspredE (Hbump : bump) :
mininspred = ex_minn (ex_intro inspred (size Row).-1 (transf Hbump)).
Lemma nbump_mininspredE : ~~bump -> mininspred = size Row.
Fixpoint insrow r l : seq T :=
if r is l0 :: r then
if (l < l0)%O then l :: r
else l0 :: (insrow r l)
else [:: l].
Fixpoint inspos r (l : T) : nat :=
if r is l0 :: r' then
if (l < l0)%O then 0
else (inspos r' l).+1
else 0.
Notation pos := (inspos Row l).
Definition ins := set_nth l Row pos l.
Lemma inspos_leq_size : pos <= size Row.
Lemma inspos_lt_size_ins : pos < size ins.
Lemma nth_inspos_ins : nth l ins pos = l.
Lemma nbump_insposE : ~~bump -> mininspred = pos.
Lemma inspred_inspos : bump -> inspred pos.
Lemma inspred_mininspred : bump -> inspred mininspred.
Lemma nth_lt_inspos i : i < pos -> (nth l Row i <= l)%O.
Lemma inspredN_lt_inspos i : i < pos -> ~~ (inspred i).
Lemma bump_insposE : bump -> mininspred = pos.
Lemma insposE : mininspred = pos.
Lemma inspos_leq_exP i : inspred i -> pos <= i.
Lemma insE : insmin = ins.
Lemma insrowE : insmin = insrow Row l.
Lemma bump_inspos_lt_size : bump -> pos < size Row.
Lemma nbump_inspos_eq_size : ~~bump -> pos = size Row.
Lemma lt_inspos_nth i : i < size Row -> (nth l Row i <= l)%O -> i < pos.
Lemma insrow_head_lt : (head l (insrow Row l) <= l)%O.
Lemma ins_head_lt : (head l ins <= l)%O.
Lemma is_row_ins : is_row ins.
Lemma bump_size_ins : bump -> size ins = size Row.
Lemma nbump_size_ins : ~~bump -> size ins = (size Row).+1.
Lemma nbump_ins_rconsE : ~~bump -> ins = rcons Row l.
Lemma size_ins_inf : (size Row) <= size ins.
Lemma size_ins_sup : size ins <= (size Row).+1.
Lemma ins_leq i : i < size Row -> (nth l ins i <= nth l Row i)%O.
Lemma ins_non_nil : ins != [::].
Lemma size_ins_non_0 : 0 < size ins.
End Insert.
Lemma bump_nil l : bump [::] l = false.
Lemma bump_tail l0 r l : bump (l0 :: r) l -> (l0 <= l -> bump r l)%O.
Variable Row : seq T.
Hypothesis HRow : is_row Row.
Variable l : T.
Definition inspred i := (l < nth l Row i)%O.
Definition bump := (l < (last l Row))%O.
Lemma notbump : ~~bump = (l >= (last l Row))%O.
Lemma transf : bump -> (l < (nth l Row (size Row).-1))%O.
Lemma inspred_any_bump i : inspred i -> bump.
Definition mininspred : nat :=
if ltP l (last l Row) is Order.LtlNotGe Hlast
then ex_minn (ex_intro inspred (size Row).-1 (transf Hlast))
else size Row.
Definition insmin := set_nth l Row mininspred l.
Lemma bump_mininspredE (Hbump : bump) :
mininspred = ex_minn (ex_intro inspred (size Row).-1 (transf Hbump)).
Lemma nbump_mininspredE : ~~bump -> mininspred = size Row.
Fixpoint insrow r l : seq T :=
if r is l0 :: r then
if (l < l0)%O then l :: r
else l0 :: (insrow r l)
else [:: l].
Fixpoint inspos r (l : T) : nat :=
if r is l0 :: r' then
if (l < l0)%O then 0
else (inspos r' l).+1
else 0.
Notation pos := (inspos Row l).
Definition ins := set_nth l Row pos l.
Lemma inspos_leq_size : pos <= size Row.
Lemma inspos_lt_size_ins : pos < size ins.
Lemma nth_inspos_ins : nth l ins pos = l.
Lemma nbump_insposE : ~~bump -> mininspred = pos.
Lemma inspred_inspos : bump -> inspred pos.
Lemma inspred_mininspred : bump -> inspred mininspred.
Lemma nth_lt_inspos i : i < pos -> (nth l Row i <= l)%O.
Lemma inspredN_lt_inspos i : i < pos -> ~~ (inspred i).
Lemma bump_insposE : bump -> mininspred = pos.
Lemma insposE : mininspred = pos.
Lemma inspos_leq_exP i : inspred i -> pos <= i.
Lemma insE : insmin = ins.
Lemma insrowE : insmin = insrow Row l.
Lemma bump_inspos_lt_size : bump -> pos < size Row.
Lemma nbump_inspos_eq_size : ~~bump -> pos = size Row.
Lemma lt_inspos_nth i : i < size Row -> (nth l Row i <= l)%O -> i < pos.
Lemma insrow_head_lt : (head l (insrow Row l) <= l)%O.
Lemma ins_head_lt : (head l ins <= l)%O.
Lemma is_row_ins : is_row ins.
Lemma bump_size_ins : bump -> size ins = size Row.
Lemma nbump_size_ins : ~~bump -> size ins = (size Row).+1.
Lemma nbump_ins_rconsE : ~~bump -> ins = rcons Row l.
Lemma size_ins_inf : (size Row) <= size ins.
Lemma size_ins_sup : size ins <= (size Row).+1.
Lemma ins_leq i : i < size Row -> (nth l ins i <= nth l Row i)%O.
Lemma ins_non_nil : ins != [::].
Lemma size_ins_non_0 : 0 < size ins.
End Insert.
Lemma bump_nil l : bump [::] l = false.
Lemma bump_tail l0 r l : bump (l0 :: r) l -> (l0 <= l -> bump r l)%O.
Section Schensted.
Implicit Type l : T.
Implicit Type r w s : seq T.
Fixpoint Sch_rev w := if w is l0 :: w' then ins (Sch_rev w') l0 else [::].
Definition Sch w := Sch_rev (rev w).
Lemma Sch_rcons l w : Sch (rcons w l) = ins (Sch w) l.
Lemma is_row_Sch w : is_row (Sch w).
Lemma Sch_size w : size (Sch w) <= size w.
Implicit Type l : T.
Implicit Type r w s : seq T.
Fixpoint Sch_rev w := if w is l0 :: w' then ins (Sch_rev w') l0 else [::].
Definition Sch w := Sch_rev (rev w).
Lemma Sch_rcons l w : Sch (rcons w l) = ins (Sch w) l.
Lemma is_row_Sch w : is_row (Sch w).
Lemma Sch_size w : size (Sch w) <= size w.
Definition subseqrow s w := subseq s w && is_row s.
Definition subseqrow_n s w n := [&& subseq s w , (size s == n) & is_row s].
Theorem Sch_exists w i :
i < size (Sch w) ->
exists s : seq T, (last inh s == nth inh (Sch w) i) && subseqrow_n s w i.+1.
Theorem Sch_leq_last w s si:
subseqrow (rcons s si) w ->
size s < size (Sch w) /\ (nth inh (Sch w) (size s) <= si)%O.
Corollary size_ndec_Sch w s : subseqrow s w -> (size s) <= size (Sch w).
Corollary exist_size_Sch w : exists s : seq T, subseqrow_n s w (size (Sch w)).
End Schensted.
Theorem Sch_max_size (w : seq T) :
size (Sch w) = \max_(s : subseqs w | is_row s) size s.
Definition subseqrow_n s w n := [&& subseq s w , (size s == n) & is_row s].
Theorem Sch_exists w i :
i < size (Sch w) ->
exists s : seq T, (last inh s == nth inh (Sch w) i) && subseqrow_n s w i.+1.
Theorem Sch_leq_last w s si:
subseqrow (rcons s si) w ->
size s < size (Sch w) /\ (nth inh (Sch w) (size s) <= si)%O.
Corollary size_ndec_Sch w s : subseqrow s w -> (size s) <= size (Sch w).
Corollary exist_size_Sch w : exists s : seq T, subseqrow_n s w (size (Sch w)).
End Schensted.
Theorem Sch_max_size (w : seq T) :
size (Sch w) = \max_(s : subseqs w | is_row s) size s.
Section Bump.
Variable Row : seq T.
Hypothesis HRow : is_row Row.
Variable l : T.
Definition bumped := nth l Row (inspos Row l).
Notation ins := (ins Row l).
Notation inspos := (inspos Row l).
Notation insRow := (insrow Row l).
Notation bump := (bump Row l).
Lemma lt_bumped : bump -> (l < bumped)%O.
Fixpoint bumprow r l : (option T) * (seq T) :=
if r is l0 :: r then
if (l < l0)%O then (Some l0, l :: r)
else let: (lr, rr) := bumprow r l in (lr, l0 :: rr)
else (None, [:: l]).
Notation bumpRow := (bumprow Row l).
Lemma ins_bumprowE : insRow = bumpRow.2.
Lemma bump_bumprowE : bump -> bumpRow = (Some bumped, ins).
Lemma nbump_bumprowE : ~~bump -> bumpRow = (None, ins).
Lemma head_ins_lt_bumped i : bump -> (head i ins < bumped)%O.
Lemma bumprow_size :
let: (lr, tr) := bumpRow in
(size Row).+1 == (size tr) + if lr is Some _ then 1 else 0.
Lemma bumprow_count p :
let: (lr, tr) := bumpRow in
count p Row + (p l) == count p tr + if lr is Some ll then (p ll) else 0.
End Bump.
Lemma bumprow_rcons r l : is_row (rcons r l) -> bumprow r l = (None, rcons r l).
Section Dominate.
Implicit Type l : T.
Implicit Type r u v : seq T.
Lemma dominate_inspos r1 r0 l :
is_row r0 -> is_row r1 -> dominate r1 r0 ->
bump r0 l -> inspos r0 l >= inspos r1 (bumped r0 l).
Lemma bump_dominate r1 r0 l :
is_row r0 -> is_row r1 -> bump r0 l ->
dominate r1 r0 -> dominate (ins r1 (bumped r0 l)) (ins r0 l).
Lemma dominateK_inspos r1 r0 l0 :
is_row r0 -> is_row r1 -> dominate (ins r1 (bumped r0 l0)) (ins r0 l0) ->
bump r0 l0 -> inspos r0 l0 >= inspos r1 (bumped r0 l0).
Lemma bump_dominateK r1 r0 l0 :
is_row r0 -> is_row r1 -> bump r0 l0 ->
dominate (ins r1 (bumped r0 l0)) (ins r0 l0) -> dominate r1 r0.
End Dominate.
Variable Row : seq T.
Hypothesis HRow : is_row Row.
Variable l : T.
Definition bumped := nth l Row (inspos Row l).
Notation ins := (ins Row l).
Notation inspos := (inspos Row l).
Notation insRow := (insrow Row l).
Notation bump := (bump Row l).
Lemma lt_bumped : bump -> (l < bumped)%O.
Fixpoint bumprow r l : (option T) * (seq T) :=
if r is l0 :: r then
if (l < l0)%O then (Some l0, l :: r)
else let: (lr, rr) := bumprow r l in (lr, l0 :: rr)
else (None, [:: l]).
Notation bumpRow := (bumprow Row l).
Lemma ins_bumprowE : insRow = bumpRow.2.
Lemma bump_bumprowE : bump -> bumpRow = (Some bumped, ins).
Lemma nbump_bumprowE : ~~bump -> bumpRow = (None, ins).
Lemma head_ins_lt_bumped i : bump -> (head i ins < bumped)%O.
Lemma bumprow_size :
let: (lr, tr) := bumpRow in
(size Row).+1 == (size tr) + if lr is Some _ then 1 else 0.
Lemma bumprow_count p :
let: (lr, tr) := bumpRow in
count p Row + (p l) == count p tr + if lr is Some ll then (p ll) else 0.
End Bump.
Lemma bumprow_rcons r l : is_row (rcons r l) -> bumprow r l = (None, rcons r l).
Section Dominate.
Implicit Type l : T.
Implicit Type r u v : seq T.
Lemma dominate_inspos r1 r0 l :
is_row r0 -> is_row r1 -> dominate r1 r0 ->
bump r0 l -> inspos r0 l >= inspos r1 (bumped r0 l).
Lemma bump_dominate r1 r0 l :
is_row r0 -> is_row r1 -> bump r0 l ->
dominate r1 r0 -> dominate (ins r1 (bumped r0 l)) (ins r0 l).
Lemma dominateK_inspos r1 r0 l0 :
is_row r0 -> is_row r1 -> dominate (ins r1 (bumped r0 l0)) (ins r0 l0) ->
bump r0 l0 -> inspos r0 l0 >= inspos r1 (bumped r0 l0).
Lemma bump_dominateK r1 r0 l0 :
is_row r0 -> is_row r1 -> bump r0 l0 ->
dominate (ins r1 (bumped r0 l0)) (ins r0 l0) -> dominate r1 r0.
End Dominate.
Section Tableaux.
Implicit Type l : T.
Implicit Type r w : seq T.
Implicit Type t : seq (seq T).
Fixpoint instab t l : seq (seq T) :=
if t is t0 :: t' then
let: (lr, rr) := bumprow t0 l in
if lr is Some ll then rr :: (instab t' ll) else rr :: t'
else [:: [:: l]].
Lemma head_instab (t0 : seq T) t l :
is_row t0 -> head [::] (instab (t0 :: t) l) = ins t0 l.
Theorem is_tableau_instab t l : is_tableau t -> is_tableau (instab t l).
Lemma instab_non_nil t l : instab t l != [::].
Fixpoint RS_rev w : seq (seq T) :=
if w is w0 :: wr then instab (RS_rev wr) w0 else [::].
Definition RS w := RS_rev (rev w).
Theorem is_tableau_RS w : is_tableau (RS w).
End Tableaux.
Implicit Type l : T.
Implicit Type r w : seq T.
Implicit Type t : seq (seq T).
Fixpoint instab t l : seq (seq T) :=
if t is t0 :: t' then
let: (lr, rr) := bumprow t0 l in
if lr is Some ll then rr :: (instab t' ll) else rr :: t'
else [:: [:: l]].
Lemma head_instab (t0 : seq T) t l :
is_row t0 -> head [::] (instab (t0 :: t) l) = ins t0 l.
Theorem is_tableau_instab t l : is_tableau t -> is_tableau (instab t l).
Lemma instab_non_nil t l : instab t l != [::].
Fixpoint RS_rev w : seq (seq T) :=
if w is w0 :: wr then instab (RS_rev wr) w0 else [::].
Definition RS w := RS_rev (rev w).
Theorem is_tableau_RS w : is_tableau (RS w).
End Tableaux.
Section InverseBump.
Implicit Type a b l : T.
Implicit Type r s w : seq T.
Implicit Type t : seq (seq T).
Definition invbump b s := ((head b s) < b)%O.
Fixpoint invbumprow b s : (seq T) * T :=
if s is l0 :: s then
if (b <= head b s)%O
then (b :: s, l0)
else let: (rr, lr) := invbumprow b s in (l0 :: rr, lr)
else ([::], b).
Definition invins b s := (invbumprow b s).1.
Definition invbumped b s := (invbumprow b s).2.
Lemma head_lt_invins b s i :
s != [::] -> invbump b s -> (head i s <= head i (invins b s))%O.
Lemma is_row_invins b s : is_row s -> is_row (invins b s).
Lemma head_leq_invbumped b s :
s != [::] -> is_row s -> (head inh s <= (invbumped b s))%O.
Lemma invbumprowK r a :
is_row r -> bump r a ->
(invbumprow (bumped r a) (ins r a)) = (r, a).
Lemma bumprowinvK b s :
s != [::] -> is_row s -> invbump b s ->
(bumprow (invins b s) (invbumped b s)) = (Some b, s).
Implicit Type a b l : T.
Implicit Type r s w : seq T.
Implicit Type t : seq (seq T).
Definition invbump b s := ((head b s) < b)%O.
Fixpoint invbumprow b s : (seq T) * T :=
if s is l0 :: s then
if (b <= head b s)%O
then (b :: s, l0)
else let: (rr, lr) := invbumprow b s in (l0 :: rr, lr)
else ([::], b).
Definition invins b s := (invbumprow b s).1.
Definition invbumped b s := (invbumprow b s).2.
Lemma head_lt_invins b s i :
s != [::] -> invbump b s -> (head i s <= head i (invins b s))%O.
Lemma is_row_invins b s : is_row s -> is_row (invins b s).
Lemma head_leq_invbumped b s :
s != [::] -> is_row s -> (head inh s <= (invbumped b s))%O.
Lemma invbumprowK r a :
is_row r -> bump r a ->
(invbumprow (bumped r a) (ins r a)) = (r, a).
Lemma bumprowinvK b s :
s != [::] -> is_row s -> invbump b s ->
(bumprow (invins b s) (invbumped b s)) = (Some b, s).
Fixpoint instabnrow t l : seq (seq T) * nat :=
if t is t0 :: t then
let: (lr, rr) := bumprow t0 l
in if lr is Some ll then
let: (tres, nres) := instabnrow t ll
in (rr :: tres, nres.+1)
else (rr :: t, 0)
else ([:: [:: l]], 0).
Lemma instabnrowE t l : (instabnrow t l).1 = instab t l.
Lemma shape_instabnrow t l :
is_tableau t ->
let: (tr, nrow) := instabnrow t l in shape tr = incr_nth (shape t) nrow.
End InverseBump.
Section Inverse.
Implicit Type a b l : T.
Implicit Type r s w : seq T.
Implicit Type t u : seq (seq T).
Lemma is_rem_corner_instabnrow t l : is_tableau t ->
let: (res, nrow) := instabnrow t l in is_rem_corner (shape res) nrow.
if t is t0 :: t then
let: (lr, rr) := bumprow t0 l
in if lr is Some ll then
let: (tres, nres) := instabnrow t ll
in (rr :: tres, nres.+1)
else (rr :: t, 0)
else ([:: [:: l]], 0).
Lemma instabnrowE t l : (instabnrow t l).1 = instab t l.
Lemma shape_instabnrow t l :
is_tableau t ->
let: (tr, nrow) := instabnrow t l in shape tr = incr_nth (shape t) nrow.
End InverseBump.
Section Inverse.
Implicit Type a b l : T.
Implicit Type r s w : seq T.
Implicit Type t u : seq (seq T).
Lemma is_rem_corner_instabnrow t l : is_tableau t ->
let: (res, nrow) := instabnrow t l in is_rem_corner (shape res) nrow.
Fixpoint invinstabnrow t nrow : seq (seq T) * T :=
if t is t0 :: t
then if nrow is nrow.+1
then let: (tr, lr) := invinstabnrow t nrow in
let: (t0r, l0r) := invbumprow lr t0 in
(t0r :: tr, l0r)
else if t0 is l0 :: t0
then if t0 == [::]
then (t, l0)
else ((belast l0 t0) :: t, last l0 t0)
else ([::], inh)
else ([::], inh).
Theorem invinstabnrowK t l :
is_tableau t -> invinstabnrow (instab t l) (instabnrow t l).2 = (t, l).
Lemma invbump_geq_head t tin l nrow :
t != [::] -> is_tableau t -> invinstabnrow t nrow = (tin, l) ->
(l >= head l (head [::] t))%O.
Lemma invbump_dom r0 t tin l nrow :
t != [::] -> is_tableau t -> invinstabnrow t nrow = (tin, l) ->
r0 != [::] -> dominate (head [::] t) r0 -> invbump l r0.
Theorem instabnrowinvK t nrow :
is_tableau t -> t != [::] -> is_rem_corner (shape t) nrow ->
let: (tin, l) := invinstabnrow t nrow in (instabnrow tin l) = (t, nrow).
if t is t0 :: t
then if nrow is nrow.+1
then let: (tr, lr) := invinstabnrow t nrow in
let: (t0r, l0r) := invbumprow lr t0 in
(t0r :: tr, l0r)
else if t0 is l0 :: t0
then if t0 == [::]
then (t, l0)
else ((belast l0 t0) :: t, last l0 t0)
else ([::], inh)
else ([::], inh).
Theorem invinstabnrowK t l :
is_tableau t -> invinstabnrow (instab t l) (instabnrow t l).2 = (t, l).
Lemma invbump_geq_head t tin l nrow :
t != [::] -> is_tableau t -> invinstabnrow t nrow = (tin, l) ->
(l >= head l (head [::] t))%O.
Lemma invbump_dom r0 t tin l nrow :
t != [::] -> is_tableau t -> invinstabnrow t nrow = (tin, l) ->
r0 != [::] -> dominate (head [::] t) r0 -> invbump l r0.
Theorem instabnrowinvK t nrow :
is_tableau t -> t != [::] -> is_rem_corner (shape t) nrow ->
let: (tin, l) := invinstabnrow t nrow in (instabnrow tin l) = (t, nrow).
Fixpoint RSmap_rev w : (seq (seq T)) * (seq nat) :=
if w is w0 :: wtl
then let: (t, rows) := RSmap_rev wtl in
let: (tr, nrow) := instabnrow t w0 in
(tr, nrow :: rows)
else ([::], [::]).
Definition RSmap w := RSmap_rev (rev w).
Lemma RSmapE w : (RSmap w).1 = RS w.
Lemma size_RSmap2 w : size ((RSmap w).2) = size w.
Lemma is_tableau_RSmap1 w : is_tableau (RSmap w).1.
Lemma shape_RSmap_eq w : shape (RSmap w).1 = evalseq (RSmap w).2.
Lemma is_yam_RSmap2 w : is_yam (RSmap w).2.
Definition is_RSpair pair :=
let: (P, Q) := pair in
[&& is_tableau (T:=T) P, is_yam Q & (shape P == evalseq Q)].
Theorem RSmap_spec w : is_RSpair (RSmap w).
if w is w0 :: wtl
then let: (t, rows) := RSmap_rev wtl in
let: (tr, nrow) := instabnrow t w0 in
(tr, nrow :: rows)
else ([::], [::]).
Definition RSmap w := RSmap_rev (rev w).
Lemma RSmapE w : (RSmap w).1 = RS w.
Lemma size_RSmap2 w : size ((RSmap w).2) = size w.
Lemma is_tableau_RSmap1 w : is_tableau (RSmap w).1.
Lemma shape_RSmap_eq w : shape (RSmap w).1 = evalseq (RSmap w).2.
Lemma is_yam_RSmap2 w : is_yam (RSmap w).2.
Definition is_RSpair pair :=
let: (P, Q) := pair in
[&& is_tableau (T:=T) P, is_yam Q & (shape P == evalseq Q)].
Theorem RSmap_spec w : is_RSpair (RSmap w).
Fixpoint RSmapinv tab yam :=
if yam is nrow :: yam'
then let: (tr, lr) := invinstabnrow tab nrow in
rcons (RSmapinv tr yam') lr
else [::].
Definition RSmapinv2 pair := RSmapinv (pair.1) (pair.2).
Theorem RSmapK w : RSmapinv2 (RSmap w) = w.
Lemma behead_incr_nth (s : seq nat) nrow :
behead (incr_nth s nrow.+1) = incr_nth (behead s) nrow.
Lemma size_invins b s : size (invins b s) = (size s).
Lemma yam_tail_non_nil (l : nat) (s : seq nat) :
is_yam (l.+1 :: s) -> s != [::].
Lemma shape_instabnrowinv1 t nrow yam :
is_yam (nrow :: yam) -> shape t == evalseq (nrow :: yam) ->
shape (invinstabnrow t nrow).1 == evalseq yam.
Lemma head_tableau_non_nil h t : is_tableau (h :: t) -> h != [::].
Lemma is_tableau_instabnrowinv1 (s : seq (seq T)) nrow :
is_tableau s -> is_rem_corner (shape s) nrow ->
is_tableau (invinstabnrow s nrow).1.
Theorem RSmapinv2K pair : is_RSpair pair -> RSmap (RSmapinv2 pair) = pair.
End Inverse.
if yam is nrow :: yam'
then let: (tr, lr) := invinstabnrow tab nrow in
rcons (RSmapinv tr yam') lr
else [::].
Definition RSmapinv2 pair := RSmapinv (pair.1) (pair.2).
Theorem RSmapK w : RSmapinv2 (RSmap w) = w.
Lemma behead_incr_nth (s : seq nat) nrow :
behead (incr_nth s nrow.+1) = incr_nth (behead s) nrow.
Lemma size_invins b s : size (invins b s) = (size s).
Lemma yam_tail_non_nil (l : nat) (s : seq nat) :
is_yam (l.+1 :: s) -> s != [::].
Lemma shape_instabnrowinv1 t nrow yam :
is_yam (nrow :: yam) -> shape t == evalseq (nrow :: yam) ->
shape (invinstabnrow t nrow).1 == evalseq yam.
Lemma head_tableau_non_nil h t : is_tableau (h :: t) -> h != [::].
Lemma is_tableau_instabnrowinv1 (s : seq (seq T)) nrow :
is_tableau s -> is_rem_corner (shape s) nrow ->
is_tableau (invinstabnrow s nrow).1.
Theorem RSmapinv2K pair : is_RSpair pair -> RSmap (RSmapinv2 pair) = pair.
End Inverse.
Section Statistics.
Implicit Type t : seq (seq T).
Lemma size_instab t l : is_tableau t -> size_tab (instab t l) = (size_tab t).+1.
Theorem size_RS w : size_tab (RS w) = size w.
Lemma count_instab t l p :
is_tableau t -> count p (to_word (instab t l)) = (p l) + count p (to_word t).
Theorem count_RS w p : count p w = count p (to_word (RS w)).
Theorem perm_RS w : perm_eq w (to_word (RS w)).
End Statistics.
Implicit Type t : seq (seq T).
Lemma size_instab t l : is_tableau t -> size_tab (instab t l) = (size_tab t).+1.
Theorem size_RS w : size_tab (RS w) = size w.
Lemma count_instab t l p :
is_tableau t -> count p (to_word (instab t l)) = (p l) + count p (to_word t).
Theorem count_RS w p : count p w = count p (to_word (RS w)).
Theorem perm_RS w : perm_eq w (to_word (RS w)).
End Statistics.
Section Bijection.
Notation Pair := (seq (seq T) * seq nat : Type).
Structure rspair : predArgType :=
RSpair { pyampair :> Pair; _ : is_RSpair pyampair }.
Lemma pyampair_inj : injective pyampair.
Definition RSbij w := RSpair (RSmap_spec w).
Definition RSbijinv (ps : rspair) := RSmapinv2 ps.
Lemma bijRS : bijective RSbij.
End Bijection.
Notation Pair := (seq (seq T) * seq nat : Type).
Structure rspair : predArgType :=
RSpair { pyampair :> Pair; _ : is_RSpair pyampair }.
Lemma pyampair_inj : injective pyampair.
Definition RSbij w := RSpair (RSmap_spec w).
Definition RSbijinv (ps : rspair) := RSmapinv2 ps.
Lemma bijRS : bijective RSbij.
End Bijection.
Section Classes.
Definition RSclass :=
[fun tab => [seq RSmapinv2 (tab, y) | y <- enum_yameval (shape tab)] ].
Lemma RSclassP tab :
is_tableau tab -> all (fun w => RS w == tab) (RSclass tab).
Lemma RSclass_countE w : count_mem w (RSclass (RS w)) = 1.
Lemma mem_RSclass w : w \in (RSclass (RS w)).
Lemma RSclassE tab w :
is_tableau tab -> w \in RSclass tab = (RS w == tab).
End Classes.
End NonEmpty.
Definition RSclass :=
[fun tab => [seq RSmapinv2 (tab, y) | y <- enum_yameval (shape tab)] ].
Lemma RSclassP tab :
is_tableau tab -> all (fun w => RS w == tab) (RSclass tab).
Lemma RSclass_countE w : count_mem w (RSclass (RS w)) = 1.
Lemma mem_RSclass w : w \in (RSclass (RS w)).
Lemma RSclassE tab w :
is_tableau tab -> w \in RSclass tab = (RS w == tab).
End Classes.
End NonEmpty.
Lemma RSperm n (p : 'S_n) : is_stdtab (RS (wordperm p)).
Lemma RSstdE (p : seq nat) : is_stdtab (RS p) = is_std p.
Section QTableau.
Context disp (T : inhOrderType disp).
Notation TabPair := (seq (seq T) * seq (seq nat) : Type).
Definition is_RStabpair (pair : TabPair) :=
let: (P, Q) := pair in [&& is_tableau P, is_stdtab Q & (shape P == shape Q)].
Structure rstabpair : predArgType :=
RSTabPair { pqpair :> TabPair; _ : is_RStabpair pqpair }.
Lemma pqpair_inj : injective pqpair.
Definition RStabmap (w : seq T) :=
let (p, q) := (RSmap w) in (p, stdtab_of_yam q).
Lemma RStabmapE (w : seq T) : (RStabmap w).1 = RS w.
Theorem RStabmap_spec w : is_RStabpair (RStabmap w).
Lemma shape_RStabmapE (w : seq T) : shape (RStabmap w).1 = shape (RStabmap w).2.
Lemma is_stdtab_RStabmap2 (w : seq T) : is_stdtab (RStabmap w).2.
Definition RStab w := RSTabPair (RStabmap_spec w).
Definition RStabinv (pair : rstabpair) :=
let: (P, Q) := pqpair pair in RSmapinv2 (P, yam_of_stdtab Q).
Lemma RStabK : cancel RStab RStabinv.
Lemma RStabinvK : cancel RStabinv RStab.
Lemma bijRStab : bijective RStab.
End QTableau.
Section Tests.
Goal (insrow [:: 1; 1; 2; 3; 5] 2) = [:: 1; 1; 2; 2; 5].
Goal (insrow [:: 1; 1; 2; 3; 5] 2) = [:: 1; 1; 2; 2; 5].
Goal (ins [:: 1; 1; 2; 3; 5] 2) = [:: 1; 1; 2; 2; 5].
Goal (Sch [:: 2; 5; 1; 6; 4; 3]) = [:: 1; 3; 6].
Goal (RS [:: 2; 5; 1; 6; 4; 3]) = [:: [:: 1; 3; 6]; [:: 2; 4]; [:: 5]].
Goal (to_word (RS [:: 2; 5; 1; 6; 4; 3])) = [:: 5; 2; 4; 1; 3; 6].
Goal is_tableau (RS [:: 2; 5; 1; 6; 4; 3]).
Goal (invbumprow 3 [:: 1; 1; 2; 2; 5]) = ([:: 1; 1; 2; 3; 5], 2).
Goal (invbumprow 3 [:: 1; 1; 2; 2; 3]) = ([:: 1; 1; 2; 3; 3], 2).
Goal instabnrow [:: [:: 1; 3; 6]; [:: 2; 4]; [:: 5]] 3 =
([:: [:: 1; 3; 3]; [:: 2; 4; 6]; [:: 5]], 1).
Goal invinstabnrow [:: [:: 1; 3; 3]; [:: 2; 4; 6]; [:: 5]] 1 =
([:: [:: 1; 3; 6]; [:: 2; 4]; [:: 5]], 3).
Goal is_part [:: 0] = false.
Goal evalseq [::] = [::].
Goal evalseq [:: 0; 1; 2; 0; 1; 3] = [:: 2; 2; 1; 1].
Goal (RSmapinv2 (RSmap [:: 4; 1; 2; 1; 3; 2])) = [:: 4; 1; 2; 1; 3; 2].
End Tests.
Lemma RSstdE (p : seq nat) : is_stdtab (RS p) = is_std p.
Section QTableau.
Context disp (T : inhOrderType disp).
Notation TabPair := (seq (seq T) * seq (seq nat) : Type).
Definition is_RStabpair (pair : TabPair) :=
let: (P, Q) := pair in [&& is_tableau P, is_stdtab Q & (shape P == shape Q)].
Structure rstabpair : predArgType :=
RSTabPair { pqpair :> TabPair; _ : is_RStabpair pqpair }.
Lemma pqpair_inj : injective pqpair.
Definition RStabmap (w : seq T) :=
let (p, q) := (RSmap w) in (p, stdtab_of_yam q).
Lemma RStabmapE (w : seq T) : (RStabmap w).1 = RS w.
Theorem RStabmap_spec w : is_RStabpair (RStabmap w).
Lemma shape_RStabmapE (w : seq T) : shape (RStabmap w).1 = shape (RStabmap w).2.
Lemma is_stdtab_RStabmap2 (w : seq T) : is_stdtab (RStabmap w).2.
Definition RStab w := RSTabPair (RStabmap_spec w).
Definition RStabinv (pair : rstabpair) :=
let: (P, Q) := pqpair pair in RSmapinv2 (P, yam_of_stdtab Q).
Lemma RStabK : cancel RStab RStabinv.
Lemma RStabinvK : cancel RStabinv RStab.
Lemma bijRStab : bijective RStab.
End QTableau.
Section Tests.
Goal (insrow [:: 1; 1; 2; 3; 5] 2) = [:: 1; 1; 2; 2; 5].
Goal (insrow [:: 1; 1; 2; 3; 5] 2) = [:: 1; 1; 2; 2; 5].
Goal (ins [:: 1; 1; 2; 3; 5] 2) = [:: 1; 1; 2; 2; 5].
Goal (Sch [:: 2; 5; 1; 6; 4; 3]) = [:: 1; 3; 6].
Goal (RS [:: 2; 5; 1; 6; 4; 3]) = [:: [:: 1; 3; 6]; [:: 2; 4]; [:: 5]].
Goal (to_word (RS [:: 2; 5; 1; 6; 4; 3])) = [:: 5; 2; 4; 1; 3; 6].
Goal is_tableau (RS [:: 2; 5; 1; 6; 4; 3]).
Goal (invbumprow 3 [:: 1; 1; 2; 2; 5]) = ([:: 1; 1; 2; 3; 5], 2).
Goal (invbumprow 3 [:: 1; 1; 2; 2; 3]) = ([:: 1; 1; 2; 3; 3], 2).
Goal instabnrow [:: [:: 1; 3; 6]; [:: 2; 4]; [:: 5]] 3 =
([:: [:: 1; 3; 3]; [:: 2; 4; 6]; [:: 5]], 1).
Goal invinstabnrow [:: [:: 1; 3; 3]; [:: 2; 4; 6]; [:: 5]] 1 =
([:: [:: 1; 3; 6]; [:: 2; 4]; [:: 5]], 3).
Goal is_part [:: 0] = false.
Goal evalseq [::] = [::].
Goal evalseq [:: 0; 1; 2; 0; 1; 3] = [:: 2; 2; 1; 1].
Goal (RSmapinv2 (RSmap [:: 4; 1; 2; 1; 3; 2])) = [:: 4; 1; 2; 1; 3; 2].
End Tests.