simplifying equation

Stream: new members

[Lawrence Lin]

hey, all! here's a mwe of my current code:

def fib : ℕ -> ℤ
| 0 := 0
| 1 := 1
| (x+2) := fib (x) + fib (x+1)

lemma binet_lemma (x : ℝ) (hx : x^2 = x + 1) (n : ℕ) (hn : n > 0) : x^n = x*(fib n) + fib (n-1)

theorem binet_formula (n : ℕ) : (fib(n) : ℝ) = (1 / real.sqrt(5)) * (((1 + real.sqrt(5)) / 2)^n - ((1 - real.sqrt(5)) / 2)^n) :=
begin
  set φ := (1 + real.sqrt(5)) / 2,
  set τ := (1 - real.sqrt(5)) / 2,

  rw [binet_lemma, binet_lemma],
  simp[φ, τ],
  field_simp,
  norm_num,
  rw [mul_comm],

  {sorry}, {sorry}, {sorry}, {sorry},
end

basically, what I want to do right now is to simplify this giant expression

↑(fib n) = ((1 + real.sqrt 5) * ↑(fib n) * 2 - 2 * ((1 - real.sqrt 5) * ↑(fib n))) / (real.sqrt 5 * 4)

But i'm unsure about how to tell lean to do this. can someone help me on this?

[Lawrence Lin]

what i want to do right now is to show that the elements on the right side essentially cancel out...

[Martin Dvořák]

MWE:

[Martin Dvořák]

import data.real.sqrt
import tactic

def fib : ℕ -> ℤ
| 0     := 0
| 1     := 1
| (x+2) := fib x + fib (x+1)

lemma binet_lemma (x : ℝ) (hx : x^2 = x + 1) (n : ℕ) (hn : n > 0) :
  x^n = x * (fib n) + fib (n-1) := sorry

theorem binet_formula (n : ℕ) :
  (fib n : ℝ) = (1 / real.sqrt 5) * (((1 + real.sqrt 5) / 2) ^ n - ((1 - real.sqrt 5) / 2) ^ n) :=
begin
  set φ := (1 + real.sqrt(5)) / 2,
  set τ := (1 - real.sqrt(5)) / 2,

  rw [binet_lemma, binet_lemma],
  simp[φ, τ],
  field_simp,
  norm_num,
  rw [mul_comm],

  repeat {sorry},
end

[Martin Dvořák]

This will get you to a simpler expression:

import data.real.sqrt
import tactic

def fib : ℕ -> ℕ
| 0     := 0
| 1     := 1
| (x+2) := fib x + fib (x+1)

lemma binet_lemma (x : ℝ) (hx : x^2 = x + 1) (n : ℕ) (hn : n > 0) :
  x^n = x * (fib n) + fib (n-1) := sorry

theorem binet_formula (n : ℕ) :
  (fib n : ℝ) = (1 / real.sqrt 5) * (((1 + real.sqrt 5) / 2) ^ n - ((1 - real.sqrt 5) / 2) ^ n) :=
begin
  --set φ := (1 + real.sqrt(5)) / 2,
  --set τ := (1 - real.sqrt(5)) / 2,

  rw [binet_lemma, binet_lemma],
  --simp[φ, τ],
  field_simp,
  norm_num,
  --rw [mul_comm],
  ring,

  repeat {sorry},
end

[Martin Dvořák]

I really like the problem you are working on! Here is some progress. Only easy goals should be remaining:

import data.real.sqrt
import tactic

def fib : ℕ -> ℕ
| 0     := 0
| 1     := 1
| (x+2) := fib x + fib (x+1)

lemma binet_lemma (x : ℝ) (hx : x^2 = x + 1) (n : ℕ) (hn : n > 0) :
  x^n = x * (fib n) + fib (n-1) := sorry

theorem binet_formula (n : ℕ) :
  (fib n : ℝ) = (1 / real.sqrt 5) * (((1 + real.sqrt 5) / 2) ^ n - ((1 - real.sqrt 5) / 2) ^ n) :=
