Library Combi.LRrule.Greene_inv: Greene subsequence theorem

Greene subsequence theorem

The goal of this file is to show that row and column Greene numbers are plactic invariants. As a consequence, for any word w, the Greene numbers of w are equal to the Greene numbers of the row reading of its insertion tableau. This ultimately allows to prove the reciprocal of Sch_plact, that is

Theorem plactic_RS u v : u =Pl v <-> RS u == RS v.

The main tool of the proof is surgery of k-supports along plactic rewriting. As a consequence, the whole file is rather technical with no external use except for the final theorems. To keep notation short while avoiding to pollute the global namespace we enclosed the different cases into Coq modules.

Here is the content of the file:

Greene numbers and duality:

The following function allows to transfer k-support through duality:

rev_ord_cast w i == size w - i : 'I_(size (revdual w))
rev_set w S == the image of S by rev_ord_cast w
rev_ksupp w P == the image of P by rev_set w
rev_ksupp_inv w == the inverse of rev_ksupp w

The Greene numbers of a word and its reversed dual agrees: Lemmas Greene_col_dual and Greene_row_dual.

Swapping two letters:

In Module Swap, we fix two words u v and two letters l0 l1. We denote x the word x := u l0 l1 v. Then we define:

pos0 u v l0 l1 == the position of l0 in x as a 'I_(size x)
pos1 u v l0 l1 == the position of l1 in x as a 'I_(size x)
swap i == exchange l0 and l1 and fixes all the other positions.
swap_set S == then image of S by swap

We prove then various lemmas such as swap_size_cover asserting that swaping keep the size of the cover.

In Module NoSetContainingBoth, we consider x := u a b v. We assume that (the position of) a and b are not in the same set of a given k-support P. We construct a k-support Q for y := u b a v of the same cover size:

swap_set S == exchange the position of a and b in S : {set 'I_(size x)} and return the result as a {set 'I_(size y)}
Q P == for a k-support P for x, then Q P is a k-support for y of the same cardinality, assuming that a and b are not in the same set of P.

The main results are lemmas ksupp_Q and size_cover_Q.

In Module SetContainingBothLeft, we denote x := u b a c v and consider a given k-support P containing both a and c. We want to deal at once with the case where a < b <= c and R := <= and c < b <= a and R := >. So we encaspulate the hypothesis in a record hypRabc which contains among other that R b c holds but not R b a. Specifically:

hypRabc R a b c == a record encapsulating that a R b R c for a total strict or non strict order R.

We construct in lemmas RabcLeqX and RabcGtnX the two records dealing with the two preceding cases.

We are looking for a k-support for y := u b c a v of the same size. To be able to apply the preceding module, we need to construct another k-support Q for x with the same cover than P, but such that a and c are not in the same set. There are two cases:

1- if b is not in cover P: We define:

Qbnotin P == P with a replaced by b. This is a still a k-support for x of the same cardinality by lemmas ksupp_bnotin and size_cover_bnotin.

2- if b is in cover P: Due to monotonic condition, b must be in a different set T in P than the set S which contains a and b. The idea is that S and T should exchange their part in c :: v. We therefore define:

S1 S T == the elements of S which are on the left of a + the elements of T which are in v S1 S T == the elements of T which are on the left of b + the elements of S which are in c :: v Qbin P S T == P where we have replaced S and T by S1 and T1. It is a k-support for x (Lemma ksupp_bin) with the same cover than p (Lemma cover_bin).

Then we prove consecutively two theorems:

SetContainingBothLeft.exists_Q_noboth which allows to to assume that there is a k-support where no set contains both a and c.
SetContainingBothLeft.exists_Qy which find a k-support for y := u b c a v of the same size of cover.

This allow to show that each plactic rewriting rule leave the Greene numbers invariant.

We conclude by the main results:

