Library Combi.LRrule.implem: A Coq implementation of the Littlewood-Richarson rule

A Coq implementation of the Littlewood-Richarson rule

This file contains a Coq implementation of the Littlewood-Richardson rule. We define the following main functions:
  • LRcoeff inner eval outer == the LR coefficient
  • LRyamtab_list inner eval outer == the list of LR tableaux of shape outer/inner and evaluation eval
The following lemma assert that LRcoeff agrees with LRyamtab_list
Lemma LRcoeffP inner eval outer : size (LRyamtab_list inner eval outer) = LRcoeff inner eval outer.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg.
From mathcomp Require Import mpoly.

Require Import tools combclass partition Yamanouchi ordtype tableau.
Require Import skewtab Schur_mpoly freeSchur therule.

Set Implicit Arguments.

Open Scope N.

Lemma sorted_is_part p :
  is_part p -> sorted geq p.

Lemma is_part_pad0 n p :
  is_part p -> sorted geq (pad 0 n p).

Lemma head_row_skew_yam innev shape l r :
  is_part innev -> sorted <=%O (l :: r) ->
  is_skew_yam innev shape (l :: r) ->
  l <= head (size innev) r.

Recursive enumeration and counting function

Section OutEval.

#[local] Fixpoint add m n := if m is m'.+1 then add m' n.+1 else n.
Lemma addE : add =2 addn.

Let tsumn := foldl add 0.
Lemma tsumnE : tsumn =1 sumn.

Variable outev : seq nat.

Possible choice of a new letter:
The new letter l must satisty the following conditions:
  • mini < l < maxi
  • l is an addable corner of innev
  • adding l to innev still is inside outev
Definition one_letter_choices innev mini maxi :=
  filter
    (fun i => is_add_corner innev i && (nth 0 innev i < nth 0 outev i))
    (iota mini ((minn (size innev) maxi).+1 - mini) ).

The possible new rows which dominates the given row
Returns a seqence of pairs (r, ev) where
  • r is the new row
  • ev is the new evaluation
Fixpoint yamtab_rows innev row :=
  if row is r0 :: tlr then
    flatten [seq
               [seq (i :: res.1, incr_nth res.2 i) |
                i <- one_letter_choices res.2 r0.+1 (head (size innev) res.1)
               ] |
             res <- yamtab_rows innev tlr ]
  else [:: ([::], innev) ].

The possible new rows which are at the bottom of the shape
  • maxi is the maximum letter (typically the head of sol below)
  • sh is the shape of the expected rows
  • sol is the already known end of the row
Returns a seqence of pairs (r, ev) where
  • r is the new row
  • ev is the new evaluation
Fixpoint yamtab_shift innev maxi sh sol :=
  if sh is s.+1 then
    flatten [seq
               [seq (i :: res.1, incr_nth res.2 i) |
                i <- one_letter_choices res.2 0 (head maxi res.1)
               ] |
             res <- yamtab_shift innev maxi s sol ]
  else [:: (sol, innev) ].

Recursive step of the enumeration functions
Compute the list of skew tableaux
  • of evaluation outev-innev
  • whose row reading is a innev-skew Yamanouchi word
  • of shape outer/inner
  • which are legitimate skew tableaux if lied over row0 shifted by sh0
Fixpoint LRyamtab_list_rec innev inner outer sh0 row0 :=
  if outer is out0 :: out then
    let inn0 := head 0 inner in let inn := behead inner in
    
    let call_rec row := LRyamtab_list_rec row.2 inn out inn0 row.1 in
    let rowres := yamtab_rows innev (take (out0 - sh0) row0) in
    let rows :=
        flatten [seq yamtab_shift res.2 (head (size innev) res.1)
                     ((minn sh0 out0) - inn0) res.1
                | res <- rowres ] in
    flatten [seq [seq row.1 :: tab | tab <- call_rec row ] | row <- rows ]
  else [:: [::]].

Recursive step of the counting functions
Compute the number of skew tableaux
  • of evaluation outev-innev
  • whose row reading is a innev-skew Yamanouchi word
  • of shape outer/inner
  • which are legitimate skew tableaux if lied over row0 shifted by sh0
Fixpoint LRyamtab_count_rec innev inner outer sh0 row0 :=
  if outer is out0 :: out then
    let inn0 := head 0 inner in let inn := behead inner in
    
    let call_rec row := LRyamtab_count_rec row.2 inn out inn0 row.1 in
    let rowres := yamtab_rows innev (take (out0 - sh0) row0) in
    tsumn [seq tsumn [seq call_rec row |
                      row <- yamtab_shift res.2 (head (size innev) res.1)
                          ((minn sh0 out0) - inn0) res.1 ]
          | res <- rowres ]
  else 1.

Lemma size_LRyamtab_listE innev inner outer sh0 row0 :
  size (LRyamtab_list_rec innev inner outer sh0 row0) =
  LRyamtab_count_rec innev inner outer sh0 row0.

