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_ssreflect.
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.
Variables (disp : unit) (T : inhOrderType disp).
From mathcomp Require Import all_ssreflect.
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.
Variables (disp : unit) (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.
Variables (disp : unit) (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.
Variables (disp : unit) (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.