Library Combi.LRrule.shuffle: Shuffle and shifted shuffle

Shuffle, shifted shuffle and plactic classes

This file contains the core of Schützenberger proof of the Littlewood-Richardson rule. Namely, the theorem saying that the shifted shuffle of two plactic classes is a union of plactic classes. The set of those class is described by the pred_LRtriple predicate.
However, to prove the rule, instead of taking the road of plactic Schur function, we follow Duchamp-Hivert-Thibon using free Schur functions. We nevertheless prove Schützenberger theorem Schutzenberger_shuffle_plact but we don't use it.
Here are the new notions:
  • shuffle u v == the sequence of shuffling of u and v
  • shiftn n u == add n to all the entries of the sequence u
  • sfiltergtn n v == filter all the entries smaller than n in v
  • sfilterleq n v == filter and substract n to the entries of v larger than n in v
  • shsh u v == the shifted shuffle of u and v
  • langQ t == the set of words whose Q-symbol is t
The Littlewood-Richardson triple:
  • LRtriple t1 t2 t == there exists three words p1 p2 p of respective P-symbol t1 t2 t such that p appears in the shifted shuffle of p1 and p2. Otherwise said, the row reading of t appears in the shifted shuffle of the plactic classes of t1 and t2. This is an inductive proposition.
  • pred_LRtriple t1 t2 t == a predicate deciding LRtriple t1 t2 t
  • pred_LRtriple_fast t1 t2 t == a faster predicate deciding LRtriple t1 t2 t only computing the shifted shuffle of (the row reading of) t1 with the plactic class of t2
The main statement is LRtriple_cat_equiv which stats the equivalence, for two standard tableau t1 and t2 and two words u1 u2 of the right length, between the two following statements:
  • u1 \in langQ t1 /\ u2 \in langQ t2
  • exists t, LRtriple t1 t2 t /\ u1 ++ u2 \in langQ t
Then to get a first version of the LR rule, we will need to do the necessary abgebraic translation of the rule and recode the triple by some standard skew tableaux.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrbool ssrfun ssrnat eqtype finfun fintype choice.
From mathcomp Require Import order seq tuple finset perm binomial bigop.
Require Import tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab.
Require Import Schensted plactic Greene_inv stdplact.

Set Implicit Arguments.

Open Scope bool.

Import Order.TTheory.

The shuffle of two sequences

Section Defs.

Variable Alph : eqType.
Let word := seq Alph.

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

A well founded recursive definition of shuffle (a :: u) v
Fixpoint shuffle_from_rec a u shuffu' v {struct v} :=
  if v is b :: v' then
    [seq a :: w | w <- shuffu' v] ++
    [seq b :: w | w <- shuffle_from_rec a u shuffu' v']
  else [:: (a :: u)].

Fixpoint shuffle u v {struct u} :=
  if u is a :: u' then
    shuffle_from_rec a u' (shuffle u') v
  else [:: v].

Lemma shuffle_nil u : shuffle u [::] = [:: u].

Lemma size_shuffle u v :
  size (shuffle u v) = binomial ((size u) + (size v)) (size u).

Lemma shuffleC u v : perm_eq (shuffle u v) (shuffle v u).

Lemma perm_shuffle u v : all (perm_eq (u ++ v)) (shuffle u v).

Lemma all_size_shuffle u v :
  all (fun s => size s == size u + size v) (shuffle u v).

Shuffling two disjoint sequences

Lemma all_in_shufflel u v :
  predI (mem u) (mem v) =i pred0 ->
  all (fun s => filter (mem u) s == u) (shuffle u v).

Lemma all_in_shuffler u v :
  predI (mem u) (mem v) =i pred0 ->
  all (fun s => filter (mem v) s == v) (shuffle u v).

Lemma mem_shuffle_predU u v s Pu Pv:
  predI Pu Pv =i pred0 ->
  filter Pu s = u -> filter Pv s = v -> size s = size u + size v ->
  filter (predU Pu Pv) s = s.

Lemma mem_shuffle_pred u v s Pu Pv:
  predI Pu Pv =i pred0 ->
  filter Pu s = u -> filter Pv s = v -> size s = size u + size v ->
  s \in shuffle u v.

Lemma mem_shuffle u v s :
  predI (mem u) (mem v) =i pred0 ->
  [&& filter (mem u) s == u,
      filter (mem v) s == v &
      (size s == size u + size v)] = (s \in shuffle u v).

