Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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 :=
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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Hanting Zhang (Dec 31 2020 at 01:26):

Fixed. I just deleted the top headers.

view this post on Zulip 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 [...].

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Alex J. Best (Dec 31 2020 at 01:40):

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

view this post on Zulip Mario Carneiro (Dec 31 2020 at 01:41):

also spaces after <- in rw

view this post on Zulip 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

view this post on Zulip Hanting Zhang (Dec 31 2020 at 02:57):

Ok, I'll put in the details.

view this post on Zulip 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'.

view this post on Zulip Bryan Gin-ge Chen (Dec 31 2020 at 03:13):

Invite sent!

view this post on Zulip Yakov Pechersky (Dec 31 2020 at 05:02):

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

view this post on Zulip 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'```

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 31 2020 at 22:01):

git checkout -b gcd-fib

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Dec 31 2020 at 22:13):

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

view this post on Zulip Johan Commelin (Jan 01 2021 at 06:07):

@Hanting Zhang congrats on your first PR

view this post on Zulip Hanting Zhang (Jan 01 2021 at 06:39):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 01 2021 at 07:18):

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

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Jan 01 2021 at 07:30):

I use the same learning strategy (-;


Last updated: May 11 2021 at 14:11 UTC