Theory Zeckendorf

section ‹Zeckendorf's Theorem›

theory Zeckendorf

imports 
  Main
  "HOL-Number_Theory.Number_Theory"

begin

subsection ‹Definitions›
text ‹
  Formulate auxiliary definitions. An increasing sequence is a predicate of a function $f$
  together with a set $I$. $f$ is an increasing sequence on $I$, if $f(x)+1 < f(x+1)$ 
  for all $x \in I$. This definition is used to ensure that the Fibonacci numbers in the sum are
  non-consecutive.
›
definition is_fib :: "nat ⇒ bool" where
  "is_fib n = (∃ i. n = fib i)"

definition le_fib_idx_set :: "nat ⇒ nat set" where
  "le_fib_idx_set n = {i .fib i < n}"

definition inc_seq_on :: "(nat ⇒ nat) ⇒ nat set ⇒ bool" where
  "inc_seq_on f I = (∀ n ∈ I. f(Suc n) > Suc(f n))"

definition fib_idx_set :: "nat ⇒ nat set" where
  "fib_idx_set n = {i. fib i = n}"

subsection ‹Auxiliary Lemmas›

lemma fib_values[simp]:
  "fib 3 = 2"
  "fib 4 = 3"
  "fib 5 = 5"
  "fib 6 = 8"
  by(auto simp: numeral_Bit0 numeral_eq_Suc)

lemma fib_strict_mono: "i ≥ 2 ⟹ fib i < fib (Suc i)"
  using fib_mono by(induct i, simp, fastforce)

lemma smaller_index_implies_fib_le: "i < j ⟹ fib(Suc i) ≤ fib j"
  using fib_mono by (induct j, auto)

lemma fib_index_strict_mono : "i ≥ 2 ⟹ j > i ⟹ fib j > fib i"
  by(induct i, simp, metis Suc_leI fib_mono fib_strict_mono nle_le nless_le)

lemma fib_implies_is_fib: "fib i = n ⟹ is_fib n"
  using is_fib_def by auto

lemma zero_fib_unique_idx: "n = fib i ⟹ n = fib 0 ⟹ i = 0"
  using fib_neq_0_nat fib_idx_set_def by fastforce

lemma zero_fib_equiv: "fib i = 0 ⟷ i = 0"
  using zero_fib_unique_idx by auto

lemma one_fib_idxs: "fib i = Suc 0 ⟹ i = Suc 0 ∨ i = Suc(Suc 0)"
  using Fib.fib0 One_nat_def Suc_1 eq_imp_le fib_2 fib_index_strict_mono less_2_cases nat_neq_iff by metis

lemma ge_two_eq_fib_implies_eq_idx: "n ≥ 2 ⟹ n = fib i ⟹ n = fib j ⟹ i = j"
  using fib_index_strict_mono fib_mono Suc_1 fib_2 nle_le nless_le not_less_eq by metis

lemma ge_two_fib_unique_idx: "fib i ≥ 2 ⟹ fib i = fib j ⟹ i = j"
  using ge_two_eq_fib_implies_eq_idx by auto

lemma no_fib_lower_bound: "¬ is_fib n ⟹ n ≥ 4"
proof(rule ccontr)
  assume "¬ is_fib n" "¬ 4 ≤ n"
  hence "n ∈ {0,1,2,3}" by auto
  have "is_fib 0" "is_fib 1" "is_fib 2" "is_fib 3"
    using fib0 fib1 fib_values fib_implies_is_fib by blast+
  then show False
    using ‹¬ is_fib n› ‹n ∈ {0,1,2,3}› by blast
qed

lemma pos_fib_has_idx_ge_two: "n > 0 ⟹ is_fib n ⟹ (∃ i. i ≥ 2 ∧ fib i = n)"
  unfolding is_fib_def by (metis One_nat_def fib_2 fib_mono less_eq_Suc_le nle_le)

lemma finite_fib0_idx: "finite({i. fib i = 0})"
  using zero_fib_unique_idx finite_nat_set_iff_bounded by auto

lemma finite_fib1_idx: "finite({i. fib i = 1})"
  using one_fib_idxs finite_nat_set_iff_bounded by auto

