Library Combi.Combi.composition: Integer Composition
Integer Compositions.
- is_comp s == s is a composition, ie. s doesn't contains any 0
- is_comp_of_n sm s == s is a composition of sum sm
- intcomp == a sigma type for is_comp
- intcompn sm == a sigma type for the predicate is_comp_of_n sm.
this is canonically a subFinType
- rowcomp n == the trivial composition
- rowcompn n == the trivial composition as a intcompn n
- colcomp n == the composition [:: 1; 1; ...]
- colcompn n == the composition [:: 1; 1; ...] as a intcompn n
- rev_intcompn c == the reverse composition inside intcompn n.
- partsums s == sorted sequence of partial sums (excluding the trivial and full sum)
- descset c == the descent set of c : intcompn n
- from_descset d == the composition (of type c : intcompn n) whose descent set is d : {set 'I_n.-1}.
- partn_of_compn n c == the partition in 'P_n obtained by sorting c : intcompn n
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import tools combclass sorted partition subseq ordtype.
Set Implicit Arguments.
Definition bottom := f' \bot%O.
Lemma isobottom x : (bottom <= x)%O.
Definition top := f' \top%O.
Lemma isotop x : (x <= top)%O.
From mathcomp Require Import all_ssreflect.
Require Import tools combclass sorted partition subseq ordtype.
Set Implicit Arguments.
Definition bottom := f' \bot%O.
Lemma isobottom x : (bottom <= x)%O.
Definition top := f' \top%O.
Lemma isotop x : (x <= top)%O.
Section Defs.
Implicit Type s : seq nat.
Definition is_comp s := 0 \notin s.
Lemma is_compP s : reflect (forall i, i \in s -> i != 0) (is_comp s).
Lemma is_comp1 i : is_comp [:: i] = (i != 0).
Lemma is_comp_cons i s : is_comp (i :: s) = (i != 0) && (is_comp s).
Lemma is_comp_rcons s sn : is_comp (rcons s sn) = (sn != 0) && (is_comp s).
Lemma is_comp_cat s1 s2 : is_comp (s1 ++ s2) = (is_comp s1) && (is_comp s2).
Lemma part_is_comp s : is_part s -> is_comp s.
Implicit Type s : seq nat.
Definition is_comp s := 0 \notin s.
Lemma is_compP s : reflect (forall i, i \in s -> i != 0) (is_comp s).
Lemma is_comp1 i : is_comp [:: i] = (i != 0).
Lemma is_comp_cons i s : is_comp (i :: s) = (i != 0) && (is_comp s).
Lemma is_comp_rcons s sn : is_comp (rcons s sn) = (sn != 0) && (is_comp s).
Lemma is_comp_cat s1 s2 : is_comp (s1 ++ s2) = (is_comp s1) && (is_comp s2).
Lemma part_is_comp s : is_part s -> is_comp s.
Compositions and sumn
Lemma comp0 s : is_comp s -> sumn s = 0 -> s = [::].
Lemma size_comp s : is_comp s -> size s <= sumn s.
End Defs.
Lemma size_comp s : is_comp s -> size s <= sumn s.
End Defs.
Structure intcomp : Type := IntComp {cval :> seq nat; _ : is_comp cval}.
Lemma intcompP (p : intcomp) : is_comp p.
#[export] Hint Resolve intcompP : core.
Fixpoint enum_compn_rec aux n : (seq (seq nat)) :=
if aux is aux'.+1 then
if n == 0 then [:: [::]]
else
flatten [seq [seq i :: p | p <- enum_compn_rec aux' (n - i) ] |
i <- iota 1 n]
else [:: [::]].
Definition enum_compn n := enum_compn_rec n n.
Definition is_comp_of_n sm := [pred s | (sumn s == sm) & is_comp s].
Lemma enum_compn_rec_any aux1 aux2 n :
n <= aux1 -> n <= aux2 -> enum_compn_rec aux1 n = enum_compn_rec aux2 n.
Lemma enum_compn_any aux n :
n <= aux -> enum_compn_rec aux n = enum_compn n.
Lemma enum_compnE n :
n != 0 ->
enum_compn n = flatten [seq [seq i :: p | p <- enum_compn (n - i) ] |
i <- iota 1 n].
Lemma enum_compn_allP n : all (is_comp_of_n n) (enum_compn n).
Lemma enum_compn_countE n :
forall s, is_comp_of_n n s -> count_mem s (enum_compn n) = 1.
Lemma enum_compnP n s : (is_comp_of_n n s) = (s \in enum_compn n).
Section CompOfn.
Variable n : nat.
Structure intcompn : Set :=
IntCompN {cnval :> seq nat; _ : is_comp_of_n n cnval}.
Implicit Type (c : intcompn) (d : {set 'I_n.-1}).
Lemma intcompnP c : is_comp c.
Hint Resolve intcompnP : core.
Definition intcomp_of_intcompn c := IntComp (intcompnP c).
Coercion intcomp_of_intcompn : intcompn >-> intcomp.
Lemma intcompn_sumn c : sumn c = n.
Lemma enum_intcompnE : map val (enum {:intcompn}) = enum_compn n.
Lemma card_intcompn : #|{:intcompn}| = 2 ^ n.-1.
Lemma rev_intcompn_spec c : is_comp_of_n n (rev c).
Definition rev_intcompn c := IntCompN (rev_intcompn_spec c).
Lemma rev_intcompnK : involutive rev_intcompn.
Lemma intcompP (p : intcomp) : is_comp p.
#[export] Hint Resolve intcompP : core.
Fixpoint enum_compn_rec aux n : (seq (seq nat)) :=
if aux is aux'.+1 then
if n == 0 then [:: [::]]
else
flatten [seq [seq i :: p | p <- enum_compn_rec aux' (n - i) ] |
i <- iota 1 n]
else [:: [::]].
Definition enum_compn n := enum_compn_rec n n.
Definition is_comp_of_n sm := [pred s | (sumn s == sm) & is_comp s].
Lemma enum_compn_rec_any aux1 aux2 n :
n <= aux1 -> n <= aux2 -> enum_compn_rec aux1 n = enum_compn_rec aux2 n.
Lemma enum_compn_any aux n :
n <= aux -> enum_compn_rec aux n = enum_compn n.
Lemma enum_compnE n :
n != 0 ->
enum_compn n = flatten [seq [seq i :: p | p <- enum_compn (n - i) ] |
i <- iota 1 n].
Lemma enum_compn_allP n : all (is_comp_of_n n) (enum_compn n).
Lemma enum_compn_countE n :
forall s, is_comp_of_n n s -> count_mem s (enum_compn n) = 1.
Lemma enum_compnP n s : (is_comp_of_n n s) = (s \in enum_compn n).
Section CompOfn.
Variable n : nat.
Structure intcompn : Set :=
IntCompN {cnval :> seq nat; _ : is_comp_of_n n cnval}.
Implicit Type (c : intcompn) (d : {set 'I_n.-1}).
Lemma intcompnP c : is_comp c.
Hint Resolve intcompnP : core.
Definition intcomp_of_intcompn c := IntComp (intcompnP c).
Coercion intcomp_of_intcompn : intcompn >-> intcomp.
Lemma intcompn_sumn c : sumn c = n.
Lemma enum_intcompnE : map val (enum {:intcompn}) = enum_compn n.
Lemma card_intcompn : #|{:intcompn}| = 2 ^ n.-1.
Lemma rev_intcompn_spec c : is_comp_of_n n (rev c).
Definition rev_intcompn c := IntCompN (rev_intcompn_spec c).
Lemma rev_intcompnK : involutive rev_intcompn.
Definition partsums s := [seq sumn (take i s) | i <- iota 1 (size s).-1].
Definition descset c : {set 'I_n.-1} :=
[set i in pmap insub [seq i.-1 | i <- partsums c]].
Lemma size_partsums s : size (partsums s) = (size s).-1.
Lemma partsums_cat s1 s2 :
s1 != [::] -> s2 != [::] ->
partsums (s1 ++ s2) =
partsums s1 ++ sumn s1 :: [seq sumn s1 + i | i <- partsums s2].
Lemma partsums_cons i s :
s != [::] -> partsums (i :: s) = i :: [seq i + j | j <- partsums s].
Lemma all_partsums c : all (fun i => 0 < i < n) (partsums c).
Lemma from_descset_spec d :
is_comp_of_n n (if n is 0 then [::]
else pairmap (fun a b => b - a) 0
(rcons [seq (val i).+1 | i in d] n)).
Definition from_descset d := IntCompN (from_descset_spec d).
Lemma diff_nth_sumn_take s i m :
m <= size s -> i.+1 < m ->
nth 0 [seq sumn (take i0 s) | i0 <- iota 1 m] i.+1 -
nth 0 [seq sumn (take i0 s) | i0 <- iota 1 m] i = nth 0 s i.+1.
Lemma sorted_ltn_partsums c : sorted ltn (partsums c).
Lemma val_descset c : [seq (val i).+1 | i in descset c] = partsums c.
Lemma card_descset c : #|descset c| = (size c).-1.
Lemma descsetK : cancel descset from_descset.
Lemma descset_inj : injective descset.
Lemma descset_bij : bijective descset.
Lemma from_descsetK : cancel from_descset descset.
End CompOfn.
Lemma intcompn0 (sh : intcompn 0) : sh = [::] :> seq nat.
Lemma intcompn1 (sh : intcompn 1) : sh = [:: 1] :> seq nat.
Lemma intcompn2 (sh : intcompn 2) :
sh = [:: 2] :> seq nat \/ sh = [:: 1; 1] :> seq nat.
Definition intcompn_cast m n (eq_mn : m = n) p :=
let: erefl in _ = n := eq_mn return intcompn n in p.
Lemma intcompn_castE m n (eq_mn : m = n) p :
val (intcompn_cast eq_mn p) = val p.
Definition rowcomp d := if d is _.+1 then [:: d] else [::].
Fact rowcompnP d : is_comp_of_n d (rowcomp d).
Canonical rowcompn d : intcompn d := IntCompN (rowcompnP d).
Definition colcomp d := nseq d 1%N.
Fact colcompnP d : is_comp_of_n d (colcomp d).
Canonical colcompn d : intcompn d := IntCompN (colcompnP d).
Section DescSet.
Variable (n : nat).
Implicit Types (c : intcompn n) (d : {set 'I_n.-1}).
Lemma mem_partsum_non0 u0 u i : i \in partsums (u0 :: u) -> u != [::].
Lemma mem_partsum_gt x v0 v1 v :
v0 < x -> x \in partsums (v0 :: v1 :: v) -> x \in partsums (v0 + v1 :: v).
Lemma subdescset_partsumP c1 c2 :
reflect {subset partsums c1 <= partsums c2} (descset c1 \subset descset c2).
Lemma subseq_partsumE c1 c2 :
(subseq (partsums c1) (partsums c2)) = (descset c1 \subset descset c2).
Lemma subdescsetP c1 c2 :
reflect (exists2 c : seq (seq nat), c1 = map sumn c :> seq nat &
c2 = flatten c :> seq nat)
(descset c1 \subset descset c2).
End DescSet.
Module RefinementOrder.
Section RefinementOrder.
Import Order.DefaultSetSubsetOrder.
Variable (n : nat).
Definition type := intcompn n.
#[local] Notation "'CRef" := type.
Implicit Types (c : 'CRef) (d : {set 'I_n.-1}).
#[local] Notation SetIn := ({set ('I_n.-1 : finType)}).
#[export] HB.instance Definition _ := SubType.copy 'CRef (intcompn n).
#[export] HB.instance Definition _ := Finite.copy 'CRef (intcompn n).
Fact compnref_display : unit.
#[export] HB.instance Definition _ : Order.isPOrder compnref_display 'CRef :=
Order.CanIsPartial compnref_display (@descsetK n).
#[export] HB.instance Definition _ :=
isInhabitedType.Build 'CRef (rowcompn n).
Lemma leEcompnref c1 c2 :
(c1 <= c2)%O = (descset c1 \subset descset c2).
Lemma descset_mono :
{mono (@descset n) : A B / (A <= B :> 'CRef)%O >-> (A <= B :> SetIn)%O}.
#[export] HB.instance Definition _ :=
Order.IsoLattice.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
Lemma descset_meet c1 c2 :
descset (c1 `&` c2)%O = descset c1 :&: descset c2.
Lemma descset_join c1 c2 :
descset (c1 `|` c2)%O = descset c1 :|: descset c2.
#[export] HB.instance Definition _ :=
Order.IsoDistrLattice.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
Lemma descset_rowcompn : descset (rowcompn n) = set0.
Lemma descset_colcompn : descset (colcompn n) = setT.
#[export] HB.instance Definition _ :=
IsoBottom.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
#[export] HB.instance Definition _ :=
IsoTop.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
Lemma topEcompnref : 1%O = colcompn n :> 'CRef.
Lemma botEcompnref : 0%O = rowcompn n :> 'CRef.
Lemma compnref_rev c1 c2 :
(rev_intcompn c1 <= rev_intcompn c2 :> 'CRef)%O = (c1 <= c2)%O.
End RefinementOrder.
Module Exports.
Notation intcompnref := type.
Definition leEcompnref := leEcompnref.
Definition descset_mono := descset_mono.
Definition descset_meet := descset_meet.
Definition descset_join := descset_join.
Definition topEcompnref := topEcompnref.
Definition botEcompnref := botEcompnref.
Definition compnref_rev := compnref_rev.
End Exports.
End RefinementOrder.
#[export] Hint Resolve intcompP intcompnP : core.
Lemma part_of_comp_subproof n (c : intcompn n) :
is_part_of_n n (sort geq c).
Canonical partn_of_compn n (c : intcompn n) :=
IntPartN (part_of_comp_subproof c).
Definition descset c : {set 'I_n.-1} :=
[set i in pmap insub [seq i.-1 | i <- partsums c]].
Lemma size_partsums s : size (partsums s) = (size s).-1.
Lemma partsums_cat s1 s2 :
s1 != [::] -> s2 != [::] ->
partsums (s1 ++ s2) =
partsums s1 ++ sumn s1 :: [seq sumn s1 + i | i <- partsums s2].
Lemma partsums_cons i s :
s != [::] -> partsums (i :: s) = i :: [seq i + j | j <- partsums s].
Lemma all_partsums c : all (fun i => 0 < i < n) (partsums c).
Lemma from_descset_spec d :
is_comp_of_n n (if n is 0 then [::]
else pairmap (fun a b => b - a) 0
(rcons [seq (val i).+1 | i in d] n)).
Definition from_descset d := IntCompN (from_descset_spec d).
Lemma diff_nth_sumn_take s i m :
m <= size s -> i.+1 < m ->
nth 0 [seq sumn (take i0 s) | i0 <- iota 1 m] i.+1 -
nth 0 [seq sumn (take i0 s) | i0 <- iota 1 m] i = nth 0 s i.+1.
Lemma sorted_ltn_partsums c : sorted ltn (partsums c).
Lemma val_descset c : [seq (val i).+1 | i in descset c] = partsums c.
Lemma card_descset c : #|descset c| = (size c).-1.
Lemma descsetK : cancel descset from_descset.
Lemma descset_inj : injective descset.
Lemma descset_bij : bijective descset.
Lemma from_descsetK : cancel from_descset descset.
End CompOfn.
Lemma intcompn0 (sh : intcompn 0) : sh = [::] :> seq nat.
Lemma intcompn1 (sh : intcompn 1) : sh = [:: 1] :> seq nat.
Lemma intcompn2 (sh : intcompn 2) :
sh = [:: 2] :> seq nat \/ sh = [:: 1; 1] :> seq nat.
Definition intcompn_cast m n (eq_mn : m = n) p :=
let: erefl in _ = n := eq_mn return intcompn n in p.
Lemma intcompn_castE m n (eq_mn : m = n) p :
val (intcompn_cast eq_mn p) = val p.
Definition rowcomp d := if d is _.+1 then [:: d] else [::].
Fact rowcompnP d : is_comp_of_n d (rowcomp d).
Canonical rowcompn d : intcompn d := IntCompN (rowcompnP d).
Definition colcomp d := nseq d 1%N.
Fact colcompnP d : is_comp_of_n d (colcomp d).
Canonical colcompn d : intcompn d := IntCompN (colcompnP d).
Section DescSet.
Variable (n : nat).
Implicit Types (c : intcompn n) (d : {set 'I_n.-1}).
Lemma mem_partsum_non0 u0 u i : i \in partsums (u0 :: u) -> u != [::].
Lemma mem_partsum_gt x v0 v1 v :
v0 < x -> x \in partsums (v0 :: v1 :: v) -> x \in partsums (v0 + v1 :: v).
Lemma subdescset_partsumP c1 c2 :
reflect {subset partsums c1 <= partsums c2} (descset c1 \subset descset c2).
Lemma subseq_partsumE c1 c2 :
(subseq (partsums c1) (partsums c2)) = (descset c1 \subset descset c2).
Lemma subdescsetP c1 c2 :
reflect (exists2 c : seq (seq nat), c1 = map sumn c :> seq nat &
c2 = flatten c :> seq nat)
(descset c1 \subset descset c2).
End DescSet.
Module RefinementOrder.
Section RefinementOrder.
Import Order.DefaultSetSubsetOrder.
Variable (n : nat).
Definition type := intcompn n.
#[local] Notation "'CRef" := type.
Implicit Types (c : 'CRef) (d : {set 'I_n.-1}).
#[local] Notation SetIn := ({set ('I_n.-1 : finType)}).
#[export] HB.instance Definition _ := SubType.copy 'CRef (intcompn n).
#[export] HB.instance Definition _ := Finite.copy 'CRef (intcompn n).
Fact compnref_display : unit.
#[export] HB.instance Definition _ : Order.isPOrder compnref_display 'CRef :=
Order.CanIsPartial compnref_display (@descsetK n).
#[export] HB.instance Definition _ :=
isInhabitedType.Build 'CRef (rowcompn n).
Lemma leEcompnref c1 c2 :
(c1 <= c2)%O = (descset c1 \subset descset c2).
Lemma descset_mono :
{mono (@descset n) : A B / (A <= B :> 'CRef)%O >-> (A <= B :> SetIn)%O}.
#[export] HB.instance Definition _ :=
Order.IsoLattice.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
Lemma descset_meet c1 c2 :
descset (c1 `&` c2)%O = descset c1 :&: descset c2.
Lemma descset_join c1 c2 :
descset (c1 `|` c2)%O = descset c1 :|: descset c2.
#[export] HB.instance Definition _ :=
Order.IsoDistrLattice.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
Lemma descset_rowcompn : descset (rowcompn n) = set0.
Lemma descset_colcompn : descset (colcompn n) = setT.
#[export] HB.instance Definition _ :=
IsoBottom.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
#[export] HB.instance Definition _ :=
IsoTop.Build compnref_display 'CRef
(@descsetK n) (@from_descsetK n) descset_mono.
Lemma topEcompnref : 1%O = colcompn n :> 'CRef.
Lemma botEcompnref : 0%O = rowcompn n :> 'CRef.
Lemma compnref_rev c1 c2 :
(rev_intcompn c1 <= rev_intcompn c2 :> 'CRef)%O = (c1 <= c2)%O.
End RefinementOrder.
Module Exports.
Notation intcompnref := type.
Definition leEcompnref := leEcompnref.
Definition descset_mono := descset_mono.
Definition descset_meet := descset_meet.
Definition descset_join := descset_join.
Definition topEcompnref := topEcompnref.
Definition botEcompnref := botEcompnref.
Definition compnref_rev := compnref_rev.
End Exports.
End RefinementOrder.
#[export] Hint Resolve intcompP intcompnP : core.
Lemma part_of_comp_subproof n (c : intcompn n) :
is_part_of_n n (sort geq c).
Canonical partn_of_compn n (c : intcompn n) :=
IntPartN (part_of_comp_subproof c).