# Theory Weak_Integer_Compositions

```section "Weak Integer Compositions"

theory Weak_Integer_Compositions
imports
"HOL-Combinatorics.Multiset_Permutations"
Common_Lemmas
begin

subsection"Definition"

definition weak_integer_compositions :: "nat ⇒ nat ⇒ nat list set" where
"weak_integer_compositions i l = {xs. length xs = l ∧ sum_list xs = i}"
text "Weak integer compositions are similar to integer compositions, with the trade-off that 0 is
allowed but the composition must have a fixed length."
text "Cardinality: ‹binomial (i + n - 1) i›"
text "Example: ‹weak_integer_compositions 2 2 = {[2,0], [1,1], [0,2]}›"

subsection"Algorithm"

fun weak_integer_composition_enum :: "nat ⇒ nat ⇒ nat list list" where
"weak_integer_composition_enum i 0 = (if i = 0 then [[]] else [])"
| "weak_integer_composition_enum i (Suc 0) = [[i]]"
| "weak_integer_composition_enum i l =
[h#r . h ← [0..< Suc i], r ← weak_integer_composition_enum (i-h) (l-1)]"

subsection"Verification"

subsubsection"Correctness"

lemma weak_integer_composition_enum_length:
"xs ∈ set (weak_integer_composition_enum i l) ⟹ length xs = l"
proof(induct l arbitrary: xs i)
case 0
then show ?case by simp
next
case (Suc l)
then show ?case by(cases l) auto
qed

lemma weak_integer_composition_enum_sum_list:
"xs ∈ set (weak_integer_composition_enum i l) ⟹ sum_list xs = i"
proof(induct l arbitrary: xs i)
case 0
then show ?case by simp
next
case (Suc l)
then show ?case by(cases l) auto
qed

assumes "xs ∈ set (weak_integer_composition_enum (sum_list xs) (length xs))"
shows "x # xs ∈ set (weak_integer_composition_enum (x + sum_list xs) (Suc (length xs)))"
proof(cases "length xs")
case 0
then show ?thesis by simp
next
case (Suc y)

(*maybe this should be proven elsewhere*)
have 1: "⟦n ∈ set xs; 0 < n⟧ ⟹ 0 < sum_list xs" for n
using sum_list_eq_0_iff by fast

have 2: "xs ∉ set (weak_integer_composition_enum 0 (Suc y)) ⟹ 0 < sum_list xs"
using Suc assms not_gr0 by fastforce

have "x # xs ∉ (#) (x + sum_list xs) ` set (weak_integer_composition_enum 0 (Suc y))
⟹ ∃xa∈{0..<x + sum_list xs}. x # xs ∈ (#) xa ` set (weak_integer_composition_enum (x + sum_list xs - xa) (Suc y))"
unfolding image_def using Suc assms 1 2 by auto

from Suc this show ?thesis
by auto
qed

lemma weak_integer_composition_enum_correct_aux:
"xs ∈ set (weak_integer_composition_enum (sum_list xs) (length xs))"
by (induct xs) (auto simp: weak_integer_composition_enum_head)

theorem weak_integer_composition_enum_correct:
"set (weak_integer_composition_enum i l) = weak_integer_compositions i l"
proof standard
show "set (weak_integer_composition_enum i l) ⊆ weak_integer_compositions i l"
unfolding weak_integer_compositions_def
using weak_integer_composition_enum_length weak_integer_composition_enum_sum_list
by auto
next
show "weak_integer_compositions i l ⊆ set (weak_integer_composition_enum i l)"
unfolding weak_integer_compositions_def
using weak_integer_composition_enum_correct_aux by auto
qed

subsubsection"Distinctness"

theorem weak_integer_composition_enum_distinct: "distinct (weak_integer_composition_enum i l)"
proof(induct rule: weak_integer_composition_enum.induct)
case (1 i)
then show ?case
by simp
next
case (2 i)
then show ?case
by simp
next
case (3 i l)
have "distinct [h#r . h ← [0..< Suc i], r ← weak_integer_composition_enum (i-h) (Suc l)]"
apply(subst Cons_distinct_concat_map_function)
using 3 by auto
then show ?case by simp
qed

subsubsection"Cardinality"

text ‹The following is a generalization of the binomial coefficient to multisets. Sometimes it
is called multiset coefficient. Here we call it "multichoose" \cite{stanleyenumerative}.›

definition multichoose:: "nat ⇒ nat ⇒ nat" (infixl "multichoose" 65) where
"n multichoose k = (n + k -1) choose k"

lemma weak_integer_composition_enum_zero: "length (weak_integer_composition_enum 0 (Suc n)) = 1"
by(induct n) auto

lemma a_choose_equivalence: "Suc (∑x←[0..<k]. n + (k - x) choose (k - x)) = Suc (n + k) choose k"
proof -
have "m ≥ k ⟹ (∑x←[0..< Suc k]. m - x choose (k - x)) = Suc m choose k" for m
using sum_choose_diagonal leq_sum_to_sum_list by metis
then have 1: "Suc (∑x←[0..<k]. (n + k) - x choose (k - x)) = Suc (n + k) choose k"
by simp

have "Suc (∑x←[0..<k]. (n + k) - x choose (k - x)) = Suc (∑x←[0..<k]. n + (k - x) choose (k - x))"

then show ?thesis using 1 by simp
qed

lemma composition_enum_length: "length (weak_integer_composition_enum i n) = n multichoose i"
unfolding multichoose_def
proof(induct i n rule: weak_integer_composition_enum.induct)
case (1 i)
then show ?case by simp
next
case (2 i)
then show ?case by simp
next
case (3 i n)

then have "x ∈ set [0..< i] ⟹
length (weak_integer_composition_enum (i - x) (Suc n)) = n + (i - x) choose (i - x)" for x
by simp

then have ev: "length [h#r . h ← [0..< i], r ← weak_integer_composition_enum (i-h) (Suc n)] =
(∑x←[0..< i]. n + (i - x) choose (i - x))"
using length_concat_map_function_sum_list [of
"[0..< i]"
"λx. (weak_integer_composition_enum (i-x) (Suc n))"
"λx. n + (i-x) choose (i-x)"
"λh r. h#r"
] by simp

have "Suc (∑x←[0..<i]. n + (i - x) choose (i - x)) = Suc (n + i) choose i"
using a_choose_equivalence by simp

then show ?case using weak_integer_composition_enum_zero ev by auto
qed

theorem weak_integer_compositions_cardinality: "card (weak_integer_compositions n k) = k multichoose n"
using weak_integer_composition_enum_correct weak_integer_composition_enum_distinct composition_enum_length
distinct_card by metis

end
```