lemma finite_fib_ge_two_idx: "n ≥ 2 ⟹ finite({i. fib i = n})"
  using ge_two_fib_unique_idx finite_nat_set_iff_bounded by auto

lemma finite_fib_index: "finite({i. fib i = n})"
  using finite_fib0_idx finite_fib1_idx finite_fib_ge_two_idx by(rule nat_induct2, auto)

lemma no_fib_implies_zero_in_le_idx_set: "¬ is_fib n ⟹ 0 ∈ {i. fib i < n}"
  using no_fib_lower_bound by fastforce

lemma no_fib_implies_le_fib_idx_set: "¬ is_fib n ⟹ {i. fib i < n} ≠ {}"
  using no_fib_implies_zero_in_le_idx_set by blast

lemma finite_smaller_fibs: "finite({i. fib i < n})"
proof(induct n)
  case (Suc n)
  moreover have "{i. fib i < Suc n} = {i. fib i < n} ∪ {i. fib i = n}" by auto
  moreover have "finite({i. fib i = n})" using finite_fib_index by auto
  ultimately show ?case  by auto
qed simp

lemma nat_ge_2_fib_idx_bound: "2 ≤ n ⟹ fib i ≤ n ⟹ n < fib (Suc i) ⟹ 2 ≤ i"
  by (metis One_nat_def fib_1 fib_2 le_Suc_eq less_2_cases linorder_not_le not_less_eq)

lemma inc_seq_on_aux: "inc_seq_on c {0..k - 1} ⟹ n - fib i < fib (i-1) ⟹ fib (c k) < fib i ⟹ 
                       (n - fib i) = (∑ i=0..k. fib (c i)) ⟹ Suc (c k) < i"
  by (metis fib_mono bot_nat_0.extremum diff_Suc_1 leD le_SucE linorder_le_less_linear not_add_less1 sum.last_plus)

lemma inc_seq_zero_at_start: "inc_seq_on c {0..k-1} ⟹ c k = 0 ⟹ k = 0"
  unfolding inc_seq_on_def
  by (metis One_nat_def Suc_pred atLeast0AtMost atMost_iff less_nat_zero_code not_gr_zero order.refl)

lemma fib_sum_zero_equiv: "(∑ i=n..m::nat . fib (c i)) = 0 ⟷ (∀ i∈{n..m}. c i = 0)"
  using finite_atLeastAtMost sum_eq_0_iff zero_fib_equiv by auto

lemma fib_idx_ge_two_fib_sum_not_zero: "n ≤ m ⟹ ∀i∈{n..m::nat}. c i ≥ 2 ⟹ ¬ (∑ i=n..m. fib (c i)) = 0"
  by (rule ccontr, simp add: fib_sum_zero_equiv)

lemma one_unique_fib_sum: "inc_seq_on c {0..k-1} ⟹ ∀i∈{0..k}. c i ≥ 2 ⟹ (∑ i=0..k. fib (c i)) = 1 ⟷ k = 0 ∧ c 0 = 2"
proof
  assume assms: "(∑i = 0..k. fib (c i)) = 1" "inc_seq_on c {0..k-1}" "∀i∈{0..k}. c i ≥ 2"
  hence "fib (c 0) + (∑i = 1..k. fib (c i)) = 1" by (simp add: sum.atLeast_Suc_atMost)
  moreover have "fib (c 0) ≥ 1" using assms fib_neq_0_nat[of "c 0"] by force
  ultimately show "k = 0 ∧ c 0 = 2"
    using fib_idx_ge_two_fib_sum_not_zero[of 1 k c] assms add_is_1 one_fib_idxs by(cases "k=0", fastforce, auto)
qed simp

lemma no_fib_betw_fibs: 
  assumes "¬ is_fib n"
  shows "∃ i. fib i < n ∧ n < fib (Suc i)"
