Library Combi.LRrule.plactic: The plactic monoid
The plactic monoid
- plact1 == rewriting rule acb -> cab if a <= b < c
- plact1i == rewriting rule cab -> acb if a <= b < c
- plact2 == rewriting rule bac -> bca if a < b <= c
- plact2i == rewriting rule bca -> bac if a < b <= c
- plactrule == the union of the four preceding rewriting rules
- plactcongr == the plactic congruence
- a =Pl b == a and b are plactic equivalent
- revdual s == rev s : seq Dual considered on the dual alphabet
- from_revdual ds == rev ds where ds : seq Dual
- Theorem congr_RS w : w =Pl (to_word (RS w)).
- Corollary Sch_plact u v : RS u == RS v -> u =Pl v.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm.
Require Import tools partition ordtype tableau stdtab Schensted congr.
Set Implicit Arguments.
Open Scope bool.
Import Order.Theory.
Section Defs.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w : word.
Definition plact1 :=
fun s => match s return seq word with
| [:: a; c; b] => if (a <= b < c)%O then [:: [:: c; a; b]] else [::]
| _ => [::]
end.
Definition plact1i :=
fun s => match s return seq word with
| [:: c; a; b] => if (a <= b < c)%O then [:: [:: a; c; b]] else [::]
| _ => [::]
end.
Definition plact2 :=
fun s => match s return seq word with
| [:: b; a; c] => if (a < b <= c)%O then [:: [:: b; c; a]] else [::]
| _ => [::]
end.
Definition plact2i :=
fun s => match s return seq word with
| [:: b; c; a] => if (a < b <= c)%O then [:: [:: b; a; c]] else [::]
| _ => [::]
end.
Lemma plact1P u v :
reflect (exists a b c,
[/\ (a <= b < c)%O, u = [:: a; c; b] & v = [:: c; a; b] ] )
(v \in plact1 u).
Lemma plact1iP u v :
reflect (exists a b c,
[/\ (a <= b < c)%O, v = [:: a; c; b] & u = [:: c; a; b] ] )
(v \in plact1i u).
Lemma plact2P u v :
reflect (exists a b c,
[/\ (a < b <= c)%O, u = [:: b; a; c] & v = [:: b; c; a] ] )
(v \in plact2 u).
Lemma plact2iP u v :
reflect (exists a b c,
[/\ (a < b <= c)%O, v = [:: b; a; c] & u = [:: b; c; a] ] )
(v \in plact2i u).
Lemma plact1I u v : u \in plact1 v <-> v \in plact1i u.
Lemma plact2I u v : u \in plact2 v <-> v \in plact2i u.
Definition plactrule := [fun s => plact1 s ++ plact1i s ++ plact2 s ++ plact2i s].
Lemma plactruleP u v :
reflect ([\/ v \in plact1 u, v \in plact1i u, v \in plact2 u | v \in plact2i u ])
(v \in plactrule u).
Lemma plactrule_sym u v : v \in (plactrule u) -> u \in (plactrule v).
Lemma plact1_homog : forall u : word, all (perm_eq u) (plact1 u).
Lemma plact1i_homog : forall u : word, all (perm_eq u) (plact1i u).
Lemma plact2_homog : forall u : word, all (perm_eq u) (plact2 u).
Lemma plact2i_homog : forall u : word, all (perm_eq u) (plact2i u).
Lemma plactrule_homog : forall u : word, all (perm_eq u) (plactrule u).
Definition plactcongr := gencongr_multhom plactrule_homog.
Lemma plact_equiv : equivalence_rel plactcongr.
Lemma plact_refl : reflexive plactcongr.
Lemma plact_sym : symmetric plactcongr.
Lemma plact_ltrans : left_transitive plactcongr.
Lemma plact_trans : transitive plactcongr.
Lemma plact_is_congr : congruence_rel plactcongr.
Definition plact_cons := congr_cons plact_is_congr.
Definition plact_rcons := congr_rcons plact_is_congr.
Definition plact_catl := congr_catl plact_is_congr.
Definition plact_catr := congr_catr plact_is_congr.
Definition plact_cat := congr_cat plact_is_congr plact_equiv.
Lemma plact_homog u v : plactcongr u v -> perm_eq u v.
Lemma size_plact u v : plactcongr u v -> size u = size v.
End Defs.
Notation "a =Pl b" := (plactcongr a b) (at level 70).
#[export] Hint Resolve plact_refl : core.
Section RowsAndCols.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Lemma plact_row u v : is_row u -> u =Pl v -> u = v.
Lemma sorted_center u v w :
sorted >%O (u ++ v ++ w) -> sorted >%O v.
Lemma plact_col u v : sorted >%O u -> u =Pl v -> u = v.
End RowsAndCols.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w : word.
Definition plact1 :=
fun s => match s return seq word with
| [:: a; c; b] => if (a <= b < c)%O then [:: [:: c; a; b]] else [::]
| _ => [::]
end.
Definition plact1i :=
fun s => match s return seq word with
| [:: c; a; b] => if (a <= b < c)%O then [:: [:: a; c; b]] else [::]
| _ => [::]
end.
Definition plact2 :=
fun s => match s return seq word with
| [:: b; a; c] => if (a < b <= c)%O then [:: [:: b; c; a]] else [::]
| _ => [::]
end.
Definition plact2i :=
fun s => match s return seq word with
| [:: b; c; a] => if (a < b <= c)%O then [:: [:: b; a; c]] else [::]
| _ => [::]
end.
Lemma plact1P u v :
reflect (exists a b c,
[/\ (a <= b < c)%O, u = [:: a; c; b] & v = [:: c; a; b] ] )
(v \in plact1 u).
Lemma plact1iP u v :
reflect (exists a b c,
[/\ (a <= b < c)%O, v = [:: a; c; b] & u = [:: c; a; b] ] )
(v \in plact1i u).
Lemma plact2P u v :
reflect (exists a b c,
[/\ (a < b <= c)%O, u = [:: b; a; c] & v = [:: b; c; a] ] )
(v \in plact2 u).
Lemma plact2iP u v :
reflect (exists a b c,
[/\ (a < b <= c)%O, v = [:: b; a; c] & u = [:: b; c; a] ] )
(v \in plact2i u).
Lemma plact1I u v : u \in plact1 v <-> v \in plact1i u.
Lemma plact2I u v : u \in plact2 v <-> v \in plact2i u.
Definition plactrule := [fun s => plact1 s ++ plact1i s ++ plact2 s ++ plact2i s].
Lemma plactruleP u v :
reflect ([\/ v \in plact1 u, v \in plact1i u, v \in plact2 u | v \in plact2i u ])
(v \in plactrule u).
Lemma plactrule_sym u v : v \in (plactrule u) -> u \in (plactrule v).
Lemma plact1_homog : forall u : word, all (perm_eq u) (plact1 u).
Lemma plact1i_homog : forall u : word, all (perm_eq u) (plact1i u).
Lemma plact2_homog : forall u : word, all (perm_eq u) (plact2 u).
Lemma plact2i_homog : forall u : word, all (perm_eq u) (plact2i u).
Lemma plactrule_homog : forall u : word, all (perm_eq u) (plactrule u).
Definition plactcongr := gencongr_multhom plactrule_homog.
Lemma plact_equiv : equivalence_rel plactcongr.
Lemma plact_refl : reflexive plactcongr.
Lemma plact_sym : symmetric plactcongr.
Lemma plact_ltrans : left_transitive plactcongr.
Lemma plact_trans : transitive plactcongr.
Lemma plact_is_congr : congruence_rel plactcongr.
Definition plact_cons := congr_cons plact_is_congr.
Definition plact_rcons := congr_rcons plact_is_congr.
Definition plact_catl := congr_catl plact_is_congr.
Definition plact_catr := congr_catr plact_is_congr.
Definition plact_cat := congr_cat plact_is_congr plact_equiv.
Lemma plact_homog u v : plactcongr u v -> perm_eq u v.
Lemma size_plact u v : plactcongr u v -> size u = size v.
End Defs.
Notation "a =Pl b" := (plactcongr a b) (at level 70).
#[export] Hint Resolve plact_refl : core.
Section RowsAndCols.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Lemma plact_row u v : is_row u -> u =Pl v -> u = v.
Lemma sorted_center u v w :
sorted >%O (u ++ v ++ w) -> sorted >%O v.
Lemma plact_col u v : sorted >%O u -> u =Pl v -> u = v.
End RowsAndCols.
Section Rev.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Lemma plact_uniq_rev u v : uniq u -> u =Pl v -> rev u =Pl rev v.
Lemma plact_uniq_revE u v : uniq u -> (u =Pl v) = (rev u =Pl rev v).
End Rev.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Lemma plact_uniq_rev u v : uniq u -> u =Pl v -> rev u =Pl rev v.
Lemma plact_uniq_revE u v : uniq u -> (u =Pl v) = (rev u =Pl rev v).
End Rev.
Section DualRule.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Definition revdual := [fun s : seq Alph => rev s : seq Alph^d].
Definition from_revdual := [fun s : seq Alph^d => (rev s) : seq Alph].
Lemma revdualK : cancel revdual from_revdual.
Lemma from_revdualK : cancel from_revdual revdual.
Lemma size_revdual u : size u = size (revdual u).
Lemma plact2dual u v :
u \in plact2 v = (revdual u \in @plact1 _ Alph^d (revdual v)).
Lemma plact1dual u v :
u \in plact1 v = (revdual u \in @plact2 _ Alph^d (revdual v)).
Lemma plact1idual u v : u \in plact1i v = (revdual u \in plact2i (revdual v)).
Lemma plact2idual u v : u \in plact2i v = (revdual u \in plact1i (revdual v)).
End DualRule.
Arguments revdual {disp Alph}.
Arguments from_revdual {disp Alph}.
Section PlactDual.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Theorem plact_revdual u v : u =Pl v -> revdual u =Pl revdual v.
Theorem plact_from_revdual (u v : seq Alph^d) :
u =Pl v -> from_revdual u =Pl from_revdual v.
Theorem plact_dualE u v : u =Pl v <-> revdual u =Pl revdual v.
Theorem plact_from_dualE (u v : seq Alph^d) :
u =Pl v <-> from_revdual u =Pl from_revdual v.
End PlactDual.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Definition revdual := [fun s : seq Alph => rev s : seq Alph^d].
Definition from_revdual := [fun s : seq Alph^d => (rev s) : seq Alph].
Lemma revdualK : cancel revdual from_revdual.
Lemma from_revdualK : cancel from_revdual revdual.
Lemma size_revdual u : size u = size (revdual u).
Lemma plact2dual u v :
u \in plact2 v = (revdual u \in @plact1 _ Alph^d (revdual v)).
Lemma plact1dual u v :
u \in plact1 v = (revdual u \in @plact2 _ Alph^d (revdual v)).
Lemma plact1idual u v : u \in plact1i v = (revdual u \in plact2i (revdual v)).
Lemma plact2idual u v : u \in plact2i v = (revdual u \in plact1i (revdual v)).
End DualRule.
Arguments revdual {disp Alph}.
Arguments from_revdual {disp Alph}.
Section PlactDual.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type u v w : word.
Theorem plact_revdual u v : u =Pl v -> revdual u =Pl revdual v.
Theorem plact_from_revdual (u v : seq Alph^d) :
u =Pl v -> from_revdual u =Pl from_revdual v.
Theorem plact_dualE u v : u =Pl v <-> revdual u =Pl revdual v.
Theorem plact_from_dualE (u v : seq Alph^d) :
u =Pl v <-> from_revdual u =Pl from_revdual v.
End PlactDual.
Section RSToPlactic.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Lemma rcons_rcons w a b : rcons (rcons w a) b = w ++ [:: a; b].
Lemma congr_row_1 r b l :
is_row (rcons r l) -> (l < b)%O -> rcons (rcons r b) l =Pl b :: rcons r l.
Lemma congr_row_2 a r l :
is_row (a :: r) -> (l < a)%O -> a :: rcons r l =Pl a :: l :: r.
Lemma set_nth_LxR L c R l pos :
(size L) = pos -> set_nth l (L ++ c :: R) pos l = L ++ l :: R.
Lemma congr_bump r l :
r != [::] -> is_row r -> bump r l -> r ++ [:: l] =Pl [:: bumped r l] ++ ins r l.
Theorem congr_RS w : w =Pl (to_word (RS w)).
Corollary Sch_plact u v : RS u == RS v -> u =Pl v .
End RSToPlactic.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Lemma rcons_rcons w a b : rcons (rcons w a) b = w ++ [:: a; b].
Lemma congr_row_1 r b l :
is_row (rcons r l) -> (l < b)%O -> rcons (rcons r b) l =Pl b :: rcons r l.
Lemma congr_row_2 a r l :
is_row (a :: r) -> (l < a)%O -> a :: rcons r l =Pl a :: l :: r.
Lemma set_nth_LxR L c R l pos :
(size L) = pos -> set_nth l (L ++ c :: R) pos l = L ++ l :: R.
Lemma congr_bump r l :
r != [::] -> is_row r -> bump r l -> r ++ [:: l] =Pl [:: bumped r l] ++ ins r l.
Theorem congr_RS w : w =Pl (to_word (RS w)).
Corollary Sch_plact u v : RS u == RS v -> u =Pl v .
End RSToPlactic.
Section RemoveBig.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Lemma rembig_plact1 u v : u \in (plact1 v) -> rembig u = rembig v.
Lemma rembig_plact1i u v : u \in (plact1i v) -> rembig u = rembig v.
Lemma rembig_plact2 u v : u \in (plact2 v) -> rembig u = rembig v.
Lemma rembig_plact2i u v : u \in (plact2i v) -> rembig u = rembig v.
Lemma rembig_plact u v : u \in (plactrule _ v) -> rembig u = rembig v.
Theorem rembig_plactcongr u v : u =Pl v -> (rembig u) =Pl (rembig v).
Lemma inspos_rcons l r b : (l < b)%O -> inspos r l = inspos (rcons r b) l.
Lemma bump_bumprow_rconsE l r b :
is_row (rcons r b) -> (l < b)%O -> bump r l ->
let: (lres, rres) := bumprow r l in
bumprow (rcons r b) l = (lres, rcons rres b).
Lemma nbump_bumprow_rconsE l r b :
is_row (rcons r b) -> (l < b)%O -> ~~bump r l ->
let: (lres, rres) := bumprow r l in bumprow (rcons r b) l = (Some b, rres).
Lemma allLeq_is_row_rcons w b :
allLeq w b -> forall row, row \in RS w -> is_row (rcons row b).
Lemma last_ins_lt r l b : (l < b -> last b r < b -> last b (ins r l) < b)%O.
Lemma bumped_lt r b l : is_row r -> (l < b -> last b r < b -> bumped r l < b)%O.
Lemma bisimul_instab t l b lb :
is_tableau t -> (l < b)%O ->
(forall row, row \in t -> is_row (rcons row b)) ->
(forall j : nat, j < lb -> (last b (nth [::] t j) < b)%O) ->
let tres := (append_nth t b lb) in
instab tres l = append_nth (instab t l) b (last_big (instab tres l) b).
Theorem rembig_RS_last_big a v :
RS (a :: v) = append_nth (RS (rembig (a :: v)))
(maxL a v)
(last_big (RS (a :: v)) (maxL a v)).
Theorem rembig_RS a v :
{i | RS (a :: v) = append_nth (RS (rembig (a :: v))) (maxL a v) i}.
End RemoveBig.
Section RestrIntervSmall.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Lemma plact1_ge L u v1 w v2 :
v2 \in plact1 v1 ->
[seq x <- u ++ v1 ++ w | (L >= x)%O] =Pl [seq x <- u ++ v2 ++ w | (L >= x)%O].
Lemma plact2_ge L u v1 w v2 :
v2 \in plact2 v1 ->
[seq x <- u ++ v1 ++ w | (L >= x)%O] =Pl [seq x <- u ++ v2 ++ w | (L >= x)%O].
Lemma plactic_filter_ge L u v :
u =Pl v -> [seq x <- u | (L >= x)%O] =Pl [seq x <- v | (L >= x)%O].
Lemma plactic_filter_gt L u v :
u =Pl v -> [seq x <- u | (L > x)%O] =Pl [seq x <- v | (L > x)%O].
End RestrIntervSmall.
Section RestrIntervBig.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Variable L : Alph.
Notation leL := (@Order.le _ Alph L).
Notation geL := (@Order.ge _ Alph^d L).
Notation ltL := (@Order.lt _ Alph L).
Notation gtL := (@Order.gt _ Alph^d L).
Lemma leL_geLdualE u :
filter leL u = from_revdual (filter geL (revdual u)).
Lemma ltL_gtLdualE u :
filter ltL u = from_revdual (filter gtL (revdual u)).
Lemma plactic_filter_le u v : u =Pl v -> filter leL u =Pl filter leL v.
Lemma plactic_filter_lt u v : u =Pl v -> filter ltL u =Pl filter ltL v.
End RestrIntervBig.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Lemma rembig_plact1 u v : u \in (plact1 v) -> rembig u = rembig v.
Lemma rembig_plact1i u v : u \in (plact1i v) -> rembig u = rembig v.
Lemma rembig_plact2 u v : u \in (plact2 v) -> rembig u = rembig v.
Lemma rembig_plact2i u v : u \in (plact2i v) -> rembig u = rembig v.
Lemma rembig_plact u v : u \in (plactrule _ v) -> rembig u = rembig v.
Theorem rembig_plactcongr u v : u =Pl v -> (rembig u) =Pl (rembig v).
Lemma inspos_rcons l r b : (l < b)%O -> inspos r l = inspos (rcons r b) l.
Lemma bump_bumprow_rconsE l r b :
is_row (rcons r b) -> (l < b)%O -> bump r l ->
let: (lres, rres) := bumprow r l in
bumprow (rcons r b) l = (lres, rcons rres b).
Lemma nbump_bumprow_rconsE l r b :
is_row (rcons r b) -> (l < b)%O -> ~~bump r l ->
let: (lres, rres) := bumprow r l in bumprow (rcons r b) l = (Some b, rres).
Lemma allLeq_is_row_rcons w b :
allLeq w b -> forall row, row \in RS w -> is_row (rcons row b).
Lemma last_ins_lt r l b : (l < b -> last b r < b -> last b (ins r l) < b)%O.
Lemma bumped_lt r b l : is_row r -> (l < b -> last b r < b -> bumped r l < b)%O.
Lemma bisimul_instab t l b lb :
is_tableau t -> (l < b)%O ->
(forall row, row \in t -> is_row (rcons row b)) ->
(forall j : nat, j < lb -> (last b (nth [::] t j) < b)%O) ->
let tres := (append_nth t b lb) in
instab tres l = append_nth (instab t l) b (last_big (instab tres l) b).
Theorem rembig_RS_last_big a v :
RS (a :: v) = append_nth (RS (rembig (a :: v)))
(maxL a v)
(last_big (RS (a :: v)) (maxL a v)).
Theorem rembig_RS a v :
{i | RS (a :: v) = append_nth (RS (rembig (a :: v))) (maxL a v) i}.
End RemoveBig.
Section RestrIntervSmall.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Lemma plact1_ge L u v1 w v2 :
v2 \in plact1 v1 ->
[seq x <- u ++ v1 ++ w | (L >= x)%O] =Pl [seq x <- u ++ v2 ++ w | (L >= x)%O].
Lemma plact2_ge L u v1 w v2 :
v2 \in plact2 v1 ->
[seq x <- u ++ v1 ++ w | (L >= x)%O] =Pl [seq x <- u ++ v2 ++ w | (L >= x)%O].
Lemma plactic_filter_ge L u v :
u =Pl v -> [seq x <- u | (L >= x)%O] =Pl [seq x <- v | (L >= x)%O].
Lemma plactic_filter_gt L u v :
u =Pl v -> [seq x <- u | (L > x)%O] =Pl [seq x <- v | (L > x)%O].
End RestrIntervSmall.
Section RestrIntervBig.
Variables (disp : unit) (Alph : inhOrderType disp).
Let word := seq Alph.
Implicit Type a b c : Alph.
Implicit Type u v w r : word.
Variable L : Alph.
Notation leL := (@Order.le _ Alph L).
Notation geL := (@Order.ge _ Alph^d L).
Notation ltL := (@Order.lt _ Alph L).
Notation gtL := (@Order.gt _ Alph^d L).
Lemma leL_geLdualE u :
filter leL u = from_revdual (filter geL (revdual u)).
Lemma ltL_gtLdualE u :
filter ltL u = from_revdual (filter gtL (revdual u)).
Lemma plactic_filter_le u v : u =Pl v -> filter leL u =Pl filter leL v.
Lemma plactic_filter_lt u v : u =Pl v -> filter ltL u =Pl filter ltL v.
End RestrIntervBig.
Section IncrMap.
Variables (disp1 disp2 : unit)
(T1 : inhOrderType disp1)
(T2 : inhOrderType disp2).
Variable F : T1 -> T2.
Variable u v : seq T1.
Hypothesis Hincr : {in u &, {homo F : x y / (x < y)%O}}.
Lemma subset_abc l a b c r :
{subset l ++ [:: a; b; c] ++ r <= u} -> [/\ a \in u, b \in u & c \in u].
Lemma plact_map_in_incr : u =Pl v -> (map F u) =Pl (map F v).
End IncrMap.
Variables (disp1 disp2 : unit)
(T1 : inhOrderType disp1)
(T2 : inhOrderType disp2).
Variable F : T1 -> T2.
Variable u v : seq T1.
Hypothesis Hincr : {in u &, {homo F : x y / (x < y)%O}}.
Lemma subset_abc l a b c r :
{subset l ++ [:: a; b; c] ++ r <= u} -> [/\ a \in u, b \in u & c \in u].
Lemma plact_map_in_incr : u =Pl v -> (map F u) =Pl (map F v).
End IncrMap.