begin
  by_cases is_n_zero : n = 0,
  {
    rw is_n_zero,
    unfold fib,
    norm_num,
  },
  rw [binet_lemma, binet_lemma],
  field_simp,
  norm_num,
  ring_nf,
  convert_to ↑(fib n) = 4 * real.sqrt 5 * (4 * real.sqrt 5)⁻¹ * ↑(fib n),
  { ring },
  convert_to ↑(fib n) = (1 : ℝ) * ↑(fib n),
  congr,
  have four_sqrt_five_not_zero : 4 * real.sqrt 5 ≠ 0, sorry,
  exact mul_inv_cancel four_sqrt_five_not_zero,
  ring,

  repeat {sorry},
end

[Martin Dvořák]

I few calls to library_search and the proof is almost done:

import data.real.sqrt
import tactic

def fib : ℕ -> ℕ
| 0     := 0
| 1     := 1
| (x+2) := fib x + fib (x+1)

lemma binet_lemma (x : ℝ) (hx : x^2 = x + 1) (n : ℕ) (hn : n > 0) :
  x^n = x * (fib n) + fib (n-1) := sorry

theorem binet_formula (n : ℕ) :
  (fib n : ℝ) = (1 / real.sqrt 5) * (((1 + real.sqrt 5) / 2) ^ n - ((1 - real.sqrt 5) / 2) ^ n) :=
begin
  by_cases is_n_zero : n = 0,
  {
    rw is_n_zero,
    unfold fib,
    norm_num,
  },
  have sqrt5_not_zero : real.sqrt 5 ≠ 0,
  {
    norm_num,
  },
  rw [binet_lemma, binet_lemma],
  {
    ring_nf,  -- note how much the expression got simplified on this line
    finish,
  },
  {
    sorry,
  },
  {
    exact zero_lt_iff.mpr is_n_zero,
  },
  {
    sorry,
  },
  {
    exact zero_lt_iff.mpr is_n_zero,
  },
end

[Martin Dvořák]

Main theorem proved:

import data.real.sqrt
import tactic

def fib : ℕ -> ℕ
| 0     := 0
| 1     := 1
| (x+2) := fib x + fib (x+1)

lemma binet_lemma (x : ℝ) (hx : x^2 = x + 1) (n : ℕ) (hn : 0 < n) :
  x^n = x * (fib n) + fib (n-1) := sorry

theorem binet_formula (n : ℕ) :
  (fib n : ℝ) = (1 / real.sqrt 5) * (((1 + real.sqrt 5) / 2) ^ n - ((1 - real.sqrt 5) / 2) ^ n) :=
begin
  by_cases is_n_zero : n = 0,
  {
    rw is_n_zero,
    unfold fib,
    norm_num,
  },
  have sqrt5_not_zero : real.sqrt 5 ≠ 0,
  {
    norm_num,
  },
  have sqrt5_mul_sqrt5 : real.sqrt 5 * real.sqrt 5 = 5,
  {
    norm_num,
  },
  rw [binet_lemma, binet_lemma],
  {
    ring_nf,  -- Note how much the expression got simplified on this line!
    finish,
  },
  {
    ring_nf,
    rw [sub_mul, mul_assoc, sqrt5_mul_sqrt5],
    ring,
  },
  {
    rwa zero_lt_iff,
  },
  {
    ring_nf,
    rw [add_mul, mul_assoc, sqrt5_mul_sqrt5],
    ring,
  },
  {
    rwa zero_lt_iff,
  },
end

[Martin Dvořák]

It was fun! Let us know whether you managed to prove binet_lemma on your own.

[Kevin Buzzard]

Re binet_lemma : a random hypothesis that 0 < n and a random natural subtraction n - 1 are kind of screaming at you, saying "don't use n, use m := n - 1 and instead just claim that for all naturals m we have x^{m+1}=x*fib(m+1)+fib(m)". It will be easier to work with!

[Kevin Buzzard]

lemma binet_lemma {R : Type*} [comm_ring R] (x : R) (hx : x*x = x + 1) (m : ℕ) :
  x^(m+1) = x * (fib (m+1)) + fib m :=
begin
  induction m with d hd,
  { simp [fib], },
  { rw [pow_succ, hd],
    simp [fib, nat.succ_eq_add_one, mul_add, ← mul_assoc, hx],
    ring, }
end

[Kevin Buzzard]

theorem binet_formula (n : ℕ) :
  (fib n : ℝ) = (1 / real.sqrt 5) * (((1 + real.sqrt 5) / 2) ^ n - ((1 - real.sqrt 5) / 2) ^ n) :=
