refactor(data/nat/fib): use nat.iterate (#10489)

The main drawback of the new definition is that `fib (n + 2) = fib n + fib (n + 1)` is no longer `rfl` but I think that we should have one API for iterates.

See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60nat.2Eiterate.60.20vs.20.60stream.2Eiterate.60

archive/imo/imo1981_q3.lean

@@ -130,7 +130,7 @@ begin
     { have h7 : nat_predicate N (n - m) m, from h2.reduction h4,
       obtain ⟨k : ℕ, hnm : n - m = fib k, rfl : m = fib (k+1)⟩ := h1 m h6 (n - m) h7,
       use [k + 1, rfl],
-      rw [fib_succ_succ, ← hnm, tsub_add_cancel_of_le h3] } }
+      rw [fib_add_two, ← hnm, tsub_add_cancel_of_le h3] } }
 end
 
 end nat_predicate
@@ -156,6 +156,7 @@ begin
          ... ≤ fib (K+1) : fib_mono h6 } },
   { have h7 : N < n,
     { have h8 : K + 2 ≤ k + 1, from succ_le_succ (not_lt.mp h2),
+      rw ← fib_add_two at HK,
       calc N < fib (K+2) : HK
          ... ≤ fib (k+1) : fib_mono h8
          ... = n         : hn.symm, },
@@ -199,6 +200,6 @@ theorem imo1981_q3 : is_greatest (specified_set 1981) 3524578 :=
 begin
   have := λ h, @solution_greatest 1981 16 h 3524578,
   simp only [show fib (16:ℕ) = 987 ∧ fib (16+1:ℕ) = 1597,
-    by norm_num [fib_succ_succ]] at this,
+    by norm_num [fib_add_two]] at this,
   apply_mod_cast this; norm_num [problem_predicate_iff],
 end

src/algebra/continued_fractions/computation/approximations.lean

@@ -198,8 +198,8 @@ begin
   clear n,
   assume n IH hyp,
   rcases n with _|_|n,
