Induction not from zero

Stream: new members

[Moti Ben-Ari]

I am trying to prove that the n'th Fibonacci number is less than (7/5)^n. Problems:

1. Is there a type positive that I can use instead of Nat? I could work around this by offseting by 1 but I don't like this.
2. For the recursive definition n=..., I get "failed to show termination".
3. For fib n < (7.0/5.0)^n,I get "failed to synthesize instance OfScientific".
4. Related to (1): can I do induction from 1 and not 0? I found Nat.le_induction, but I don't understand: To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction' and I can't find an example.

import Mathlib.Tactic
import Mathlib.Data.Real.Basic
def fib : Nat → Nat
  | 1 => 1
  | 2 => 1
  | n => fib (n - 1) + fib (n - 2)

#eval fib 12  -- Prints 144
#eval (7.0/5.0)^2 -- Prints 1.960000

theorem seven_fifths (n : Nat) :
    fib n < (7.0/5.0)^n := by
  induction' n with k ih
  · sorry
  · sorry
  done

[Ruben Van de Velde]

1. docs#PNat exists
2. | n + 2 => fib (n + 1) + fin n
3. What type should 7/5 be? Rational? Real?

[Kevin Buzzard]

Naturals start at 0 in Lean and your result is still true for 0; but mathlib already has docs#Nat.fib and I suspect that you would be better off using that rather than rolling your own.

[Eric Rodriguez]

The reason it allows you to write - is because there is a subtraction defined on the naturals, but it's truncating. Your definition at the moment reads "if 1 then 1, if 2 then 1, else fib (n - 1) + fib (n - 2)"; as 0 - 2 = 0 in this truncating division, the definition for n = 0 is an infinite loop.

[Moti Ben-Ari]

Thanks. I found mkRat and am using Nat.fib.

[Kevin Buzzard]

If you want rationals then (7/5 : \Q) will be fine, you don't need to get your hands dirty.

[Kevin Buzzard]

By the way, I suspect the result isn't true: doesn't the nth Fibonacci number grow approximately like (1.618...)^n?

[Kevin Buzzard]

Indeed by your own calculation fib 12 = 144 but (7/5)^12<144.

[Moti Ben-Ari]

Kevin Buzzard said:

By the way, I suspect the result isn't true: doesn't the nth Fibonacci number grow approximately like (1.618...)^n?

Sorry, it should be 7/4 = 1.75

[Chris Wong]

For examples, you can use GitHub code search on the mathlib4 repo, like this:
https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4+induction+using+Nat.le_induction&type=code

[Moti Ben-Ari]

Chris Wong said:

For examples, you can use GitHub code search on the mathlib4 repo, like this:
https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4+induction+using+Nat.le_induction&type=code

Thanks ... no Fibonacci theorems ... so far

[Chris Wong]

Kevin Buzzard said:

By the way, I suspect the result isn't true: doesn't the nth Fibonacci number grow approximately like (1.618...)^n?

I was going to ask why we don't have this in mathlib, but it turns out we do... docs#geom_gold_isSol_fibRec

[Kevin Buzzard]

It's docs#Real.coe_fib_eq I guess, although the docstring mentions "dependent equality" which will probably confuse a lot of people :-/

[Ruben Van de Velde]

Count me confused

[Yaël Dillies]

Is "dependent equality" just referring to the fact that there's a free variable in the equality?

[Yaël Dillies]

If so, almost all equalities stated in mathlib are dependent.

[Dan Velleman]

By the way, the theorem that the nth Fibonacci number is at most 2 ^ n is an example in both my book How To Prove It with Lean and also Heather Macbeth's book The Mechanics of Proof. In my book, the example is in Section 6.4. In Heather's, it is in Section 6.3, Example 6.3.3. Both of us use tactics in this example that are not standard Lean tactics. I use a tactic I called by_strong_induc, and Heather uses a tactic called two_step_induction.

