Library Combi.Combi.Yamanouchi: Yamanouchi Words
Yamanouchi words.
- evalseq s == the evaluation of the sequence s stored as a sequence, that is the sequence whose i-th entry is the number of occurences of i in s; the final zeroes are not stored so that the sequence ends with a non zero entry.
- evalseq_count == an alternate definition of the previous sequence
- is_yam s == s is a Yamanouchi word
- is_yam_of_eval ev s == s is a Yamanouchi word of evaluation ev.
- decr_yam s == the Yamanouchi word obtained by removing the zero and decrassing all the other entries by 1
- hyper_yam ev == the hyperstandard (decreasing) Yamanouchi word of evaluation ev such as 33 2222 11111 0000000
- is_yam_of_eval ev y == y is a yamanouchi word of evalutation ev
- is_yam_of_size n y == y is a yamanouchi word of size n
- enum_yameval ev == the lists of all yamanouchi word of evalutation ev
- yameval ev == a type for seq nat which are Yamanouchi words of evaluation ev; it is canonically a finType
- yamn n == a type for seq nat which are Yamanouchi words of size n; it is canonically a finType
- hyper_yameval ev == the the hyperstandard (decreasing) Yamanouchi word of evaluation ev such as 33 2222 11111 0000000 as a yameval
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import tools combclass partition.
Set Implicit Arguments.
Section Yama.
Implicit Type s : seq nat.
From mathcomp Require Import all_ssreflect.
Require Import tools combclass partition.
Set Implicit Arguments.
Section Yama.
Implicit Type s : seq nat.
equivalent definition
Definition evalseq_count :=
[fun s => [seq (count_mem i) s | i <- iota 0 (foldr maxn 0 (map S s))]].
Lemma foldr_maxn s : foldr maxn 0 [seq i.+1 | i <- s] = \max_(i <- s) S i.
Lemma evalseq_countE : evalseq_count =1 evalseq.
Lemma nth_evalseq s i : nth 0 (evalseq s) i = count_mem i s.
Lemma perm_evalseq s t : perm_eq s t = (evalseq s == evalseq t).
Lemma evalseq0 y : evalseq y = [::] -> y = [::].
Lemma evalseq_cons l s : evalseq (l :: s) = incr_nth (evalseq s) l.
Lemma evalseq_eq_size y : sumn (evalseq y) = size y.
[fun s => [seq (count_mem i) s | i <- iota 0 (foldr maxn 0 (map S s))]].
Lemma foldr_maxn s : foldr maxn 0 [seq i.+1 | i <- s] = \max_(i <- s) S i.
Lemma evalseq_countE : evalseq_count =1 evalseq.
Lemma nth_evalseq s i : nth 0 (evalseq s) i = count_mem i s.
Lemma perm_evalseq s t : perm_eq s t = (evalseq s == evalseq t).
Lemma evalseq0 y : evalseq y = [::] -> y = [::].
Lemma evalseq_cons l s : evalseq (l :: s) = incr_nth (evalseq s) l.
Lemma evalseq_eq_size y : sumn (evalseq y) = size y.
Yamanouchi words:
Sequence of rows of the corners for an increasing sequence of partitions. They are in bijection with standard tableaux
Fixpoint is_yam s :=
if s is s0 :: s'
then is_part (evalseq s) && is_yam s'
else true.
Definition is_yam_of_eval ev y := (is_yam y) && (evalseq y == ev).
Lemma is_yamP s :
reflect
(forall i n, count_mem n (drop i s) >= count_mem n.+1 (drop i s))
(is_yam s).
Lemma is_yam_ijP s :
reflect
(forall d i j, i <= j -> count_mem i (drop d s) >= count_mem j (drop d s))
(is_yam s).
Lemma is_part_eval_yam s : is_yam s -> is_part (evalseq s).
Lemma is_yam_tl l0 s : is_yam (l0 :: s) -> is_yam s.
Lemma is_yam_catr s t : is_yam (s ++ t) -> is_yam t.
Lemma last_yam y : is_yam y -> last 0 y = 0.
if s is s0 :: s'
then is_part (evalseq s) && is_yam s'
else true.
Definition is_yam_of_eval ev y := (is_yam y) && (evalseq y == ev).
Lemma is_yamP s :
reflect
(forall i n, count_mem n (drop i s) >= count_mem n.+1 (drop i s))
(is_yam s).
Lemma is_yam_ijP s :
reflect
(forall d i j, i <= j -> count_mem i (drop d s) >= count_mem j (drop d s))
(is_yam s).
Lemma is_part_eval_yam s : is_yam s -> is_part (evalseq s).
Lemma is_yam_tl l0 s : is_yam (l0 :: s) -> is_yam s.
Lemma is_yam_catr s t : is_yam (s ++ t) -> is_yam t.
Lemma last_yam y : is_yam y -> last 0 y = 0.
Remove the zeroes from a yam and decrease all the other entries by 1
Fixpoint decr_yam s :=
if s is s0 :: s'
then if s0 is s0'.+1
then s0' :: (decr_yam s')
else (decr_yam s')
else [::].
Lemma evalseq_decr_yam s : evalseq (decr_yam s) = behead (evalseq s).
Lemma is_yam_decr s : is_yam s -> is_yam (decr_yam s).
Lemma is_rem_corner_yam l0 s :
is_yam (l0 :: s) -> is_rem_corner (evalseq (l0 :: s)) l0.
Lemma is_add_corner_yam l0 s :
is_yam (l0 :: s) -> is_add_corner (evalseq s) l0.
if s is s0 :: s'
then if s0 is s0'.+1
then s0' :: (decr_yam s')
else (decr_yam s')
else [::].
Lemma evalseq_decr_yam s : evalseq (decr_yam s) = behead (evalseq s).
Lemma is_yam_decr s : is_yam s -> is_yam (decr_yam s).
Lemma is_rem_corner_yam l0 s :
is_yam (l0 :: s) -> is_rem_corner (evalseq (l0 :: s)) l0.
Lemma is_add_corner_yam l0 s :
is_yam (l0 :: s) -> is_add_corner (evalseq s) l0.
Fixpoint hyper_yam_rev ev :=
if ev is s0 :: s then
nseq s0 (size s) ++ hyper_yam_rev s
else [::].
Definition hyper_yam ev := hyper_yam_rev (rev ev).
Lemma size_hyper_yam ev : size (hyper_yam ev) = sumn ev.
Lemma incr_nth_size s : incr_nth s (size s) = rcons s 1.
Lemma part_rcons_ind s sn : is_part (rcons s sn.+2) -> is_part (rcons s sn.+1).
if ev is s0 :: s then
nseq s0 (size s) ++ hyper_yam_rev s
else [::].
Definition hyper_yam ev := hyper_yam_rev (rev ev).
Lemma size_hyper_yam ev : size (hyper_yam ev) = sumn ev.
Lemma incr_nth_size s : incr_nth s (size s) = rcons s 1.
Lemma part_rcons_ind s sn : is_part (rcons s sn.+2) -> is_part (rcons s sn.+1).
"is_part ev" is just here to ensure that sh doesn't ends with a 0
Lemma evalseq_hyper_yam ev : is_part ev -> evalseq (hyper_yam ev) = ev.
Lemma hyper_yamP ev : is_part ev -> is_yam (hyper_yam ev).
Lemma hyper_yam_of_eval ev : is_part ev -> is_yam_of_eval ev (hyper_yam ev).
End Yama.
Lemma is_yam_cat_any y0 y1 z :
is_yam y0 -> is_yam y1 -> evalseq y0 = evalseq y1 ->
is_yam (z ++ y0) -> is_yam (z ++ y1).
Lemma hyper_yamP ev : is_part ev -> is_yam (hyper_yam ev).
Lemma hyper_yam_of_eval ev : is_part ev -> is_yam_of_eval ev (hyper_yam ev).
End Yama.
Lemma is_yam_cat_any y0 y1 z :
is_yam y0 -> is_yam y1 -> evalseq y0 = evalseq y1 ->
is_yam (z ++ y0) -> is_yam (z ++ y1).
Fixpoint enum_yamevaln n ev :=
if n is n'.+1 then
flatten [seq [seq i :: y | y <- enum_yamevaln n' (decr_nth ev i)] |
i <- iota 0 (size ev) & is_rem_corner ev i]
else [:: [::]].
Definition enum_yameval ev := enum_yamevaln (sumn ev) ev.
Definition is_yam_of_size n y := (is_yam y) && (size y == n).
Lemma enum_yamevalP ev:
is_part ev -> all (is_yam_of_eval ev) (enum_yameval ev).
Lemma enum_yameval_countE ev :
is_part ev ->
forall y, is_yam_of_eval ev y -> count_mem y (enum_yameval ev) = 1.
if n is n'.+1 then
flatten [seq [seq i :: y | y <- enum_yamevaln n' (decr_nth ev i)] |
i <- iota 0 (size ev) & is_rem_corner ev i]
else [:: [::]].
Definition enum_yameval ev := enum_yamevaln (sumn ev) ev.
Definition is_yam_of_size n y := (is_yam y) && (size y == n).
Lemma enum_yamevalP ev:
is_part ev -> all (is_yam_of_eval ev) (enum_yameval ev).
Lemma enum_yameval_countE ev :
is_part ev ->
forall y, is_yam_of_eval ev y -> count_mem y (enum_yameval ev) = 1.
Section YamOfEval.
Variable ev : intpart.
Structure yameval : Set :=
YamEval {yamevalval :> seq nat; _ : is_yam_of_eval ev yamevalval}.
Lemma yamevalP (y : yameval) : is_yam y.
Lemma eval_yameval (y : yameval) : evalseq y = ev.
Lemma size_yameval (y : yameval) : size y = sumn ev.
Lemma enum_yamevalE : map val (enum {:yameval}) = enum_yameval ev.
Definition hyper_yameval := YamEval (hyper_yam_of_eval (intpartP ev)).
End YamOfEval.
#[export] Hint Resolve yamevalP : core.
Section YamOfSize.
Variable n : nat.
Lemma yamn_PredEq (ev : intpartn n) :
predI (is_yam_of_size n) (pred1 (val ev) \o evalseq)
=1 is_yam_of_eval (val ev).
Lemma yamn_partition_evalseq yam :
is_yam_of_size n yam -> (is_part_of_n n) (evalseq yam).
Structure yamn : Set :=
Yamn {yamnval :> seq nat; _ : is_yam_of_size n yamnval}.
Lemma yamnP (y : yamn) : is_yam y.
Lemma size_yamn (y : yamn) : size y = n.
Variable ev : intpart.
Structure yameval : Set :=
YamEval {yamevalval :> seq nat; _ : is_yam_of_eval ev yamevalval}.
Lemma yamevalP (y : yameval) : is_yam y.
Lemma eval_yameval (y : yameval) : evalseq y = ev.
Lemma size_yameval (y : yameval) : size y = sumn ev.
Lemma enum_yamevalE : map val (enum {:yameval}) = enum_yameval ev.
Definition hyper_yameval := YamEval (hyper_yam_of_eval (intpartP ev)).
End YamOfEval.
#[export] Hint Resolve yamevalP : core.
Section YamOfSize.
Variable n : nat.
Lemma yamn_PredEq (ev : intpartn n) :
predI (is_yam_of_size n) (pred1 (val ev) \o evalseq)
=1 is_yam_of_eval (val ev).
Lemma yamn_partition_evalseq yam :
is_yam_of_size n yam -> (is_part_of_n n) (evalseq yam).
Structure yamn : Set :=
Yamn {yamnval :> seq nat; _ : is_yam_of_size n yamnval}.
Lemma yamnP (y : yamn) : is_yam y.
Lemma size_yamn (y : yamn) : size y = n.
Check of disjoint union enumeration
Lemma enum_yamnE :
map val (enum {:yamn}) = flatten [seq enum_yameval p | p <- enum_partn n].
End YamOfSize.
#[export] Hint Resolve yamnP yamevalP : core.
map val (enum {:yamn}) = flatten [seq enum_yameval p | p <- enum_partn n].
End YamOfSize.
#[export] Hint Resolve yamnP yamevalP : core.