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 :=
begin
induction n with n ih,
{ simp },
{ convert ih using 1,
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),
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,
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)) :
... = 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 (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'.

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: May 11 2021 at 14:11 UTC