Heather and I also both have custom tactics to deal with induction that doesn't start with 0. Heather's is called induction_from_starting_point. Mine is a version of induction that automatically detects if the goal has the form ∀ n ≥ k, ..., and if so it sets up the induction to start at k.

[Moti Ben-Ari]

Dan Velleman said:

Both of us use tactics in this example that are not standard Lean tactics. I use a tactic I called by_strong_induc, and Heather uses a tactic called two_step_induction.

In my opinion, it is not a good idea to use non-standard tactics, because the student will find it difficult to understand how to do such proofs with standard tactics. For example, Heather uses a tactic:

example (n : ℕ) : F n ≤ 2 ^ n := by
  two_step_induction n with k IH1 IH2

based on the definition of Nat.twoStepInduction. How do I start a proof of this theorem using a standard tactic?

[Mauricio Collares]

There's a section of the book hinting at the correct syntax, which in this case is induction' n using Nat.twoStepInduction with k IH1 IH2.

[Kevin Buzzard]

Whether or not it's appropriate to use non-standard tactics depends very much on the context.

If you want to prove this from first principles, another way is to state and prove the theorem which can be proved by usual induction tactic (which here is F n <= 2^n \and F (n+1) <= 2^(n+1) and then deduce the result from that.

[Ruben Van de Velde]

I personally don't think induction' should be used in new code, the unprimed version is much nicer

[Mauricio Collares]

Ruben Van de Velde said:

I personally don't think induction' should be used in new code, the unprimed version is much nicer

Good point. For reference, the syntax would be

  induction n using Nat.twoStepInduction with
  | H1 => sorry
  | H2 => sorry
  | H3 k IH1 IH2 => sorry

where the case names H1, H2 and H3 are defined by Nat.twoStepInduction.

[Michael Stoll]

docs#Nat.twoStepInduction
These names are bad, I think, H0, H1 and H (or so) would be better.

[Yaël Dillies]

zero, one, ind probably

[Dan Velleman]

Kevin Buzzard said:

Whether or not it's appropriate to use non-standard tactics depends very much on the context.

I agree. If your purpose is to teach Lean, then it's best to use standard tactics. If your purpose is to use Lean as a tool to teach proof writing, then I think nonstandard tactics are appropriate.

Note that Heather has an appendix on "Transitioning to mainstream Lean". I am planning to add such an appendix to How To Prove It with Lean as well.

[Heather Macbeth]

By the way, in addition to the $2^n$ Fibonacci bound, I have an exercise (end of section 6.3) proving decimal bounds similar to the OP's original question:

example : forall_sufficiently_large n : ℕ, (0.4:ℚ) * 1.6 ^ n < F n ∧ F n < (0.5:ℚ) * 1.7 ^ n := by sorry

[Heather Macbeth]

Unfortunately the Lean core issue lean4#2159 intersects with that question so the infoview prints weird output during part of the proof.

[Chris Wong]

Kevin Buzzard said:

It's docs#Real.coe_fib_eq I guess, although the docstring mentions "dependent equality" which will probably confuse a lot of people :-/

It seems strange to me that we have two versions, one of which is just funext of the the other. Is this pattern common?

[Moti Ben-Ari]

Ruben Van de Velde said:

I personally don't think induction' should be used in new code, the unprimed version is much nicer

Could someone please explain the difference between induction and induction' and when to use which one? MIL uses induction' exclusively (except for p. 130) and TPIN4 uses induction exclusively!

[Kevin Buzzard]

NNG uses induction' and calls it induction!

[Notification Bot]

Christian Merten has marked this topic as resolved.

[Notification Bot]

Christian Merten has marked this topic as unresolved.

[ZHAO Jiecheng]

Chris Wong said:

Kevin Buzzard said:

It's docs#Real.coe_fib_eq I guess, although the docstring mentions "dependent equality" which will probably confuse a lot of people :-/

It seems strange to me that we have two versions, one of which is just funext of the the other. Is this pattern common?

I guess it is quite common for some tactics are not smart enough and sometimes you have to prepare some theorems for them to eat although people may feel another one is just the same.