begin
  have sqrt5_not_zero : real.sqrt 5 ≠ 0 := by norm_num,
  induction n with d hd,
  { simp [fib], },
  { rw [nat.succ_eq_add_one, binet_lemma, binet_lemma],
    { field_simp, norm_num, ring, },
    { field_simp [mul_sub, sub_mul], norm_num, ring, },
    { field_simp [mul_add, add_mul], norm_num, ring, },
  },
end

[Kevin Buzzard]

It's the same proof, it's just a bit less clunky without the n!=0 thing.

[Lawrence Lin]

woah o__o u guys are good...
thanks for the help! i have a lot to learn :)

[Jake Levinson]

Kevin's advice applies somewhat more broadly, for instance it may be more convenient in Lean to prove statements like a = b * c rather than a/c = b with hypothesis c ≠ 0. There are similar patterns elsewhere in mathlib too, for example the statement that "deleting an element from a finset s reduces its cardinality by one" is phrased as a ∈ s → (s.erase a).card + 1 = s.card, rather than, say, a ∈ s → (s.erase a).card = s.card - 1. (See https://leanprover-community.github.io/mathlib_docs/data/finset/card.html#finset.card_erase_add_one)

edit: Oops, now that I've written this, I see that in fact both statements about deleting an element are in mathlib (https://leanprover-community.github.io/mathlib_docs/data/finset/card.html#finset.card_erase_of_mem). Still, for some purposes the subtraction-free one may be preferable.

Tactics like ring and linarith are intended to save us from having to do unnecessary algebra simplification, but they aren't able to do things that require extra hypotheses to be applied.

[Jeremy Tan]

Kevin Buzzard said:

lemma binet_lemma {R : Type*} [comm_ring R] (x : R) (hx : x*x = x + 1) (m : ℕ) :
  x^(m+1) = x * (fib (m+1)) + fib m :=
begin
  induction m with d hd,
  { simp [fib], },
  { rw [pow_succ, hd],
    simp [fib, nat.succ_eq_add_one, mul_add, ← mul_assoc, hx],
    ring, }
end

[Jeremy Tan]

this code doesn't work in Lean 4, what must I change in order for it to work?

[Jeremy Tan]

I understand it has to start with, in L4,

lemma binet_lemma {R} [CommRing R] (x : R) (hx : x*x = x + 1) (m : ℕ) :
  x^(m+1) = x * (fib (m+1)) + fib m :=

but then how does the induction get expressed?

[Jeremy Tan]

There appear to be zero instances of induction like this in mathlib4

[Jeremy Tan]

making some progress

lemma binet_lemma {R} [CommRing R] (x : R) (phi : x*x = x + 1) (m : ℕ) :
  x^(m+1) = x * (fib (m+1)) + fib m := by
  induction m with
    | zero => simp [fib]
    | succ n ih => rw [pow_succ]

[Jeremy Tan]

OK I did it:

lemma binet_lemma {R} [CommRing R] (x : R) (phi : x*x = x+1) (m : ℕ) :
  x^(m+1) = x * (fib (m+1)) + fib m := by
  induction m with
  | zero => simp [fib]
  | succ _ ih => {rw [pow_succ, ih, fib]; simp [mul_add, ←mul_assoc, phi]; ring}

but how can I put the rw, simp and ring of the succ proof on different lines? And does this conform to mathlib4 style?

[Jeremy Tan]

now how do I write the actual formula proof in Lean 4?

theorem binet_formula (n : ℕ) : (fib n : ℝ) = (1 / Real.sqrt 5) *
  (((1 + Real.sqrt 5) / 2) ^ n - ((1 - Real.sqrt 5) / 2) ^ n) :=
  have sqrt5_not_zero : Real.sqrt 5 ≠ 0 := by norm_num
  by induction n with
  | zero => simp [fib]
  | succ _ ih => {simp [fib]; rw [Nat.succ_eq_add_one, binet_lemma, binet_lemma]; field_simp} -- ???

[Mario Carneiro]

Parcly Taxel said:

OK I did it:

