Library Combi.Combi.vectNK: Integer Vector of Given Sums and Sizes
Integer vectors of sum n and size k
- vect_n_k n k == the list of integer vectors of sum n and size k
- cut_k k s == the list of the cutting of s in k slices (the result is of type seq (seq T))
- cut3 s == the list of the cutting of s in 3 slices (the result is of type seq (seq T) * (seq T) * (seq T))
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrbool ssrfun ssrnat eqtype seq.
Require Import tools.
Set Implicit Arguments.
Section VectNK.
Fixpoint vect_n_k n k :=
if k is k'.+1
then flatten (mkseq (fun i => map (cons i) (vect_n_k (n-i) k') ) n.+1)
else if n is 0 then [:: [::]] else [::].
Lemma vect_n_k_in n k s : sumn s == n -> size s == k -> s \in vect_n_k n k.
Lemma in_vect_n_k n k s : s \in vect_n_k n k -> (sumn s == n) && (size s == k).
Lemma vect_n_kP n k s : s \in vect_n_k n k = (sumn s == n) && (size s == k).
Lemma vect_0_k k : vect_n_k 0 k = [:: nseq k 0].
Lemma count_mem_vect_n_k_eq_1 n k s :
s \in vect_n_k n k -> count_mem s (vect_n_k n k) = 1.
Lemma uniq_vect_n_k n k : uniq (vect_n_k n k).
End VectNK.
From mathcomp Require Import ssrbool ssrfun ssrnat eqtype seq.
Require Import tools.
Set Implicit Arguments.
Section VectNK.
Fixpoint vect_n_k n k :=
if k is k'.+1
then flatten (mkseq (fun i => map (cons i) (vect_n_k (n-i) k') ) n.+1)
else if n is 0 then [:: [::]] else [::].
Lemma vect_n_k_in n k s : sumn s == n -> size s == k -> s \in vect_n_k n k.
Lemma in_vect_n_k n k s : s \in vect_n_k n k -> (sumn s == n) && (size s == k).
Lemma vect_n_kP n k s : s \in vect_n_k n k = (sumn s == n) && (size s == k).
Lemma vect_0_k k : vect_n_k 0 k = [:: nseq k 0].
Lemma count_mem_vect_n_k_eq_1 n k s :
s \in vect_n_k n k -> count_mem s (vect_n_k n k) = 1.
Lemma uniq_vect_n_k n k : uniq (vect_n_k n k).
End VectNK.
Cutting a seq in k slices : the result is of type seq (seq T)
Section CutK.
Variable T : eqType.
Implicit Type (s : seq T) (ss : seq (seq T)).
Lemma mem_shape_vect_n_k ss :
(shape ss) \in vect_n_k (size (flatten ss)) (size ss).
Definition cut_k k s := [seq reshape sh s | sh <- vect_n_k (size s) k].
Lemma cut_k_flatten ss : ss \in cut_k (size ss) (flatten ss).
Lemma flatten_equiv_cut_k s ss : s == flatten ss <-> ss \in cut_k (size ss) s.
Lemma size_cut_k k s ss : ss \in (cut_k k s) -> size ss = k.
End CutK.
Cutting a seq in 3 slices : the result is of type
seq (seq T) * (seq T) * (seq T)
Section Cut3.
Variable T : eqType.
Implicit Type (s : seq T) (ss : seq (seq T)).
Let match3 :=
fun ss => match ss return (seq T) * (seq T) * (seq T) with
| [:: a; b; c] => (a, b, c) | _ => ([::], [::], [::]) end.
Definition cut3 s : seq ((seq T) * (seq T) * (seq T)) :=
[seq match3 ss | ss <- cut_k 3 s].
Lemma cat3_equiv_cut3 s a b c : s == a ++ b ++ c <-> (a, b, c) \in cut3 s.
End Cut3.