proof - 
  have finite_le_fib: "finite {i. fib i < n}" using finite_smaller_fibs by auto
  obtain i where max_def: "i = Max {i. fib i < n}" by blast
  show "∃ i. fib i < n ∧ n < fib (Suc i)"
  proof(intro exI conjI)
    have "(Suc i) ∉ {i. fib i < n}" using max_def Max_ge Suc_n_not_le_n finite_le_fib by blast
    thus "fib (Suc i) > n" 
      using ‹¬ is_fib n› fib_implies_is_fib linorder_less_linear by blast
  qed(insert max_def Max_in ‹¬ is_fib n› finite_le_fib no_fib_implies_le_fib_idx_set, auto)
qed

lemma betw_fibs: 
  shows "∃ i. fib i ≤ n ∧ fib(Suc i) > n"   
proof(cases "is_fib n")
  case True
  then obtain i where a: "n = fib i" unfolding is_fib_def by auto
  then show ?thesis
    by (metis fib1 Suc_le_eq fib_2 fib_mono fib_strict_mono le0 le_eq_less_or_eq not_less_eq_eq)
qed(insert no_fib_betw_fibs, force)

text ‹
  Proof that the sum of non-consecutive Fibonacci numbers with largest member $F_i$ is strictly
  less then $F_{i+1}$. This lemma is used for the uniqueness proof.
›
lemma fib_sum_upper_bound:
  assumes "inc_seq_on c {0..k-1}" "∀i∈{0..k}. c i ≥ 2"
  shows "(∑ i=0..k. fib (c i)) < fib (Suc (c k))"
proof(insert assms, induct "c k" arbitrary: k rule: nat_less_induct)
  case 1
  then show ?case
  proof(cases "c k")
    case (Suc _)
    show ?thesis
    proof(cases k)
      case k_Suc: (Suc _)
      hence  ck_bounds: "c(k-1) + 1 < c k" "c(k-1) < c k"
        using 1(2) unfolding inc_seq_on_def by (force)+
      moreover have "(∑i = 0..k. fib (c i)) = fib(c k) + (∑i = 0..k-1. fib (c i))" 
        using k_Suc by simp
      moreover have "(∑i = 0..(k-1). fib (c i)) < fib (Suc (c (k-1)))" 
        using ck_bounds(2) 1 unfolding inc_seq_on_def by auto
      ultimately show ?thesis 
        using Suc smaller_index_implies_fib_le by fastforce
    qed(simp add: fib_index_strict_mono assms(2))
  qed(insert inc_seq_zero_at_start[OF 1(2)], auto)
qed

lemma last_fib_sum_index_constraint:
  assumes "n ≥ 2" "n = (∑ i=0..k. fib (c i))" "inc_seq_on c {0..k-1}" 
  assumes "∀i∈{0..k}. c i ≥ 2" "fib i ≤ n" "fib(Suc i) > n"
  shows "c k = i"
proof -
  have "2 ≤ i" using assms(1,5,6) nat_ge_2_fib_idx_bound by simp 
  have "c k > i ⟶ False"
    using smaller_index_implies_fib_le assms 
    by (metis bot_nat_0.extremum leD sum.last_plus trans_le_add1)
  moreover have "c k < i ⟶ False"
  proof 
    assume "c k < i"
    have seq: "inc_seq_on c {0..k - 1 - 1}" "∀i∈{0..k-1}. 2 ≤ c i"
      using assms unfolding inc_seq_on_def by simp+
    have "k > 0"
      by(rule ccontr, insert ‹c k < i› assms fib_index_strict_mono leD, auto)
    hence "c (k-1) + 1 < c k" "c (k-1) + 3 ≤ i"
      using ‹c k < i› assms unfolding inc_seq_on_def by force+
    have "(∑i = 0..k-1. fib (c i)) + fib (c k) = (∑i = 0..k. fib (c i))"
      using sum.atLeast0_atMost_Suc Suc_pred'[OF ‹k > 0›] by metis
    moreover have "fib (Suc (c (k-1))) ≤ fib (i-2)"
      using ‹c k < i› ‹c (k-1) + 1 < c k› by (simp add: fib_mono)
    moreover have "fib (c k) ≤ fib (i-1)"
      using ‹c k < i› fib_mono by fastforce
    ultimately have "(∑i = 0..k. fib (c i)) < fib (i-1) + fib (i-2)"
      using assms ‹c k < i› ‹k > 0› fib_sum_upper_bound[OF seq(1) seq(2)] by simp
    hence "(∑i = 0..k. fib (c i)) < fib i"
      using fib.simps(3)[of "i-2"] assms(4) ‹c k < i› 
      by (metis add_2_eq_Suc diff_Suc_1 ‹2 ≤ i› le_add_diff_inverse)
    then show False
      using assms by simp
    qed
    ultimately show ?thesis by simp
  qed