lemma binet_lemma {R} [CommRing R] (x : R) (phi : x*x = x+1) (m : ℕ) :
  x^(m+1) = x * (fib (m+1)) + fib m := by
  induction m with
  | zero => simp [fib]
  | succ _ ih => {rw [pow_succ, ih, fib]; simp [mul_add, ←mul_assoc, phi]; ring}

but how can I put the rw, simp and ring of the succ proof on different lines? And does this conform to mathlib4 style?

mathlib style:

lemma binet_lemma {R} [CommRing R] (x : R) (phi : x * x = x + 1) (m : ℕ) :
    x ^ (m + 1) = x * fib (m + 1) + fib m := by
  induction m with
  | zero => simp [fib]
  | succ _ ih =>
    rw [pow_succ, ih, fib]
    simp [mul_add, ← mul_assoc, phi]
    ring

[Jeremy Tan]

Kevin Buzzard said:

theorem binet_formula (n : ℕ) :
  (fib n : ℝ) = (1 / real.sqrt 5) * (((1 + real.sqrt 5) / 2) ^ n - ((1 - real.sqrt 5) / 2) ^ n) :=
begin
  have sqrt5_not_zero : real.sqrt 5 ≠ 0 := by norm_num,
  induction n with d hd,
  { simp [fib], },
  { rw [nat.succ_eq_add_one, binet_lemma, binet_lemma],
    { field_simp, norm_num, ring, },
    { field_simp [mul_sub, sub_mul], norm_num, ring, },
    { field_simp [mul_add, add_mul], norm_num, ring, },
  },
end

trying to port this to Lean 4…

[Jeremy Tan]

whee I did the main formula

theorem binet_formula (n : ℕ) : (fib n : ℝ) = (1 / Real.sqrt 5) *
    (((1 + Real.sqrt 5) / 2) ^ n - ((1 - Real.sqrt 5) / 2) ^ n) :=
  have sqrt5_not_zero : Real.sqrt 5 ≠ 0 := by norm_num;
  by induction n with
  | zero => simp [fib]
  | succ =>
    rw [Nat.succ_eq_add_one, binet_lemma, binet_lemma]
    field_simp; norm_num; ring
    field_simp [mul_sub, sub_mul]; norm_num; ring
    field_simp [mul_add, add_mul]; norm_num; ring

the braces in { field_simp, norm_num, ring, } and elsewhere are just grouping in Lean 3, right?

[Alex J. Best]

the braces are used to focus a subgoal, in Lean 4 the language is whitespace sensitive and we use

some_tactic_that_leaves_several_goals
. proof of goal 1
  more of this proof
. proof of goal 2

for this

[Jeremy Tan]

norm_num is not needed for the first subproof:

theorem binet_formula (n : ℕ) : (fib n : ℝ) = (1 / Real.sqrt 5) *
    (((1 + Real.sqrt 5) / 2) ^ n - ((1 - Real.sqrt 5) / 2) ^ n) :=
  have sqrt5_not_zero : Real.sqrt 5 ≠ 0 := by norm_num;
  by induction n with
  | zero => simp [fib]
  | succ =>
    rw [Nat.succ_eq_add_one, binet_lemma, binet_lemma]
    field_simp; ring
    field_simp [mul_sub, sub_mul]; norm_num; ring
    field_simp [mul_add, add_mul]; norm_num; ring

[Jeremy Tan]

is putting several short tactics on one line with ; correct mathlib4 style?

[Mario Carneiro]

yes, it's fine

[Mario Carneiro]

you can use it to group lemmas

[Mario Carneiro]

you should not use it for goal management though, you should always use \. after a tactic which produces multiple goals

[Mario Carneiro]

since ring is a closing tactic, I think you are probably dealing with multiple subgoals after the rw, in which case it should be written

theorem binet_formula (n : ℕ) : (fib n : ℝ) = (1 / Real.sqrt 5) *
    (((1 + Real.sqrt 5) / 2) ^ n - ((1 - Real.sqrt 5) / 2) ^ n) :=
  have sqrt5_not_zero : Real.sqrt 5 ≠ 0 := by norm_num;
  by induction n with
  | zero => simp [fib]
  | succ =>
    rw [Nat.succ_eq_add_one, binet_lemma, binet_lemma]
    · field_simp; ring
    · field_simp [mul_sub, sub_mul]; norm_num; ring
    · field_simp [mul_add, add_mul]; norm_num; ring

