Fibonacci Divisibility Sequence

Stream: new members

[Lawrence Lin]

Hi, guys!! I just need to resolve some final steps in my Fibonacci code - can someone help with this?

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

lemma fib_rule (n : ℕ) : fib(n + 2) = fib(n) + fib(n + 1) := rfl

theorem strong_induction {P : ℕ → Prop} {H : ∀ n : ℕ, (∀ m : ℕ, m < n → P m) → P n} (n : ℕ) : P n := sorry, -- this is already proven
theorem fib_add (m n : ℕ) (hm : m > 0) (hn : n > 0): fib(m + n) = fib(n + 1) * fib(m) + fib(n) * fib(m - 1) := sorry, -- this is also proven

example (m n : ℕ) (hm : m > 0) (hyp_div : m ∣ n): fib(m) ∣ fib(n) :=
begin
  rcases hyp_div with ⟨k, rfl⟩,
  induction k,
  {
    simp [fib],
  },
  {
    change fib m ∣ fib(m * (k_n + 1)),
    rw [mul_add, add_comm, mul_one],
    rw fib_add (m) (m * k_n),
    apply dvd_add,
    simp,
    apply dvd_mul_of_dvd_left,
    apply k_ih,
    exact hm,
  },
end

now, all we have to do is say that since we're inducting on k and that this is the induction step, k must be greater than the base case (where k = 0). therefore, m and k are both positive -> their product is positive. how would i write this in LEAN?

[Gareth Ma]

@Lawrence Lin Sounds like something I would be good at by this point (I am new too) :P Firstly, the thing you are trying to prove right now is false, since your goal looks like

m: ℕ
hm: m > 0
k_n: ℕ
k_ih: fib m ∣ fib (m * k_n)
⊢ m * k_n > 0

Which is false for m = 1 and k_n = 0, since k | 0

[Gareth Ma]

I think you can treat the case n = 0 separately. Not sure if it's the best way but it's an easy way. So something like cases n at the start.

[Gareth Ma]

By the way here are some "I wish someone told me" for you
(1) almost always write <, since most theorems are written that way and it makes searching for theorems easier. So write 0 < m and such.
(2) you don't need a lot of the (), since lean interprets expressions after a function as its arguments. So fib m (m * k)would work instead of fib_add (m) (m * k_n)
(3) After you write simp you can change it to a squeeze_simp, then it will tell you which theorems it used. It will help you learn too!
(4) Also, I don't think you know this, but for induction you can name the arguments generated. The syntax is induction ... using ... .... In this case, you can write induction k with k ik, if you hate underscores like me

[Gareth Ma]

Oh and to answer your original question, you need mul_pos. Here:

example (m n : ℕ) (hm : m > 0) (hyp_div : m ∣ n): fib(m) ∣ fib(n) :=
begin
  rcases hyp_div with ⟨k, rfl⟩,
  induction k,
  { simp [fib], },
  { by_cases h : k_n = 0,
    { rw [h, mul_one], },
    { replace h := nat.one_le_iff_ne_zero.2 h,
      change fib m ∣ fib(m * (k_n + 1)),
      rw [mul_add, add_comm, mul_one],
      rw fib_add (m) (m * k_n),
      apply dvd_add,
      simp,
      apply dvd_mul_of_dvd_left,
      apply k_ih,
      exact hm,
      apply mul_pos hm h, }, },
end

[Gareth Ma]

example (m n : ℕ) (hm : m > 0) (hyp_div : m ∣ n): fib(m) ∣ fib(n) :=
begin
  rcases hyp_div with ⟨k, rfl⟩,
  induction k,
  { simp [fib], },
  -- by the way, you can use `cases k_n` too, but then... you can try :)
  { by_cases h : k_n = 0,
    { rw [h, mul_one], },
    { replace h := nat.one_le_iff_ne_zero.2 h,
      -- rw [] writes each in order
      rw [nat.succ_eq_add_one, mul_add, add_comm, mul_one, fib_add m (m * k_n) hm _],
      apply dvd_add,
      apply dvd_mul_left,
      apply dvd_mul_of_dvd_left k_ih,
      apply mul_pos hm h, }, },
end

[Lawrence Lin]

thank you! let me digest this rq ;w;
also... i'm pretty sure lean was cool with the case fib(n) | 0? hm..

[Gareth Ma]

Yea lean is fine, that's exact what I prove in the { rw [h, mul_one] }. But to use mul_pos, it's not fine

[Gareth Ma]

Oh I think I know why. I think your (hn : n > 0) in fib_add is unnecessary.

[Lawrence Lin]

oh...

[Lawrence Lin]

yep, it was.

[Lawrence Lin]

i often find myself doing a lot of like, "nasty conversions" just to get lean to listen to me... sigh. i'll try to avoid it!! thank you for your help gareth c:

[Gareth Ma]

After removing that the proof is 7 lines (with the inlined brackets like I wrote it) :D

[Gareth Ma]

No problem!

[Lawrence Lin]

ooh 1s lemme try

[Lawrence Lin]

wait, the proof is 7 lines?

[Gareth Ma]

5 if I try

[Gareth Ma]

example (m n : ℕ) (hm : m > 0) (hyp_div : m ∣ n): fib(m) ∣ fib(n) :=
begin
  rcases hyp_div with ⟨k, rfl⟩,
  induction k,
  { simp [fib], },
  { rw [nat.succ_eq_add_one, mul_add, add_comm, mul_one, fib_add m (m * k_n) hm],
    apply dvd_add,
    apply dvd_mul_left,
    apply dvd_mul_of_dvd_left k_ih, },
end

[Lawrence Lin]

oh...