subsection ‹Theorem›
text ‹
  Now, both parts of Zeckendorf's Theorem can be proven. Firstly, the existence of an increasing 
  sequence for a positive integer $N$ such that the corresponding Fibonacci numbers sum up to $N$ 
  is proven. Then, the uniqueness of such an increasing sequence is proven.
›
lemma fib_implies_zeckendorf:
  assumes "is_fib n" "n > 0"
  shows "∃ c k. n = (∑ i=0..k. fib(c i)) ∧ inc_seq_on c {0..k-1} ∧ (∀ i∈{0..k}. c i ≥ 2)" 
proof - 
  from assms obtain i where i_def: "fib i = n" "i ≥ 2" using pos_fib_has_idx_ge_two by auto
  define c where c_def: "(c :: nat ⇒ nat) = (λ n::nat. if n = 0 then i else i + 3)"
  from i_def have "n = (∑i = 0..0. fib (c i))" by (simp add: c_def) 
  moreover have "inc_seq_on c {0..0}" by (simp add: c_def inc_seq_on_def)
  ultimately show "∃ c k. n = (∑ i=0..k. fib(c i)) ∧ inc_seq_on c {0..k-1} ∧ (∀ i∈{0..k}. c i ≥ 2)"
    using i_def c_def by fastforce
qed

theorem zeckendorf_existence:
  assumes "n > 0"
  shows "∃ c k. n = (∑ i=0..k. fib (c i)) ∧ inc_seq_on c {0..k-1} ∧ (∀i∈{0..k}. c i ≥ 2)" 
  using assms
proof(induct n rule: nat_less_induct)
  case (1 n)
  then show ?case
  proof(cases "is_fib n")
    case False
    obtain i where bounds: "fib i < n" "n < fib (Suc i)" "i > 0"
      using no_fib_betw_fibs 1(2) False by force
    then obtain c k where seq: "(n - fib i) = (∑ i=0..k. fib (c i))" "inc_seq_on c {0..k-1}" "∀ i∈{0..k}. c i ≥ 2"
      using 1 fib_neq_0_nat zero_less_diff diff_less by metis
    let ?c' = "(λ n. if n = k+1 then i else c n)"
    have diff_le_fib: "n - fib i < fib(i-1)"
      using bounds fib2 not0_implies_Suc[of i] by auto
    hence ck_lt_fib: "fib (c k) < fib i" 
      using fib_Suc_mono[of "i-1"] bounds by (simp add: sum.last_plus seq)
    have "inc_seq_on ?c' {0..k}"
      using inc_seq_on_aux[OF seq(2) diff_le_fib ck_lt_fib seq(1)] One_nat_def 
            inc_seq_on_def leI seq by force
    moreover have "n = (∑ i=0..k+1. fib (?c' i))" 
      using bounds seq by simp
    moreover have "∀ i ∈ {0..k+1}. ?c' i ≥ 2" 
      using seq bounds fib2 not0_implies_Suc[of i] atLeastAtMost_iff 
            diff_is_0_eq' less_nat_zero_code not_less_eq_eq by fastforce
    ultimately show ?thesis by fastforce
  qed(insert fib_implies_zeckendorf, auto)
qed

lemma fib_unique_fib_sum:
  fixes k :: nat
  assumes "n ≥ 2" "inc_seq_on c {0..k-1}" "∀i∈{0..k}. c i ≥ 2" 
  assumes "n = fib i"
  shows "n = (∑i=0..k. fib (c i)) ⟷ k = 0 ∧ c 0 = i"
