Library Combi.LRrule.Greene: Greene monotone subsequence numbers
Greene monotone subsequences numbers
- trivIseq U == u : seq {set T} contains pairwise disjoint sets.
- wt : an n.-tuple Alph for an alphabet Alph.
- R : a relation on Alph
- extractpred wt P == the sequence of the entries of wt whose index verify the predicate P.
- extract wt S == the sequence of the entries of wt supported by S, that is, whose index are in S.
- P \is a k.-supp[R, wt] == P : {set {set 'I_N}} is a k-support of wt w.r.t R. This means that P is of cardinality at most k, contains pairwise disjoint sets and finally that for all S in P, the subsequence of wt of support S is sorted for the relation R.
- Greene_rel_t R wt k == the maximal cardinality of the union of a k-support of wt w.r.t R
- Greene_rel R s k == Greene_rel_t R (in_tuple s) k
- tabrows t == the sequence of the supports in the row-reading of t of the rows of t
- tabcols t == the sequence of the supports in the row-reading of t of the columns of t
- tabrowsk t k == the sequence of the supports in the row-reading of t of the k first rows of t
- tabcolsk t k == the sequence of the supports in the row-reading of t of
the k first columns of t
- Greene_row s k == Greene number for nondecreasing subsequence
- Greene_col s k == Greene number for strictly decreasing subsequence
- ksupp_inj R1 R2 k u1 u2 == for each k-support for R1 of u1 there exists a k-support for R2 of u2 of the same size.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm.
Require Import sorted tools subseq partition tableau.
Require Import Schensted congr plactic ordcast.
Set Implicit Arguments.
Import Order.Theory.
Open Scope bool.
Lemma unlift_seqE n (l : seq 'I_n.+1) :
sorted (fun i j : 'I_n.+1 => i < j) (ord0 :: l) ->
exists l1 : seq 'I_n,
sorted (fun i j : 'I_n => i < j) l1 /\ l = map (lift ord0) l1.
Lemma ord0_in_map_liftF n (l : seq 'I_n) :
ord0 \in [seq lift ord0 i | i <- l] = false.
Lemma mem_enum_seqE n (l : seq 'I_n) :
sorted (fun i j : 'I_n => val i < val j) l ->
[seq i <- enum 'I_n | i \in l] = l.
From mathcomp Require Import perm.
Require Import sorted tools subseq partition tableau.
Require Import Schensted congr plactic ordcast.
Set Implicit Arguments.
Import Order.Theory.
Open Scope bool.
Lemma unlift_seqE n (l : seq 'I_n.+1) :
sorted (fun i j : 'I_n.+1 => i < j) (ord0 :: l) ->
exists l1 : seq 'I_n,
sorted (fun i j : 'I_n => i < j) l1 /\ l = map (lift ord0) l1.
Lemma ord0_in_map_liftF n (l : seq 'I_n) :
ord0 \in [seq lift ord0 i | i <- l] = false.
Lemma mem_enum_seqE n (l : seq 'I_n) :
sorted (fun i j : 'I_n => val i < val j) l ->
[seq i <- enum 'I_n | i \in l] = l.
Section TrivISeq.
Variable T : finType.
Lemma bigcup_seq_cover (u : seq {set T}) :
\bigcup_(s <- u) s = cover [set s in u].
Lemma card_seq (s : seq T) : #|[set i in s]| <= size s.
Definition trivIseq (u : seq {set T}) : Prop :=
forall i j, i < j < size u -> [disjoint (nth set0 u i) & (nth set0 u j)].
Lemma trivIseq_consK u0 u : trivIseq (u0 :: u) -> trivIseq u.
Lemma trivIsubseq u v :
subseq u v -> trivIseq v -> trivIseq u.
Lemma trivIs u : trivIseq u -> trivIset [set i | i \in u].
Lemma trivIseq_cover S :
trivIseq S -> \sum_(i <- S) #|i| = #|\bigcup_(i <- S) i|.
Lemma size_coverI (S : {set {set T}}) B :
trivIset S -> \sum_(i in S) #|i :&: B| = #|cover S :&: B|.
Lemma trivIset_I (S : {set {set T}}) B :
trivIset S -> \sum_(i in S) #|i :&: B| <= #|B|.
End TrivISeq.
Lemma trivIseq_map (T1 T2 : finType) (f : T1 -> T2) (S : seq {set T1}) :
injective f -> trivIseq S -> trivIseq (map (fun s : {set T1} => f @: s) S).
Lemma set_nil (T : finType) : [set s : T in [::]] = set0.
Lemma cover_nil (T : finType) : #|cover [set s : {set T} in [::]]| = 0.
Lemma subseq_take (T : eqType) k (l : seq T) : subseq (take k l) l.
Section BigTrivISeq.
Variable T : finType.
Variables (R : Type) (idx : R) (op : Monoid.com_law idx).
Lemma bigop_trivIseq (S : seq {set T}) F :
all (fun s => s != set0) S -> trivIseq S ->
\big[op/idx]_(i in [set x in S]) F i = \big[op/idx]_(i <- S) F i.
End BigTrivISeq.
Require Import ordtype.
Variable T : finType.
Lemma bigcup_seq_cover (u : seq {set T}) :
\bigcup_(s <- u) s = cover [set s in u].
Lemma card_seq (s : seq T) : #|[set i in s]| <= size s.
Definition trivIseq (u : seq {set T}) : Prop :=
forall i j, i < j < size u -> [disjoint (nth set0 u i) & (nth set0 u j)].
Lemma trivIseq_consK u0 u : trivIseq (u0 :: u) -> trivIseq u.
Lemma trivIsubseq u v :
subseq u v -> trivIseq v -> trivIseq u.
Lemma trivIs u : trivIseq u -> trivIset [set i | i \in u].
Lemma trivIseq_cover S :
trivIseq S -> \sum_(i <- S) #|i| = #|\bigcup_(i <- S) i|.
Lemma size_coverI (S : {set {set T}}) B :
trivIset S -> \sum_(i in S) #|i :&: B| = #|cover S :&: B|.
Lemma trivIset_I (S : {set {set T}}) B :
trivIset S -> \sum_(i in S) #|i :&: B| <= #|B|.
End TrivISeq.
Lemma trivIseq_map (T1 T2 : finType) (f : T1 -> T2) (S : seq {set T1}) :
injective f -> trivIseq S -> trivIseq (map (fun s : {set T1} => f @: s) S).
Lemma set_nil (T : finType) : [set s : T in [::]] = set0.
Lemma cover_nil (T : finType) : #|cover [set s : {set T} in [::]]| = 0.
Lemma subseq_take (T : eqType) k (l : seq T) : subseq (take k l) l.
Section BigTrivISeq.
Variable T : finType.
Variables (R : Type) (idx : R) (op : Monoid.com_law idx).
Lemma bigop_trivIseq (S : seq {set T}) F :
all (fun s => s != set0) S -> trivIseq S ->
\big[op/idx]_(i in [set x in S]) F i = \big[op/idx]_(i <- S) F i.
End BigTrivISeq.
Require Import ordtype.
Section GreeneDef.
Context {disp : unit} {Alph : inhOrderType disp}.
Definition extractpred n (wt : n.-tuple Alph) (P : pred 'I_n) :=
[seq tnth wt i | i <- enum P].
Lemma extractIE n (wt : n.-tuple Alph) P :
extractpred wt P = [seq tnth wt i | i <- enum 'I_n & P i].
Lemma extractmaskE n (wt : n.-tuple Alph) P :
extractpred wt P = mask [seq P i | i <- enum 'I_n] wt.
Lemma extsubsIm n wt (P1 P2 : pred 'I_n) :
subpred P1 P2 -> subseq (extractpred wt P1) (extractpred wt P2).
Lemma extsubsm n (w : n.-tuple Alph) (P : pred 'I_n) :
subseq (extractpred w P) w.
Variable R : rel Alph.
Hypothesis HR : transitive R.
Variable N : nat.
Variable wt : N.-tuple Alph.
Definition extract := [fun s : {set 'I_N} => extractpred wt (mem s)].
Lemma size_extract s : size (extract s) = #|s|.
Lemma extsubsI (s1 s2 : {set 'I_N}) :
s1 \subset s2 -> subseq (extract s1) (extract s2).
Lemma sorted_extract_cond s P :
sorted R (extract s) -> sorted R (extract (s :&: P)).
Definition ksupp (k : nat) :=
[qualify a P : {set {set 'I_N}} |
[&& (#|P| <= k)%N, trivIset P & [forall (s | s \in P), sorted R (extract s)]]].
#[local] Notation "k .-supp" := (ksupp k)
(at level 2, format "k .-supp") : form_scope.
Lemma ksupp0 k : set0 \is a k.-supp.
Definition Greene_rel_t k := \max_(P | P \is a k.-supp) #|cover P|.
Notation Ik k := [set i : 'I_N | i < k].
Lemma iotagtnk k : [seq x <- iota 0 N | gtn k x] = iota 0 (minn N k).
Lemma sizeIk k : #|Ik k| = minn N k.
Lemma extract0 : extract set0 = [::].
Lemma extract1 i : extract [set i] = [:: tnth wt i].
Lemma extractS (l : seq 'I_N) :
sorted (fun i j : 'I_N => val i < val j) l ->
extract [set i in l] = [seq tnth wt i | i <- l].
Lemma extract2 i j :
val i < val j -> extract [set i; j] = [:: tnth wt i; tnth wt j].
Lemma Greene_rel_t_inf k : Greene_rel_t k >= minn N k.
Lemma Greene_rel_t_sup k : Greene_rel_t k <= N.
Lemma Greene_rel_t_0 : Greene_rel_t 0 = 0.
End GreeneDef.
Notation "k '.-supp' [ R , wt ]" := (@ksupp _ _ R _ wt k)
(at level 2, format "k '.-supp' [ R , wt ]") : form_scope.
Section Cast.
Variable (d : unit) (T : inhOrderType d).
Lemma ksupp_cast R (w1 w2 : seq T) (H : w1 = w2) k Q :
Q \is a k.-supp[R, in_tuple w1] ->
(cast_set (congr1 size H)) @: Q \is a k.-supp[R, in_tuple w2].
Lemma eq_Greene_rel_t (R1 R2 : rel T) N (u : N.-tuple T) :
R1 =2 R2 -> Greene_rel_t R1 u =1 Greene_rel_t R2 u.
Lemma Greene_rel_t_cast R M N (Heq : M = N) k (V : M.-tuple T) :
Greene_rel_t R (tcast Heq V) k = Greene_rel_t R V k.
Lemma Greene_rel_t_uniq (leT : rel T) N (u : N.-tuple T) :
uniq u ->
Greene_rel_t leT u =1 Greene_rel_t (fun x y => (x != y) && (leT x y)) u.
End Cast.
Context {disp : unit} {Alph : inhOrderType disp}.
Definition extractpred n (wt : n.-tuple Alph) (P : pred 'I_n) :=
[seq tnth wt i | i <- enum P].
Lemma extractIE n (wt : n.-tuple Alph) P :
extractpred wt P = [seq tnth wt i | i <- enum 'I_n & P i].
Lemma extractmaskE n (wt : n.-tuple Alph) P :
extractpred wt P = mask [seq P i | i <- enum 'I_n] wt.
Lemma extsubsIm n wt (P1 P2 : pred 'I_n) :
subpred P1 P2 -> subseq (extractpred wt P1) (extractpred wt P2).
Lemma extsubsm n (w : n.-tuple Alph) (P : pred 'I_n) :
subseq (extractpred w P) w.
Variable R : rel Alph.
Hypothesis HR : transitive R.
Variable N : nat.
Variable wt : N.-tuple Alph.
Definition extract := [fun s : {set 'I_N} => extractpred wt (mem s)].
Lemma size_extract s : size (extract s) = #|s|.
Lemma extsubsI (s1 s2 : {set 'I_N}) :
s1 \subset s2 -> subseq (extract s1) (extract s2).
Lemma sorted_extract_cond s P :
sorted R (extract s) -> sorted R (extract (s :&: P)).
Definition ksupp (k : nat) :=
[qualify a P : {set {set 'I_N}} |
[&& (#|P| <= k)%N, trivIset P & [forall (s | s \in P), sorted R (extract s)]]].
#[local] Notation "k .-supp" := (ksupp k)
(at level 2, format "k .-supp") : form_scope.
Lemma ksupp0 k : set0 \is a k.-supp.
Definition Greene_rel_t k := \max_(P | P \is a k.-supp) #|cover P|.
Notation Ik k := [set i : 'I_N | i < k].
Lemma iotagtnk k : [seq x <- iota 0 N | gtn k x] = iota 0 (minn N k).
Lemma sizeIk k : #|Ik k| = minn N k.
Lemma extract0 : extract set0 = [::].
Lemma extract1 i : extract [set i] = [:: tnth wt i].
Lemma extractS (l : seq 'I_N) :
sorted (fun i j : 'I_N => val i < val j) l ->
extract [set i in l] = [seq tnth wt i | i <- l].
Lemma extract2 i j :
val i < val j -> extract [set i; j] = [:: tnth wt i; tnth wt j].
Lemma Greene_rel_t_inf k : Greene_rel_t k >= minn N k.
Lemma Greene_rel_t_sup k : Greene_rel_t k <= N.
Lemma Greene_rel_t_0 : Greene_rel_t 0 = 0.
End GreeneDef.
Notation "k '.-supp' [ R , wt ]" := (@ksupp _ _ R _ wt k)
(at level 2, format "k '.-supp' [ R , wt ]") : form_scope.
Section Cast.
Variable (d : unit) (T : inhOrderType d).
Lemma ksupp_cast R (w1 w2 : seq T) (H : w1 = w2) k Q :
Q \is a k.-supp[R, in_tuple w1] ->
(cast_set (congr1 size H)) @: Q \is a k.-supp[R, in_tuple w2].
Lemma eq_Greene_rel_t (R1 R2 : rel T) N (u : N.-tuple T) :
R1 =2 R2 -> Greene_rel_t R1 u =1 Greene_rel_t R2 u.
Lemma Greene_rel_t_cast R M N (Heq : M = N) k (V : M.-tuple T) :
Greene_rel_t R (tcast Heq V) k = Greene_rel_t R V k.
Lemma Greene_rel_t_uniq (leT : rel T) N (u : N.-tuple T) :
uniq u ->
Greene_rel_t leT u =1 Greene_rel_t (fun x y => (x != y) && (leT x y)) u.
End Cast.
Section GreeneCat.
Context {disp : unit} {Alph : inhOrderType disp}.
Variable R : rel Alph.
Hypothesis HR : transitive R.
Variable M N : nat.
Variable V : M.-tuple Alph.
Variable W : N.-tuple Alph.
#[local] Notation lsh := (@lshift M N).
#[local] Notation rsh := (@rshift M N).
Lemma enumIMN : enum 'I_(M + N) = map lsh (enum 'I_M) ++ map rsh (enum 'I_N).
Let lsplit := [fun s : {set 'I_(M+N)} => lsh @^-1: s].
Let rsplit := [fun s : {set 'I_(M+N)} => rsh @^-1: s].
Lemma disjoint_inj (sM : {set 'I_M}) (sN : {set 'I_N}) :
[disjoint lsh @: sM & rsh @: sN].
Lemma splitsetK (s : {set 'I_(M+N)}) :
s = (lsh @: lsplit s) :|: (rsh @: rsplit s).
Lemma cutcover (p : {set {set 'I_(M + N)}}) :
cover p = lsh @: (cover (lsplit @: p)) :|: rsh @: (cover (rsplit @: p)).
Lemma extlsplit s :
extract V (lsplit s) =
extract [tuple of V ++ W] (s :&: [set i : 'I_(M+N)| i < M]).
Lemma extrsplit s :
extract W (rsplit s) =
extract [tuple of V ++ W] (s :&: [set i : 'I_(M+N)| i >= M]).
#[local] Notation scover := (fun x => #|cover x|).
Lemma Greene_rel_t_cat k :
Greene_rel_t R [tuple of V ++ W] k <= Greene_rel_t R V k + Greene_rel_t R W k.
End GreeneCat.
Section GreeneSeq.
Context {disp : unit} {Alph : inhOrderType disp}.
Variable R : rel Alph.
Hypothesis HR : transitive R.
Definition Greene_rel u := [fun k => Greene_rel_t R (in_tuple u) k].
Lemma Greene_rel_cat k v w :
Greene_rel (v ++ w) k <= Greene_rel v k + Greene_rel w k.
Let negR := (fun a b => ~~(R a b)).
Hypothesis HnegR : transitive negR.
Lemma Greene_rel_seq r k : sorted negR r -> Greene_rel r k = minn (size r) k.
End GreeneSeq.
Lemma eq_Greene_rel (d : unit) (T : inhOrderType d) (R1 R2 : rel T) u :
R1 =2 R2 -> Greene_rel R1 u =1 Greene_rel R2 u.
Lemma Greene_rel_uniq (d : unit) (T : inhOrderType d) (leT : rel T) u :
uniq u ->
Greene_rel leT u =1 Greene_rel (fun x y => (x != y) && (leT x y)) u.
Lemma size_cover_inj (T1 T2 : finType) (F : T1 -> T2) (P : {set {set T1}}):
injective F -> #|cover P| = #|cover [set F @: S | S : {set T1} in P]|.
Context {disp : unit} {Alph : inhOrderType disp}.
Variable R : rel Alph.
Hypothesis HR : transitive R.
Variable M N : nat.
Variable V : M.-tuple Alph.
Variable W : N.-tuple Alph.
#[local] Notation lsh := (@lshift M N).
#[local] Notation rsh := (@rshift M N).
Lemma enumIMN : enum 'I_(M + N) = map lsh (enum 'I_M) ++ map rsh (enum 'I_N).
Let lsplit := [fun s : {set 'I_(M+N)} => lsh @^-1: s].
Let rsplit := [fun s : {set 'I_(M+N)} => rsh @^-1: s].
Lemma disjoint_inj (sM : {set 'I_M}) (sN : {set 'I_N}) :
[disjoint lsh @: sM & rsh @: sN].
Lemma splitsetK (s : {set 'I_(M+N)}) :
s = (lsh @: lsplit s) :|: (rsh @: rsplit s).
Lemma cutcover (p : {set {set 'I_(M + N)}}) :
cover p = lsh @: (cover (lsplit @: p)) :|: rsh @: (cover (rsplit @: p)).
Lemma extlsplit s :
extract V (lsplit s) =
extract [tuple of V ++ W] (s :&: [set i : 'I_(M+N)| i < M]).
Lemma extrsplit s :
extract W (rsplit s) =
extract [tuple of V ++ W] (s :&: [set i : 'I_(M+N)| i >= M]).
#[local] Notation scover := (fun x => #|cover x|).
Lemma Greene_rel_t_cat k :
Greene_rel_t R [tuple of V ++ W] k <= Greene_rel_t R V k + Greene_rel_t R W k.
End GreeneCat.
Section GreeneSeq.
Context {disp : unit} {Alph : inhOrderType disp}.
Variable R : rel Alph.
Hypothesis HR : transitive R.
Definition Greene_rel u := [fun k => Greene_rel_t R (in_tuple u) k].
Lemma Greene_rel_cat k v w :
Greene_rel (v ++ w) k <= Greene_rel v k + Greene_rel w k.
Let negR := (fun a b => ~~(R a b)).
Hypothesis HnegR : transitive negR.
Lemma Greene_rel_seq r k : sorted negR r -> Greene_rel r k = minn (size r) k.
End GreeneSeq.
Lemma eq_Greene_rel (d : unit) (T : inhOrderType d) (R1 R2 : rel T) u :
R1 =2 R2 -> Greene_rel R1 u =1 Greene_rel R2 u.
Lemma Greene_rel_uniq (d : unit) (T : inhOrderType d) (leT : rel T) u :
uniq u ->
Greene_rel leT u =1 Greene_rel (fun x y => (x != y) && (leT x y)) u.
Lemma size_cover_inj (T1 T2 : finType) (F : T1 -> T2) (P : {set {set T1}}):
injective F -> #|cover P| = #|cover [set F @: S | S : {set T1} in P]|.
Section GreeneInj.
Context {disp1 disp2 : unit}
{T1 : inhOrderType disp1}
{T2 : inhOrderType disp2}.
Variable R1 : rel T1.
Variable R2 : rel T2.
Definition ksupp_inj k (u1 : seq T1) (u2 : seq T2) :=
forall s1, s1 \is a k.-supp[R1, in_tuple u1] ->
exists s2, (#|cover s1| == #|cover s2|)
&& (s2 \is a k.-supp[R2, in_tuple u2]).
Lemma leq_Greene k (u1 : seq T1) (u2 : seq T2) :
ksupp_inj k u1 u2 -> Greene_rel R1 u1 k <= Greene_rel R2 u2 k.
End GreeneInj.
Context {disp1 disp2 : unit}
{T1 : inhOrderType disp1}
{T2 : inhOrderType disp2}.
Variable R1 : rel T1.
Variable R2 : rel T2.
Definition ksupp_inj k (u1 : seq T1) (u2 : seq T2) :=
forall s1, s1 \is a k.-supp[R1, in_tuple u1] ->
exists s2, (#|cover s1| == #|cover s2|)
&& (s2 \is a k.-supp[R2, in_tuple u2]).
Lemma leq_Greene k (u1 : seq T1) (u2 : seq T2) :
ksupp_inj k u1 u2 -> Greene_rel R1 u1 k <= Greene_rel R2 u2 k.
End GreeneInj.
Section Rev.
Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type u v w : seq Alph.
Implicit Type p : seq nat.
Implicit Type t : seq (seq Alph).
#[local] Definition revset n (s : {set 'I_n}) : {set 'I_n} :=
[set rev_ord x | x in s].
Lemma revsetK {n} : involutive (@revset n).
Lemma ksupp_inj_rev (leT : rel Alph) u k :
ksupp_inj leT (fun y x => leT x y) k u (rev u).
Lemma Greene_rel_rev (leT : rel Alph) u :
Greene_rel leT u =1 Greene_rel (fun y x => leT x y) (rev u).
End Rev.
Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type u v w : seq Alph.
Implicit Type p : seq nat.
Implicit Type t : seq (seq Alph).
#[local] Definition revset n (s : {set 'I_n}) : {set 'I_n} :=
[set rev_ord x | x in s].
Lemma revsetK {n} : involutive (@revset n).
Lemma ksupp_inj_rev (leT : rel Alph) u k :
ksupp_inj leT (fun y x => leT x y) k u (rev u).
Lemma Greene_rel_rev (leT : rel Alph) u :
Greene_rel leT u =1 Greene_rel (fun y x => leT x y) (rev u).
End Rev.
Section GreeneRec.
Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type u v w : seq Alph.
Implicit Type t : seq (seq Alph).
Let sym_cast m n (i : 'I_(m + n)) : 'I_(n + m) := cast_ord (addnC m n) i.
#[local] Definition shiftset s0 sh :=
[fun s : {set 'I_(sumn sh)} => (sym_cast \o (@lshift (sumn sh) s0)) @: s].
#[local] Fixpoint shrows sh : seq {set 'I_(sumn sh)} :=
if sh is s0 :: sh then
[set (sym_cast \o (@rshift (sumn sh) s0)) i | i in 'I_s0] ::
map (@shiftset s0 sh) (shrows sh)
else [::].
#[local] Fixpoint shcols sh : seq {set 'I_(sumn sh)} :=
if sh is s0 :: sh then
[seq (sym_cast (@rshift (sumn sh) s0 i)) |:
(@shiftset s0 sh (nth set0 (shcols sh) i))
| i <- enum 'I_s0]
else [::].
Let cast_set_tab t :=
[fun s : {set 'I_(sumn (shape t))} => (cast_ord (esym (size_to_word t))) @: s].
Definition tabrows t := map (cast_set_tab t) (shrows (shape t)).
Definition tabcols t := map (cast_set_tab t) (shcols (shape t)).
Definition tabrowsk t := [fun k => take k (tabrows t)].
Definition tabcolsk t := [fun k => take k (tabcols t)].
Lemma size_shcols_cons s0 sh : size (shcols (s0 :: sh)) = s0.
Lemma size_shcols sh : size (shcols sh) = head 0 sh.
Lemma size_tabcols t : size (tabcols t) = size (head [::] t).
Lemma size_shrows sh : size (shrows sh) = size sh.
Lemma size_tabrows t : size (tabrows t) = size t.
Lemma shcol_cards sh :
is_part sh ->
map (fun S : {set 'I_(sumn sh)} => #|S|) (shcols sh) = conj_part sh.
Lemma shrows_cards sh :
map (fun S : {set 'I_(sumn sh)} => #|S|) (shrows sh) = sh.
Lemma tabrows_non0 t :
is_part (shape t) -> forall s, s \in tabrows t -> s != set0.
Lemma trivIseq_shrows sh : trivIseq (shrows sh).
Lemma trivIset_tabrowsk k t : trivIset [set s | s \in (tabrowsk t k)].
Lemma trivIseq_shcols sh : trivIseq (shcols sh).
Lemma trivIseq_tabcols (t : seq (seq Alph)) : trivIseq (tabcols t).
Lemma trivIset_tabcolsk k t : trivIset [set s | s \in (tabcolsk t k)].
Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type u v w : seq Alph.
Implicit Type t : seq (seq Alph).
Let sym_cast m n (i : 'I_(m + n)) : 'I_(n + m) := cast_ord (addnC m n) i.
#[local] Definition shiftset s0 sh :=
[fun s : {set 'I_(sumn sh)} => (sym_cast \o (@lshift (sumn sh) s0)) @: s].
#[local] Fixpoint shrows sh : seq {set 'I_(sumn sh)} :=
if sh is s0 :: sh then
[set (sym_cast \o (@rshift (sumn sh) s0)) i | i in 'I_s0] ::
map (@shiftset s0 sh) (shrows sh)
else [::].
#[local] Fixpoint shcols sh : seq {set 'I_(sumn sh)} :=
if sh is s0 :: sh then
[seq (sym_cast (@rshift (sumn sh) s0 i)) |:
(@shiftset s0 sh (nth set0 (shcols sh) i))
| i <- enum 'I_s0]
else [::].
Let cast_set_tab t :=
[fun s : {set 'I_(sumn (shape t))} => (cast_ord (esym (size_to_word t))) @: s].
Definition tabrows t := map (cast_set_tab t) (shrows (shape t)).
Definition tabcols t := map (cast_set_tab t) (shcols (shape t)).
Definition tabrowsk t := [fun k => take k (tabrows t)].
Definition tabcolsk t := [fun k => take k (tabcols t)].
Lemma size_shcols_cons s0 sh : size (shcols (s0 :: sh)) = s0.
Lemma size_shcols sh : size (shcols sh) = head 0 sh.
Lemma size_tabcols t : size (tabcols t) = size (head [::] t).
Lemma size_shrows sh : size (shrows sh) = size sh.
Lemma size_tabrows t : size (tabrows t) = size t.
Lemma shcol_cards sh :
is_part sh ->
map (fun S : {set 'I_(sumn sh)} => #|S|) (shcols sh) = conj_part sh.
Lemma shrows_cards sh :
map (fun S : {set 'I_(sumn sh)} => #|S|) (shrows sh) = sh.
Lemma tabrows_non0 t :
is_part (shape t) -> forall s, s \in tabrows t -> s != set0.
Lemma trivIseq_shrows sh : trivIseq (shrows sh).
Lemma trivIset_tabrowsk k t : trivIset [set s | s \in (tabrowsk t k)].
Lemma trivIseq_shcols sh : trivIseq (shcols sh).
Lemma trivIseq_tabcols (t : seq (seq Alph)) : trivIseq (tabcols t).
Lemma trivIset_tabcolsk k t : trivIset [set s | s \in (tabcolsk t k)].
Section Induction.
Variable (t0 : seq Alph) (t : seq (seq Alph)).
Lemma size_to_word_cons : size (to_word t) + size t0 = size (to_word (t0 :: t)).
#[local] Definition cast_cons := cast_ord size_to_word_cons.
#[local] Definition rsh_rec := (cast_cons \o (@rshift (size (to_word t)) (size t0))).
#[local] Definition lsh_rec := (cast_cons \o (@lshift (size (to_word t)) (size t0))).
Lemma lshift_recP : injective lsh_rec.
Lemma rshift_recP : injective rsh_rec.
Lemma lrshift_recF i j : (lsh_rec i == rsh_rec j) = false.
Lemma rshift_in_lshift_recF i (s : {set 'I_(size (to_word t))}) :
rsh_rec i \in [set lsh_rec x | x in s] = false.
Lemma lshift_in_rshift_recF i (s : {set 'I_(size t0)}) :
lsh_rec i \in [set rsh_rec x | x in s] = false.
Lemma disjoint_inj_rec (st : {set 'I_(size (to_word t))}) (s0 : {set 'I_(size t0)}) :
[disjoint lsh_rec @: st & rsh_rec @: s0].
#[local] Definition lsplit_rec :=
[fun s : {set 'I_(size (to_word (t0 :: t)))} => lsh_rec @^-1: s].
#[local] Definition rsplit_rec :=
[fun s : {set 'I_(size (to_word (t0 :: t)))} => rsh_rec @^-1: s].
Lemma split_recabK (s : {set 'I_(size (to_word (t0 :: t)))}) :
s = (lsh_rec @: lsplit_rec s) :|: (rsh_rec @: rsplit_rec s).
Lemma split_rec_cover (p : {set {set 'I_(size (to_word (t0 :: t)))}}) :
cover p =
lsh_rec @: (cover (lsplit_rec @: p)) :|: rsh_rec @: (cover (rsplit_rec @: p)).
Lemma lcast_com :
(cast_ord (esym (size_to_word (t0 :: t))))
\o sym_cast \o (@lshift (sumn (shape t)) (size t0))
=1 lsh_rec \o (cast_ord (esym (size_to_word t))).
Lemma rcast_com :
(cast_ord (esym (size_to_word (t0 :: t))))
\o sym_cast \o (@rshift (sumn (shape t)) (size t0)) =1 rsh_rec.
Lemma enumIsize_to_word :
enum 'I_(size (to_word (t0 :: t))) =
map lsh_rec (enum 'I_(size (to_word t))) ++ map rsh_rec (enum 'I_(size t0)).
Lemma extract_tabrows_0 :
extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabrows (t0 :: t)) 0) = t0.
Lemma extract_tabrows_rec i :
i < size t ->
extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabrows (t0 :: t)) i.+1) =
extract (in_tuple (to_word t)) (nth set0 (tabrows t) i).
Lemma tabcols_cons :
tabcols (t0 :: t) =
[seq rsh_rec i |: (lsh_rec @: (nth set0 (tabcols t) i))
| i <- enum 'I_(size t0)].
Lemma size_tabcols_cons : size (tabcols (t0 :: t)) = size t0.
Lemma extract_tabcols_rec i :
i < size t0 ->
extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabcols (t0 :: t)) i) =
rcons (extract (in_tuple (to_word t)) (nth set0 (tabcols t) i))
(nth inh t0 i).
Lemma lsplit_rec_tab k :
head 0 (shape t) <= size t0 ->
cover [set lsplit_rec x | x in [set s in tabcolsk (t0 :: t) k]] =
cover [set s in tabcolsk t k].
Lemma rsplit_rec_tab k :
cover [set rsplit_rec x | x in [set s in (tabcolsk (t0 :: t)) k]] =
[set i : 'I_(size t0) | i < k].
Lemma cover_tabcols_rec k :
head 0 (shape t) <= size t0 ->
cover [set s in (tabcolsk (t0 :: t) k)] =
rsh_rec @: [set s : 'I_(size t0) | s < k]
:|: lsh_rec @: cover [set s in (tabcolsk t k)].
End Induction.
Lemma size_cover_tabrows k t :
is_part (shape t) ->
#|cover [set s | s \in (tabrowsk t k)]| = sumn (take k (shape t)).
Lemma sorted_leqX_tabrows t i :
is_tableau t -> i < size (tabrows t) ->
sorted <=%O (extract (in_tuple (to_word t)) (nth set0 (tabrows t) i)).
Lemma ksupp_leqX_tabrowsk k t :
is_tableau t ->
[set s | s \in (tabrowsk t k)] \is a k.-supp[<=%O, in_tuple (to_word t)].
Lemma size_cover_tabcolsk k t :
is_part (shape t) ->
#|cover [set s | s \in (tabcolsk t k)]| = \sum_(l <- (shape t)) minn l k.
Lemma cover_tabcols t :
is_part (shape t) -> cover [set s | s \in tabcols t] = setT.
Lemma sorted_gt_tabcols t i :
is_tableau t -> i < size (tabcols t) ->
sorted >%O (extract (in_tuple (to_word t)) (nth set0 (tabcols t) i)).
Lemma ksupp_gt_tabcolsk k t :
is_tableau t ->
[set s | s \in (tabcolsk t k)] \is a k.-supp[>%O, in_tuple (to_word t)].
End GreeneRec.
Variable (t0 : seq Alph) (t : seq (seq Alph)).
Lemma size_to_word_cons : size (to_word t) + size t0 = size (to_word (t0 :: t)).
#[local] Definition cast_cons := cast_ord size_to_word_cons.
#[local] Definition rsh_rec := (cast_cons \o (@rshift (size (to_word t)) (size t0))).
#[local] Definition lsh_rec := (cast_cons \o (@lshift (size (to_word t)) (size t0))).
Lemma lshift_recP : injective lsh_rec.
Lemma rshift_recP : injective rsh_rec.
Lemma lrshift_recF i j : (lsh_rec i == rsh_rec j) = false.
Lemma rshift_in_lshift_recF i (s : {set 'I_(size (to_word t))}) :
rsh_rec i \in [set lsh_rec x | x in s] = false.
Lemma lshift_in_rshift_recF i (s : {set 'I_(size t0)}) :
lsh_rec i \in [set rsh_rec x | x in s] = false.
Lemma disjoint_inj_rec (st : {set 'I_(size (to_word t))}) (s0 : {set 'I_(size t0)}) :
[disjoint lsh_rec @: st & rsh_rec @: s0].
#[local] Definition lsplit_rec :=
[fun s : {set 'I_(size (to_word (t0 :: t)))} => lsh_rec @^-1: s].
#[local] Definition rsplit_rec :=
[fun s : {set 'I_(size (to_word (t0 :: t)))} => rsh_rec @^-1: s].
Lemma split_recabK (s : {set 'I_(size (to_word (t0 :: t)))}) :
s = (lsh_rec @: lsplit_rec s) :|: (rsh_rec @: rsplit_rec s).
Lemma split_rec_cover (p : {set {set 'I_(size (to_word (t0 :: t)))}}) :
cover p =
lsh_rec @: (cover (lsplit_rec @: p)) :|: rsh_rec @: (cover (rsplit_rec @: p)).
Lemma lcast_com :
(cast_ord (esym (size_to_word (t0 :: t))))
\o sym_cast \o (@lshift (sumn (shape t)) (size t0))
=1 lsh_rec \o (cast_ord (esym (size_to_word t))).
Lemma rcast_com :
(cast_ord (esym (size_to_word (t0 :: t))))
\o sym_cast \o (@rshift (sumn (shape t)) (size t0)) =1 rsh_rec.
Lemma enumIsize_to_word :
enum 'I_(size (to_word (t0 :: t))) =
map lsh_rec (enum 'I_(size (to_word t))) ++ map rsh_rec (enum 'I_(size t0)).
Lemma extract_tabrows_0 :
extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabrows (t0 :: t)) 0) = t0.
Lemma extract_tabrows_rec i :
i < size t ->
extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabrows (t0 :: t)) i.+1) =
extract (in_tuple (to_word t)) (nth set0 (tabrows t) i).
Lemma tabcols_cons :
tabcols (t0 :: t) =
[seq rsh_rec i |: (lsh_rec @: (nth set0 (tabcols t) i))
| i <- enum 'I_(size t0)].
Lemma size_tabcols_cons : size (tabcols (t0 :: t)) = size t0.
Lemma extract_tabcols_rec i :
i < size t0 ->
extract (in_tuple (to_word (t0 :: t))) (nth set0 (tabcols (t0 :: t)) i) =
rcons (extract (in_tuple (to_word t)) (nth set0 (tabcols t) i))
(nth inh t0 i).
Lemma lsplit_rec_tab k :
head 0 (shape t) <= size t0 ->
cover [set lsplit_rec x | x in [set s in tabcolsk (t0 :: t) k]] =
cover [set s in tabcolsk t k].
Lemma rsplit_rec_tab k :
cover [set rsplit_rec x | x in [set s in (tabcolsk (t0 :: t)) k]] =
[set i : 'I_(size t0) | i < k].
Lemma cover_tabcols_rec k :
head 0 (shape t) <= size t0 ->
cover [set s in (tabcolsk (t0 :: t) k)] =
rsh_rec @: [set s : 'I_(size t0) | s < k]
:|: lsh_rec @: cover [set s in (tabcolsk t k)].
End Induction.
Lemma size_cover_tabrows k t :
is_part (shape t) ->
#|cover [set s | s \in (tabrowsk t k)]| = sumn (take k (shape t)).
Lemma sorted_leqX_tabrows t i :
is_tableau t -> i < size (tabrows t) ->
sorted <=%O (extract (in_tuple (to_word t)) (nth set0 (tabrows t) i)).
Lemma ksupp_leqX_tabrowsk k t :
is_tableau t ->
[set s | s \in (tabrowsk t k)] \is a k.-supp[<=%O, in_tuple (to_word t)].
Lemma size_cover_tabcolsk k t :
is_part (shape t) ->
#|cover [set s | s \in (tabcolsk t k)]| = \sum_(l <- (shape t)) minn l k.
Lemma cover_tabcols t :
is_part (shape t) -> cover [set s | s \in tabcols t] = setT.
Lemma sorted_gt_tabcols t i :
is_tableau t -> i < size (tabcols t) ->
sorted >%O (extract (in_tuple (to_word t)) (nth set0 (tabcols t) i)).
Lemma ksupp_gt_tabcolsk k t :
is_tableau t ->
[set s | s \in (tabcolsk t k)] \is a k.-supp[>%O, in_tuple (to_word t)].
End GreeneRec.
Section GreeneTab.
Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type t : seq (seq Alph).
Definition Greene_row := Greene_rel (@Order.le _ Alph).
Definition Greene_col := Greene_rel (@Order.gt _ Alph).
Lemma gt_trans : transitive (@Order.gt _ Alph).
Lemma size_row_extract t U V :
is_tableau t -> V \in (tabcols t) ->
sorted <=%O (extract (in_tuple (to_word t)) U) ->
#|U :&: V| <= 1.
Lemma tabcol_cut t :
is_part (shape t) -> forall B, \sum_(U <- tabcols t) #|B :&: U| = #|B|.
Lemma shape_tabcols t:
is_tableau t ->
conj_part (shape t) = [seq #|s : {set 'I_(size (to_word t))}| | s <- tabcols t].
Theorem Greene_row_tab k t :
is_tableau t -> Greene_row (to_word t) k = sumn (take k (shape t)).
Theorem Greene_col_tab k t :
is_tableau t -> Greene_col (to_word t) k = sumn (take k (conj_part (shape t))).
End GreeneTab.
Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type t : seq (seq Alph).
Definition Greene_row := Greene_rel (@Order.le _ Alph).
Definition Greene_col := Greene_rel (@Order.gt _ Alph).
Lemma gt_trans : transitive (@Order.gt _ Alph).
Lemma size_row_extract t U V :
is_tableau t -> V \in (tabcols t) ->
sorted <=%O (extract (in_tuple (to_word t)) U) ->
#|U :&: V| <= 1.
Lemma tabcol_cut t :
is_part (shape t) -> forall B, \sum_(U <- tabcols t) #|B :&: U| = #|B|.
Lemma shape_tabcols t:
is_tableau t ->
conj_part (shape t) = [seq #|s : {set 'I_(size (to_word t))}| | s <- tabcols t].
Theorem Greene_row_tab k t :
is_tableau t -> Greene_row (to_word t) k = sumn (take k (shape t)).
Theorem Greene_col_tab k t :
is_tableau t -> Greene_col (to_word t) k = sumn (take k (conj_part (shape t))).
End GreeneTab.
Theorem Greene_row_tab_eq_shape
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(t1 : seq (seq T1)) (t2 : seq (seq T2)) :
is_tableau t1 -> is_tableau t2 ->
(forall k, Greene_row (to_word t1) k = Greene_row (to_word t2) k) ->
(shape t1 = shape t2).
Theorem Greene_col_tab_eq_shape
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(t1 : seq (seq T1)) (t2 : seq (seq T2)) :
is_tableau t1 -> is_tableau t2 ->
(forall k, Greene_col (to_word t1) k = Greene_col (to_word t2) k) ->
(shape t1 = shape t2).
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(t1 : seq (seq T1)) (t2 : seq (seq T2)) :
is_tableau t1 -> is_tableau t2 ->
(forall k, Greene_row (to_word t1) k = Greene_row (to_word t2) k) ->
(shape t1 = shape t2).
Theorem Greene_col_tab_eq_shape
(d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(t1 : seq (seq T1)) (t2 : seq (seq T2)) :
is_tableau t1 -> is_tableau t2 ->
(forall k, Greene_col (to_word t1) k = Greene_col (to_word t2) k) ->
(shape t1 = shape t2).