[Jeremy Tan]

Mario Carneiro said:

since ring is a closing tactic, I think you are probably dealing with multiple subgoals after the rw

of course I was dealing with multiple subgoals

[Jeremy Tan]

after the rw there is the first subgoal that is just algebraic simplification of the inductive step,
and then two other subgoals succ.phi for which I must prove that the two constants satisfy the phi relation

[Jeremy Tan]

⊢ (1 - Real.sqrt 5) / 2 * ((1 - Real.sqrt 5) / 2) = (1 - Real.sqrt 5) / 2 + 1 and the one where - is replaced with +

[Jeremy Tan]

oh, and even Nat.succ_eq_add_one in the rw isn't needed!

[Mario Carneiro]

Parcly Taxel said:

Mario Carneiro said:

since ring is a closing tactic, I think you are probably dealing with multiple subgoals after the rw

of course I was dealing with multiple subgoals

the purpose of the \. is to make it clear to readers that don't have lean in front of them (like me, looking at zulip) what the structure of the proof is. rw can spit out multiple goals, it is not syntactically obvious how many your proof produces

[Jeremy Tan]

why doesn't this work?

theorem cassini_identity (n : ℕ) : fib n * fib (n + 2) + (-1) ^ n = (fib (n + 1) : ℤ) ^ 2 := by
  induction n with
  | zero => simp [fib]
  | succ _ ih =>
    rw [fib, fib, add_pow_two]

[Jeremy Tan]

After the first two fib rewrites I have on the RHS ↑(fib n✝ + fib (n✝ + 1)) ^ 2

[Jeremy Tan]

so I suppose I can expand this, but I can't

[Jeremy Tan]

I realise I need to coerce the inner fibs to integers somehow since add_pow_two only works on semirings – or should I?

[Martin Dvořák]

You want to match Int.ofNat (fib n✝ + fib (n✝ + 1)) ^ 2 right?

[Jeremy Tan]

yeah, so I can then apply the IH

[Martin Dvořák]

It actually is (Int.ofNat (fib n✝ + fib (n✝ + 1))) ^ 2 unfortunately.

[Jeremy Tan]

now what? \N is a semiring

[Martin Dvořák]

I suggest we change the place where we go from ℕ to ℤ.

[Jeremy Tan]

but putting (fib (n + 1) ^ 2 : ℤ) at the proof start doesn't work

[Jeremy Tan]

I get a "failed to synthesize instance" error

[Martin Dvořák]

I assume you are working with the following definition of Fibonacci numbers:

def fib : Nat → Nat
| 0   => 0
| 1   => 1
| n+2 => fib n + fib (n+1)

[Martin Dvořák]

I think we can express your theorem in terms of ℕ only.

[Jeremy Tan]

so I would have two theorems like this:

theorem cassini_identity_even (k : ℕ) : fib (2 * k) * fib (2 * k + 2) + 1 = fib (2 * k + 1) ^ 2 :=
  _

theorem cassini_identity_odd (k : ℕ) : fib (2 * k + 1) * fib (2 * k + 3) = fib (2 * k + 2) ^ 2 + 1:=
  _

how do I do mutual induction now?

[Martin Dvořák]

Lemme try it without mutual induction.

[Martin Dvořák]

Something like:

theorem cassini_identity (n : Nat) : fib n * fib (n + 2) + ((n+1) % 2) * 2 - 1 = (fib (n + 1)) ^ 2 := by
  induction n with
  | zero => rfl
  | succ _ ih =>
    sorry

[Jeremy Tan]

now rw [...\l ih] works, but how do I handle the modulo? I suspect I would have to use cases for this, but what is the syntax?

[Martin Dvořák]

Wip:

theorem cassini_identity (n : ℕ) : fib n * fib (n + 2) + ((n+1)%2) * 2 - 1 = (fib (n + 1)) ^ 2 := by
  induction n with
  | zero => rfl
  | succ m ih =>
    by_cases m_even : (Nat.succ m + 1) % 2 = 0
    · rw [m_even]
      norm_num
      sorry
    · sorry

[Jeremy Tan]

oh, by_cases

[Martin Dvořák]

Disclaimer: I don't know if my approach will be easier in the end.