Basic lemmas
Lemma yamtab_shift_drop innev maxi sh y :
  forall res shape, (res, shape) \in yamtab_shift innev maxi sh y ->
  drop sh res = y.

LRyamtab_list_rec returns only Yamanouchi words

Lemma one_letter_choicesP innev mini maxi :
  forall i, i \in one_letter_choices innev mini maxi ->
  is_skew_yam innev (incr_nth innev i) [:: i].

Lemma yamtab_rowsP innev row :
  forall res shape, (res, shape) \in yamtab_rows innev row ->
  is_skew_yam innev shape res.

Lemma yamtab_shiftP innev maxi sh row shrow :
  is_skew_yam innev shrow row ->
  forall res shape, (res, shape) \in yamtab_shift shrow maxi sh row ->
  is_skew_yam innev shape res.

Lemma LRyamtab_list_recP innev inner outer sh0 row0 y :
  is_yam_of_eval innev y ->
  forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 ->
  is_yam (to_word res ++ y).

LRyamtab_list_rec returns words whose evaluation in included in outev

Lemma one_letter_included innev mini maxi :
  included innev outev ->
  forall i, i \in one_letter_choices innev mini maxi ->
                  included (incr_nth innev i) outev.

Lemma yamtab_rows_included innev row :
  included innev outev ->
  forall res shape, (res, shape) \in yamtab_rows innev row ->
  included shape outev.

Lemma yamtab_shift_included innev maxi sh y :
  included innev outev ->
  forall res shape, (res, shape) \in yamtab_shift innev maxi sh y ->
  included shape outev.

Lemma LRyamtab_list_included innev inner outer sh0 row0 y :
  included innev outev ->
  is_yam_of_eval innev y ->
  forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 ->
  included (evalseq (to_word res ++ y)) outev.

LRyamtab_list_rec returns fillings of skew shape inner/outer

Lemma yamtab_rows_size innev row :
  forall res shape, (res, shape) \in yamtab_rows innev row ->
  size res = size row.

Lemma yamtab_shift_size innev maxi sh y :
  forall res shape, (res, shape) \in yamtab_shift maxi innev sh y ->
  size res = sh + size y.

Lemma LRyamtab_list_pad0 innev inner outer sh0 row0 :
      LRyamtab_list_rec innev inner outer sh0 row0 =
      LRyamtab_list_rec innev (pad 0 (size outer) inner) outer sh0 row0.

Lemma LRyamtab_list_size innev inner outer sh0 row0 :
  forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 ->
  size res = size outer.

inner is padded with 0
Lemma LRyamtab_list_shape0 innev inner outer sh0 row0 :
  sorted geq (sh0 :: inner) -> is_part (sh0 + size row0 :: outer) ->
  included inner outer -> size inner = size outer ->
  forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 ->
  shape res = outer / inner.

LRyamtab_list_rec returns legitimate skew_tableaux

Lemma yamtab_rows_dominate innev row :
  forall res shape, (res, shape) \in yamtab_rows innev row ->
  dominate res row.

Lemma yamtab_shift_dominate innev maxi sh row y :
  dominate y row ->
  forall res shape, (res, shape) \in yamtab_shift innev maxi sh y ->
  skew_dominate sh res row.

Lemma yamtab_rows_is_row innev row :
  forall res shape, (res, shape) \in yamtab_rows innev row ->
  is_row res.

Lemma yamtab_shift_is_row innev maxi sh y :
  is_row y ->
  forall res shape, (res, shape) \in yamtab_shift innev maxi sh y ->
  is_row res.

inner is padded with 0
Lemma LRyamtab_list_skew_tableau0 innev inner outer sh0 row0 :
  sorted geq (sh0 :: inner) -> is_part (sh0 + size row0 :: outer) ->
  included inner outer -> size inner = size outer ->
  is_row row0 ->
  forall res, res \in LRyamtab_list_rec innev inner outer sh0 row0 ->
  is_skew_tableau (sh0 :: inner) (row0 :: res).

Mutiplicities are all one

Lemma choose_one_countE shr innev shape mini maxi row l :
  is_part innev ->
  is_skew_yam innev shr row ->
  is_skew_yam innev shape (l :: row) ->
  included shape outev ->
  mini <= l <= maxi ->
  is_row (l :: row) ->
  (count_mem l) (one_letter_choices shr mini maxi) = 1.

Lemma yamtab_rows_countE innev shape row base :
  is_part innev ->
  size row = size base ->
  dominate row base ->
  is_row row ->
  is_skew_yam innev shape row ->
  included shape outev ->
  count (preim (fst (B:=seq nat)) (pred1 row))
        (yamtab_rows innev base) = 1.

Lemma yamtab_shift_countE inn0 innev shape sh row sol :
  is_part inn0 ->
  is_row (row ++ sol) ->
  size row = sh ->
  is_skew_yam inn0 innev sol ->
  is_skew_yam innev shape row ->
  included shape outev ->
  count (preim (fst (B:=seq nat)) (pred1 (row ++ sol)))
        (yamtab_shift innev (head (size inn0) sol) sh sol) = 1.

