Zulip Chat Archive

Stream: new members

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

Hanting Zhang (Dec 31 2020 at 01:18):

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 :=
  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))], }

/-- 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) :=
  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, }

lemma fib_add (m n : ) (hm2 : 1  m) :
  fib (m + n) = fib (m - 1) * fib n + fib m * fib (n + 1) :=
  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,

lemma gcd_fib_add_self' (m n : ) : gcd (fib m) (fib n) = gcd (fib m) (fib(n + m)) :=
  cases eq_zero_or_pos n,
  { rw h, simp },
  calc m.fib.gcd n.fib
        = gcd (fib m) (fib n * fib(m + 1)) :
      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,
    ... = 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,

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

lemma gcd_fib_fib' (m' n' : ) (hmn : m'  n') : gcd (fib m') (fib n') = fib(gcd m' n') :=
  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, }

/-- `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):=
  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 nat

Alex J. Best (Dec 31 2020 at 01:24):

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 (Dec 31 2020 at 01:26):

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 (Dec 31 2020 at 01:26):

Fixed. I just deleted the top headers.

Bryan Gin-ge Chen (Dec 31 2020 at 01:29):

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 (Dec 31 2020 at 01:29):

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 (Dec 31 2020 at 01:35):

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 (Dec 31 2020 at 01:38):

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 (Dec 31 2020 at 01:40):

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

Mario Carneiro (Dec 31 2020 at 01:41):

also spaces after <- in rw

Mario Carneiro (Dec 31 2020 at 01:41):

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

Hanting Zhang (Dec 31 2020 at 02:57):

Ok, I'll put in the details.

Hanting Zhang (Dec 31 2020 at 03:11):

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 (Dec 31 2020 at 03:13):

Invite sent!

Yakov Pechersky (Dec 31 2020 at 05:02):

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

Hanting Zhang (Dec 31 2020 at 21:59):

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 (Dec 31 2020 at 22:00):

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

Johan Commelin (Dec 31 2020 at 22:01):

git checkout -b gcd-fib

Hanting Zhang (Dec 31 2020 at 22:11):

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

Bryan Gin-ge Chen (Dec 31 2020 at 22:13):

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

Johan Commelin (Jan 01 2021 at 06:07):

@Hanting Zhang congrats on your first PR

Hanting Zhang (Jan 01 2021 at 06:39):

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

Johan Commelin (Jan 01 2021 at 07:05):

@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 (Jan 01 2021 at 07:13):

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 (Jan 01 2021 at 07:18):

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

Johan Commelin (Jan 01 2021 at 07:18):

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

Hanting Zhang (Jan 01 2021 at 07:28):

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 (Jan 01 2021 at 07:30):

I use the same learning strategy (-;

Last updated: Dec 20 2023 at 11:08 UTC