[Martin Dvořák]

Update: It looks like too much work. I am quitting for now.

[Jeremy Tan]

Simpler idea:

theorem cassini_identity (n : ℕ) : fib n * fib (n + 2) +
  (if Even n then 2 else 0) - 1 = fib (n + 1) ^ 2 := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [fib, fib, add_sq, ← ih, fib]
    by_cases v : Even n
    · simp [v]
    · _

but how to get Lean to understand that if n is even, n+1 is odd so I can simplify if Even (Nat.succ n) then 2 else 0?

[Alex J. Best]

does simpa [parity_simps] work?

[Alex J. Best]

parity_simps is a custom simp set for dealing with parity related questions, it should help with problems like this, in any case lemmas in this file will help https://github.com/leanprover-community/mathlib4/blob/69108c782429c57637807f32d923e34c195ec823/Mathlib/Data/Nat/Parity.lean

[Alex J. Best]

maybe doing rw [if_neg] first will be easier

[Jeremy Tan]

Alex J. Best said:

maybe doing rw [if_neg] first will be easier

Here's my plan, which involves not using the IH until the equation is simplified enough:

F(n+1) * (F(n+1)+F(n+2)) + (if Even (Nat.succ n) then 2 else 0) - 1) = F(n)^2 + 2 F(n) F(n+1) + F(n+1)^2

F(n+1) * (F(n) + F(n+1)) + (if Even (Nat.succ n) then 2 else 0) - 1) = F(n)^2 + 2 F(n) F(n+1)

F(n+1)^2 + (if Even (Nat.succ n) then 2 else 0) - 1) = F(n) * (F(n) + F(n+1))

F(n+1)^2 + (if Even (Nat.succ n) then 2 else 0) - 1) = F(n) * F(n+2)

I need a way to "cancel the same thing from both sides of an equation"

[Jeremy Tan]

Oh, and how can I turn a = b into a + c - c = b and specify what c is, and distribute coercions, if I go down the route below?

[Jeremy Tan]

theorem cassini_identity (n : ℕ) : (fib n : ℤ) * fib (n + 2) -
    (fib (n + 1) : ℤ) ^ 2 = (-1) ^ (n + 1) := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [sq, ←add_sub_cancel] -- ...

[Jeremy Tan]

I think the formulation immediately above with internal \Z coercions in the statement is absolutely necessary, since if the (-1)^n term in Cassini's identity is represented with \N-only constructs it won't be true for half the integers because of the way \N-subtraction floors out at 0

[Kevin Buzzard]

Yes, any mathematical statement involving subtraction of naturals should be formalised via coercion to integers, because natural subtraction as thought of by lean is not what mathematicians mean by subtraction. Similarly anything involving division should first be coerced into rationals.

[Jeremy Tan]

Martin Dvořák said:

I think we can express your theorem in terms of ℕ only.

right, I'm not trusting this now

[Martin Dvořák]

Parcly Taxel said:

Martin Dvořák said:

I think we can express your theorem in terms of ℕ only.

right, I'm not trusting this now

I mean, in the way I wrote it, flooring at 0 never happened, but it is likely that my formulation would lead to an overcomplicated proof.

[Jeremy Tan]

https://en.wikipedia.org/wiki/Cassini_and_Catalan_identities on this page I see a proof by induction, and when I pasted this in I intended to follow said proof, which involves adding a a-a term

[Martin Dvořák]

Yeah, that's better to be done in integers.

[Martin Dvořák]

You can start with

def fib : Nat → Int
| 0   => 0
| 1   => 1
| n+2 => fib n + fib (n+1)

to avoid problems with coercion. I mean, not for the "production version", but for prototyping your proof.

[Jeremy Tan]

hey, this works! :tada:

def fib : ℕ → ℤ
  | 0       => 0
  | 1       => 1
  | (x + 2) => fib x + fib (x + 1)

theorem cassini_identity (n : ℕ) : fib n * fib (n + 2) -
    fib (n + 1) ^ 2 = (-1) ^ (n + 1) := by
  induction n with
  | zero => rfl
  | succ n ih =>
    conv => rhs; rw [pow_succ, ← ih]
    rw [fib, fib]; ring

[Reid Barton]

Turns out negative numbers were a great idea.