More on Fibonacci numbers, with equational reasoning

20 Oct 2021

[ examples  Fibonacci  gcd  Isar  ]

The previous post introduced a definition of the Fibonacci function along with some simple proofs by induction. We continue our tour with examples of equational reasoning. Chains of equalities and inequalities are common in proofs and a proof assistant should allow them to be written.

Today our objective is a result involving greatest common divisors. The lemma below is proved by cases on whether the natural number m equals zero or not. The former case is trivial and in the latter case, m is written as Suc k:

lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
proof (cases m)
  case 0
  then show ?thesis by simp
next
  case (Suc k)
  then have "gcd (fib m) (fib (n + m))
           = gcd (fib k * fib n) (fib (Suc k))"
    by (metis add_Suc_right fib_add gcd.commute gcd_add_mult mult.commute)
  also have "… = gcd (fib n) (fib (Suc k))"
    using coprime_commute coprime_fib_Suc gcd_mult_left_left_cancel by blast
  also have "… = gcd (fib m) (fib n)"
    using Suc by (simp add: ac_simps)
  finally show ?thesis .
qed

Less usual but convenient is equational reasoning within another expression. In the little proof below, the left hand side of the desired identity is transformed using the addition law proved above. Then a subexpression of the result is simplified to n. Chaining the two steps (which is the purpose of finally) yield the desired result.

lemma gcd_fib_diff: "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" if "m ≤ n"
proof -
  have "gcd (fib m) (fib (n - m)) = gcd (fib m) (fib (n - m + m))"
    by (simp add: gcd_fib_add)
  also from ‹m ≤ n› have "n - m + m = n"
    by simp
  finally show ?thesis .
qed

Another example of chaining equalities involving subexpressions appears below. Operating on a subexpression eliminates the need to copy out the entire context. The ellipsis (…) refers to the previous right-hand side. It works and is clear but I confess this is not my style.

lemma gcd_fib_mod: "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" if "0 < m"
proof (induction n rule: less_induct)
  case (less n)
  show ?case
  proof -
    have "n mod m = (if n < m then n else (n - m) mod m)"
      by (rule mod_if)
    also have "gcd (fib m) (fib …) = gcd (fib m) (fib n)"
      using gcd_fib_diff less.IH that by fastforce
    finally show ?thesis .
  qed
qed

The work that we have done here and in the previous post finally takes us to our conclusion, an amusing theorem relating Fibonacci numbers and greatest common divisors. A clever step below is the use of gcd_nat_induct, which refers to an induction principle for the GCD function. In the induction step, in order to prove $P(m,n)$ for a given property $P$, we have the induction hypothesis $P(n, m \bmod n)$ for all $n>0$. Here it follows immediately with the help of the previous lemma and a fact from Isabelle’s built-in GCD library.

theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
proof (induction m n rule: gcd_nat_induct)
  case (step m n)
  then show ?case
    by (metis gcd.commute gcd_fib_mod gcd_red_nat)
qed auto

The proofs presented in this post are due to Gertrud Bauer. [Post corrected 2024-01-08 as suggested by suzuyu1729.]