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
  
lemma weak_integer_composition_enum_head:
  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))"
    by (metis (no_types, opaque_lifting) Nat.diff_add_assoc2 add.commute binomial_n_0 diff_is_0_eq' nle_le)
  
  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