End Defs.

The shifted shuffle of two standard words

Section ShiftedShuffle.

Implicit Type u v w : seq nat.

Definition shiftn n := map (addn n).
Definition sfiltergtn n := [fun v => filter (gtn n) v].
Definition sfilterleq n := [fun v => map (subn^~ n) (filter (leq n) v)].

Lemma shiftuK n : cancel (shiftn n) (map (subn^~ n)).

Lemma sfilterleqK n v : shiftn n (sfilterleq n v) = [seq x <- v | n <= x].

Lemma sfilterleqE n u v : u = sfilterleq n v <-> shiftn n u = filter (leq n) v.

Lemma mem_sfilterleqK n v i : i \in (sfilterleq n v) = (i + n \in v).

Lemma perm_shiftn_std n s :
  is_std s -> perm_eq (shiftn n s) (iota n (size s)).

Definition shsh u v := shuffle u (shiftn (size u) v).

Lemma std_shsh u v : is_std u -> is_std v -> all is_std (shsh u v).

Lemma pred0_std u v : is_std u -> [predI u & shiftn (size u) v] =i pred0.

Lemma shsh_sfiltergtn p u v :
  is_std u -> p \in shsh u v -> u = sfiltergtn (size u) p.

Lemma shsh_sfilterleq p u v :
  is_std u -> p \in shsh u v -> v = sfilterleq (size u) p.

Lemma mem_shsh p u v :
  is_std u ->
  (p \in shsh u v) =
  ((sfiltergtn (size u) p == u) && (sfilterleq (size u) p == v)).

Lemma shift_plactcongr n u v : (u =Pl v) = (shiftn n u =Pl shiftn n v).

Schützenberger theorem

Theorem Schutzenberger_shuffle_plact u1 v1 w1 w2 :
  is_std u1 -> is_std v1 -> w1 \in shsh u1 v1 ->
  (w1 =Pl w2) ->
  exists u2 v2, [/\ u1 =Pl u2, v1 =Pl v2 & w2 \in shsh u2 v2].

End ShiftedShuffle.

Shifted shuffle and inverse standardized

Section LRTriple.

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

Implicit Type a b c : Alph.
Implicit Type u v w : word.
Implicit Type t : seq (seq nat).

Lemma perm_sfiltergtn p n :
  is_std p -> perm_eq (sfiltergtn n p) (iota 0 (minn n (size p))).

Lemma perm_sfilterleq p n :
  is_std p -> perm_eq (sfilterleq n p) (iota 0 ((size p) - n)).

Lemma size_sfiltergtn p n :
  is_std p -> size (sfiltergtn n p) = minn n (size p).
Lemma size_sfilterleq p n :
  is_std p -> size (sfilterleq n p) = (size p) - n.

Lemma sfiltergtn_is_std p n : is_std p -> is_std (sfiltergtn n p).
Lemma sfilterleq_is_std p n : is_std p -> is_std (sfilterleq n p).

Lemma size_sfiltergtn_cat u v :
  size (sfiltergtn (size u) (invstd (std (u ++ v)))) = size u.
Lemma size_sfilterleq_cat u v :
  size (sfilterleq (size u) (invstd (std (u ++ v)))) = size v.

Lemma index_leq_filter s (P : pred nat) i j :
  P i -> P j ->
  (index i (filter P s)) <= (index j (filter P s)) = (index i s <= index j s).

Lemma index_sfilterleq n s i :
  index i (sfilterleq n s) = index (i + n) (filter (leq n) s).

Lemma index_invstd l i :
  is_std l -> i < size l -> index i (invstd l) = nth inh l i.

Lemma invstd_catgtn u v :
  invstd (std u) = sfiltergtn (size u) (invstd (std (u ++ v))).

Lemma invstd_catleq u v :
  invstd (std v) = sfilterleq (size u) (invstd (std (u ++ v))).

This is essentially the product rule of FQSym
Theorem invstd_cat_in_shsh u v :
  invstd (std (u ++ v)) \in shsh (invstd (std u)) (invstd (std v)).

Free Schur functions as predicates
Definition langQ t := [pred w : word | (RStabmap w).2 == t].

Lemma langQE u t : (u \in langQ t) = (RS (invstd (std u)) == t).

Lemma size_langQ t u : u \in langQ t -> size u = size_tab t.

Littlewood-Richardson-Schützenberger triple

