recursive

Stream: new members

[BANGJI HU]

import Mathlib.Data.Nat.Pairing
import Mathlib.Data.Nat.PartENat
import Mathlib.Data.Nat.Periodic

/- Recursive definition of the function f(n) -/
def f : ℕ → ℕ
| 0 => 0
| 1 => 1
| 2 => 5
| (n+3) => f (n+2) + 2 * f (n+1)
theorem f_eq_two_pow_n_plus_neg_one_pow_n (n : ℕ) :
  f n = 2^n + (-1)^n :=

[BANGJI HU]

failed to synthesize
Neg ℕ?

[Edward van de Meent]

indeed, -1 is not a natural number.

[Edward van de Meent]

also, the statement isn't true? f 0 = 0, while 2 ^ 0 + (-1) ^ 0 = 1 + 1 = 2

[BANGJI HU]

We define a function recursively for all positive integers $n$ by $f(1)=1$, $f(2)=5$, and for $n>2, f(n+1)=f(n)+2 f(n-1)$. Show that $f(n)=$ $2^{n}+(-1)^{n}$, using the second principle of mathematical induction.

[BANGJI HU]

any sugestion？

[Edward van de Meent]

defining f 0 = 2 does seem to fix things?

[Edward van de Meent]

also, (n+2) => f (n+1) + 2 * f n is good enough for defining the recursive step.

[Edward van de Meent]

as for proving the statement, it might be easier to prove the statement (f n : Int) = 2 ^ n + (-1) ^ n

[BANGJI HU]

import Mathlib.Data.Nat.Pairing
import Mathlib.Data.Nat.PartENat
import Mathlib.Data.Nat.Periodic

/- Recursive definition of the function f(n) -/
def f : ℕ → ℕ
| 0 => 2
| 1 => 1
| 2 => 5
| (n+2) => f (n+1) + 2 * f n
theorem f_eq_two_pow_n_plus_neg_one_pow_n (n : ℕ) :
  (f n : Int) = 2 ^ n + (-1) ^ n:=by
induction n with
 rw?

[Kevin Buzzard]

f : \N \to \R so -1 makes sense

[Alexander Hilbert]

You need second principle of mathematical induction.

example {f : ℕ → ℤ} (h0 : f 0 = 2) (h1 : f 1 = 1)
    (h : ∀ n ≥ 2, f n = f (n - 1) + 2 * f (n - 2)) :
    ∀ n, f n = 2 ^ n + (-1) ^ n := by
  intro n
  induction' n using Nat.strongInductionOn with n ihn
  sorry

[BANGJI HU]

import Mathlib.Data.Nat.Pairing
import Mathlib.Data.Nat.PartENat
import Mathlib.Data.Nat.Periodic
import Mathlib.Data.Int.SuccPred
/- Recursive definition of the function f(n) -/
example {f : ℕ → ℤ} (h0 : f 0 = 2) (h1 : f 1 = 1)
    (h : ∀ n ≥ 2, f n = f (n - 1) + 2 * f (n - 2)) :
    ∀ n, f n = 2 ^ n + (-1) ^ n := by
  intro n
  induction' n using Nat.strongInductionOn with n ihn
  cases n
  rw [h0]
  simp
  rw [← h1]

[BANGJI HU]

n>2?

[Ilmārs Cīrulis]

Here is my unfinished try.

import Mathlib

example {f : ℕ → ℤ} (h0 : f 0 = 2) (h1 : f 1 = 1)
    (h : ∀ n, f (n + 2) = f (n + 1) + 2 * f n) :
    ∀ n, f n = 2 ^ n + (-1) ^ n := by
  intro n
  induction' n using Nat.strongInductionOn with n ihn
  cases n
  . simp
    exact h0
  . rename_i n'
    cases n'
    . simp
      exact h1
    . rename_i n'
      have aux0: n' + 1 + 1 = n' + 2 := by linarith
      rw [aux0] at *
      rw [h]
      have aux1: n' + 1 < n' + 2 := by linarith
      apply ihn at aux1
      rw [aux1]
      have aux2: n' < n' + 2 := by linarith
      apply ihn at aux2
      rw [aux2]
      sorry

As can be seen from it, I'm beginner too. :sweat_smile:

[Ilmārs Cīrulis]

Anyway, I reached the state where one has to replace 2^(n+2) with 4*2^n etc and then simplify.

[Ilmārs Cīrulis]

Thanks to rw? command, I managed to finish it:

import Mathlib

example {f : ℕ → ℤ} (h0 : f 0 = 2) (h1 : f 1 = 1)
    (h : ∀ n, f (n + 2) = f (n + 1) + 2 * f n) :
    ∀ n, f n = 2 ^ n + (-1) ^ n := by
  intro n
  induction' n using Nat.strongInductionOn with n ihn
  cases n
  . simp
    exact h0
  . rename_i n'
    cases n'
    . simp
      exact h1
    . rename_i n'
      have aux0: n' + 1 + 1 = n' + 2 := by linarith
      rw [aux0] at *
      rw [h]
      have aux1: n' + 1 < n' + 2 := by linarith
      apply ihn at aux1
      rw [aux1]
      have aux2: n' < n' + 2 := by linarith
      apply ihn at aux2
      rw [aux2]
      clear aux0 aux1 aux2
      repeat rw [@npow_add]
      omega

[Kevin Buzzard]

import Mathlib

theorem foo {f : ℕ → ℤ} (h0 : f 0 = 2) (h1 : f 1 = 1)
    (h : ∀ n, f (n + 2) = f (n + 1) + 2 * f n) :
    ∀ n, f n = 2 ^ n + (-1) ^ n
| 0 => h0
| 1 => h1
| (n + 2) => by
  rw [h n, foo h0 h1 h (n + 1), foo h0 h1 h n]
  ring

[Alexandre Rademaker]

But @hand bob said above that f is not over Nat but "a function recursively for all positive integers"