Greene_row_invar_plactic and Greene_col_invar_plactic asserting than Greene numbers are plactic invariants.
plactic_RS which shows that the plactic classes are the fiber of the Robinson-Schensted map.
RS_rev_uniq asserting that reverting a uniq word conjugate its insertion tableau.

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm.
Require Import tools ordcast ordtype subseq partition tableau Yamanouchi stdtab.
Require Import Schensted congr plactic Greene.

Set Implicit Arguments.

Import Order.Theory.

Open Scope bool.

Section Duality.

Context {disp : unit} {Alph : inhOrderType disp}.
Let word := seq Alph.

Lemma extract_cut (N : nat) (wt : N.-tuple Alph) (i : 'I_N) (S : {set 'I_N}) :
  i \in S ->
  extract wt S =
  extract wt (S :&: [set j : 'I_N | j < i]) ++
          (tnth wt i) :: extract wt (S :&: [set j : 'I_N | j > i]).

k-Support and order duality

Implicit Type a b c : Alph.
Implicit Type u v w r : word.

Variable w : word.
Variable k : nat.

#[local] Definition rev_ord_cast : 'I_(size w) -> 'I_(size (revdual w)) :=
  (cast_ord (size_revdual w)) \o (@rev_ord _).
#[local] Definition rev_set (s : {set 'I_(size w)}) : {set 'I_(size (revdual w))} :=
  [set rev_ord_cast i | i in s].

#[local] Definition rev_ksupp (P : {set {set 'I_(size w)}}) :
  {set {set 'I_(size (revdual w))}} :=
  [set rev_set u | u in P].
#[local] Definition rev_ksupp_inv (S : {set {set 'I_(size (revdual w))}}) :
  {set {set 'I_(size w)}} :=
  [set rev_ord_cast @^-1: s | s : {set 'I_(_)} in S].

Lemma rev_ord_cast_inj : injective rev_ord_cast.

Lemma rev_set_inj : injective rev_set.

Lemma rev_ksuppK : cancel rev_ksupp rev_ksupp_inv.

Lemma rev_ksuppKV : cancel rev_ksupp_inv rev_ksupp.

#[local] Lemma irev_w i : i < size w -> size w - i.+1 < size w.

Lemma rev_enum :
  enum 'I_(size (revdual w)) = rev [seq rev_ord_cast i | i : 'I_(size w )].

Lemma extract_rev_set S :
  (extract (in_tuple (revdual w))) (rev_set S) = revdual (extract (in_tuple w) S).

Lemma is_row_dual T :
  sorted <=%O (extract (in_tuple w) T) =
  sorted <=%O (extract (in_tuple (revdual w)) (rev_set T)).

Lemma is_col_dual T :
  sorted >%O (extract (in_tuple w) T) =
  sorted >%O (extract (in_tuple (revdual w)) (rev_set T)).

Lemma size_rev_ksupp P : #|rev_ksupp P| = #|P|.

Lemma trivIset_setrev P : trivIset P = trivIset (rev_ksupp P).

Lemma rev_is_ksupp_row P :
  (P \is a k .-supp [<=%O, in_tuple w ]) =
  (rev_ksupp P \is a k .-supp [<=%O, in_tuple (revdual w)]).

Lemma rev_is_ksupp_col P :
  (P \is a k .-supp [>%O, in_tuple w ]) =
  (rev_ksupp P \is a k .-supp [>%O, in_tuple (revdual w)]).

Lemma size_cover_rev P : #|cover (rev_ksupp P)| = #|cover P|.

Lemma Greene_col_dual : Greene_col w k = Greene_col (revdual w) k.

Lemma Greene_row_dual : Greene_row w k = Greene_row (revdual w) k.

End Duality.

Swaping two letters in a word and its k-supports

Module Swap.
Section Swap.

Context {disp : unit} {Alph : inhOrderType disp}.
Let word := seq Alph.

Implicit Type a b c : Alph.
Implicit Type u v w r : word.

Variable R : rel Alph.

Variable u v : word.
Variable l0 l1 : Alph.
Let x := u ++ [:: l0; l1] ++ v.

Lemma ult : size u < size x.
Definition pos0 := Ordinal ult.
Lemma u1lt : (size u).+1 < size x.
Definition pos1 := Ordinal u1lt.

Lemma tnth_pos0 : tnth (in_tuple x) pos0 = l0.

Lemma tnth_pos1 : tnth (in_tuple x) pos1 = l1.

Lemma pos01F : (pos0 == pos1 ) = false.

Definition swap (i : 'I_(size x)) : 'I_(size x) :=
  if i == pos0 then pos1 else if i == pos1 then pos0 else i.

Lemma swap_invol : involutive swap.
Lemma swap_inj : injective swap.

Lemma swap0 : swap pos0 = pos1.
Lemma swap1 : swap pos1 = pos0.
Lemma swapL (i : 'I_(size x)) : i < size u -> swap i = i.
Lemma swapR (i : 'I_(size x)) : i > (size u).+1 -> swap i = i.

Definition swap_set :=
  [fun s : {set 'I_(size x)} => swap @: s : {set 'I_(size x)}].
Lemma swap_set_invol : involutive swap_set.
Lemma swap_set_inj : injective swap_set.

Lemma swap_cover (P : {set {set 'I_(size x)}}) :
  cover (swap_set @: P) = swap_set (cover P).

Lemma swap_size_cover (P : {set {set 'I_(size x)}}) :
  #|cover (swap_set @: P)| = #|cover P|.

Lemma enum_cut : enum 'I_(size x) =
                 [seq i <- enum 'I_(size x) | val i < size u]
                   ++ [:: pos0; pos1]
                   ++ [seq i <- enum 'I_(size x) | val i >= (size u) + 2].

Lemma size_cut_sizeu :
  size [seq i <- enum 'I_(size x) | val i < size u] = size u.

End Swap.
End Swap.

Case where no sets contains both

The goal of this module is the following: given a k-support P for the word u ++ [:: a; b] ++ v which doesn't have as subsequence containing both a and b to construct a k-support Q for u ++ [:: b; a] ++ v with the same cover size. These statements are Lemmas ksupp_Q and size_cover_Q

Module NoSetContainingBoth.

Section Case.

Context {disp : unit} {Alph : inhOrderType disp}.
Let word := seq Alph.

Implicit Type a b c : Alph.
Implicit Type u v w r : word.

Variable R : rel Alph.

Variable u v : word.
Variable a b : Alph.
Variable k : nat.
Let x := u ++ [:: a; b] ++ v.
Let y := u ++ [:: b; a] ++ v.

Variable P : {set {set 'I_(size x)}}.
Hypothesis Px : P \is a k .-supp [R , in_tuple x ].

Notation posa := (Swap.pos0 u v a b).
Notation posb := (Swap.pos1 u v a b).
Notation swapX := (@Swap.swap _ u v a b).
Notation swap_setX := (Swap.swap_set u v a b).

Hypothesis HnoBoth :
forall S : {set 'I_(size x)}, S \in P -> ~ ((posa \in S ) && (posb \in S )).

Lemma Hcast : size x = size y.

This is essentially : set cast_ord Hcast x | x in swap_setX S.

Definition swap_set : {set 'I_(size x)} -> {set 'I_(size y)} :=
(fun S : {set 'I_(size x)} => [set cast_ord Hcast x | x in S]) \o swap_setX.

This is essentially : set swap_set x | x in P

Definition Q : {set {set 'I_(size y)}} := imset swap_set (mem P).

Lemma swap_set_inj : injective swap_set.

Lemma extract_swap_set S :
S \in P -> extract (in_tuple y) (swap_set S) = extract (in_tuple x) S.

Lemma ksupp_Q : Q \is a k .-supp [R , in_tuple y ].

Lemma size_cover_Q : #|cover P| == #|cover Q|.

End Case.

End NoSetContainingBoth.

Cover surgery

Section CoverSurgery.

Variable N : nat.
Variable S : {set 'I_N}.
Variable P Q : {set {set 'I_N}}.

Lemma trivIset_coverU1 :
  trivIset P -> [disjoint S & cover P] -> trivIset (S |: P).

Lemma disjoint_cover (A B : {set 'I_N}) :
  [disjoint cover P & cover Q] -> A \in P -> B \in Q -> [disjoint A & B].

Lemma trivIset_coverU :
  trivIset P -> trivIset Q -> [disjoint cover P & cover Q] -> trivIset (P :|: Q).

Lemma trivIset_coverD1 : trivIset P -> S \in P -> [disjoint S & cover (P :\ S)].

End CoverSurgery.

Case where a set in P contains both a and c

In Module SetContainingBothLeft, we denote x := u b a c v and consider a given k-support P containing both a and c. We construct another k-support Q for x with the same cover than P, but such that a and c are not in the same set.

Module SetContainingBothLeft.

Generic order hypothesis

Section RelHypothesis.

Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type a b c : Alph.

Record hypRabc R a b c := HypRabc {
                      Rtrans : transitive R;
                      Hbc : R b c;
                      Hba : ~~ R b a;
                      Hxba : forall l, R l a -> R l b;
                      Hbax : forall l, R b l -> R a l
                  }.

Lemma RabcLeqX a b c :
  (a < b <= c)%O -> hypRabc <=%O a b c.

Lemma RabcGtnX a b c :
  (a < b <= c)%O -> hypRabc >%O c b a.

End RelHypothesis.

Section Case.

Context {disp : unit} {Alph : inhOrderType disp}.
Let word := seq Alph.

Implicit Type u v w r : word.

Variable R : rel Alph.
Variable u v : word.
Variable a b c : Alph.

Hypothesis HRabc : hypRabc R a b c.

Let x := u ++ [:: b; a; c] ++ v.

Variable k : nat.
Variable P : {set {set 'I_(size x)}}.
Hypothesis Px : P \is a k .-supp [R , in_tuple x ].

Notation posb := (Swap.pos0 u (c :: v) b a).
Notation posa := (Swap.pos1 u (c :: v) b a).
Notation swap := (@Swap.swap _ u (c :: v) b a).
Notation swap_set := (Swap.swap_set u (c :: v) b a).

Lemma u2lt : (size u).+2 < size x.
Definition posc := Ordinal u2lt.

Lemma tnth_posc : tnth (in_tuple x) posc = c.

Variable S : {set 'I_(size x)}.
Hypothesis HS : S \in P.
Hypothesis Hposa : (posa \in S).
Hypothesis Hposc : (posc \in S).

Case where b is not in cover P

Replacing a by b gives another k-support.

Section BNotIn.

Hypothesis HbNin : posb \notin (cover P ).

Lemma posbinSF : posb \in S = false.

Definition Qbnotin : {set {set 'I_(size x)}} := imset swap_set (mem P).

Lemma size_cover_bnotin : #|cover P| == #|cover Qbnotin|.

Lemma inPQE T : T != swap_set S -> T \in Qbnotin -> T \in P.

Lemma extract_swap_set T :
  T != swap_set S -> T \in Qbnotin -> sorted R (extract (in_tuple x) T).

Lemma extract_SE :
  extract (in_tuple x) S =
  (extract (in_tuple x) (S :&: [set j : 'I_(size x) | j < size u])) ++
    a :: c ::
    extract (in_tuple x) (S :&: [set j : 'I_(size x) | (size u).+2 < j]).

Lemma extract_swap_setSE :
  extract (in_tuple x) (swap_set S) =
  (extract (in_tuple x) (S :&: [set j : 'I_(size x) | j < size u])) ++
    b :: c ::
    extract (in_tuple x) (S :&: [set j : 'I_(size x) | (size u).+2 < j]).

Lemma extract_swap_set_S : sorted R (extract (in_tuple x) (swap_set S)).

Lemma ksupp_bnotin : Qbnotin \is a k .-supp [R , in_tuple x ].

Lemma Qbnotin_noboth T : T \in Qbnotin -> ~ ((posa \in T ) && (posc \in T )).

End BNotIn.

Case where b is in cover P

We assume that is is in a set T and switch the right part of S and T

Section BIn.

Variable T : {set 'I_(size x)}.
Hypothesis HT : T \in P.
Hypothesis Hposb : posb \in T.

Lemma TSneq : T != S.

Lemma TS_disjoint : [disjoint S & T].

Lemma posb_inSF : (posb \in S ) = false.

Lemma posa_inTF : (posa \in T ) = false.

Lemma posc_inTF : (posc \in T ) = false.

Definition S1 := (S :&: [set j : 'I_(size x) | j <= posa])
                   :|: (T :&: [set j : 'I_(size x) | j > posc]).
Definition T1 := (T :&: [set j : 'I_(size x) | j <= posb])
                   :|: (S :&: [set j : 'I_(size x) | j >= posc]).

Lemma S1_subsST : S1 \subset (S :|: T).

Lemma T1_subsST : T1 \subset (S :|: T).

Lemma coverS1T1 : cover [set S1; T1] = (S :|: T ).

Lemma disjointS1T1 : [disjoint S1 & T1].

Lemma ST_cover_disjoint : [disjoint S :|: T & cover (P :\: [set S; T])].

Definition Qbin : {set {set 'I_(size x)}} :=
  [set S1; T1] :|: (P :\: [set S; T]).

Lemma trivIset_Qbin : trivIset Qbin.

Lemma cover_bin : cover Qbin = cover P.

Lemma enumUltV (U V : {set 'I_(size x)}) d :
  (forall l, l \in U -> l <= d ) ->
  (forall l, l \in V -> l > d ) ->
  enum (mem (U :|: V)) = enum U ++ enum V.

Lemma extract_S1E :
  extract (in_tuple x) S1 =
  extract (in_tuple x) (S :&: [set j : 'I_(size x) | j <= posa]) ++
  extract (in_tuple x) (T :&: [set j : 'I_(size x) | j > posc]).

Lemma extract_T1E :
  extract (in_tuple x) T1 =
  extract (in_tuple x) (T :&: [set j : 'I_(size x) | j <= posb]) ++
  extract (in_tuple x) (S :&: [set j : 'I_(size x) | j >= posc]).

Lemma extract_Sa :
  extract (in_tuple x) (S :&: [set j : 'I_(size x) | j <= posa]) =
  rcons (extract (in_tuple x) (S :&: [set j : 'I_(size x) | j < posa])) a.

Lemma extract_cS :
  extract (in_tuple x) (S :&: [set j : 'I_(size x) | j >= posc]) =
  c :: extract (in_tuple x) (S :&: [set j : 'I_(size x) | j > posc]).

Lemma extract_Tb :
  extract (in_tuple x) (T :&: [set j : 'I_(size x) | j <= posb]) =
  rcons (extract (in_tuple x) (T :&: [set j : 'I_(size x) | j < posb])) b.

Lemma extract_bT :
  extract (in_tuple x) (T :&: [set j : 'I_(size x) | j >= posb]) =
  b :: extract (in_tuple x) (T :&: [set j : 'I_(size x) | j > posc]).

Lemma extract_S1 : sorted R (extract (in_tuple x) S1).

Lemma extract_T1 : sorted R (extract (in_tuple x) T1).

Lemma ksupp_bin : Qbin \is a k .-supp [R , in_tuple x ].

Lemma posaS1_bin : posa \in S1.

Lemma posaT1_bin : posb \in T1.

Lemma Qbin_noboth U : U \in Qbin -> ~ ((posa \in U ) && ((posc \in U ))).

End BIn.

Existence theorem for k-supports

Theorem exists_Q_noboth :
  exists Q : {set {set 'I_(size x)}},
    [/\ Q \is a k .-supp [R , in_tuple x ], #|cover Q| = #|cover P| &
      forall S, S \in Q -> ~ ((posa \in S ) && ((posc \in S )))].

Let x' := (u ++ [:: b]) ++ [:: a; c] ++ v.
Let y := (u ++ [:: b]) ++ [:: c; a] ++ v.

Theorem exists_Qy :
  exists Q : {set {set 'I_(size y)}},
    #|cover Q| = #|cover P| /\ Q \is a k .-supp [R , in_tuple y ].

End Case.
End SetContainingBothLeft.

Greene numbers are invariant by each plactic rules

Section GreeneInvariantsRule.

Context {disp : unit} {Alph : inhOrderType disp}.
Let word := seq Alph.

Variable u v1 w v2 : word.
Variable k : nat.

Rule: [:: c; a; b] => if (a <= b < c)%Ord then [:: [:: a; c; b]] else [::]

Lemma ksuppRow_inj_plact1i :
  v2 \in plact1i v1 -> ksupp_inj <=%O <=%O k (u ++ v1 ++ w) (u ++ v2 ++ w).

Corollary Greene_row_leq_plact1i :
  v2 \in plact1i v1 ->
  Greene_row (u ++ v1 ++ w) k <= Greene_row (u ++ v2 ++ w) k.

Rule: [:: b; a; c] => if (a < b <= c)%Ord then [:: [:: b; c; a]] else [::]

Lemma ksuppRow_inj_plact2 :
  v2 \in plact2 v1 -> ksupp_inj <=%O <=%O k (u ++ v1 ++ w) (u ++ v2 ++ w).

Corollary Greene_row_leq_plact2 :
  v2 \in plact2 v1 ->
  Greene_row (u ++ v1 ++ w) k <= Greene_row (u ++ v2 ++ w) k.

Rule: [:: a; c; b] => if (a <= b < c)%Ord then [:: [:: c; a; b]] else [::]

Lemma ksuppCol_inj_plact1 :
  v2 \in plact1 v1 -> ksupp_inj >%O >%O k (u ++ v1 ++ w) (u ++ v2 ++ w).

Corollary Greene_col_leq_plact1 :
  v2 \in plact1 v1 ->
  Greene_col (u ++ v1 ++ w) k <= Greene_col (u ++ v2 ++ w) k.

Rule: [:: b; c; a] => if (a < b <= c)%Ord then [:: [:: b; a; c]] else [::]

Lemma ksuppCol_inj_plact2i :
  v2 \in plact2i v1 -> ksupp_inj >%O >%O k (u ++ v1 ++ w) (u ++ v2 ++ w).

Corollary Greene_col_leq_plact2i :
  v2 \in plact2i v1 ->
  Greene_col (u ++ v1 ++ w) k <= Greene_col (u ++ v2 ++ w) k.

End GreeneInvariantsRule.

Deducing the other comparisons by duality

Section GreeneInvariantsDual.

Context {disp : unit} {Alph : inhOrderType disp}.
Let word := seq Alph.
Implicit Type u v w : word.

Lemma Greene_row_leq_plact2i u v1 w v2 k :
  v2 \in plact2i v1 ->
  Greene_row (u ++ v1 ++ w) k <= Greene_row (u ++ v2 ++ w) k.

Lemma Greene_row_leq_plact1 u v1 w v2 k :
  v2 \in plact1 v1 ->
  Greene_row (u ++ v1 ++ w) k <= Greene_row (u ++ v2 ++ w) k.

Lemma Greene_col_leq_plact1i u v1 w v2 k :
  v2 \in plact1i v1 ->
  Greene_col (u ++ v1 ++ w) k <= Greene_col (u ++ v2 ++ w) k.

Lemma Greene_col_leq_plact2 u v1 w v2 k :
  v2 \in plact2 v1 ->
  Greene_col (u ++ v1 ++ w) k <= Greene_col (u ++ v2 ++ w) k.

Invariance by the rules

Lemma Greene_row_invar_plact1 u v1 w v2 k :
  v2 \in plact1 v1 ->
  Greene_row (u ++ v1 ++ w) k = Greene_row (u ++ v2 ++ w) k.

Lemma Greene_row_invar_plact1i u v1 w v2 k :
  v2 \in plact1i v1 ->
  Greene_row (u ++ v1 ++ w) k = Greene_row (u ++ v2 ++ w) k.

Lemma Greene_row_invar_plact2 u v1 w v2 k :
  v2 \in plact2 v1 ->
  Greene_row (u ++ v1 ++ w) k = Greene_row (u ++ v2 ++ w) k.

Lemma Greene_row_invar_plact2i u v1 w v2 k :
  v2 \in plact2i v1 ->
  Greene_row (u ++ v1 ++ w) k = Greene_row (u ++ v2 ++ w) k.

Lemma Greene_col_invar_plact1 u v1 w v2 k :
  v2 \in plact1 v1 ->
  Greene_col (u ++ v1 ++ w) k = Greene_col (u ++ v2 ++ w) k.

Lemma Greene_col_invar_plact1i u v1 w v2 k :
  v2 \in plact1i v1 ->
  Greene_col (u ++ v1 ++ w) k = Greene_col (u ++ v2 ++ w) k.

Lemma Greene_col_invar_plact2 u v1 w v2 k :
  v2 \in plact2 v1 ->
  Greene_col (u ++ v1 ++ w) k = Greene_col (u ++ v2 ++ w) k.

Lemma Greene_col_invar_plact2i u v1 w v2 k :
  v2 \in plact2i v1 ->
  Greene_col (u ++ v1 ++ w) k = Greene_col (u ++ v2 ++ w) k.

End GreeneInvariantsDual.

Main theorem

Section GreeneInvariants.

Context {disp : unit} {Alph : inhOrderType disp}.
Let word := seq Alph.

Implicit Type a b c : Alph.
Implicit Type u v w r : word.

Row Greene number

Theorem Greene_row_invar_plactic u v :
u =Pl v -> forall k, Greene_row u k = Greene_row v k.

Corollary Greene_row_RS k w : Greene_row w k = sumn (take k (shape (RS w))).

Corollary plactic_shapeRS_row_proof u v : u =Pl v -> shape (RS u) = shape (RS v).

Column Greene number

Theorem Greene_col_invar_plactic u v :
u =Pl v -> forall k, Greene_col u k = Greene_col v k.

Corollary Greene_col_RS k w :
Greene_col w k = sumn (take k (conj_part (shape (RS w)))).

Corollary plactic_shapeRS u v : u =Pl v -> shape (RS u) = shape (RS v).

Robinson-Schensted and the plactic monoid

Theorem plactic_RS u v : u =Pl v <-> RS u == RS v.

Corollary RS_tabE (t : seq (seq Alph)) : is_tableau t -> RS (to_word t) = t.

End GreeneInvariants.

Corollary Greene_row_eq_shape_RS
          (d1 d2 : unit) (S : inhOrderType d1) (T : inhOrderType d2)
          (s : seq S) (t : seq T) :
  (forall k, Greene_row s k = Greene_row t k ) -> (shape (RS s) = shape (RS t)).

Corollary Greene_col_eq_shape_RS
          (d1 d2 : unit) (S : inhOrderType d1) (T : inhOrderType d2)
          (s : seq S) (t : seq T) :
  (forall k, Greene_col s k = Greene_col t k ) -> (shape (RS s) = shape (RS t)).

Reverting uniq words

Section RevConj.

Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type s : seq Alph.

Theorem RS_rev_uniq s : uniq s -> RS (rev s) = conj_tab (RS s).

End RevConj.