Lemma LRyamtab_list_countE innev inner sh0 row0 yamtab :
  is_part innev ->
  sorted geq (sh0 :: inner) ->
  is_part (sh0 + size row0 :: (outer_shape inner (shape yamtab))) ->
  size inner = size yamtab ->
  is_skew_tableau (sh0 :: inner) (row0 :: yamtab) ->
  is_skew_yam innev outev (to_word yamtab) ->
  count_mem yamtab
    (LRyamtab_list_rec innev inner (outer_shape inner (shape yamtab)) sh0 row0) = 1.

End OutEval.

The main functions

Definition LRyamtab_list inner eval outer :=
  LRyamtab_list_rec eval [::] inner outer (head 1 outer) [::].
Definition LRcoeff inner eval outer :=
  LRyamtab_count_rec eval [::] inner outer (head 1 outer) [::].

Lemma LRcoeffP inner eval outer :
  size (LRyamtab_list inner eval outer) = LRcoeff inner eval outer.

Lemma LRyamtab_yam inner eval outer tab:
  tab \in (LRyamtab_list inner eval outer) -> is_yam (to_word tab).

Lemma LRyamtab_included inner eval outer tab:
  tab \in (LRyamtab_list inner eval outer) -> included (evalseq (to_word tab)) eval.

Lemma LRyamtab_shape inner eval outer tab :
  is_part inner -> is_part outer -> included inner outer ->
  tab \in (LRyamtab_list inner eval outer) -> shape tab = outer / inner.

Lemma LRyamtab_skew_tableau inner eval outer tab :
  is_part inner -> is_part outer -> included inner outer ->
  tab \in (LRyamtab_list inner eval outer) -> is_skew_tableau inner tab.

Lemma LRyamtab_eval inner eval outer tab:
  is_part inner -> is_part outer -> included inner outer ->
  is_part eval -> sumn eval = sumn (outer / inner) ->
  tab \in (LRyamtab_list inner eval outer) -> evalseq (to_word tab) = eval.

Lemma count_mem_LRyamtab_list inner eval outer yamtab :
  is_part inner -> is_part outer -> included inner outer ->
  is_skew_tableau inner yamtab -> shape yamtab = outer / inner ->
  is_yam_of_eval eval (to_word yamtab) ->
  count_mem yamtab (LRyamtab_list inner eval outer) = 1.

The specification of the enumeration function

Section PackedSpec.

Variable inner eval outer : seq nat.

Record inputSpec :=
  InputSpec {
      inner_part : is_part inner;
      outer_part : is_part outer;
      incl : included inner outer;
      eval_part : is_part eval;
      sumn_eq : sumn eval = sumn (outer / inner)
    }.

Record outputSpec (tab : seq (seq nat)) :=
  OutputSpec {
      skew : is_skew_tableau inner tab;
      shaps_eq : shape tab = outer / inner;
      yam_to_word : is_yam (to_word tab);
      eval_eq : evalseq (to_word tab) = eval
    }.

Lemma outputSpecP tab :
  inputSpec -> tab \in (LRyamtab_list inner eval outer) -> outputSpec tab.

Lemma outputSpec_count_mem tab :
  inputSpec -> outputSpec tab -> count_mem tab (LRyamtab_list inner eval outer) = 1.

End PackedSpec.

The specification on sigma types

Section Spec.

Variables d1 d2 : nat.
Variables (P1 : 'P_d1) (P2 : 'P_d2).
Variable P : 'P_(d1 + d2).
Hypothesis Hincl : included P1 P.

Lemma LRyamtabP tab :
  tab \in (LRyamtab_list P1 P2 P) -> is_yam_of_eval P2 (to_word tab).

Lemma LRyamtab_all :
  all (is_yam_of_eval P2) (map to_word (LRyamtab_list P1 P2 P)).
Definition LRyam_list :=
  subType_seq (yameval P2) (map to_word (LRyamtab_list P1 P2 P)).

Lemma LRyamtab_spec_recip yam :
  yam \in LRyam_set P1 P2 P ->
  count_mem (val yam) (map to_word (LRyamtab_list P1 P2 P)) = 1.

Lemma LRyam_spec_recip yam :
  yam \in LRyam_set P1 P2 P -> count_mem yam LRyam_list = 1.

Theorem LRcoeffE : LRyam_coeff P1 P2 P = LRcoeff P1 P2 P.

End Spec.

From mathcomp Require Import ssralg.

Back to the rule

Section LR.

Variables d1 d2 : nat.
Variables (P1 : 'P_d1) (P2 : 'P_d2).

#[local] Open Scope ring_scope.
Import GRing.Theory.

Variable (n0 : nat) (R : comRingType).
#[local] Notation n := (n0.+1).
Notation Schur p := (Schur n0 R p).

Theorem LRtab_coeffP :
  Schur P1 * Schur P2 =
  \sum_(P : 'P_(d1 + d2) | included P1 P) Schur P *+ LRcoeff P1 P2 P.

End LR.