Theory Falling_Factorial_Sum_Combinatorics

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Proving Falling Factorial of a Sum with Combinatorics›

theory Falling_Factorial_Sum_Combinatorics
imports
  Discrete_Summation.Factorials
  Card_Partitions.Injectivity_Solver
begin

subsection ‹Preliminaries›

subsubsection ‹Addition to Factorials Theory›

lemma card_lists_distinct_length_eq:
  assumes "finite A"
  shows "card {xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A} = ffact n (card A)"
proof cases
  assume "n ≤ card A"
  have "card {xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A} = ∏{card A - n + 1..card A}"
    using ‹finite A› ‹n ≤ card A› by (rule card_lists_distinct_length_eq)
  also have "… = ffact n (card A)"
    using ‹n ≤ card A› by (simp add: prod_rev_ffact_nat'[symmetric])
  finally show ?thesis .
next
  assume "¬ n ≤ card A"
  from this ‹finite A› have "∀xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A ⟶ False"
    by (metis card_mono distinct_card)
  from this have eq_empty: "{xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A} = {}"
    using ‹finite A› by auto
  from ‹¬ n ≤ card A› show ?thesis
    by (simp add: ffact_nat_triv eq_empty)
qed

subsection ‹Interleavings of Two Lists›

inductive interleavings :: "'a list ⇒ 'a list ⇒ 'a list ⇒ bool"
where
  "interleavings [] ys ys"
| "interleavings xs [] xs"
| "interleavings xs ys zs ⟹ interleavings (x#xs) ys (x#zs)"
| "interleavings xs ys zs ⟹ interleavings xs (y#ys) (y#zs)"

lemma interleaving_Nil_implies_eq1:
  assumes "interleavings xs ys zs"
  assumes "xs = []"
  shows "ys = zs"
using assms by (induct rule: interleavings.induct) auto

lemma interleaving_Nil_iff1:
  "interleavings [] ys zs ⟷ (ys = zs)"
using interleaving_Nil_implies_eq1
by (auto simp add: interleavings.intros(1))

lemma interleaving_Nil_implies_eq2:
  assumes "interleavings xs ys zs"
  assumes "ys = []"
  shows "xs = zs"
using assms by (induct rule: interleavings.induct) auto

lemma interleaving_Nil_iff2:
  "interleavings xs [] zs ⟷ (xs = zs)"
using interleaving_Nil_implies_eq2
by (auto simp add: interleavings.intros(2))

lemma interleavings_Cons:
  "{zs. interleavings (x#xs) (y#ys) zs} =
    {x#zs|zs. interleavings xs (y#ys) zs} ∪ {y#zs|zs. interleavings (x#xs) ys zs}"
  (is "?S = ?expr")
proof
  show "?S ⊆ ?expr"
    by (auto elim: interleavings.cases)
next
  show "?expr ⊆ ?S"
    by (auto intro: interleavings.intros)
qed

lemma interleavings_filter:
  assumes "X ∩ Y = {}" "set zs ⊆ X ∪ Y"
  shows "interleavings [z←zs . z ∈ X] [z←zs . z ∈ Y] zs"
using assms by (induct zs) (auto intro: interleavings.intros)

lemma interleavings_filter_eq1:
  assumes "interleavings xs ys zs"
  assumes "(∀x∈set xs. P x) ∧ (∀y∈set ys. ¬ P y)"
  shows "filter P zs = xs"
using assms by (induct rule: interleavings.induct) auto

lemma interleavings_filter_eq2:
  assumes "interleavings xs ys zs"
  assumes "(∀x∈set xs. ¬ P x) ∧ (∀y∈set ys. P y)"
  shows "filter P zs = ys"
using assms by (induct rule: interleavings.induct) auto

lemma interleavings_length:
  assumes "interleavings xs ys zs"
  shows "length xs + length ys = length zs"
using assms by (induct xs ys zs rule: interleavings.induct) auto

lemma interleavings_set:
  assumes "interleavings xs ys zs"
  shows "set xs ∪ set ys = set zs"
using assms by (induct xs ys zs rule: interleavings.induct) auto

lemma interleavings_distinct:
  assumes "interleavings xs ys zs"
  shows "distinct xs ∧ distinct ys ∧ set xs ∩ set ys = {} ⟷ distinct zs"
using assms interleavings_set by (induct xs ys zs rule: interleavings.induct) fastforce+

lemma two_mutual_lists_induction:
  assumes "⋀ys. P [] ys"
  assumes "⋀xs. P xs []"
  assumes "⋀x xs y ys. P xs (y#ys) ⟹ P (x#xs) ys ⟹ P (x#xs) (y#ys)"
  shows "P xs ys"
using assms by (induction_schema) (pat_completeness, lexicographic_order)

lemma finite_interleavings:
  "finite {zs. interleavings xs ys zs}"
proof (induct xs ys rule: two_mutual_lists_induction)
  case (1 ys)
  show ?case by (simp add: interleaving_Nil_iff1)
next
  case (2 xs)
  then show ?case by (simp add: interleaving_Nil_iff2)
next
  case (3 x xs y ys)
  then show ?case by (simp add: interleavings_Cons)
qed

lemma card_interleavings:
  assumes "set xs ∩ set ys = {}"
  shows "card {zs. interleavings xs ys zs} = (length xs + length ys choose (length xs))"
using assms
proof (induct xs ys rule: two_mutual_lists_induction)
  case (1 ys)
  have "card {zs. interleavings [] ys zs} = card {ys}"
    by (simp add: interleaving_Nil_iff1)
  also have "… = (length [] + length ys choose (length []))" by simp
  finally show ?case .
next
  case (2 xs)
  have "card {zs. interleavings xs [] zs} = card {xs}"
    by (simp add: interleaving_Nil_iff2)
  also have "… = (length xs + length [] choose (length xs))" by simp
  finally show ?case .
next
  case (3 x xs y ys)
  have "card {zs. interleavings (x # xs) (y # ys) zs} =
    card ({x#zs|zs. interleavings xs (y#ys) zs} ∪ {y#zs|zs. interleavings (x#xs) ys zs})"
    by (simp add: interleavings_Cons)
  also have "… = card {x#zs|zs. interleavings xs (y#ys) zs} + card {y#zs|zs. interleavings (x#xs) ys zs}"
  proof -
    have "finite {x # zs |zs. interleavings xs (y # ys) zs}"
      by (simp add: finite_interleavings)
    moreover have "finite {y # zs |zs. interleavings (x # xs) ys zs}"
      by (simp add: finite_interleavings)
    moreover have "{x # zs |zs. interleavings xs (y # ys) zs} ∩ {y # zs |zs. interleavings (x # xs) ys zs} = {}"
      using ‹set (x # xs) ∩ set (y # ys) = {}› by auto
    ultimately show ?thesis by (simp add: card_Un_disjoint)
  qed
  also have "… = card ((λzs. x # zs) ` {zs. interleavings xs (y # ys) zs}) +
    card ((λzs. y # zs) ` {zs. interleavings (x#xs) ys zs})"
    by (simp add: setcompr_eq_image)
  also have "… = card {zs. interleavings xs (y # ys) zs} + card {zs. interleavings (x#xs) ys zs}"
    by (simp add: card_image)
  also have "… = (length xs + length (y # ys) choose length xs) + (length (x # xs) + length ys choose length (x # xs))"
    using 3 by simp
  also have "… = length (x # xs) + length (y # ys) choose length (x # xs)" by simp
  finally show ?case .
qed

subsection ‹Cardinality of Distinct Fixed-Length Lists from a Union of Two Sets›

lemma lists_distinct_union_by_interleavings:
  assumes "X ∩ Y = {}"
  shows "{zs. length zs = n ∧ distinct zs ∧ set zs ⊆ X ∪ Y} = do {
    k ← {0..n};
    xs ← {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ X};
    ys ← {ys. length ys = n - k ∧ distinct ys ∧ set ys ⊆ Y};
    {zs. interleavings xs ys zs}
  }" (is "?S = ?expr")
proof
  show "?S ⊆ ?expr"
  proof
    fix zs
    assume "zs ∈ ?S"
    from this have "length zs = n" and "distinct zs" and "set zs ⊆ X ∪ Y" by auto
    define xs where "xs = filter (λz. z ∈ X) zs"
    define ys where "ys = filter (λz. z ∈ Y) zs"
    have eq: "[z←zs . z ∈ Y] = [z←zs . z ∉ X]"
      using ‹set zs ⊆ X ∪ Y› ‹X ∩ Y = {}›
      by (auto intro: filter_cong)
    have "length xs ≤ n ∧ distinct xs ∧ set xs ⊆ X"
      using ‹length zs = n› ‹distinct zs› unfolding xs_def by auto
    moreover have "length ys = n - length xs"
      using ‹set zs ⊆ X ∪ Y› ‹length zs = n›
      unfolding xs_def ys_def eq
      by (metis diff_add_inverse sum_length_filter_compl)
    moreover have "distinct ys ∧ set ys ⊆ Y"
      using ‹distinct zs› unfolding ys_def by auto
    moreover have "interleavings xs ys zs"
      using xs_def ys_def ‹X ∩ Y = {}› ‹set zs ⊆ X ∪ Y›
      by (simp add: interleavings_filter)
    ultimately show "zs ∈ ?expr" by force
  qed
next
  show "?expr ⊆ ?S"
  proof
    fix zs
    assume "zs ∈ ?expr"
    from this obtain xs ys where "length xs ≤ n" "distinct xs" "set xs ⊆ X"
      and "length ys = n - length xs" "distinct ys" "set ys ⊆ Y" "interleavings xs ys zs" by auto
    have "length zs = n"
      using ‹length xs ≤ n› ‹length ys = n - length xs› ‹interleavings xs ys zs›
      using interleavings_length by force
    moreover have "distinct zs"
      using ‹distinct xs› ‹distinct ys› ‹interleavings xs ys zs› ‹set xs ⊆ X› ‹set ys ⊆ Y›
      using ‹X ∩ Y = {}› interleavings_distinct by fastforce
    moreover have "set zs ⊆ X ∪ Y"
      using ‹interleavings xs ys zs› ‹set xs ⊆ X› ‹set ys ⊆ Y› interleavings_set by blast
    ultimately show "zs ∈ ?S" by blast
  qed
qed

lemma interleavings_inject:
  assumes "(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}"
  assumes "interleavings xs ys zs" "interleavings xs' ys' zs'"
  assumes "zs = zs'"
  shows "xs = xs'" and "ys = ys'"
proof -
  have "xs = filter (λz. z ∈ set xs ∪ set xs') zs"
    using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs ys zs›
    by (auto intro: interleavings_filter_eq1[symmetric])
  also have "… = filter (λz. z ∈ set xs ∪ set xs') zs'"
    using ‹zs = zs'› by simp
  also have "… = xs'"
    using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs' ys' zs'›
    by (auto intro: interleavings_filter_eq1)
  finally show "xs = xs'" by simp
  have "ys = filter (λz. z ∈ set ys ∪ set ys') zs"
    using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs ys zs›
    by (auto intro: interleavings_filter_eq2[symmetric])
  also have "… = filter (λz. z ∈ set ys ∪ set ys') zs'"
    using ‹zs = zs'› by simp
  also have "… = ys'"
    using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs' ys' zs'›
    by (auto intro: interleavings_filter_eq2)
  finally show "ys = ys'" .
qed

lemma injectivity:
  assumes "X ∩ Y = {}"
  assumes "k ∈ {0..n} ∧ k' ∈ {0..n}"
  assumes "(length xs = k ∧ distinct xs ∧ set xs ⊆ X) ∧ (length xs' = k' ∧ distinct xs' ∧ set xs' ⊆ X)"
  assumes "(length ys = n - k ∧ distinct ys ∧ set ys ⊆ Y) ∧ (length ys' = n - k' ∧ distinct ys' ∧ set ys' ⊆ Y)"
  assumes "interleavings xs ys zs ∧ interleavings xs' ys' zs'"
  assumes "zs = zs'"
  shows "k = k'" and "xs = xs'" and "ys = ys'"
proof -
  from assms(1,3,4) have "(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}" by blast
  from this assms(5) ‹zs = zs'› show "xs = xs'" and "ys = ys'"
    using interleavings_inject by fastforce+
  from this assms(3) show "k = k'" by auto
qed

lemma finite_length_distinct: "finite X ⟹  finite {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ X}"
by(fast elim: rev_finite_subset[OF finite_subset_distinct])

lemma card_lists_distinct_length_eq_union:
  assumes "finite X" "finite Y" "X ∩ Y = {}"
  shows "card {zs. length zs = n ∧ distinct zs ∧ set zs ⊆ X ∪ Y} =
    (∑k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
  (is "card ?S = _")
proof -
  let ?expr = "do {
    k ← {0..n};
    xs ← {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ X};
    ys ← {ys. length ys = n - k ∧ distinct ys ∧ set ys ⊆ Y};
    {zs. interleavings xs ys zs}
  }"
  from ‹X ∩ Y = {}› have "card ?S = card ?expr"
    by (simp add: lists_distinct_union_by_interleavings)
  let "?S ⤜ ?comp" = "?expr"
  {
    fix k
    assume "k ∈ ?S"
    let "?expr" = "?comp k"
    let "?S ⤜ ?comp" = "?expr"
    from ‹finite X› have "finite ?S" by(rule finite_length_distinct)
    moreover {
      fix xs
      assume xs: "xs ∈ ?S"
      let ?expr = "?comp xs"
      let "?S ⤜ ?comp" = ?expr
      from ‹finite Y› have "finite ?S" by(rule finite_length_distinct)
      moreover {
        fix ys
        assume ys: "ys ∈ ?S"
        let ?expr = "?comp ys"
        have "finite ?expr"
          by (simp add: finite_interleavings)
        moreover have "card ?expr = (n choose k)"
          using xs ys ‹X ∩ Y = {}› ‹k ∈ _›
          by (subst card_interleavings) auto
        ultimately have "finite ?expr ∧ card ?expr = (n choose k)" ..
      }
      moreover have "disjoint_family_on ?comp ?S"
        using ‹k ∈ {0..n}› ‹xs ∈ {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ X}›
        by (injectivity_solver rule: injectivity(3)[OF ‹X ∩ Y = {}›])
      moreover have "card ?S = ffact (n - k) (card Y)"
        using ‹finite Y› by (simp add: card_lists_distinct_length_eq)
      ultimately have "card ?expr = (n choose k) * ffact (n - k) (card Y)"
        by (subst card_bind_constant) auto
      moreover have "finite ?expr"
        using ‹finite ?S› by (auto intro!: finite_bind finite_interleavings)
      ultimately have "finite ?expr ∧ card ?expr = (n choose k) * ffact (n - k) (card Y)"
        by blast
    }
    moreover have "disjoint_family_on ?comp ?S"
      using ‹k ∈ {0..n}›
      by (injectivity_solver rule: injectivity(2)[OF ‹X ∩ Y = {}›])
    moreover have "card ?S = ffact k (card X)"
      using ‹finite X› by (simp add: card_lists_distinct_length_eq)
    ultimately have "card ?expr = (n choose k) * ffact k (card X) * ffact (n - k) (card Y)"
      by (subst card_bind_constant) auto
    moreover have "finite ?expr"
      using ‹finite ?S› ‹finite Y› by (auto intro!: finite_bind finite_interleavings finite_length_distinct)
    ultimately have "finite ?expr ∧ card ?expr = (n choose k) * ffact k (card X) * ffact (n - k) (card Y)"
      by blast
  }
  moreover have "disjoint_family_on ?comp ?S"
    by (injectivity_solver rule: injectivity(1)[OF ‹X ∩ Y = {}›])
  ultimately have "card ?expr = (∑k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
    by (auto simp add: card_bind)
  from ‹card _ = card ?expr› this show ?thesis by simp
qed

lemma
  "ffact n (x + y) = (∑k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
proof -
  define X where "X = {..<x}"
  define Y where "Y = {x..<x+y}"
  have "finite X" and "card X = x" unfolding X_def by auto
  have "finite Y" and "card Y = y" unfolding Y_def by auto
  have "X ∩ Y = {}" unfolding X_def Y_def by auto
  have "ffact n (x + y) = ffact n (card X + card Y)"
    using ‹card X = x› ‹card Y = y› by simp
  also have "… = ffact n (card (X ∪ Y))"
    using ‹X ∩ Y = {}› ‹finite X› ‹finite Y› by (simp add: card_Un_disjoint)
  also have "… = card {xs. length xs = n ∧ distinct xs ∧ set xs ⊆ X ∪ Y}"
   using ‹finite X› ‹finite Y› by (simp add: card_lists_distinct_length_eq)
  also have "… = (∑k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
    using ‹X ∩ Y = {}› ‹finite X› ‹finite Y› by (simp add: card_lists_distinct_length_eq_union)
  also have "… = (∑k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
    using ‹card X = x› ‹card Y = y› by simp
  finally show ?thesis .
qed

end