[Lawrence Lin]

let me re-digest that :')

[Gareth Ma]

Here's one more thing you can try and explore. You see those repeated applys? It's annoying to type them out, especially when you have 9187359723859 different things. With simp, you can provide lemmas to it to tell lean which lemmas to use. So you can write this!

example (m n : ℕ) (hm : m > 0) (hyp_div : m ∣ n): fib(m) ∣ fib(n) :=
begin
  rcases hyp_div with ⟨k, rfl⟩,
  induction k,
  { simp only [fib, mul_zero, dvd_zero], },
  { rw [nat.succ_eq_add_one, mul_add, add_comm, mul_one, fib_add m (m * k_n) hm],
    simp only [dvd_add, dvd_mul_left, dvd_mul_of_dvd_left k_ih], },
end

The only just means... "only". It speeds up computation too.

[Lawrence Lin]

oh wow.

[Lawrence Lin]

lemme try applying that to my old code

[Lawrence Lin]

seems like simp only doesn't really work sometimes

[Lawrence Lin]

specifically with lt_trans

[Gareth Ma]

Oh yea, essentially if uses it only if it knows everything it needs

[Gareth Ma]

For lt_trans you need two arguments lt_trans [[a < b]] [[b < c]], so you should provide those.

[Lawrence Lin]

fair enough
let me try

[Lawrence Lin]

ouch lean isn't happy with it, 1s

[Lawrence Lin]

simp only [lt_add_one, lt_trans [[lt_add_one]] [[lt_add_one]]],
did this

[Lawrence Lin]

theorem fib_add (m n : ℕ) (hm : m > 0) : fib(m + n) = fib(n + 1) * fib(m) + fib(n) * fib(m - 1) :=
begin
  apply strong_induction n,
  intro k,
  intro h,
  cases k,
  { simp [fib] },
  {
    cases k,
    {
      simp [fib],
      simp only [fib_rule', hm],
    },
    {
      change fib(m + k) + fib(m + k + 1) = fib (k.succ.succ + 1) * fib m + fib k.succ.succ * fib (m - 1),
      rw [h, add_assoc m k 1, h (k+1), ←add_assoc],

      have H1 : fib (k + 1) * fib m + fib k * fib (m - 1) + fib (k + 1 + 1) * fib m + fib (k + 1) * fib (m - 1) = (fib (k + 1) + fib (k + 1 + 1)) * fib m + (fib(k) + fib(k + 1)) * fib (m - 1),
      {
        ring_nf,
      },

      rw H1,
      rw [←fib_rule, ←fib_rule],

      simp only [lt_add_one],
      apply lt_trans,
      apply lt_add_one,
      apply lt_add_one,
    },
  },
end

here was the working lean code for fib_add

[Lawrence Lin]

(it is messy sorry)

[Gareth Ma]

Try exact lt_trans (lt_add_one _) (lt_add_one _) instead.

[Lawrence Lin]

why exact and not apply?

[Gareth Ma]

exact means (you guessed it) you have the exact statement

[Gareth Ma]

Here lt_trans ... is exactly what you want, so exact works

[Lawrence Lin]

ah

[Lawrence Lin]

do you know how i can get rid of my H1

[Lawrence Lin]

i think it's pretty unnecessary but...

[Gareth Ma]

By the way consider using by_cases like I did in my origin answer all the way up, it will decluster all the succ

[Gareth Ma]

Maybe I can try to prove that part from scratch, then you can see?

[Lawrence Lin]

ah- sure!

[Lawrence Lin]

thank you u.u

[Lawrence Lin]

(i don't know, been playing with lean for a few months and yet i still can't get the hang of it :( )

[Lawrence Lin]

i rmb implementing strong induction just to make that proof work haha

[Gareth Ma]

Hahaha, it's in mathlib already

[Gareth Ma]

https://leanprover-community.github.io/mathlib_docs/find/nat.strong_induction_on/
You use this by writing induction n using nat.strong_induction_on

[Lawrence Lin]

._.

[Lawrence Lin]

aaaaaaaaaa

[Lawrence Lin]

tbf i did try using that one then gave up ahaha ;w;
idk...

[Gareth Ma]

Sorry it took a while, I am slow too hahahaha. Here you go:

theorem fib_add (m n : ℕ) (hm : 0 < m) : fib(m + n) = fib(n + 1) * fib(m) + fib(n) * fib(m - 1) :=
begin
  apply strong_induction n,
  -- use `intros` instead of `intro`
  intros k h,
  -- using by_cases instead of cases for... my eyes
  cases k,
  { simp [fib], },
  { cases k,
    { -- see how `fib_rule'` takes arguments, so i supply them? in `fib_rule' m hm`
      simp [fib, fib_rule' m hm],
    },
    { simp only [nat.succ_eq_add_one, add_assoc],
      norm_num,
      -- we "massage" things into the right form, then expand everything
      rw [← add_assoc, fib, nat.succ_eq_add_one, add_assoc m k 1],
      rw [h k _, h (k + 1) _],
      rw [fib_rule (k + 1), fib_rule k],
      -- and then ring gets rid of everything
      ring,
      exact nat.lt_succ_self _,
      exact lt_trans (nat.lt_succ_self _) (nat.lt_succ_self _),
    },
  },
end

[Gareth Ma]

but yea, my proof idea is "expand everything to base case, then deal with it", which seems to be yours too

[Kevin Buzzard]

You would be better off using r:=m-1 as your variable and not m, so you don't have to deal with natural subtraction and the hypothesis that m>0

[Lawrence Lin]

Gareth Ma said:

but yea, my proof idea is "expand everything to base case, then deal with it", which seems to be yours too

yep :3c