Some theorems about Fibonacci numbers sums in Isabelle/HOL

Fibonacci_Sums.thy

theory Fibonacci_Sums
imports Main
begin

(* Isabelle/HOL/Isar *)

section \<open>Fibonacci numbers and their sums\<close>

fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0" |
"fib (Suc 0) = 1" |
"fib (Suc (Suc n)) = fib n + fib (n + 1)"

value "fib 7"
value "upt 0 10"
value "map fib (upt 1 10)"

definition fib_sum :: "nat \<Rightarrow> nat" where
"fib_sum n = (sum_list \<circ> map fib) (upt 0 n)"

value "fib_sum 3"
value "fib_sum 6"

definition fib_odd_sum :: "nat \<Rightarrow> nat" where
"fib_odd_sum n = (sum_list \<circ> map (\<lambda>m. fib (2*m + 1))) (upt 0 n)"

definition fib_even_sum :: "nat \<Rightarrow> nat" where
"fib_even_sum n = (sum_list \<circ> map (\<lambda>m. fib (2*m))) (upt 0 n)"


export_code fib_even_sum in Haskell


theorem fib_odd_sum_eq: "fib_odd_sum n = fib (2*n)"
  apply (induction n)
   apply (simp add: fib_odd_sum_def)
   apply (simp add: fib_odd_sum_def)
  done


lemma fib_sub_lemma[simp]: "n > 1 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
proof (cases n)
  case 0
  then show "n > 1 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)" by simp
next
  case (Suc nat)
  then show "n > 1 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
  proof (induction nat)
    case 0
    then show "n > 1 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)" using 0 by simp
  next
    case (Suc n1)
    then show ?thesis by simp
  qed
qed

theorem fib_even_sum_eq: "n > 0 \<Longrightarrow> fib_even_sum n + 1 = fib (2*n - 1)"
proof (induction n rule: fib.induct)
  case 1
  then show ?case by simp
next
  case 2
  then show ?case by (simp add: fib_even_sum_def)
next
  case (3 n)
  then show ?case by (simp add: fib_even_sum_def)
qed

(* proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc nat)
  then show ?case
  proof (cases nat)
    case 0
    then show ?thesis by (simp add: fib_even_sum_def)
  next
    case (Suc n1)
    then show ?thesis
    proof -
      have "fib_even_sum (n1 + 2) + 1 = Suc ((\<Sum>m\<leftarrow>[0..<(Suc n1)]. fib (2 * m)) + fib (2 * n1 + 2))" using Suc.prems by (simp add: fib_even_sum_def)
      also have "... = Suc ((\<Sum>m\<leftarrow>[0..<(Suc n1)]. fib (2 * m))) + fib (2 * n1 + 2)" by simp
      also have "... = Suc (fib_even_sum (Suc n1)) + fib (2 * n1 + 2)" by (simp add: fib_even_sum_def)
      also have "... = fib (2 * n1 + 1) + fib (2 * n1 + 2)" using Suc and Suc.IH by simp
      also have "... = fib (2 * n1 + 3)"  by simp
      finally show "fib_even_sum (Suc nat) + 1 = fib (2 * Suc nat - 1)" using Suc by simp
    qed
  qed
qed *)

theorem fib_sum_eq: "fib_sum n + 1 = fib (n + 1)"
  apply (induction n)
  apply (simp add: fib_sum_def)
  apply (simp add: fib_sum_def)
  done


section \<open>Car parking\<close>

datatype car = rabbit | cadillac

primrec car_size :: "car \<Rightarrow> nat" where
"car_size rabbit = 1" |
"car_size cadillac = 2"

definition sum_size :: "car list \<Rightarrow> nat" where
"sum_size \<equiv> sum_list \<circ> map car_size"

fun packings :: "nat \<Rightarrow> car list list" where
"packings 0 = [[]]" |
"packings (Suc 0) = [[rabbit]]" |
"packings (Suc (Suc n)) = append (map (Cons rabbit) (packings (Suc n))) (map (Cons cadillac) (packings n))"


theorem num_packings_eq_fib: "length (packings n) = fib (n+1)"
proof (induction n rule: packings.induct)
  case 1
  then show ?case by simp
next
  case 2
  then show ?case by simp
next
  case (3 n)
  then show ?case by simp
qed