Feedback for a gcd( F_n, F_m) = F_{gcd(n, m)} proof

Stream: new members

[Hanting Zhang]

Hi, I want some feedback on a proof on the GCD of the Fibonacci numbers. Part of the problem is that I don't really know what kind of feedback I'm supposed to be looking for, so please say whatever comes to mind. I think my tactic writing could be cleaner, and proofs could be shorter. Also, how can I clean up the calc proof for gcd_fib_add_self'? Below should be a MWE.

import data.nat.fib
import data.nat.gcd
import tactic

namespace nat

lemma gcd_add_self (m n : ℕ) : gcd m n = gcd m (n + m) :=
by simp [gcd_rec m (n + m), gcd_rec m n]

/-- https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime -/
lemma fib_succ_coprime (n : ℕ) : gcd (fib n) (fib(n + 1)) = 1 :=
begin
  induction n with n ih,
  { simp },
  { convert ih using 1,
    rw [fib_succ_succ, succ_eq_add_one, gcd_rec, add_mod_right, gcd_comm (fib n),
      gcd_rec (fib (n + 1))], }
end

/-- https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers -/
lemma fib_add_succ (m n : ℕ) :
  fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1) :=
begin
  induction n with n ih generalizing m,
  { simp },
  { intros,
    specialize ih (m + 1),
    rw [add_right_comm m 1, add_assoc m] at ih,
    simp only [fib_succ_succ, ih],
    ring, }
end

lemma fib_add (m n : ℕ) (hm2 : 1 ≤ m) :
  fib (m + n) = fib (m - 1) * fib n + fib m * fib (n + 1) :=