proof
  assume ass: "n = (∑i = 0..k. fib (c i))"
  obtain j where bounds: "fib j ≤ n" "fib(Suc j) > n" "j ≥ 2" 
    using betw_fibs assms nat_ge_2_fib_idx_bound by blast
  have idx_eq: "c k = j"
    using last_fib_sum_index_constraint assms(1-3) ass bounds by simp
  have "i = j"
    using bounds ass assms 
    by (metis Suc_leI fib_mono ge_two_fib_unique_idx le_neq_implies_less linorder_not_le)
  have "k > 0 ⟶ fib i = fib i + (∑i = 0..k-1. fib (c i))"
    using ass assms by (metis idx_eq One_nat_def Suc_pred ‹i = j› add.commute sum.atLeast0_atMost_Suc)
  hence "k > 0 ⟶ False"
    using fib_idx_ge_two_fib_sum_not_zero[of 0 "k-1" c] assms by auto
  then show "k = 0 ∧ c 0 = i" using ‹i = j› idx_eq by simp
qed(auto simp: assms)

theorem zeckendorf_unique:
  assumes "n > 0"
  assumes "n = (∑ i=0..k. fib (c i))" "inc_seq_on c {0..k-1}" "∀i∈{0..k}. c i ≥ 2" 
  assumes "n = (∑ i=0..k'. fib (c' i))" "inc_seq_on c' {0..k'-1}" "∀i∈{0..k'}. c' i ≥ 2"
  shows "k = k' ∧ (∀ i ∈ {0..k}. c i = c' i)"
  using assms
proof(induct n arbitrary: k k' rule: nat_less_induct)
  case IH: (1 n)
  consider "n = 0" | "n = 1" | "n ≥ 2" by linarith
  then show ?case
  proof(cases)
    case 3
    obtain i where bounds: "fib i ≤ n" "fib(Suc i) > n" "2 ≤ i" 
      using betw_fibs nat_ge_2_fib_idx_bound 3 by blast
    have last_idx_eq: "c' k' = i" "c k = i" "c' k' = c k"
      using last_fib_sum_index_constraint[OF 3] IH(6-8) IH(3-5) bounds by blast+
    then show ?thesis
    proof(cases "is_fib n")
      case True
      hence "fib i = n" 
        unfolding is_fib_def using bounds IH(2-8) fib_mono leD nle_le not_less_eq_eq by metis
      hence "k = 0" "c 0 = i" "k' = 0" "c' 0 = i"
        using fib_unique_fib_sum 3 IH(3-8) by metis+
        then show ?thesis by simp
    next
      case False
      have "k > 0" 
        using IH(3) False unfolding is_fib_def by fastforce
      have "k' > 0"
        using IH(6) False  unfolding is_fib_def by fastforce
      have "0 < n - fib (c k)" using False bounds last_idx_eq(2) unfolding is_fib_def by fastforce
      moreover have "n - fib (c k) < n" 
        using bounds last_idx_eq by (simp add: dual_order.strict_trans1 fib_neq_0_nat)
      moreover have "n - fib (c k) = (∑i = 0..k-1. fib (c i))" 
        using sum.atLeast0_atMost_Suc[of "λ i. fib (c i)" "k-1"] Suc_diff_1 ‹k > 0› IH(3) by simp
      moreover have "n - fib (c' k' ) = (∑i = 0..k'-1. fib (c' i))" 
        using sum.atLeast0_atMost_Suc[of "λ i. fib (c' i)" "k'-1"] Suc_diff_1 ‹k' > 0› IH(6) by simp
      moreover have "inc_seq_on c {0..k-1 - 1}" "∀i∈{0..k-1}. 2 ≤ c i"
        using IH(4,5) unfolding inc_seq_on_def by auto
      moreover have "inc_seq_on c' {0..k'-1 - 1}" "∀i∈{0..k'-1}. 2 ≤ c' i"
        using IH(7,8) unfolding inc_seq_on_def by auto
      ultimately have "k-1 = k'-1 ∧ (∀i∈{0..k-1}. c i = c' i)"
        using IH(1) unfolding last_idx_eq by blast 
      then show ?thesis
        using IH(1) last_idx_eq by (metis One_nat_def Suc_pred ‹0 < k'› ‹0 < k› atLeastAtMost_iff le_Suc_eq)
    qed
  qed(insert IH one_unique_fib_sum, auto)
qed

end