Zulip Chat Archive

Stream: new members

Topic: brec_on and below


view this post on Zulip 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

view this post on Zulip Sayantan Majumdar (Apr 24 2020 at 18:46):

the (n + 2) := sorry part


Last updated: May 06 2021 at 20:13 UTC