begin
  obtain ⟨m', hm'⟩ : (∃ m', m' + 1 = m) := begin use m - 1, exact nat.sub_add_cancel hm2 end,
  rw [←hm', add_assoc, add_comm 1 _, ←add_assoc],
  exact fib_add_succ m' n,
end

lemma gcd_fib_add_self' (m n : ℕ) : gcd (fib m) (fib n) = gcd (fib m) (fib(n + m)) :=
begin
  cases eq_zero_or_pos n,
  { rw h, simp },
  calc m.fib.gcd n.fib
        = gcd (fib m) (fib n * fib(m + 1)) :
    begin
      have hcop := coprime.symm (fib_succ_coprime m),
      rw [gcd_comm, gcd_comm (fib m) _, mul_comm _ (fib (m + 1)), coprime.gcd_mul_left_cancel],
      exact hcop,
    end
    ... = gcd (fib m) (fib(n - 1) * (fib m) + fib n * fib(m + 1)) :
    by rw [←gcd_add_self (fib m) _ (fib(n - 1)), add_comm]
    ... = m.fib.gcd (n + m).fib :
    begin rw fib_add n _ _, assumption end
    ... = m.fib.gcd (n + m).fib : by ring,
end

lemma gcd_fib_add_self (m n k : ℕ) : gcd (fib m) (fib n) = gcd (fib m) (fib(n + k * m)) :=
begin
  induction k with k hk,
  { simp },
  { rw [hk, gcd_fib_add_self' _ _],
    ring, }
end

lemma gcd_fib_fib' (m' n' : ℕ) (hmn : m' ≤ n') : gcd (fib m') (fib n') = fib(gcd m' n') :=
begin
  apply gcd.induction m' n',
  { simp },
  { intros m n mpos h,
    rw ←gcd_rec m n at h,
    conv_lhs { rw ←mod_add_div n m },
    rw [mul_comm, ←gcd_fib_add_self m (n % m) (n / m), gcd_comm],
    exact h, }
end

/-- `fib n` is a strong divisibility sequence
  https://proofwiki.org/wiki/GCD_of_Fibonacci_Numbers -/
lemma gcd_fib_fib (m n : ℕ) : gcd (fib m) (fib n) = fib(gcd m n):=
begin
  cases le_total m n with m_le_n n_le_m,
  { exact gcd_fib_fib' m n m_le_n },
  { rw [gcd_comm, gcd_comm m n],
    exact gcd_fib_fib' n m n_le_m }
end

end nat

[Alex J. Best]

You shouldn't need to redefine fib if you've imported nat.fib there is already a definition of fib there (its a little different in definition but the functions are equal) so you should be able to use the existing one and its api.

[Alex J. Best]

rw gcd_rec m (n + m), simp, rw gcd_rec m n, contains what we call a "nonterminal simp", that is some use of simp that doesn't close the goal, these can sometimes make code hard to maintain (if simp gets smarter/better in future your proof might break). In this case you can replace the whole proof with

by simp [gcd_rec m (n + m), gcd_rec m n]

so the simp call is the only thing :smile:

[Hanting Zhang]

Fixed. I just deleted the top headers.

[Bryan Gin-ge Chen]

rw [...] followed by assumption or exact h where h is the name of a hypothesis in the context can usually be replaced by rwa [...].

[Alex J. Best]

The buisness with obtain ⟨m', hm'⟩ : (∃ m', m' + 1 = m) := begin use m - 1, exact nat.sub_add_cancel hm2 end, looks more complicated than it needs to be, there is a lemma docs#nat.succ_pred_eq_of_pos which you should be able to use with hm2 to simplify the proof.

[Alex J. Best]

Personally I would try and see if everything can be done only with fib_add_succ rather than fib_add, subtracting nats is always annoying and if all the lemmas can be stated without it it might be possible to avoid it.

[Alex J. Best]

We tend to always put spaces after functions, like fib (m + 1) instead of fib(m + 1) even though it isn't needed when there are brackets

[Alex J. Best]

But yeah this mostly looks pretty good to me :grinning:

[Mario Carneiro]

also spaces after <- in rw

[Mario Carneiro]

we really need a formatter, but given the state of lean parsing that's certainly not going to happen

[Hanting Zhang]

Ok, I'll put in the details.

[Hanting Zhang]

I'll try to see if using fib_add_succ makes things shorter. Can I get push access for mathlib? Err, I'm not too familiar with git, but my user is 'acxxa'.

[Bryan Gin-ge Chen]

Invite sent!

[Yakov Pechersky]

I would flip gcd_add_self to have the simpler expression on the RHS

[Hanting Zhang]

I'm in the process of making a PR to mathlib, but it seems I don't have access to push, even though I should. Maybe I need another invite? Here's the error message.

remote: error: You're not authorized to push to this branch. Visit https://docs.github.com/articles/about-protected-branches/ for more information.
To https://github.com/leanprover-community/mathlib
 ! [remote rejected]     master -> master (protected branch hook declined)
error: failed to push some refs to 'https://github.com/leanprover-community/mathlib'```

[Bryan Gin-ge Chen]

You cannot push to the master branch. You should create a new branch and push to that.

[Johan Commelin]

git checkout -b gcd-fib

[Hanting Zhang]

#5549 ? I suspect that I must be doing something wrong. Sorry in advance for any git mistakes.

[Bryan Gin-ge Chen]

I don't see any git issues there. Congrats on opening your first PR!

[Johan Commelin]

@Hanting Zhang congrats on your first PR

[Hanting Zhang]

Thanks! That was simultaneously easier and harder than I expected it to be.

[Johan Commelin]

@Hanting Zhang In what sense? If there are any painpoints that we can make easier, we'd be happy to hear about them

[Hanting Zhang]

The opposite, actually. The PR itself felt smooth. It was working with Git that tripped me, and I had to get a friend to step me through everything. But that's more of a "just keeping doing it and you'll figure it out" thing.

[Johan Commelin]

Yeah, git can take some time to get used to. But there are good tutorials out there.

[Johan Commelin]

Did you make use of our video tutorial on how to make a PR?

[Hanting Zhang]

Huh, I've just been diving in and picking things up when I need them. I guess I definitely should look through the community resources now, though... maybe even actually read Theorem Proving in Lean. :sweat_smile:

[Johan Commelin]

I use the same learning strategy (-;