## Stream: new members

### Topic: brec_on and below

#### Sayantan Majumdar (Apr 24 2020 at 18:46):

I was checking out the nat.below and nat.brec_on things and I was having some problems with a few proofs

def fib1 : ℕ → ℕ
| 0 := 1
| 1 := 1
| (n + 2) := fib1 (n + 1) + fib1 n

def fib2 : ℕ → ℕ :=
assume n : ℕ,
@nat.brec_on (λ n : ℕ, ℕ) n
(
assume n : ℕ,
assume h : nat.below (λ n : ℕ, ℕ) n,
(
λ (n : ℕ) (h : nat.below (λ n : ℕ, ℕ) n),
(@nat.cases_on (λ n : ℕ, nat.below (λ n : ℕ, ℕ) n → ℕ) n
(λ h : nat.below (λ n : ℕ, ℕ) 0, 1)
(
assume n : ℕ,
assume h : nat.below (λ n : ℕ, ℕ) (nat.succ n),
(@nat.cases_on (λ n : ℕ, nat.below (λ n : ℕ, ℕ) (nat.succ n) → ℕ) n
(λ h : nat.below (λ n : ℕ, ℕ) 1, 1)
(
assume n : ℕ,
assume h : nat.below (λ n : ℕ, ℕ) (nat.succ (nat.succ n)),
(h.fst.fst + h.fst.snd.fst.fst)
)) h
)) h
) n h
)

#reduce fib1 0
#reduce fib1 1
#reduce fib1 2
#reduce fib1 3
#reduce fib1 4
#reduce fib1 5
#reduce fib1 7

#reduce fib2 0
#reduce fib2 1
#reduce fib2 2
#reduce fib2 3
#reduce fib2 4
#reduce fib2 5
#reduce fib2 7

example : ∀ n : ℕ, fib1 n = fib2 n
| 0 := rfl
| 1 := rfl
| (n + 2) := sorry


#### Sayantan Majumdar (Apr 24 2020 at 18:46):

the (n + 2) := sorry part

Last updated: May 06 2021 at 20:13 UTC