Inductive LRtriple t1 t2 t : Prop :=
  LRTriple :
    forall p1 p2 p, RS p1 = t1 -> RS p2 = t2 -> RS p = t ->
                    p \in shsh p1 p2 -> LRtriple t1 t2 t.
Definition pred_LRtriple (t1 t2 : seq (seq nat)) :=
  [pred t : (seq (seq nat)) |
   has (fun p => RS p == t)
       (flatten [seq shsh p1 p2 | p1 <- RSclass _ t1, p2 <- RSclass _ t2])].
Definition pred_LRtriple_fast (t1 t2 : seq (seq nat)) :=
  [pred t : (seq (seq nat)) |
   has (fun p2 => to_word t \in shsh (to_word t1) p2) (RSclass _ t2)].

Lemma LRtripleP t1 t2 t :
  is_stdtab t1 -> is_stdtab t2 ->
  reflect (LRtriple t1 t2 t) (pred_LRtriple t1 t2 t).

Lemma filter_gt_RS (d : unit) (T : inhOrderType d) (w : seq T) n :
  RS (filter (>%O n) w) = filter_gt_tab n (RS w).

Lemma pred_LRtriple_fast_filter_gt t1 t2 t :
  is_stdtab t1 -> is_stdtab t ->
  pred_LRtriple_fast t1 t2 t -> t1 = filter_gt_tab (size_tab t1) t.

Lemma LRtriple_fastE t1 t2 t :
  is_stdtab t1 -> is_stdtab t2 -> is_stdtab t ->
  pred_LRtriple t1 t2 t = pred_LRtriple_fast t1 t2 t.

Lemma is_stdtab_of_n_LRtriple t1 t2 t :
  is_stdtab t1 -> is_stdtab t2 -> LRtriple t1 t2 t ->
  is_stdtab_of_n ((size_tab t1) + (size_tab t2)) t.

Theorem LRtriple_cat_langQ t1 t2 u1 u2:
  is_stdtab t1 -> is_stdtab t2 -> u1 \in langQ t1 -> u2 \in langQ t2 ->
  LRtriple t1 t2 (RStabmap (u1 ++ u2)).2.

This is essentially the free LR rule:
The concatenation of langQ t1 and langQ t2 is the union of langQ t for t such that LRtriple t1 t2 t.
Theorem LRtriple_cat_equiv t1 t2 :
  is_stdtab t1 -> is_stdtab t2 ->
  forall u1 u2 : word,
  ( (u1 \in langQ t1 /\ u2 \in langQ t2) <->
    [/\ size u1 = size_tab t1, size u2 = size_tab t2 &
     exists t, LRtriple t1 t2 t /\ u1 ++ u2 \in langQ t] ).

A longer alternative road

In the following we goes along the proof of Schützenberger theorem but we end up duplicating the whole proof: compare the statement and proofs of
  • sfiltergtn_invstd below with invstd_catgtn
  • sfilterleq_invstd below with invstd_catleq

Lemma sfiltergtn_invstd w n :
  n <= size w -> sfiltergtn n (invstd (std w)) = invstd (std (take n w)).

Lemma sfilterleq_invstd w n :
  n <= size w -> sfilterleq n (invstd (std w)) = invstd (std (drop n w)).

Yet another form of Schützenberger theorem
Theorem LRrule_langQ t1 t2 w :
  is_stdtab t1 ->
  (exists u v, [/\ w = u ++ v, u \in langQ t1 & v \in langQ t2]) <->
  (exists t, LRtriple t1 t2 t /\ w \in langQ t).

Alternative proof from LRtriple_cat_equiv
Theorem LRrule_langQ_alternate t1 t2 w :
  is_stdtab t1 -> is_stdtab t2 ->
  (exists u v, [/\ w = u ++ v, u \in langQ t1 & v \in langQ t2]) <->
  (exists t, LRtriple t1 t2 t /\ w \in langQ t).

Conjugating LRtriple

Theorem LRtriple_conj t1 t2 t :
  is_stdtab t1 -> is_stdtab t2 -> is_stdtab t ->
  LRtriple t1 t2 t -> LRtriple (conj_tab t1) (conj_tab t2) (conj_tab t).

Theorem pred_LRtriple_conj t1 t2 t :
  is_stdtab t1 -> is_stdtab t2 -> is_stdtab t ->
  pred_LRtriple t1 t2 t = pred_LRtriple (conj_tab t1) (conj_tab t2) (conj_tab t).

End LRTriple.

Arguments langQ {disp} [Alph].