Feedback for a proof of Cassini's identity

Stream: new members

[Olcay Oransoy]

Hello! I'm new to Lean and wrote a proof of Cassini's identity as an exercise. This is my first proof in Lean, so I thought getting some feedback would be a good idea. Here's my proof:

import Mathlib.Data.Nat.Fib.Basic

open Nat Int

theorem cassini_identity (n : ℕ) (n_pos : 0 < n) : fib (n + 1) * fib (n - 1) - fib n ^ 2 = (-1 : ℤ) ^ n := by
induction' n_pos with n n_pos IH
rfl
have h0 : fib (n - 1) + fib n = fib (n + 1) := by rw [fib_add_one]; rw [← zero_lt_iff]; exact n_pos
have h1 : fib (n + 1) * (fib (n - 1) + fib n) - fib n * (fib n + fib (n + 1)) = (-1 : ℤ) ^ n := by rw [mul_add, mul_add, sub_add_eq_sub_sub, add_sub_right_comm, add_sub_assoc]; nth_rewrite 4 [mul_comm]; simp; rw [← pow_two]; exact IH
rw [← ofNat_add, ← ofNat_add, ← fib_add_two, h0] at h1
rw [succ_eq_add_one, add_assoc, one_add_one_eq_two]
simp
rw [← neg_sub, pow_two]
nth_rewrite 2 [mul_comm]
rw [h1, neg_eq_neg_one_mul, pow_succ]

I'm especially unsure of my usage of rewrites - it seems kind of unreadable and clunky. Is there a way to do this more concisely? Any feedback would be appreciated. Thanks!

[Kevin Buzzard]

My first reaction: why fight with natural subtraction when you can just phrase the theorem like this:

theorem cassini_identity (m : ℕ) : fib (m + 2) * fib m - fib (m + 1) ^ 2 = (-1 : ℤ) ^ (m + 1) := by

[Kevin Buzzard]

theorem cassini_identity (m : ℕ) :
    fib (m + 2) * fib m - fib (m + 1) ^ 2 = (-1 : ℤ) ^ (m + 1) := by
  induction m with
  | zero => rfl
  | succ n ih =>
    rw [Nat.succ_eq_add_one, pow_add, pow_one]
    repeat rw [fib_add_two] at *
    push_cast at *
    polyrith

[Kevin Buzzard]

Mathematically, in the inductive step I'm saying that the hypothesis is $F_{m+2}F_m-F_{m+1}^2=\pm1$ and replacing $F_{m+2}$ with $F_{m+1}+F_m$ gives us $F_m^2+F_mF_{m+1}-F_{m+1}^2=\pm1$, a standard identity relating consecutive Fibonacci numbers. Our goal is some mess involving $F_{m+3}$ etc but if we just keep applying the formula for Fibonacci numbers it will necessarily reduce to a statement involving only $F_m$ and $F_{m+1}$ which must surely be the same statement (up to some constant at least). I then use Lean's Groebner basis tactic to check this, although I had to do some tinkering to make it work: the first line of the inductive step replaces n.succ with n + 1 everywhere, and also changes $(-1)^{n+1+1}$ to $(-1)\times(-1)^{n+1}$, and the third line is repeatedly applying results of the form "the natural map from naturals to integers commutes with multiplication / addition".

[Olcay Oransoy]

This is very nice; I will do some reading about push_cast and polyrith. Thanks!

I phrased the theorem with n > 0 because I was originally reading the source for Nat.Fib and found this:

theorem le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ fib n := by
  induction' five_le_n with n five_le_n IH
  ·-- 5 ≤ fib 5
    rfl
  · -- n + 1 ≤ fib (n + 1) for 5 ≤ n
    rw [succ_le_iff]
    calc
      n ≤ fib n := IH
      _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)

My first instinct was to do something similar to this proof, although I hadn't realized that natural subtraction would need some extra work.