-  { simp [fib_succ_succ, continuants_aux] }, -- case n = 0
-  { simp [fib_succ_succ, continuants_aux] }, -- case n = 1
+  { simp [fib_add_two, continuants_aux] }, -- case n = 0
+  { simp [fib_add_two, continuants_aux] }, -- case n = 1
   { let g := of v,  -- case 2 ≤ n
     have : ¬(n + 2 ≤ 1), by linarith,
     have not_terminated_at_n : ¬g.terminated_at n, from or.resolve_left hyp this,
@@ -209,7 +209,7 @@ begin
     set ppconts := g.continuants_aux n with ppconts_eq,
     -- use the recurrence of continuants_aux
     suffices : (fib n : K) + fib (n + 1) ≤ gp.a * ppconts.b + gp.b * pconts.b, by
-      simpa [fib_succ_succ, add_comm,
+      simpa [fib_add_two, add_comm,
         (continuants_aux_recurrence s_ppred_nth_eq ppconts_eq pconts_eq)],
     -- make use of the fact that gp.a = 1
     suffices : (fib n : K) + fib (n + 1) ≤ ppconts.b + gp.b * pconts.b, by

src/data/nat/fib.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
 import data.nat.gcd
-import data.stream.init
 import tactic.ring
 
 /-!
@@ -20,8 +19,8 @@ Definition of the Fibonacci sequence `F₀ = 0, F₁ = 1, Fₙ₊₂ = Fₙ + F
 
 ## Main Statements
 
-- `fib_succ_succ` : shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁.`.
-- `fib_gcd`       : `fib n` is a strong divisibility sequence.
+- `fib_add_two` : shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁.`.
+- `fib_gcd`     : `fib n` is a strong divisibility sequence.
 
 ## Implementation Notes
 
@@ -34,12 +33,6 @@ fib, fibonacci
 
 namespace nat
 
-/-- Auxiliary function used in the definition of `fib_aux_stream`. -/
-private def fib_aux_step : (ℕ × ℕ) → (ℕ × ℕ) := λ p, ⟨p.snd, p.fst + p.snd⟩
-
-/-- Auxiliary stream creating Fibonacci pairs `⟨Fₙ, Fₙ₊₁⟩`. -/
-private def fib_aux_stream : stream (ℕ × ℕ) := stream.iterate fib_aux_step ⟨0, 1⟩
-
 /--
 Implementation of the fibonacci sequence satisfying
 `fib 0 = 0, fib 1 = 1, fib (n + 2) = fib n + fib (n + 1)`.
@@ -48,70 +41,59 @@ Implementation of the fibonacci sequence satisfying
 implementation.
 -/
 @[pp_nodot]
-def fib (n : ℕ) : ℕ := (fib_aux_stream n).fst
+def fib (n : ℕ) : ℕ := ((λ p : ℕ × ℕ, (p.snd, p.fst + p.snd))^[n] (0, 1)).fst
 
 @[simp] lemma fib_zero : fib 0 = 0 := rfl
 @[simp] lemma fib_one : fib 1 = 1 := rfl
 @[simp] lemma fib_two : fib 2 = 1 := rfl
 
-private lemma fib_aux_stream_succ {n : ℕ} :
-    fib_aux_stream (n + 1) = fib_aux_step (fib_aux_stream n) :=
-begin
-  change (stream.nth (n + 1) $ stream.iterate fib_aux_step ⟨0, 1⟩) =
-      fib_aux_step (stream.nth n $ stream.iterate fib_aux_step ⟨0, 1⟩),
-  rw [stream.nth_succ_iterate, stream.map_iterate, stream.nth_map]
-end
-
 /-- Shows that `fib` indeed satisfies the Fibonacci recurrence `Fₙ₊₂ = Fₙ + Fₙ₊₁.` -/
-lemma fib_succ_succ {n : ℕ} : fib (n + 2) = fib n + fib (n + 1) :=
-by simp only [fib, fib_aux_stream_succ, fib_aux_step]
-
-lemma fib_pos {n : ℕ} (n_pos : 0 < n) : 0 < fib n :=
-begin
-  induction n with n IH,
-  case nat.zero { norm_num at n_pos },
-  case nat.succ
-  { cases n,
-    case nat.zero { simp [fib_succ_succ, zero_lt_one] },
-    case nat.succ
-    { have : 0 ≤ fib n, by simp,
-      exact (lt_add_of_nonneg_of_lt this $ IH n.succ_pos) }}
-end
+lemma fib_add_two {n : ℕ} : fib (n + 2) = fib n + fib (n + 1) :=
+by simp only [fib, function.iterate_succ']
 
-lemma fib_le_fib_succ {n : ℕ} : fib n ≤ fib (n + 1) := by { cases n; simp [fib_succ_succ] }
+lemma fib_le_fib_succ {n : ℕ} : fib n ≤ fib (n + 1) := by { cases n; simp [fib_add_two] }
 
 @[mono] lemma fib_mono : monotone fib :=
 monotone_nat_of_le_succ $ λ _, fib_le_fib_succ
 
+lemma fib_pos {n : ℕ} (n_pos : 0 < n) : 0 < fib n :=
+calc 0 < fib 1 : dec_trivial
+   ... ≤ fib n : fib_mono n_pos
+
+lemma fib_lt_fib_succ {n : ℕ} (hn : 2 ≤ n) : fib n < fib (n + 1) :=
+begin
+  rcases le_iff_exists_add.1 hn with ⟨n, rfl⟩,
+  simp only [add_comm 2, fib_add_two], rw add_comm,
+  exact lt_add_of_pos_left _ (fib_pos succ_pos')
+end
+
 /-- `fib (n + 2)` is strictly monotone. -/
 lemma fib_add_two_strict_mono : strict_mono (λ n, fib (n + 2)) :=
-strict_mono_nat_of_lt_succ $ λ n, lt_add_of_pos_left _ $ fib_pos succ_pos'
+begin
+  refine strict_mono_nat_of_lt_succ (λ n, _),
+  rw add_right_comm,
+  exact fib_lt_fib_succ (self_le_add_left _ _)
+end
 
 lemma le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ fib n :=
 begin
   induction five_le_n with n five_le_n IH,
-  { have : 5 = fib 5, by refl,  -- 5 ≤ fib 5
-    exact le_of_eq this },
+  { -- 5 ≤ fib 5
+    refl },
   { -- n + 1 ≤ fib (n + 1) for 5 ≤ n
-    cases n with n', -- rewrite n = succ n' to use fib.succ_succ
-    { have : 5 = 0, from nat.le_zero_iff.elim_left five_le_n, contradiction },
-    rw fib_succ_succ,
-    suffices : 1 + (n' + 1) ≤ fib n' + fib (n' + 1), by rwa [nat.succ_eq_add_one, add_comm],
-    have : n' ≠ 0, by { intro h, have : 5 ≤ 1, by rwa h at five_le_n, norm_num at this },
-    have : 1 ≤ fib n', from nat.succ_le_of_lt (fib_pos $ pos_iff_ne_zero.mpr this),
-    mono }
+    rw succ_le_iff,
+    calc n ≤ fib n       : IH
+       ... < fib (n + 1) : fib_lt_fib_succ (le_trans dec_trivial five_le_n) }
 end
 
 /-- Subsequent Fibonacci numbers are coprime,
   see https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime -/
 lemma fib_coprime_fib_succ (n : ℕ) : nat.coprime (fib n) (fib (n + 1)) :=
 begin
-  unfold coprime,
   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))], }
+  { rw [fib_add_two, coprime_add_self_right],
+    exact ih.symm }
 end
 
 /-- See https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers -/
@@ -123,7 +105,7 @@ begin
   { intros,
     specialize ih (m + 1),
     rw [add_assoc m 1 n, add_comm 1 n] at ih,
-    simp only [fib_succ_succ, ← ih],
+    simp only [fib_add_two, ← ih],
     ring, }
 end
 

src/data/nat/gcd.lean

@@ -137,17 +137,28 @@ by rw [gcd_comm, gcd_gcd_self_right_right]
 @[simp] lemma gcd_gcd_self_left_left (m n : ℕ) : gcd (gcd m n) m = gcd m n :=
 by rw [gcd_comm m n, gcd_gcd_self_left_right]
 
-lemma gcd_add_mul_self (m n k : ℕ) : gcd m (n + k * m) = gcd m n :=
+@[simp] lemma gcd_add_mul_self (m n k : ℕ) : gcd m (n + k * m) = gcd m n :=
 by simp [gcd_rec m (n + k * m), gcd_rec m n]
 
-theorem gcd_eq_zero_iff {i j : ℕ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
+@[simp] lemma gcd_add_self_right (m n : ℕ) : gcd m (n + m) = gcd m n :=
+eq.trans (by rw one_mul) (gcd_add_mul_self m n 1)
+
+@[simp] lemma gcd_add_self_left (m n : ℕ) : gcd (m + n) n = gcd m n :=
+by rw [gcd_comm, gcd_add_self_right, gcd_comm]
+
+@[simp] lemma gcd_self_add_left (m n : ℕ) : gcd (m + n) m = gcd n m :=
+by rw [add_comm, gcd_add_self_left]
+
+@[simp] lemma gcd_self_add_right (m n : ℕ) : gcd m (m + n) = gcd m n :=
+by rw [add_comm, gcd_add_self_right]
+
+@[simp] theorem gcd_eq_zero_iff {i j : ℕ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
 begin
   split,
   { intro h,
     exact ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩, },
-  { intro h,
-    rw [h.1, h.2],
-    exact nat.gcd_zero_right _ }
+  { rintro ⟨rfl, rfl⟩,
+    exact nat.gcd_zero_right 0 }
 end
 
 /-! ### `lcm` -/
@@ -278,6 +289,18 @@ theorem exists_coprime' {m n : ℕ} (H : 0 < gcd m n) :
   ∃ g m' n', 0 < g ∧ coprime m' n' ∧ m = m' * g ∧ n = n' * g :=
 let ⟨m', n', h⟩ := exists_coprime H in ⟨_, m', n', H, h⟩
 
+@[simp] theorem coprime_add_self_right {m n : ℕ} : coprime m (n + m) ↔ coprime m n :=
+by rw [coprime, coprime, gcd_add_self_right]
+
+@[simp] theorem coprime_self_add_right {m n : ℕ} : coprime m (m + n) ↔ coprime m n :=
+by rw [add_comm, coprime_add_self_right]
+
+@[simp] theorem coprime_add_self_left {m n : ℕ} : coprime (m + n) n ↔ coprime m n :=
+by rw [coprime, coprime, gcd_add_self_left]
+
+@[simp] theorem coprime_self_add_left {m n : ℕ} : coprime (m + n) m ↔ coprime n m :=
+by rw [coprime, coprime, gcd_self_add_left]
+
 theorem coprime.mul {m n k : ℕ} (H1 : coprime m k) (H2 : coprime n k) : coprime (m * n) k :=
 (H1.gcd_mul_left_cancel n).trans H2
 

src/data/real/golden_ratio.lean

@@ -153,7 +153,7 @@ begin
   rw fib_rec,
   intros n,
   simp only,
-  rw [nat.fib_succ_succ, add_comm],
+  rw [nat.fib_add_two, add_comm],
   simp [finset.sum_fin_eq_sum_range, finset.sum_range_succ'],
 end