Library Combi.Combi.partition: Integer Partitions
Shapes and Integer Partitions
- in_shape sh (r, c) == the box with coordinate (r, c) belongs to the shape sh, that is: c < sh[r].
- in_skew inn out (r, c) == the box with coordinate (r, c) belongs to the out but not inn
- box_in sh == a sigma type for boxes in sh : { b | in_shape sh b } it is canonically a subFinType.
- box_skew inn out == a sigma type for boxes in the skew shape out / inn
- enum_box_in sh == a full duplicate free list of the boxes in sh.
- enum_box_skew inn out == a full duplicate free list of the boxes in the skew shape out / inn
- is_part sh == sh is a partition
- rem_trail0 sh == remove the trailing zeroes of a shape
- is_add_corner sh i == i is the row of an addable corner of sh
- is_rem_corner sh i == i is the row of a removable corner of sh
- incr_nth sh i == the shape obtained by adding a box at the end of the i-th row. This gives a partition if i is an addable corner of sh (Lemma is_part_incr_nth)
- decr_nth sh i == the shape obtained by removing a box at the end of the i-th row. This gives a partition if i is an removable corner of sh (Lemma is_part_decr_nth)
- rem_corners sh == the list of the rows of the removable corners of sh.
- incr_first_n sh n == adding 1 to the n'th first part of sh, always gives a partitions
- conj_part sh == the conjugate of a partition
- included s t == the Ferrer's diagram of s is included in the Ferrer's diagram of t. This is an order.
- s / t = diff_shape s t == the difference of the shape s and t
- outer_shape s t == add t to the shape s
- is_part_of_n sm sh == sh in a partition of n
- is_part_of_ns sm sz sh == sh in a partitionfo n of size sz
- is_part_of_nsk sm sz mx sh == sh in a partition of n of size sz in parts at most mx
- enum_partn sm == the lists of all partitions of n
- enum_partns sm sz == the lists of all partitions of n of size sz
- enum_partnsk sm sz mx == the lists of all partitions of n of size sz in parts at most mx
- intpartn_nb sm == the number of partitions of n
- intpartns_nb sm sz == the number of partitions of n of size sz
- intpartnsk_nb sm sz mx == the number of partitions of n of size sz in parts at most mx
- intpart == a type for seq nat which are partitions; canonically a subCountType of seq nat
- conj_intpart == the conjugate of a intpart as a intpart
- empty_intpart == the empty intpart
- 'P_n == a type for seq nat which are partitions of n; canonically a finType
- cast_intpartn m n eq_mn == the cast from 'P_m to 'P_n
- rowpartn n == the one row partition of sum n as a 'P_n
- colpartn n == the one column partition of sum n as a 'P_n
- conj_intpartn == the conjugate of a 'P_n as a 'P_n
- hookpartm n k == then hook shape partition of sum n.+1 as a 'P_n.+1
whose arm length is k (not counting the corner),
that is (k+1, 1, ..., 1).
- decr_nth_intpart p i == the shape obtained by removing a box at the end of the i-th row if the result is a partition else p
- union_intpart l k == the partition of type intpart obtained by gathering the parts of l and k
- l +|+ k = union_intpartn l k == the partition of type 'P_(m + n) obtained by gathering the parts of l : 'P_m and k : 'P_n
- 'YL == a type convertible to intpart which is canonically a lattice partially ordered by included.
- partdom s t == s is dominated by t, that is the partial sum of s are smaller that the partial sum of t.
- 'PDom_d == a type convertible to 'P_d which is canonically a finite lattice partially ordered by partdom.
- 'PLexi_d == a type convertible to 'P_n which is canonically finite and totally ordered by the lexicographic order.
- setpart_shape P == the shape of a set partition, i.e. the sorted list of the cardinal of the parts
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import div ssralg ssrint ssrnum binomial.
Require Import tools combclass sorted ordtype.
Set Implicit Arguments.
Import LeqGeqOrder.
Import Order.TTheory.
Open Scope nat_scope.
Declare Scope Combi_scope.
Delimit Scope Combi_scope with Combi.
Open Scope Combi_scope.
Reserved Notation "''P_' n"
(at level 8, n at level 2, format "''P_' n").
Reserved Notation "''PDom_' n"
(at level 8, n at level 2, format "''PDom_' n").
Reserved Notation "''PLexi_' n"
(at level 8, n at level 2, format "''PLexi_' n").
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import div ssralg ssrint ssrnum binomial.
Require Import tools combclass sorted ordtype.
Set Implicit Arguments.
Import LeqGeqOrder.
Import Order.TTheory.
Open Scope nat_scope.
Declare Scope Combi_scope.
Delimit Scope Combi_scope with Combi.
Open Scope Combi_scope.
Reserved Notation "''P_' n"
(at level 8, n at level 2, format "''P_' n").
Reserved Notation "''PDom_' n"
(at level 8, n at level 2, format "''PDom_' n").
Reserved Notation "''PLexi_' n"
(at level 8, n at level 2, format "''PLexi_' n").
Definition in_shape sh b := b.2 < nth 0 sh b.1.
Definition in_skew inn out b := nth 0 inn b.1 <= b.2 < nth 0 out b.1.
Lemma in_skewE inn out b :
in_skew inn out b = ~~ in_shape inn b && in_shape out b.
Lemma in_skew_out inn out b : in_skew inn out b -> in_shape out b.
Lemma in_skew_in inn out b : in_skew inn out b -> ~~ in_shape inn b.
Lemma in_shape_nil : in_shape [::] =1 pred0.
Lemma in_skew_nil : in_skew [::] =2 in_shape.
Lemma in_shape_size sh r c : in_shape sh (r, c) -> r < size sh.
Definition in_skew inn out b := nth 0 inn b.1 <= b.2 < nth 0 out b.1.
Lemma in_skewE inn out b :
in_skew inn out b = ~~ in_shape inn b && in_shape out b.
Lemma in_skew_out inn out b : in_skew inn out b -> in_shape out b.
Lemma in_skew_in inn out b : in_skew inn out b -> ~~ in_shape inn b.
Lemma in_shape_nil : in_shape [::] =1 pred0.
Lemma in_skew_nil : in_skew [::] =2 in_shape.
Lemma in_shape_size sh r c : in_shape sh (r, c) -> r < size sh.
Section Defs.
Implicit Types (s sh : seq nat) (i j r c : nat).
Fixpoint is_part sh :=
if sh is sh0 :: sh'
then (sh0 >= head 1 sh') && (is_part sh')
else true.
Implicit Types (s sh : seq nat) (i j r c : nat).
Fixpoint is_part sh :=
if sh is sh0 :: sh'
then (sh0 >= head 1 sh') && (is_part sh')
else true.
Partitions don't have 0 parts
Lemma part_head0F sh : head 1 sh == 0 -> is_part sh = false.
Lemma part_head_non0 sh : is_part sh -> head 1 sh != 0.
Lemma notin0_part sh : is_part sh -> 0 \notin sh.
Lemma in_part_non0 sh i : is_part sh -> i \in sh -> i != 0.
Lemma nth_part_non0 sh i : is_part sh -> i < size sh -> nth 0 sh i != 0.
Lemma leq_head_sumn sh : head 0 sh <= sumn sh.
Lemma part_leq_head sh i : is_part sh -> i \in sh -> i <= head 0 sh.
Lemma part_head_non0 sh : is_part sh -> head 1 sh != 0.
Lemma notin0_part sh : is_part sh -> 0 \notin sh.
Lemma in_part_non0 sh i : is_part sh -> i \in sh -> i != 0.
Lemma nth_part_non0 sh i : is_part sh -> i < size sh -> nth 0 sh i != 0.
Lemma leq_head_sumn sh : head 0 sh <= sumn sh.
Lemma part_leq_head sh i : is_part sh -> i \in sh -> i <= head 0 sh.
Three equivalent definitions
Lemma is_partP sh :
reflect
(last 1 sh != 0 /\ forall i, (nth 0 sh i) >= nth 0 sh i.+1)
(is_part sh).
Lemma is_part_ijP sh :
reflect
(last 1 sh != 0 /\ forall i j, i <= j -> (nth 0 sh i) >= nth 0 sh j)
(is_part sh).
Lemma is_part_sortedE sh : (is_part sh) = (sorted geq sh) && (0 \notin sh).
reflect
(last 1 sh != 0 /\ forall i, (nth 0 sh i) >= nth 0 sh i.+1)
(is_part sh).
Lemma is_part_ijP sh :
reflect
(last 1 sh != 0 /\ forall i j, i <= j -> (nth 0 sh i) >= nth 0 sh j)
(is_part sh).
Lemma is_part_sortedE sh : (is_part sh) = (sorted geq sh) && (0 \notin sh).
Sub-partitions
Lemma is_part_consK l0 sh : is_part (l0 :: sh) -> is_part sh.
Lemma is_part_behead sh : is_part sh -> is_part (behead sh).
Lemma is_part_subseq sh1 sh2 : subseq sh1 sh2 -> is_part sh2 -> is_part sh1.
Lemma is_part_rconsK sh sn : is_part (rcons sh sn) -> is_part sh.
Lemma is_part_catl sh1 sh2 : is_part (sh1 ++ sh2) -> is_part sh2.
Lemma is_part_catr sh1 sh2 : is_part (sh1 ++ sh2) -> is_part sh1.
Boxes in a partitions
Lemma in_part_le sh r c j k :
is_part sh -> in_shape sh (r, c) -> j <= r -> k <= c -> in_shape sh (j, k).
Lemma in_part_is_part sh :
(forall r c j k, j <= r -> k <= c ->
in_shape sh (r, c) -> in_shape sh (j, k)) ->
last 1 sh != 0 -> is_part sh.
Equality of partitions
Partitions and sumn
Lemma part0 sh : is_part sh -> sumn sh = 0 -> sh = [::].
Lemma size_part sh : is_part sh -> size sh <= sumn sh.
Lemma part_sumn_rectangle sh :
is_part sh -> sumn sh <= (head 0 sh) * (size sh).
Lemma size_part sh : is_part sh -> size sh <= sumn sh.
Lemma part_sumn_rectangle sh :
is_part sh -> sumn sh <= (head 0 sh) * (size sh).
Removing trailing zeroes
Fixpoint rem_trail0 s :=
if s is s0 :: s' then
if (rem_trail0 s') is t1 :: t' then s0 :: t1 :: t'
else if s0 == 0 then [::] else [:: s0]
else [::].
Lemma size_rem_trail0 s : size (rem_trail0 s) <= size s.
Lemma nth_rem_trail0 s i : nth 0 (rem_trail0 s) i = nth 0 s i.
Lemma sumn_rem_trail0 s : sumn (rem_trail0 s) = sumn s.
Lemma is_part_rem_trail0 s : sorted geq s -> is_part (rem_trail0 s).
if s is s0 :: s' then
if (rem_trail0 s') is t1 :: t' then s0 :: t1 :: t'
else if s0 == 0 then [::] else [:: s0]
else [::].
Lemma size_rem_trail0 s : size (rem_trail0 s) <= size s.
Lemma nth_rem_trail0 s i : nth 0 (rem_trail0 s) i = nth 0 s i.
Lemma sumn_rem_trail0 s : sumn (rem_trail0 s) = sumn s.
Lemma is_part_rem_trail0 s : sorted geq s -> is_part (rem_trail0 s).
Definition is_rem_corner sh i := nth 0 sh i > nth 0 sh i.+1.
Definition is_add_corner sh i := (i == 0) || (nth 0 sh i < nth 0 sh i.-1).
Lemma last_incr_nth_non0 sh i : last 1 sh != 0 -> last 1 (incr_nth sh i) != 0.
Lemma is_part_incr_nth_size sh i :
is_part sh -> is_part (incr_nth sh i) -> i <= size sh.
Lemma is_part_incr_nth sh i :
is_part sh -> is_add_corner sh i -> is_part (incr_nth sh i).
Lemma del_rem_corner sh i :
last 1 sh != 0 -> is_part (incr_nth sh i) ->
is_rem_corner (incr_nth sh i) i = is_part sh.
Lemma rem_corner_incr_nth sh i :
is_part sh -> is_add_corner sh i -> is_rem_corner (incr_nth sh i) i.
Lemma is_rem_cornerP sh i : is_part sh ->
(i < size sh) && (~~ in_shape sh (i.+1, (nth 0 sh i).-1)) =
(is_rem_corner sh i).
Fixpoint decr_nth v i {struct i} :=
if v is n :: v' then
if i is i'.+1 then n :: decr_nth v' i'
else if n is n'.+1 then
if n' is _.+1 then
n' :: v'
else [::]
else [::]
else [::].
Lemma incr_nthK sh i :
is_part sh -> is_part (incr_nth sh i) -> decr_nth (incr_nth sh i) i = sh.
Lemma decr_nthK sh i :
is_part sh -> is_rem_corner sh i -> incr_nth (decr_nth sh i) i = sh.
Lemma sumn_incr_nth s i : sumn (incr_nth s i) = (sumn s).+1.
Lemma nth_decr_nth sh i :
nth 0 (decr_nth sh i) i = (nth 0 sh i).-1.
Lemma nth_decr_nth_neq sh i j :
is_part sh -> is_rem_corner sh i -> i != j ->
nth 0 (decr_nth sh i) j = nth 0 sh j.
Lemma sumn_decr_nth sh i :
is_part sh -> is_rem_corner sh i -> (sumn (decr_nth sh i)) = (sumn sh).-1.
Lemma is_part_decr_nth sh i :
is_part sh -> is_rem_corner sh i -> is_part (decr_nth sh i).
Lemma add_corner_decr_nth sh i :
is_part sh -> is_rem_corner sh i -> is_add_corner (decr_nth sh i) i.
Definition rem_corners sh := filter (is_rem_corner sh) (iota 0 (size sh)).
Lemma rem_corners_uniq sh : uniq (rem_corners sh).
Definition is_add_corner sh i := (i == 0) || (nth 0 sh i < nth 0 sh i.-1).
Lemma last_incr_nth_non0 sh i : last 1 sh != 0 -> last 1 (incr_nth sh i) != 0.
Lemma is_part_incr_nth_size sh i :
is_part sh -> is_part (incr_nth sh i) -> i <= size sh.
Lemma is_part_incr_nth sh i :
is_part sh -> is_add_corner sh i -> is_part (incr_nth sh i).
Lemma del_rem_corner sh i :
last 1 sh != 0 -> is_part (incr_nth sh i) ->
is_rem_corner (incr_nth sh i) i = is_part sh.
Lemma rem_corner_incr_nth sh i :
is_part sh -> is_add_corner sh i -> is_rem_corner (incr_nth sh i) i.
Lemma is_rem_cornerP sh i : is_part sh ->
(i < size sh) && (~~ in_shape sh (i.+1, (nth 0 sh i).-1)) =
(is_rem_corner sh i).
Fixpoint decr_nth v i {struct i} :=
if v is n :: v' then
if i is i'.+1 then n :: decr_nth v' i'
else if n is n'.+1 then
if n' is _.+1 then
n' :: v'
else [::]
else [::]
else [::].
Lemma incr_nthK sh i :
is_part sh -> is_part (incr_nth sh i) -> decr_nth (incr_nth sh i) i = sh.
Lemma decr_nthK sh i :
is_part sh -> is_rem_corner sh i -> incr_nth (decr_nth sh i) i = sh.
Lemma sumn_incr_nth s i : sumn (incr_nth s i) = (sumn s).+1.
Lemma nth_decr_nth sh i :
nth 0 (decr_nth sh i) i = (nth 0 sh i).-1.
Lemma nth_decr_nth_neq sh i j :
is_part sh -> is_rem_corner sh i -> i != j ->
nth 0 (decr_nth sh i) j = nth 0 sh j.
Lemma sumn_decr_nth sh i :
is_part sh -> is_rem_corner sh i -> (sumn (decr_nth sh i)) = (sumn sh).-1.
Lemma is_part_decr_nth sh i :
is_part sh -> is_rem_corner sh i -> is_part (decr_nth sh i).
Lemma add_corner_decr_nth sh i :
is_part sh -> is_rem_corner sh i -> is_add_corner (decr_nth sh i) i.
Definition rem_corners sh := filter (is_rem_corner sh) (iota 0 (size sh)).
Lemma rem_corners_uniq sh : uniq (rem_corners sh).
Fixpoint incr_first_n sh n :=
if sh is s0 :: s then
if n is n'.+1 then s0.+1 :: incr_first_n s n'
else sh
else nseq n 1.
Fixpoint conj_part sh :=
if sh is s0 :: sh then incr_first_n (conj_part sh) s0
else [::].
Lemma is_part_nseq1 n : is_part (nseq n 1).
Lemma nth_incr_first_n sh n i :
nth 0 (incr_first_n sh n) i = if i < n then (nth 0 sh i).+1 else nth 0 sh i.
Lemma incr_first_n_nthC sh i j :
incr_first_n (incr_nth sh i) j = incr_nth (incr_first_n sh j) i.
Lemma is_part_incr_first_n sh n :
is_part sh -> is_part (incr_first_n sh n).
Lemma is_part_conj sh : is_part sh -> is_part (conj_part sh).
Lemma conj_nseq n : 0 < n -> conj_part (nseq n 1) = [:: n].
Lemma size_incr_first_n sh n :
size sh <= n -> size (incr_first_n sh n) = n.
Lemma size_conj_part sh : is_part sh -> size (conj_part sh) = head 0 sh.
Lemma sumn_incr_first_n sh n : sumn (incr_first_n sh n) = sumn sh + n.
Lemma sumn_conj_part sh : sumn (conj_part sh) = sumn sh.
Lemma conj_part_ind sh l :
sh != [::] -> is_part sh -> l >= size sh ->
conj_part (incr_first_n sh l) = l :: conj_part sh.
Lemma conj_partK sh : is_part sh -> conj_part (conj_part sh) = sh.
Lemma conj_part_incr_nth sh i :
is_part sh -> is_add_corner sh i ->
conj_part (incr_nth sh i) = incr_nth (conj_part sh) (nth 0 sh i).
Lemma in_conj_part_impl sh : is_part sh ->
forall r c, in_shape sh (r, c) -> in_shape (conj_part sh) (c, r).
Lemma in_conj_part sh : is_part sh ->
forall r c, in_shape sh (r, c) = in_shape (conj_part sh) (c, r).
Lemma conj_ltnE sh :
is_part sh -> forall i j, nth 0 sh i > j = (nth 0 (conj_part sh) j > i).
Lemma conj_leqE sh :
is_part sh -> forall i j, (nth 0 sh i <= j) = (nth 0 (conj_part sh) j <= i).
Lemma nth_conjE sh r c :
is_part sh -> c != 0 ->
(nth 0 (conj_part sh) r == c) = (nth 0 sh c <= r < nth 0 sh c.-1).
Lemma rem_corner_incr_first_n sh i :
is_part sh -> is_rem_corner (incr_first_n sh i.+1) i.
Lemma rem_corner_incr_first_nE sh n i :
is_part sh -> is_rem_corner sh i -> is_rem_corner (incr_first_n sh n) i.
Lemma is_add_corner_conj_part sh r :
is_part sh -> is_add_corner sh r -> is_add_corner (conj_part sh) (nth 0 sh r).
Lemma rem_corner_conj_part sh i :
is_part sh -> is_rem_corner sh i ->
is_rem_corner (conj_part sh) (nth 0 sh i).-1.
Lemma sumn_take_leq s k1 k2 :
k1 <= k2 -> sumn (take k1 s) <= sumn (take k2 s).
Lemma sum_conj sh k : \sum_(l <- sh) minn l k = sumn (take k (conj_part sh)).
Lemma sumn_take_inj s t :
is_part s -> is_part t ->
(forall k, sumn (take k s) = sumn (take k t)) -> s = t.
Fixpoint included inner outer :=
if inner is inn0 :: inn then
if outer is out0 :: out then
(inn0 <= out0) && (included inn out)
else false
else true.
Lemma includedP inner outer :
reflect (size inner <= size outer /\ forall i, nth 0 inner i <= nth 0 outer i)
(included inner outer).
Lemma part_includedP inner outer :
is_part inner ->
reflect (forall i, nth 0 inner i <= nth 0 outer i) (included inner outer).
Lemma included_behead p1 p2 :
included p1 p2 -> included (behead p1) (behead p2).
Lemma included_refl sh : included sh sh.
Lemma included_trans : transitive included.
Lemma included_incr_nth sh i : included sh (incr_nth sh i).
Lemma included_decr_nth u i : included (decr_nth u i) u.
Lemma included_incr_nth_inner inner outer i :
nth 0 inner i < nth 0 outer i ->
included inner outer -> included (incr_nth inner i) outer.
Lemma size_included inner outer :
included inner outer -> size inner <= size outer.
Lemma sumn_included inner outer :
included inner outer -> sumn inner <= sumn outer.
Lemma included_sumnE inner outer :
is_part outer ->
included inner outer ->
sumn inner = sumn outer ->
inner = outer.
Lemma included_anti sh1 sh2 :
is_part sh1 -> is_part sh2 ->
included sh1 sh2 -> included sh2 sh1 ->
sh1 = sh2.
Lemma included_conj_part inner outer :
is_part inner -> is_part outer ->
included inner outer -> included (conj_part inner) (conj_part outer).
Lemma included_conj_partE inner outer :
is_part inner -> is_part outer ->
included inner outer = included (conj_part inner) (conj_part outer).
Fixpoint diff_shape inner outer :=
if inner is inn0 :: inn then
if outer is out0 :: out then
out0 - inn0 :: diff_shape inn out
else [::]
else outer.
Notation "outer / inner" := (diff_shape inner outer) : Combi_scope.
Definition pad (T : Type) (x : T) sz := [fun s => s ++ nseq (sz - size s) x].
Lemma nth_pad (T : Type) n (p : T) (s : seq T) i :
nth p (pad p n s) i = nth p s i.
Lemma head_pad (T : Type) n (p : T) (s : seq T) :
head p (pad p n s) = head p s.
Definition outer_shape inner size_seq :=
[seq p.1 + p.2 | p <- zip (pad 0 (size (size_seq)) inner) size_seq].
Lemma diff_shape_eq s : s / s = nseq (size s) 0.
Lemma sumn_diff_shape_eq s : sumn (s / s) = 0.
Lemma size_diff_shape inner outer : size (outer / inner) = size outer.
Lemma nth_diff_shape inn out i :
nth 0 (out / inn) i = nth 0 out i - nth 0 inn i.
Lemma sumn_diff_shape inner outer :
included inner outer -> sumn (outer / inner) = sumn outer - sumn inner.
Lemma diff_shape_pad0 inner outer :
outer / ((pad 0 (size outer)) inner) = outer / inner.
Lemma diff_shapeK inner outer :
included inner outer -> outer_shape inner (outer / inner) = outer.
Lemma outer_shapeK inner diff :
size inner <= size diff -> (outer_shape inner diff) / inner = diff.
Lemma outer_shape_pad0 inner sz :
outer_shape (pad 0 (size sz) inner) sz = outer_shape inner sz.
Lemma included_pad0 inner outer :
included inner outer = included (pad 0 (size outer) inner) outer.
End Defs.
Notation "outer / inner" := (diff_shape inner outer) : Combi_scope.
Structure intpart : Set := IntPart {pval :> seq nat; _ : is_part pval}.
Lemma intpartP (p : intpart) : is_part p.
Lemma intpart_sorted (p : intpart) : sorted geq p.
#[export] Hint Resolve intpartP intpart_sorted : core.
Lemma intpart_eqP (p q : intpart) :
reflect (forall i, nth 0 p i = nth 0 q i) (p == q).
Canonical conj_intpart p := IntPart (is_part_conj (intpartP p)).
Lemma conj_intpartK : involutive conj_intpart.
Lemma intpart_sumn_take_inj (s t : intpart) :
(forall k, sumn (take k s) = sumn (take k t)) -> s = t.
Canonical empty_intpart := IntPart (pval := [::]) is_true_true.
Lemma empty_intpartP (p : intpart) : sumn p = 0 -> p = empty_intpart.
Fixpoint enum_partnsk sm sz mx : (seq (seq nat)) :=
if sz is sz.+1 then
flatten [seq [seq i :: p | p <- enum_partnsk (sm - i) sz i] |
i <- iota 1 (minn sm mx)]
else if sm is sm.+1 then [::] else [:: [::]].
Definition enum_partns sm sz := enum_partnsk sm sz sm.
Definition enum_partn sm := flatten [seq enum_partns sm sz | sz <- iota 0 sm.+1 ].
Definition is_part_of_n sm :=
[pred p | (sumn p == sm) & is_part p ].
Definition is_part_of_ns sm sz :=
[pred p | (size p == sz) & is_part_of_n sm p].
Definition is_part_of_nsk sm sz mx :=
[pred p | (head 1 p <= mx) & is_part_of_ns sm sz p].
Lemma enum_partnsk_allP sm sz mx :
mx >= 1 -> all (is_part_of_nsk sm sz mx) (enum_partnsk sm sz mx).
Lemma enum_partnsk_countE sm sz mx :
mx >= 1 ->
forall p, is_part_of_nsk sm sz mx p ->
count_mem p (enum_partnsk sm sz mx) = 1.
Lemma enum_partnskE sm sz mx :
mx >= 1 ->
forall p, count_mem p (enum_partnsk sm sz mx) = is_part_of_nsk sm sz mx p.
Lemma enum_partns_allP sm sz : all (is_part_of_ns sm sz) (enum_partns sm sz).
Lemma enum_partns_countE sm sz p :
is_part_of_ns sm sz p -> count_mem p (enum_partns sm sz) = 1.
Lemma enum_partnsE sm sz p :
count_mem p (enum_partns sm sz) = is_part_of_ns sm sz p.
Lemma enum_partn_allP sm : all (is_part_of_n sm) (enum_partn sm).
Lemma enum_partn_countE sm p :
is_part_of_n sm p -> count_mem p (enum_partn sm) = 1.
Lemma enum_partnP n p : (is_part_of_n n p) = (p \in enum_partn n).
Section PartOfn.
Variable n : nat.
Structure intpartn : Set :=
IntPartN {pnval :> seq nat; _ : is_part_of_n n pnval}.
#[local] Notation "''P'" := intpartn.
Implicit Type (p : 'P).
Lemma intpartnP p : is_part p.
Lemma intpartn_sorted p : sorted geq p.
Hint Resolve intpartnP intpartn_sorted : core.
Definition intpart_of_intpartn p := IntPart (intpartnP p).
Coercion intpart_of_intpartn : intpartn >-> intpart.
Lemma sumn_intpartn p : sumn p = n.
Lemma intpartn_leq_head p i : i \in pnval p -> i <= head 0 p.
Lemma intpartn_leq p i : i \in pnval p -> i <= n.
Lemma enum_intpartnE : map val (enum {:'P}) = enum_partn n.
Fact conj_intpartnP p : is_part_of_n n (conj_part p).
Canonical conj_intpartn p := IntPartN (conj_intpartnP p).
Lemma conj_intpartnK : involutive conj_intpartn.
End PartOfn.
Notation "''P_' n" := (intpartn n).
Lemma val_intpartn0 (sh : 'P_0) : sh = [::] :> seq nat.
Lemma val_intpartn1 (sh : 'P_1) : sh = [:: 1] :> seq nat.
Lemma val_intpartn2 (sh : 'P_2) :
sh = [:: 2] :> seq nat \/ sh = [:: 1; 1] :> seq nat.
Lemma val_intpartn3 (sh : 'P_3) :
[\/ sh = [:: 3] :> seq nat,
sh = [:: 2; 1] :> seq nat |
sh = [:: 1; 1; 1] :> seq nat].
Definition cast_intpartn m n (eq_mn : m = n) p :=
let: erefl in _ = n := eq_mn return 'P_n in p.
Lemma cast_intpartnE m n (eq_mn : m = n) p :
val (cast_intpartn eq_mn p) = val p.
Lemma cast_intpartn_id n eq_n (s : 'P_n) : cast_intpartn eq_n s = s.
Lemma cast_intpartnK m n eq_m_n :
cancel (@cast_intpartn m n eq_m_n) (cast_intpartn (esym eq_m_n)).
Lemma cast_intpartnKV m n eq_m_n :
cancel (cast_intpartn (esym eq_m_n)) (@cast_intpartn m n eq_m_n).
Lemma cast_intpartn_inj m n eq_m_n : injective (@cast_intpartn m n eq_m_n).
Lemma cast_intpartn_bij m n eq_m_n : bijective (@cast_intpartn m n eq_m_n).
Lemma cast_conj_inpart m n eq_m_n (s : 'P_m) :
(@cast_intpartn m n eq_m_n) (conj_intpartn s) =
conj_intpartn (@cast_intpartn m n eq_m_n s).
Fact rowpartn_subproof d : is_part_of_n d (if d is 0 then [::] else [:: d]).
Definition rowpartn d : 'P_d := locked (IntPartN (rowpartn_subproof d)).
Fact colpartn_subproof d : is_part_of_n d (nseq d 1%N).
Definition colpartn d : 'P_d := locked (IntPartN (colpartn_subproof d)).
Lemma rowpartnE d : rowpartn d = (if d is 0 then [::] else [:: d]) :> seq nat.
Lemma colpartnE d : colpartn d = nseq d 1%N :> seq nat.
Lemma rowpartn0E : rowpartn 0 = [::] :> seq nat.
Lemma rowpartnSE d : rowpartn d.+1 = [:: d.+1] :> seq nat.
Lemma size_colpartn d : size (colpartn d) = d.
Lemma size_rowpartn d : size (rowpartn d) = (d != 0).
Lemma part_nseq1P x0 sh :
is_part sh -> head x0 sh <= 1 -> sh = nseq (sumn sh) 1.
Lemma colpartnP x0 d (la : 'P_d) : head x0 la <= 1 -> la = colpartn d.
Lemma conj_rowpartn d : conj_intpartn (rowpartn d) = colpartn d.
Lemma conj_colpartn d : conj_intpartn (colpartn d) = rowpartn d.
Definition hookpart d k :=
if d is d'.+1 then minn d'.+1 k.+1 :: nseq (d' - k) 1%N else [::].
Fact hookpartn_subproof d k : is_part_of_n d (hookpart d k).
Definition hookpartn d k : 'P_d :=
locked (IntPartN (hookpartn_subproof d k)).
Lemma hookpartnE d k :
k < d -> (hookpartn d k) = k.+1 :: nseq (d.-1 - k) 1%N :> seq nat.
Lemma size_hookpartn d k : k < d -> size (hookpartn d k) = d - k.
Lemma behead_hookpartn d k : behead (hookpartn d k) = nseq (d.-1 - k) 1%N.
Lemma hookpartn_col d : hookpartn d 0 = colpartn d.
Lemma hookpartn_row d : hookpartn d d.-1 = rowpartn d.
Lemma conj_hookpartn d k :
k < d -> conj_intpartn (hookpartn d k) = hookpartn d (d.-1 - k).
Lemma sorted_geq_count_leq2E (s : seq nat) :
sorted geq s -> (count (leq 2) s <= 1) = (nth 0 s 1 <= 1).
Lemma sorted_geq_nth0E (s : seq nat) :
sorted geq s -> nth 0 s 0 = \max_(i <- s) i.
Lemma intpartn_count_leq2E d (la : 'P_d) :
(count (leq 2) la <= 1) = (nth 0 la 1 <= 1).
Lemma intpartn_nth0 d (la : 'P_d) :
nth 0 la 0 = \max_(i <- la) i.
Lemma hookpartnPE x0 x1 d (la : 'P_d) :
nth x0 la 1 <= 1 -> la = hookpartn d (nth x1 la 0).-1.
Lemma hookpartnP d (la : 'P_d.+1) :
reflect (exists k, k < d.+1 /\ la = hookpartn d.+1 k) (nth 0 la 1 <= 1).
Lemma intpartn0 : all_equal_to (rowpartn 0).
Lemma intpartn1 : all_equal_to (rowpartn 1).
Lemma intpartn2 (sh : 'P_2) : sh = rowpartn 2 \/ sh = colpartn 2.
Lemma intpartn3 (sh : 'P_3) :
[\/ sh = rowpartn 3, sh = hookpartn 3 1 | sh = colpartn 3].
Lemma is_part_decr_nth_part (p : intpart) i :
is_part (if is_rem_corner p i then decr_nth p i else p).
Definition decr_nth_intpart (p : intpart) i : intpart :=
IntPart (is_part_decr_nth_part p i).
Lemma decr_nth_intpartE (p : intpart) i :
is_rem_corner p i -> decr_nth_intpart p i = decr_nth p i :> seq nat.
Lemma intpart_rem_corner_ind (F : intpart -> Type) :
F empty_intpart ->
(forall p : intpart,
(forall i, is_rem_corner p i -> F (decr_nth_intpart p i)) -> F p) ->
forall p : intpart, F p.
Lemma part_rem_corner_ind (F : seq nat -> Type) :
F [::] ->
(forall p, is_part p ->
(forall i, is_rem_corner p i -> F (decr_nth p i)) -> F p) ->
forall p, is_part p -> F p.
Module IntPartNLexi.
Section IntPartNLexi.
Import DefaultSeqLexiOrder.
Variable d : nat.
Definition intpartnlexi := 'P_d.
#[local] Notation "'PLexi" := intpartnlexi.
Implicit Type (sh : 'PLexi).
#[export] HB.instance Definition _ := SubType.copy 'PLexi 'P_d.
#[export] HB.instance Definition _ := Finite.copy 'PLexi 'P_d.
#[export] HB.instance Definition _ := [Order of 'PLexi by <:].
Lemma leEintpartnlexi sh1 sh2 :
(sh1 <= sh2)%O = (sh1 <= sh2 :> seqlexi nat)%O.
Lemma ltEintpartnlexi sh1 sh2 :
(sh1 < sh2)%O = (sh1 < sh2 :> seqlexi nat)%O.
Lemma rowpartn_top sh : (sh <= rowpartn d :> 'PLexi)%O.
Lemma colpartn_bot sh : (colpartn d <= sh :> 'PLexi)%O.
#[export] HB.instance Definition _ :=
Order.hasBottom.Build Order.lexi_display 'PLexi colpartn_bot.
#[export] HB.instance Definition _ :=
Order.hasTop.Build Order.lexi_display 'PLexi rowpartn_top.
#[export] HB.instance Definition _ :=
isInhabitedType.Build 'PLexi (rowpartn d).
Lemma botEintpartnlexi : 0%O = colpartn d :> 'PLexi.
Lemma topEintpartnlexi : 1%O = rowpartn d :> 'PLexi.
End IntPartNLexi.
Module Exports.
Notation "''PLexi_' n" := (intpartnlexi n).
Definition leEintpartnlexi := leEintpartnlexi.
Definition ltEintpartnlexi := ltEintpartnlexi.
Definition botEintpartnlexi := botEintpartnlexi.
Definition topEintpartnlexi := topEintpartnlexi.
End Exports.
End IntPartNLexi.
Fixpoint intpartnsk_nb sm sz mx : nat :=
if sz is sz.+1 then
iteri (minn sm mx) (fun i n => n + intpartnsk_nb (sm - i.+1) sz i.+1) 0
else if sm is sm.+1 then 0 else 1.
Definition intpartns_nb sm sz := intpartnsk_nb sm sz sm.
Definition intpartn_nb sm :=
iteri (sm.+1) (fun sz n => n + intpartns_nb sm sz) 0.
Lemma size_enum_partnsk sm sz mx :
size (enum_partnsk sm sz mx) = (intpartnsk_nb sm sz mx).
Lemma size_enum_partns sm sz : size (enum_partns sm sz) = (intpartns_nb sm sz).
Lemma size_enum_partn sm : size (enum_partn sm) = intpartn_nb sm.
Lemma card_intpartn sm : #|{:'P_sm}| = intpartn_nb sm.
#[export] Hint Resolve intpartP intpart_sorted intpartnP intpartn_sorted : core.
Section BoxInSkew.
Variable inner outer : seq nat.
Structure box_skew : Set :=
BoxSkew {box_skewval :> nat * nat; _ : in_skew inner outer box_skewval}.
Lemma box_skewP (rc : box_skew) : in_skew inner outer rc.
Definition enum_box_skew :=
[seq (r, c) | r <- iota 0 (size outer),
c <- iota (nth 0 inner r) (nth 0 outer r - nth 0 inner r)].
Lemma enum_box_skew_uniq : uniq enum_box_skew.
Lemma mem_enum_box_skew : enum_box_skew =i in_skew inner outer.
Lemma enum_box_skewE : map val (enum {: box_skew}) = enum_box_skew.
Lemma card_box_skew : #|{: box_skew}| = sumn (outer / inner).
Variable inner outer : seq nat.
Structure box_skew : Set :=
BoxSkew {box_skewval :> nat * nat; _ : in_skew inner outer box_skewval}.
Lemma box_skewP (rc : box_skew) : in_skew inner outer rc.
Definition enum_box_skew :=
[seq (r, c) | r <- iota 0 (size outer),
c <- iota (nth 0 inner r) (nth 0 outer r - nth 0 inner r)].
Lemma enum_box_skew_uniq : uniq enum_box_skew.
Lemma mem_enum_box_skew : enum_box_skew =i in_skew inner outer.
Lemma enum_box_skewE : map val (enum {: box_skew}) = enum_box_skew.
Lemma card_box_skew : #|{: box_skew}| = sumn (outer / inner).
Lemma big_box_skew R (idx : R) (op : Monoid.com_law idx) (f : nat * nat -> R):
\big[op/idx]_(b : box_skew) f b = \big[op/idx]_(b <- enum_box_skew) f b.
Lemma big_box_skew2 R (idx : R) (op : Monoid.com_law idx) (f : nat -> nat -> R):
\big[op/idx]_(b : box_skew) f b.1 b.2 =
\big[op/idx]_(b <- enum_box_skew) f b.1 b.2.
Lemma big_enum_box_skew
(R : Type) (idx : R) (op : Monoid.law idx) (f : nat -> nat -> R):
\big[op/idx]_(b <- enum_box_skew) f b.1 b.2 =
\big[op/idx]_(0 <= r < size outer)
\big[op/idx]_(nth 0 inner r <= c < nth 0 outer r) f r c.
End BoxInSkew.
#[export] Hint Resolve box_skewP : core.
Notation box_in := (box_skew [::]).
Notation enum_box_in := (enum_box_skew [::]).
Lemma BoxIn_subproof sh rc : in_shape sh rc -> in_skew [::] sh rc.
Definition BoxIn sh rc (rc_sh : in_shape sh rc) : box_in sh :=
BoxSkew (BoxIn_subproof rc_sh).
Lemma box_inP sh (rc : box_in sh) : in_shape sh rc.
Lemma big_enum_box_in sh
(R : Type) (idx : R) (op : Monoid.law idx) (f : nat -> nat -> R):
\big[op/idx]_(b <- enum_box_in sh ) f b.1 b.2 =
\big[op/idx]_(0 <= r < size sh)
\big[op/idx]_(0 <= c < nth 0 sh r) f r c.
Lemma card_box_in sh : #|{: box_in sh}| = sumn sh.
Lemma enum_box_in_uniq sh : uniq (enum_box_in sh).
Lemma mem_enum_box_in sh : enum_box_in sh =i in_shape sh.
\big[op/idx]_(b : box_skew) f b = \big[op/idx]_(b <- enum_box_skew) f b.
Lemma big_box_skew2 R (idx : R) (op : Monoid.com_law idx) (f : nat -> nat -> R):
\big[op/idx]_(b : box_skew) f b.1 b.2 =
\big[op/idx]_(b <- enum_box_skew) f b.1 b.2.
Lemma big_enum_box_skew
(R : Type) (idx : R) (op : Monoid.law idx) (f : nat -> nat -> R):
\big[op/idx]_(b <- enum_box_skew) f b.1 b.2 =
\big[op/idx]_(0 <= r < size outer)
\big[op/idx]_(nth 0 inner r <= c < nth 0 outer r) f r c.
End BoxInSkew.
#[export] Hint Resolve box_skewP : core.
Notation box_in := (box_skew [::]).
Notation enum_box_in := (enum_box_skew [::]).
Lemma BoxIn_subproof sh rc : in_shape sh rc -> in_skew [::] sh rc.
Definition BoxIn sh rc (rc_sh : in_shape sh rc) : box_in sh :=
BoxSkew (BoxIn_subproof rc_sh).
Lemma box_inP sh (rc : box_in sh) : in_shape sh rc.
Lemma big_enum_box_in sh
(R : Type) (idx : R) (op : Monoid.law idx) (f : nat -> nat -> R):
\big[op/idx]_(b <- enum_box_in sh ) f b.1 b.2 =
\big[op/idx]_(0 <= r < size sh)
\big[op/idx]_(0 <= c < nth 0 sh r) f r c.
Lemma card_box_in sh : #|{: box_in sh}| = sumn sh.
Lemma enum_box_in_uniq sh : uniq (enum_box_in sh).
Lemma mem_enum_box_in sh : enum_box_in sh =i in_shape sh.
Lemma box_in_incr_nth sh i :
perm_eq ((i, nth 0 sh i) :: enum_box_in sh) (enum_box_in (incr_nth sh i)).
perm_eq ((i, nth 0 sh i) :: enum_box_in sh) (enum_box_in (incr_nth sh i)).
Lemma merge_is_part l k :
is_part l -> is_part k -> is_part (merge geq l k).
Lemma merge_sortedE l k :
is_part l -> is_part k -> merge geq l k = sort geq (l ++ k).
Lemma sumn_union_part l k : sumn (merge geq l k) = sumn l + sumn k.
Fact union_intpart_subproof (l : intpart) (k : intpart) :
is_part (merge geq l k).
Definition union_intpart (l : intpart) (k : intpart) :=
IntPart (union_intpart_subproof l k).
Lemma union_intpartE l k : val (union_intpart l k) = sort geq (l ++ k).
Lemma perm_union_intpart l k : perm_eq (union_intpart l k) (l ++ k).
Lemma union_intpartC l k : union_intpart l k = union_intpart k l.
Lemma union_intpartA l k j :
union_intpart l (union_intpart k j) = union_intpart (union_intpart k l) j.
Section UnionPart.
Variables (m n : nat) (l : 'P_m) (k : 'P_n).
Lemma union_intpartn_subproof : is_part_of_n (m + n) (merge geq l k).
Definition union_intpartn := IntPartN union_intpartn_subproof.
Lemma union_intpartnE : val union_intpartn = sort geq (l ++ k).
Lemma perm_union_intpartn : perm_eq union_intpartn (l ++ k).
End UnionPart.
Notation "a +|+ b" := (union_intpartn a b) (at level 50) : Combi_scope.
Bind Scope Combi_scope with intpartn.
Section IntpartnCons.
Import LeqGeqOrder.
Variables (d l0 : nat) (la : seq nat).
Hypotheses (Hla : is_part_of_n d la)
(Hlla : is_part_of_n (l0 + d)%N (l0 :: la)).
Lemma intpartn_cons : IntPartN Hlla = rowpartn l0 +|+ IntPartN Hla.
End IntpartnCons.
Module YoungLattice.
Section YoungLattice.
Definition intpartYoung := intpart.
#[local] Notation "'YL" := intpartYoung.
Implicit Type (p q sh : 'YL).
Definition le_Young p q := included p q.
Fact le_Young_refl : reflexive le_Young.
Fact le_Young_trans : transitive le_Young.
Fact le_Young_anti : antisymmetric le_Young.
#[export] HB.instance Definition _ := Countable.copy 'YL intpart.
#[export] HB.instance Definition _ := Inhabited.copy 'YL intpart.
Fact Young_display : unit.
#[export] HB.instance Definition _ :=
Order.Le_isPOrder.Build
Young_display 'YL le_Young_refl le_Young_anti le_Young_trans.
Lemma le_YoungE sh1 sh2 : (sh1 <= sh2)%O = (included sh1 sh2).
Lemma le_YoungP sh1 sh2 :
reflect (forall i, nth 0 sh1 i <= nth 0 sh2 i) (sh1 <= sh2)%O.
Lemma le_Young_sumn: {homo (fun x : 'YL => sumn x) : x y / (x <= y)%O }.
Lemma lt_Young_sumn: {homo (fun x : 'YL => sumn x) : x y / (x < y)%O }.
Definition meet_Young_fun sh1 sh2 := [seq minn a.1 a.2 | a <- zip sh1 sh2].
Lemma size_meet_Young sh1 sh2 :
size (meet_Young_fun sh1 sh2) = minn (size sh1) (size sh2).
Lemma nth_meet_Young sh1 sh2 i :
nth 0 (meet_Young_fun sh1 sh2) i = minn (nth 0 sh1 i) (nth 0 sh2 i).
Fact meet_Young_subproof sh1 sh2 : is_part (meet_Young_fun sh1 sh2).
Definition meet_Young sh1 sh2 : 'YL := IntPart (meet_Young_subproof sh1 sh2).
Lemma meet_YoungC : commutative meet_Young.
Lemma meet_Young_le sh1 sh2 : (meet_Young sh1 sh2 <= sh1)%O.
Fact meet_YoungP sh sh1 sh2 :
(sh <= meet_Young sh1 sh2)%O = (sh <= sh1)%O && (sh <= sh2)%O.
Definition join_Young_fun sh1 sh2 :=
[seq maxn a.1 a.2 | a <- zip (pad 0 (maxn (size sh1) (size sh2)) sh1)
(pad 0 (maxn (size sh1) (size sh2)) sh2)].
Lemma size_join_Young sh1 sh2 :
size (join_Young_fun sh1 sh2) = maxn (size sh1) (size sh2).
Lemma nth_join_Young sh1 sh2 i :
nth 0 (join_Young_fun sh1 sh2) i = maxn (nth 0 sh1 i) (nth 0 sh2 i).
Fact join_Young_subproof sh1 sh2 : is_part (join_Young_fun sh1 sh2).
Definition join_Young sh1 sh2 : 'YL := IntPart (join_Young_subproof sh1 sh2).
Lemma join_Young_le sh1 sh2 : (sh1 <= join_Young sh1 sh2)%O.
Lemma join_YoungC : commutative join_Young.
Fact join_YoungP sh1 sh2 sh :
(join_Young sh1 sh2 <= sh)%O = (sh1 <= sh)%O && (sh2 <= sh)%O.
#[export] HB.instance Definition _ :=
Order.POrder_MeetJoin_isLattice.Build
Young_display 'YL meet_YoungP join_YoungP.
Fact emptypart_bottom sh : (empty_intpart <= sh :> 'YL)%O.
Lemma bottom_YoungE : 0%O = empty_intpart :> 'YL.
Fact Young_meetUl : @left_distributive 'YL 'YL Order.meet Order.join.
#[export] HB.instance Definition _ :=
Order.Lattice_Meet_isDistrLattice.Build Young_display 'YL Young_meetUl.
End YoungLattice.
Module Exports.
Implicit Type (p q : intpartYoung).
Notation intpartYoung := intpartYoung.
Definition le_YoungE := le_YoungE.
Definition le_YoungP := le_YoungP.
Definition le_Young_sumn := le_Young_sumn.
Definition lt_Young_sumn := lt_Young_sumn.
Lemma meet_YoungE p q :
(p `&` q)%O = [seq minn a.1 a.2 | a <- zip p q] :> seq nat.
Lemma nth_meet_Young p q i :
nth 0 (p `&` q)%O i = minn (nth 0 p i) (nth 0 q i).
Lemma size_meet_Young p q : size (p `&` q)%O = minn (size p) (size q).
Lemma join_YoungE p q :
(p `|` q)%O =
[seq maxn a.1 a.2 | a <- zip (pad 0 (maxn (size p) (size q)) p)
(pad 0 (maxn (size p) (size q)) q)] :> seq nat.
Lemma nth_join_Young p q i :
nth 0 (p `|` q)%O i = maxn (nth 0 p i) (nth 0 q i).
Lemma size_join_Young p q : size (p `|` q)%O = maxn (size p) (size q).
Definition bottom_YoungE := bottom_YoungE.
End Exports.
End YoungLattice.
Section YoungLattice.
Definition intpartYoung := intpart.
#[local] Notation "'YL" := intpartYoung.
Implicit Type (p q sh : 'YL).
Definition le_Young p q := included p q.
Fact le_Young_refl : reflexive le_Young.
Fact le_Young_trans : transitive le_Young.
Fact le_Young_anti : antisymmetric le_Young.
#[export] HB.instance Definition _ := Countable.copy 'YL intpart.
#[export] HB.instance Definition _ := Inhabited.copy 'YL intpart.
Fact Young_display : unit.
#[export] HB.instance Definition _ :=
Order.Le_isPOrder.Build
Young_display 'YL le_Young_refl le_Young_anti le_Young_trans.
Lemma le_YoungE sh1 sh2 : (sh1 <= sh2)%O = (included sh1 sh2).
Lemma le_YoungP sh1 sh2 :
reflect (forall i, nth 0 sh1 i <= nth 0 sh2 i) (sh1 <= sh2)%O.
Lemma le_Young_sumn: {homo (fun x : 'YL => sumn x) : x y / (x <= y)%O }.
Lemma lt_Young_sumn: {homo (fun x : 'YL => sumn x) : x y / (x < y)%O }.
Definition meet_Young_fun sh1 sh2 := [seq minn a.1 a.2 | a <- zip sh1 sh2].
Lemma size_meet_Young sh1 sh2 :
size (meet_Young_fun sh1 sh2) = minn (size sh1) (size sh2).
Lemma nth_meet_Young sh1 sh2 i :
nth 0 (meet_Young_fun sh1 sh2) i = minn (nth 0 sh1 i) (nth 0 sh2 i).
Fact meet_Young_subproof sh1 sh2 : is_part (meet_Young_fun sh1 sh2).
Definition meet_Young sh1 sh2 : 'YL := IntPart (meet_Young_subproof sh1 sh2).
Lemma meet_YoungC : commutative meet_Young.
Lemma meet_Young_le sh1 sh2 : (meet_Young sh1 sh2 <= sh1)%O.
Fact meet_YoungP sh sh1 sh2 :
(sh <= meet_Young sh1 sh2)%O = (sh <= sh1)%O && (sh <= sh2)%O.
Definition join_Young_fun sh1 sh2 :=
[seq maxn a.1 a.2 | a <- zip (pad 0 (maxn (size sh1) (size sh2)) sh1)
(pad 0 (maxn (size sh1) (size sh2)) sh2)].
Lemma size_join_Young sh1 sh2 :
size (join_Young_fun sh1 sh2) = maxn (size sh1) (size sh2).
Lemma nth_join_Young sh1 sh2 i :
nth 0 (join_Young_fun sh1 sh2) i = maxn (nth 0 sh1 i) (nth 0 sh2 i).
Fact join_Young_subproof sh1 sh2 : is_part (join_Young_fun sh1 sh2).
Definition join_Young sh1 sh2 : 'YL := IntPart (join_Young_subproof sh1 sh2).
Lemma join_Young_le sh1 sh2 : (sh1 <= join_Young sh1 sh2)%O.
Lemma join_YoungC : commutative join_Young.
Fact join_YoungP sh1 sh2 sh :
(join_Young sh1 sh2 <= sh)%O = (sh1 <= sh)%O && (sh2 <= sh)%O.
#[export] HB.instance Definition _ :=
Order.POrder_MeetJoin_isLattice.Build
Young_display 'YL meet_YoungP join_YoungP.
Fact emptypart_bottom sh : (empty_intpart <= sh :> 'YL)%O.
Lemma bottom_YoungE : 0%O = empty_intpart :> 'YL.
Fact Young_meetUl : @left_distributive 'YL 'YL Order.meet Order.join.
#[export] HB.instance Definition _ :=
Order.Lattice_Meet_isDistrLattice.Build Young_display 'YL Young_meetUl.
End YoungLattice.
Module Exports.
Implicit Type (p q : intpartYoung).
Notation intpartYoung := intpartYoung.
Definition le_YoungE := le_YoungE.
Definition le_YoungP := le_YoungP.
Definition le_Young_sumn := le_Young_sumn.
Definition lt_Young_sumn := lt_Young_sumn.
Lemma meet_YoungE p q :
(p `&` q)%O = [seq minn a.1 a.2 | a <- zip p q] :> seq nat.
Lemma nth_meet_Young p q i :
nth 0 (p `&` q)%O i = minn (nth 0 p i) (nth 0 q i).
Lemma size_meet_Young p q : size (p `&` q)%O = minn (size p) (size q).
Lemma join_YoungE p q :
(p `|` q)%O =
[seq maxn a.1 a.2 | a <- zip (pad 0 (maxn (size p) (size q)) p)
(pad 0 (maxn (size p) (size q)) q)] :> seq nat.
Lemma nth_join_Young p q i :
nth 0 (p `|` q)%O i = maxn (nth 0 p i) (nth 0 q i).
Lemma size_join_Young p q : size (p `|` q)%O = maxn (size p) (size q).
Definition bottom_YoungE := bottom_YoungE.
End Exports.
End YoungLattice.
Definition partdomsh n1 n2 (s1 s2 : seq nat) :=
all
(fun i => n1 + sumn (take i s1) <= n2 + sumn (take i s2))
(iota 0 (size s1).+1).
Definition partdom := partdomsh 0 0.
Lemma partdomshP {n1 n2 s1 s2} :
reflect (forall i, n1 + sumn (take i s1) <= n2 + sumn (take i s2))
(partdomsh n1 n2 s1 s2).
Lemma partdomP s1 s2 :
reflect (forall i, sumn (take i s1) <= sumn (take i s2)) (partdom s1 s2).
Lemma partdomsh_add y n1 n2 s1 s2 :
partdomsh (y + n1) (y + n2) s1 s2 = partdomsh n1 n2 s1 s2.
Lemma partdom_nil s : partdom [::] s.
Lemma partdom_refl : reflexive partdom.
#[export] Hint Resolve partdom_nil partdom_refl : core.
Lemma partdom_trans : transitive partdom.
Lemma partdom_anti s1 s2 :
is_part s1 -> is_part s2 -> partdom s1 s2 -> partdom s2 s1 -> s1 = s2.
Lemma partdomsh_cons2 y1 y2 s t n1 n2 :
partdomsh n1 n2 (y1 :: s) (y2 :: t) =
(n1 <= n2) && (partdomsh (n1 + y1) (n2 + y2) s t).
Lemma partdomsh_cons2E y s t n1 n2 :
partdomsh n1 n2 (y :: s) (y :: t) = partdomsh n1 n2 s t.
Lemma partdom_consK x s1 s2 : partdom (x :: s1) (x :: s2) -> partdom s1 s2.
Lemma sumn_take_merge t x i :
is_part t ->
sumn (take i.+1 (merge geq [:: x] t)) =
maxn (sumn (take i.+1 t)) (x + sumn (take i t)).
Lemma merge_cons x s t :
is_part (x :: s) -> is_part t ->
merge geq (x :: s) t = merge geq [:: x] (merge geq s t).
Lemma partdomsh_merge1 n1 n2 x t1 t2 :
is_part t1 -> is_part t2 ->
partdomsh n1 n2 t1 t2 ->
partdomsh n1 n2 (merge geq [:: x] t1) (merge geq [:: x] t2).
Lemma partdomsh_merge n1 n2 s t1 t2 :
is_part s -> is_part t1 -> is_part t2 ->
partdomsh n1 n2 t1 t2 ->
partdomsh n1 n2 (merge geq s t1) (merge geq s t2).
Lemma partdom_union_intpartl (s t1 t2 : intpart) :
partdom t1 t2 -> partdom (union_intpart s t1) (union_intpart s t2).
Lemma partdom_union_intpartr (s t1 t2 : intpart) :
partdom t1 t2 -> partdom (union_intpart t1 s) (union_intpart t2 s).
Lemma partdom_union_intpart (s1 s2 t1 t2 : intpart) :
partdom s1 s2 -> partdom t1 t2 ->
partdom (union_intpart s1 t1) (union_intpart s2 t2).
Module IntPartNDom.
Section IntPartNDom.
Variable d : nat.
Definition intpartndom := 'P_d.
#[local] Notation "'PDom" := intpartndom.
Implicit Type (sh : 'PDom).
#[export] HB.instance Definition _ := Finite.copy 'PDom 'P_d.
#[export] HB.instance Definition _ := Inhabited.copy 'PDom 'P_d.
Fact partdom_antisym : antisymmetric (fun x y : 'P_d => partdom x y).
Lemma partdom_display : unit.
#[export] HB.instance Definition _ :=
Order.Le_isPOrder.Build partdom_display 'PDom
partdom_refl partdom_antisym partdom_trans.
Lemma leEpartdom : @Order.le partdom_display 'PDom = partdom.
#[local] Notation "sh '^#'" := (conj_intpartn sh : 'PDom)
(at level 10, format "sh '^#'").
Lemma sum_diff sh i :
\sum_(l <- sh) (l - i) =
\sum_(l <- take (nth 0 (conj_part sh) i) sh) (l - i).
Lemma partdom_conj_intpartn sh1 sh2 : (sh2^# <= sh1^#)%O = (sh1 <= sh2)%O.
Lemma take_intpartn_over sh i : d <= i -> take i sh = sh.
Implicit Type t : d.+1.-tuple nat.
Definition parttuple sh := [tuple sumn (take i sh) | i < d.+1].
Definition from_parttuple t :=
rem_trail0 [seq nth 0 t i.+1 - nth 0 t i | i <- iota 0 d].
Definition is_parttuple t :=
[&& tnth t ord0 == 0, tnth t ord_max == d, sorted leq t &
all (fun i => (nth 0 t i).*2 >= nth 0 t i.-1 + nth 0 t i.+1)
(iota 1 d.-1)].
Lemma is_parttupleP t :
reflect
[/\ tnth t ord0 = 0, tnth t ord_max = d, sorted leq t &
forall i, 0 < i < d -> (nth 0 t i).*2 >= nth 0 t i.-1 + nth 0 t i.+1]
(is_parttuple t).
Lemma nth_parttuple i sh :
i < d.+1 -> nth 0 (parttuple sh) i = sumn (take i sh).
Lemma parttupleP sh : is_parttuple (parttuple sh).
Lemma sum_diff_tuple t :
sorted leq t ->
forall i, i < d.+1 ->
\sum_(0 <= j < i) (nth 0 t j.+1 - nth 0 t j) = nth 0 t i - nth 0 t 0.
Lemma from_parttupleP t : is_parttuple t -> is_part_of_n d (from_parttuple t).
Definition part_fromtuple t (H : is_parttuple t) :=
IntPartN (from_parttupleP H).
Lemma sumn_take_part_fromtuple t (H : is_parttuple t) i :
i < d.+1 -> sumn (take i (part_fromtuple H)) = nth 0 t i.
Lemma from_parttupleK t (H : is_parttuple t) :
parttuple (part_fromtuple H) = t.
Lemma parttupleK sh : from_parttuple (parttuple sh) = sh.
Lemma parttuplePK sh : part_fromtuple (parttupleP sh) = sh.
Definition parttuple_minn sh1 sh2 :=
[tuple minn (tnth (parttuple sh1) i) (tnth (parttuple sh2) i) | i < d.+1].
Lemma parttuple_minnC sh1 sh2 :
parttuple_minn sh1 sh2 = parttuple_minn sh2 sh1.
Lemma nth_parttuple_minn i sh1 sh2 :
i < d.+1 -> nth 0 (parttuple_minn sh1 sh2) i =
minn (sumn (take i sh1)) (sumn (take i sh2)).
Lemma double_minn m n : (minn m n).*2 = minn m.*2 n.*2.
Lemma parttuple_minnP sh1 sh2 : is_parttuple (parttuple_minn sh1 sh2).
Definition meet_intpartn sh1 sh2 : 'PDom :=
IntPartN (from_parttupleP (parttuple_minnP sh1 sh2)).
Definition join_intpartn sh1 sh2 := (meet_intpartn (sh1^#) (sh2^#))^#.
Lemma meet_intpartnC sh1 sh2 : meet_intpartn sh1 sh2 = meet_intpartn sh2 sh1.
Lemma le_meet_intpartn sh1 sh2 : (meet_intpartn sh1 sh2 <= sh1)%O.
Fact meet_intpartnP sh sh1 sh2 :
(sh <= meet_intpartn sh1 sh2)%O = (sh <= sh1)%O && (sh <= sh2)%O.
Fact join_intpartnP sh1 sh2 sh :
(join_intpartn sh1 sh2 <= sh)%O = (sh1 <= sh)%O && (sh2 <= sh)%O.
#[export] HB.instance Definition _ :=
Order.POrder_MeetJoin_isLattice.Build partdom_display
'PDom meet_intpartnP join_intpartnP.
Lemma sumn_take_pardom_meet i sh1 sh2 :
sumn (take i (sh1 `&` sh2)%O) = minn (sumn (take i sh1)) (sumn (take i sh2)).
Lemma join_intpartnE sh1 sh2 : (sh1 `|` sh2)%O = (sh1^# `&` sh2^#)%O^#.
End IntPartNDom.
Section IntPartNTopBottom.
Variable d : nat.
#[local] Notation "'PDom" := (intpartndom d).
Implicit Type (sh : 'PDom).
Lemma partdom_rowpartn sh : (sh <= rowpartn d)%O.
Lemma partdom_colpartn sh : (colpartn d <= sh :> 'PDom)%O.
#[export] HB.instance Definition _ :=
Order.hasBottom.Build partdom_display 'PDom partdom_colpartn.
#[export] HB.instance Definition _ :=
Order.hasTop.Build partdom_display 'PDom partdom_rowpartn.
Lemma botEintpartndom : 0%O = colpartn d :> 'PDom.
Lemma topEintpartndom : 1%O = rowpartn d :> 'PDom.
End IntPartNTopBottom.
Module Exports.
Notation "''PDom_' n" := (intpartndom n).
Definition leEpartdom := leEpartdom.
Definition partdom_conj_intpartn := partdom_conj_intpartn.
Definition sumn_take_pardom_meet := sumn_take_pardom_meet.
Definition join_intpartnE := join_intpartnE.
Definition botEintpartndom := botEintpartndom.
Definition topEintpartndom := topEintpartndom.
End Exports.
End IntPartNDom.
Lemma le_intpartndomlexi d :
{homo (id : 'PDom_d -> 'PLexi_d) : x y / (x <= y)%O}.
Lemma lt_intpartndomlexi d :
{homo (id : 'PDom_d -> 'PLexi_d) : x y / (x < y)%O}.
all
(fun i => n1 + sumn (take i s1) <= n2 + sumn (take i s2))
(iota 0 (size s1).+1).
Definition partdom := partdomsh 0 0.
Lemma partdomshP {n1 n2 s1 s2} :
reflect (forall i, n1 + sumn (take i s1) <= n2 + sumn (take i s2))
(partdomsh n1 n2 s1 s2).
Lemma partdomP s1 s2 :
reflect (forall i, sumn (take i s1) <= sumn (take i s2)) (partdom s1 s2).
Lemma partdomsh_add y n1 n2 s1 s2 :
partdomsh (y + n1) (y + n2) s1 s2 = partdomsh n1 n2 s1 s2.
Lemma partdom_nil s : partdom [::] s.
Lemma partdom_refl : reflexive partdom.
#[export] Hint Resolve partdom_nil partdom_refl : core.
Lemma partdom_trans : transitive partdom.
Lemma partdom_anti s1 s2 :
is_part s1 -> is_part s2 -> partdom s1 s2 -> partdom s2 s1 -> s1 = s2.
Lemma partdomsh_cons2 y1 y2 s t n1 n2 :
partdomsh n1 n2 (y1 :: s) (y2 :: t) =
(n1 <= n2) && (partdomsh (n1 + y1) (n2 + y2) s t).
Lemma partdomsh_cons2E y s t n1 n2 :
partdomsh n1 n2 (y :: s) (y :: t) = partdomsh n1 n2 s t.
Lemma partdom_consK x s1 s2 : partdom (x :: s1) (x :: s2) -> partdom s1 s2.
Lemma sumn_take_merge t x i :
is_part t ->
sumn (take i.+1 (merge geq [:: x] t)) =
maxn (sumn (take i.+1 t)) (x + sumn (take i t)).
Lemma merge_cons x s t :
is_part (x :: s) -> is_part t ->
merge geq (x :: s) t = merge geq [:: x] (merge geq s t).
Lemma partdomsh_merge1 n1 n2 x t1 t2 :
is_part t1 -> is_part t2 ->
partdomsh n1 n2 t1 t2 ->
partdomsh n1 n2 (merge geq [:: x] t1) (merge geq [:: x] t2).
Lemma partdomsh_merge n1 n2 s t1 t2 :
is_part s -> is_part t1 -> is_part t2 ->
partdomsh n1 n2 t1 t2 ->
partdomsh n1 n2 (merge geq s t1) (merge geq s t2).
Lemma partdom_union_intpartl (s t1 t2 : intpart) :
partdom t1 t2 -> partdom (union_intpart s t1) (union_intpart s t2).
Lemma partdom_union_intpartr (s t1 t2 : intpart) :
partdom t1 t2 -> partdom (union_intpart t1 s) (union_intpart t2 s).
Lemma partdom_union_intpart (s1 s2 t1 t2 : intpart) :
partdom s1 s2 -> partdom t1 t2 ->
partdom (union_intpart s1 t1) (union_intpart s2 t2).
Module IntPartNDom.
Section IntPartNDom.
Variable d : nat.
Definition intpartndom := 'P_d.
#[local] Notation "'PDom" := intpartndom.
Implicit Type (sh : 'PDom).
#[export] HB.instance Definition _ := Finite.copy 'PDom 'P_d.
#[export] HB.instance Definition _ := Inhabited.copy 'PDom 'P_d.
Fact partdom_antisym : antisymmetric (fun x y : 'P_d => partdom x y).
Lemma partdom_display : unit.
#[export] HB.instance Definition _ :=
Order.Le_isPOrder.Build partdom_display 'PDom
partdom_refl partdom_antisym partdom_trans.
Lemma leEpartdom : @Order.le partdom_display 'PDom = partdom.
#[local] Notation "sh '^#'" := (conj_intpartn sh : 'PDom)
(at level 10, format "sh '^#'").
Lemma sum_diff sh i :
\sum_(l <- sh) (l - i) =
\sum_(l <- take (nth 0 (conj_part sh) i) sh) (l - i).
Lemma partdom_conj_intpartn sh1 sh2 : (sh2^# <= sh1^#)%O = (sh1 <= sh2)%O.
Lemma take_intpartn_over sh i : d <= i -> take i sh = sh.
Implicit Type t : d.+1.-tuple nat.
Definition parttuple sh := [tuple sumn (take i sh) | i < d.+1].
Definition from_parttuple t :=
rem_trail0 [seq nth 0 t i.+1 - nth 0 t i | i <- iota 0 d].
Definition is_parttuple t :=
[&& tnth t ord0 == 0, tnth t ord_max == d, sorted leq t &
all (fun i => (nth 0 t i).*2 >= nth 0 t i.-1 + nth 0 t i.+1)
(iota 1 d.-1)].
Lemma is_parttupleP t :
reflect
[/\ tnth t ord0 = 0, tnth t ord_max = d, sorted leq t &
forall i, 0 < i < d -> (nth 0 t i).*2 >= nth 0 t i.-1 + nth 0 t i.+1]
(is_parttuple t).
Lemma nth_parttuple i sh :
i < d.+1 -> nth 0 (parttuple sh) i = sumn (take i sh).
Lemma parttupleP sh : is_parttuple (parttuple sh).
Lemma sum_diff_tuple t :
sorted leq t ->
forall i, i < d.+1 ->
\sum_(0 <= j < i) (nth 0 t j.+1 - nth 0 t j) = nth 0 t i - nth 0 t 0.
Lemma from_parttupleP t : is_parttuple t -> is_part_of_n d (from_parttuple t).
Definition part_fromtuple t (H : is_parttuple t) :=
IntPartN (from_parttupleP H).
Lemma sumn_take_part_fromtuple t (H : is_parttuple t) i :
i < d.+1 -> sumn (take i (part_fromtuple H)) = nth 0 t i.
Lemma from_parttupleK t (H : is_parttuple t) :
parttuple (part_fromtuple H) = t.
Lemma parttupleK sh : from_parttuple (parttuple sh) = sh.
Lemma parttuplePK sh : part_fromtuple (parttupleP sh) = sh.
Definition parttuple_minn sh1 sh2 :=
[tuple minn (tnth (parttuple sh1) i) (tnth (parttuple sh2) i) | i < d.+1].
Lemma parttuple_minnC sh1 sh2 :
parttuple_minn sh1 sh2 = parttuple_minn sh2 sh1.
Lemma nth_parttuple_minn i sh1 sh2 :
i < d.+1 -> nth 0 (parttuple_minn sh1 sh2) i =
minn (sumn (take i sh1)) (sumn (take i sh2)).
Lemma double_minn m n : (minn m n).*2 = minn m.*2 n.*2.
Lemma parttuple_minnP sh1 sh2 : is_parttuple (parttuple_minn sh1 sh2).
Definition meet_intpartn sh1 sh2 : 'PDom :=
IntPartN (from_parttupleP (parttuple_minnP sh1 sh2)).
Definition join_intpartn sh1 sh2 := (meet_intpartn (sh1^#) (sh2^#))^#.
Lemma meet_intpartnC sh1 sh2 : meet_intpartn sh1 sh2 = meet_intpartn sh2 sh1.
Lemma le_meet_intpartn sh1 sh2 : (meet_intpartn sh1 sh2 <= sh1)%O.
Fact meet_intpartnP sh sh1 sh2 :
(sh <= meet_intpartn sh1 sh2)%O = (sh <= sh1)%O && (sh <= sh2)%O.
Fact join_intpartnP sh1 sh2 sh :
(join_intpartn sh1 sh2 <= sh)%O = (sh1 <= sh)%O && (sh2 <= sh)%O.
#[export] HB.instance Definition _ :=
Order.POrder_MeetJoin_isLattice.Build partdom_display
'PDom meet_intpartnP join_intpartnP.
Lemma sumn_take_pardom_meet i sh1 sh2 :
sumn (take i (sh1 `&` sh2)%O) = minn (sumn (take i sh1)) (sumn (take i sh2)).
Lemma join_intpartnE sh1 sh2 : (sh1 `|` sh2)%O = (sh1^# `&` sh2^#)%O^#.
End IntPartNDom.
Section IntPartNTopBottom.
Variable d : nat.
#[local] Notation "'PDom" := (intpartndom d).
Implicit Type (sh : 'PDom).
Lemma partdom_rowpartn sh : (sh <= rowpartn d)%O.
Lemma partdom_colpartn sh : (colpartn d <= sh :> 'PDom)%O.
#[export] HB.instance Definition _ :=
Order.hasBottom.Build partdom_display 'PDom partdom_colpartn.
#[export] HB.instance Definition _ :=
Order.hasTop.Build partdom_display 'PDom partdom_rowpartn.
Lemma botEintpartndom : 0%O = colpartn d :> 'PDom.
Lemma topEintpartndom : 1%O = rowpartn d :> 'PDom.
End IntPartNTopBottom.
Module Exports.
Notation "''PDom_' n" := (intpartndom n).
Definition leEpartdom := leEpartdom.
Definition partdom_conj_intpartn := partdom_conj_intpartn.
Definition sumn_take_pardom_meet := sumn_take_pardom_meet.
Definition join_intpartnE := join_intpartnE.
Definition botEintpartndom := botEintpartndom.
Definition topEintpartndom := topEintpartndom.
End Exports.
End IntPartNDom.
Lemma le_intpartndomlexi d :
{homo (id : 'PDom_d -> 'PLexi_d) : x y / (x <= y)%O}.
Lemma lt_intpartndomlexi d :
{homo (id : 'PDom_d -> 'PLexi_d) : x y / (x < y)%O}.
Section SetPartitionShape.
Variable T : finType.
Implicit Types (A B X : {set T}) (P Q : {set {set T}}).
Lemma count_set_of_card (p : pred nat) P :
count p [seq #{x} | x in P] = #|P :&: [set x | p #{x}]|.
Definition setpart_shape P := sort geq [seq #{X} | X in P].
Lemma setpart_shapeP P D :
partition P D -> is_part_of_n #|D| (setpart_shape P).
Lemma ex_subset_card B k :
k <= #{B} -> exists2 A : {set T}, A \subset B & #{A} == k.
Lemma ex_setpart_shape (s : seq nat) (A : {set T}) :
sumn s = #|A| -> 0 \notin s ->
exists P : seq {set T},
[/\ uniq P, partition [set X in P] A & [seq #{X} | X <- P] = s].
Lemma ex_set_setpart_shape A (sh : 'P_#|A|) :
exists2 P, partition P A & setpart_shape P = sh.
Lemma setpart_shape_union P Q :
[disjoint P & Q] ->
setpart_shape (P :|: Q) = sort geq (setpart_shape P ++ setpart_shape Q).
End SetPartitionShape.
Lemma setpart_shape_imset
(T1 T2 : finType) (f : T1 -> T2) (A : {set {set T1}}) :
injective f ->
setpart_shape [set f @: x | x : {set T1} in A] = setpart_shape A.
Variable T : finType.
Implicit Types (A B X : {set T}) (P Q : {set {set T}}).
Lemma count_set_of_card (p : pred nat) P :
count p [seq #{x} | x in P] = #|P :&: [set x | p #{x}]|.
Definition setpart_shape P := sort geq [seq #{X} | X in P].
Lemma setpart_shapeP P D :
partition P D -> is_part_of_n #|D| (setpart_shape P).
Lemma ex_subset_card B k :
k <= #{B} -> exists2 A : {set T}, A \subset B & #{A} == k.
Lemma ex_setpart_shape (s : seq nat) (A : {set T}) :
sumn s = #|A| -> 0 \notin s ->
exists P : seq {set T},
[/\ uniq P, partition [set X in P] A & [seq #{X} | X <- P] = s].
Lemma ex_set_setpart_shape A (sh : 'P_#|A|) :
exists2 P, partition P A & setpart_shape P = sh.
Lemma setpart_shape_union P Q :
[disjoint P & Q] ->
setpart_shape (P :|: Q) = sort geq (setpart_shape P ++ setpart_shape Q).
End SetPartitionShape.
Lemma setpart_shape_imset
(T1 T2 : finType) (f : T1 -> T2) (A : {set {set T1}}) :
injective f ->
setpart_shape [set f @: x | x : {set T1} in A] = setpart_shape A.