More on Fibonacci numbers
authoreberlm <eberlm@in.tum.de>
Thu Oct 20 13:53:36 2016 +0200 (2016-10-20)
changeset 64317029e6247210e
parent 64316 96fef7745c68
child 64318 1e92b5c35615
child 64324 416f4d031afd
More on Fibonacci numbers
src/HOL/Archimedean_Field.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/document/root.tex
     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Oct 20 11:05:16 2016 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Thu Oct 20 13:53:36 2016 +0200
     1.3 @@ -736,6 +736,9 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 +lemma round_unique': "\<bar>x - of_int n\<bar> < 1/2 \<Longrightarrow> round x = n"
     1.8 +  by (subst (asm) abs_less_iff, rule round_unique) (simp_all add: field_simps)
     1.9 +
    1.10  lemma round_altdef: "round x = (if frac x \<ge> 1/2 then \<lceil>x\<rceil> else \<lfloor>x\<rfloor>)"
    1.11    by (cases "frac x \<ge> 1/2")
    1.12      (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef; linarith)+)[2])+
     2.1 --- a/src/HOL/Number_Theory/Fib.thy	Thu Oct 20 11:05:16 2016 +0200
     2.2 +++ b/src/HOL/Number_Theory/Fib.thy	Thu Oct 20 13:53:36 2016 +0200
     2.3 @@ -1,12 +1,13 @@
     2.4  (*  Title:      HOL/Number_Theory/Fib.thy
     2.5      Author:     Lawrence C. Paulson
     2.6      Author:     Jeremy Avigad
     2.7 +    Author:     Manuel Eberl
     2.8  *)
     2.9  
    2.10  section \<open>The fibonacci function\<close>
    2.11  
    2.12  theory Fib
    2.13 -imports Main GCD Binomial
    2.14 +  imports Complex_Main
    2.15  begin
    2.16  
    2.17  
    2.18 @@ -38,6 +39,34 @@
    2.19    by (induct n rule: fib.induct) (auto simp add: )
    2.20  
    2.21  
    2.22 +subsection \<open>More efficient code\<close>
    2.23 +
    2.24 +text \<open>
    2.25 +  The naive approach is very inefficient since the branching recursion leads to many
    2.26 +  values of @{term fib} being computed multiple times. We can avoid this by ``remembering''
    2.27 +  the last two values in the sequence, yielding a tail-recursive version.
    2.28 +  This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the 
    2.29 +  time required to multiply two $n$-bit integers), but much better than the naive version,
    2.30 +  which is exponential.
    2.31 +\<close>
    2.32 +
    2.33 +fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
    2.34 +  "gen_fib a b 0 = a"
    2.35 +| "gen_fib a b (Suc 0) = b"
    2.36 +| "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
    2.37 +
    2.38 +lemma gen_fib_recurrence: "gen_fib a b (Suc (Suc n)) = gen_fib a b n + gen_fib a b (Suc n)"
    2.39 +  by (induction a b n rule: gen_fib.induct) simp_all
    2.40 +  
    2.41 +lemma gen_fib_fib: "gen_fib (fib n) (fib (Suc n)) m = fib (n + m)"
    2.42 +  by (induction m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
    2.43 +
    2.44 +lemma fib_conv_gen_fib: "fib n = gen_fib 0 1 n"
    2.45 +  using gen_fib_fib[of 0 n] by simp
    2.46 +
    2.47 +declare fib_conv_gen_fib [code]
    2.48 +
    2.49 +
    2.50  subsection \<open>A Few Elementary Results\<close>
    2.51  
    2.52  text \<open>
    2.53 @@ -104,6 +133,114 @@
    2.54    by (induct n rule: nat.induct) (auto simp add:  field_simps)
    2.55  
    2.56  
    2.57 +subsection \<open>Closed form\<close>
    2.58 +
    2.59 +lemma fib_closed_form:
    2.60 +  defines "\<phi> \<equiv> (1 + sqrt 5) / (2::real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2::real)"
    2.61 +  shows   "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
    2.62 +proof (induction n rule: fib.induct)
    2.63 +  fix n :: nat
    2.64 +  assume IH1: "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
    2.65 +  assume IH2: "of_nat (fib (Suc n)) = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5"
    2.66 +  have "of_nat (fib (Suc (Suc n))) = of_nat (fib (Suc n)) + of_nat (fib n)" by simp
    2.67 +  also have "... = (\<phi>^n*(\<phi> + 1) - \<psi>^n*(\<psi> + 1)) / sqrt 5"
    2.68 +    by (simp add: IH1 IH2 field_simps)
    2.69 +  also have "\<phi> + 1 = \<phi>\<^sup>2" by (simp add: \<phi>_def field_simps power2_eq_square)
    2.70 +  also have "\<psi> + 1 = \<psi>\<^sup>2" by (simp add: \<psi>_def field_simps power2_eq_square)
    2.71 +  also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"  
    2.72 +    by (simp add: power2_eq_square)
    2.73 +  finally show "of_nat (fib (Suc (Suc n))) = (\<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)) / sqrt 5" .
    2.74 +qed (simp_all add: \<phi>_def \<psi>_def field_simps)
    2.75 +
    2.76 +lemma fib_closed_form':
    2.77 +  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
    2.78 +  assumes "n > 0"
    2.79 +  shows   "fib n = round (\<phi> ^ n / sqrt 5)"
    2.80 +proof (rule sym, rule round_unique')
    2.81 +  have "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> = \<bar>\<psi>\<bar> ^ n / sqrt 5"
    2.82 +    by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power_abs)
    2.83 +  also {
    2.84 +    from assms have "\<bar>\<psi>\<bar>^n \<le> \<bar>\<psi>\<bar>^1"
    2.85 +      by (intro power_decreasing) (simp_all add: algebra_simps real_le_lsqrt)
    2.86 +    also have "... < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
    2.87 +    finally have "\<bar>\<psi>\<bar>^n / sqrt 5 < 1/2" by (simp add: field_simps)
    2.88 +  }
    2.89 +  finally show "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> < 1/2" .
    2.90 +qed
    2.91 +
    2.92 +lemma fib_asymptotics:
    2.93 +  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)"
    2.94 +  shows   "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
    2.95 +proof -
    2.96 +  define \<psi> where "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
    2.97 +  have "\<phi> > 1" by (simp add: \<phi>_def)
    2.98 +  hence A: "\<phi> \<noteq> 0" by auto
    2.99 +  have "(\<lambda>n. (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 0"
   2.100 +    by (rule LIMSEQ_power_zero) (simp_all add: \<phi>_def \<psi>_def field_simps add_pos_pos)
   2.101 +  hence "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0" by (intro tendsto_diff tendsto_const)
   2.102 +  with A show ?thesis
   2.103 +    by (simp add: divide_simps fib_closed_form [folded \<phi>_def \<psi>_def])
   2.104 +qed
   2.105 +
   2.106 +
   2.107 +subsection \<open>Divide-and-Conquer recurrence\<close>
   2.108 +
   2.109 +text \<open>
   2.110 +  The following divide-and-conquer recurrence allows for a more efficient computation 
   2.111 +  of Fibonacci numbers; however, it requires memoisation of values to be reasonably 
   2.112 +  efficient, cutting the number of values to be computed to logarithmically many instead of
   2.113 +  linearly many. The vast majority of the computation time is then actually spent on the 
   2.114 +  multiplication, since the output number is exponential in the input number.
   2.115 +\<close>
   2.116 +
   2.117 +lemma fib_rec_odd:
   2.118 +  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
   2.119 +  shows   "fib (Suc (2*n)) = fib n^2 + fib (Suc n)^2"
   2.120 +proof -
   2.121 +  have "of_nat (fib n^2 + fib (Suc n)^2) = ((\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2)/5"
   2.122 +    by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power2_eq_square)
   2.123 +  also have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = 
   2.124 +    \<phi>^(2*n) + \<psi>^(2*n) - 2*(\<phi>*\<psi>)^n + \<phi>^(2*n+2) + \<psi>^(2*n+2) - 2*(\<phi>*\<psi>)^(n+1)" (is "_ = ?A")
   2.125 +      by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
   2.126 +  also have "\<phi> * \<psi> = -1" by (simp add: \<phi>_def \<psi>_def field_simps)
   2.127 +  hence "?A = \<phi>^(2*n+1) * (\<phi> + inverse \<phi>) + \<psi>^(2*n+1) * (\<psi> + inverse \<psi>)" 
   2.128 +    by (auto simp: field_simps power2_eq_square)
   2.129 +  also have "1 + sqrt 5 > 0" by (auto intro: add_pos_pos)
   2.130 +  hence "\<phi> + inverse \<phi> = sqrt 5" by (simp add: \<phi>_def field_simps)
   2.131 +  also have "\<psi> + inverse \<psi> = -sqrt 5" by (simp add: \<psi>_def field_simps)
   2.132 +  also have "(\<phi> ^ (2*n+1) * sqrt 5 + \<psi> ^ (2*n+1)* - sqrt 5) / 5 =
   2.133 +               (\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * (sqrt 5 / 5)" by (simp add: field_simps)
   2.134 +  also have "sqrt 5 / 5 = inverse (sqrt 5)" by (simp add: field_simps)
   2.135 +  also have "(\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * ... = of_nat (fib (Suc (2*n)))"
   2.136 +    by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] divide_inverse)
   2.137 +  finally show ?thesis by (simp only: of_nat_eq_iff)
   2.138 +qed
   2.139 +
   2.140 +lemma fib_rec_even: "fib (2*n) = (fib (n - 1) + fib (n + 1)) * fib n"
   2.141 +proof (induction n)
   2.142 +  case (Suc n)
   2.143 +  let ?rfib = "\<lambda>x. real (fib x)"
   2.144 +  have "2 * (Suc n) = Suc (Suc (2*n))" by simp
   2.145 +  also have "real (fib ...) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n" 
   2.146 +    by (simp add: fib_rec_odd Suc)
   2.147 +  also have "(?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n = (2 * ?rfib (n + 1) - ?rfib n) * ?rfib n"
   2.148 +    by (cases n) simp_all
   2.149 +  also have "?rfib n^2 + ?rfib (Suc n)^2 + ... = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
   2.150 +    by (simp add: algebra_simps power2_eq_square)
   2.151 +  also have "... = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
   2.152 +  finally show ?case by (simp only: of_nat_eq_iff)
   2.153 +qed simp
   2.154 +
   2.155 +lemma fib_rec_even': "fib (2*n) = (2*fib (n - 1) + fib n) * fib n"
   2.156 +  by (subst fib_rec_even, cases n) simp_all
   2.157 +
   2.158 +lemma fib_rec:
   2.159 +  "fib n = (if n = 0 then 0 else if n = 1 then 1 else
   2.160 +            if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
   2.161 +            else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
   2.162 +  by (auto elim: evenE oddE simp: fib_rec_odd fib_rec_even' Let_def)
   2.163 +
   2.164 +
   2.165  subsection \<open>Fibonacci and Binomial Coefficients\<close>
   2.166  
   2.167  lemma sum_drop_zero: "(\<Sum>k = 0..Suc n. if 0<k then (f (k - 1)) else 0) = (\<Sum>j = 0..n. f j)"
     3.1 --- a/src/HOL/Number_Theory/document/root.tex	Thu Oct 20 11:05:16 2016 +0200
     3.2 +++ b/src/HOL/Number_Theory/document/root.tex	Thu Oct 20 13:53:36 2016 +0200
     3.3 @@ -1,6 +1,8 @@
     3.4  \documentclass[11pt,a4paper]{article}
     3.5  \usepackage{graphicx}
     3.6  \usepackage{isabelle,isabellesym}
     3.7 +\usepackage{amssymb}
     3.8 +\usepackage{amsmath}
     3.9  \usepackage{pdfsetup}
    3.10  
    3.11  \urlstyle{rm}