## Stream: new members

### Topic: Course-of-values recursion

#### Adrián Doña Mateo (Oct 07 2020 at 23:44):

Hi! I was trying to wrap my head around course-of-values recursion in lean by inspecting nat.below and nat.brec_on. I noticed that nat.below generates a lot of useless pprod and punit:

variable C : ℕ → Type

#reduce nat.below C 0 -- punit
#reduce nat.below C 1 -- pprod (pprod (C 0) punit) punit
#reduce nat.below C 2 -- pprod (pprod (C 1) (pprod (C 0) punit) punit)) punit


In fact, I wrote my own version of these functions without using so many generating so many pprod:

universe u

def below (C : ℕ → Sort u) (n : ℕ) : Sort (max 1 u) :=
nat.rec_on n punit (λ n ih, pprod (C n) ih)

def brec_on (C : ℕ → Sort u) (n : ℕ) (F : Π n, below C n → C n) : C n :=
pprod.fst (@nat.rec
(λ n, pprod (C n) (below C n))
⟨F 0 punit.star, punit.star⟩
(λ n ih, ⟨F n.succ ih, ih⟩)
n)

#reduce below C 0 -- punit
#reduce below C 1 -- pprod (C 0) punit
#reduce below C 2 -- pprod (C 1) (pprod (C 0) punit)


My question is: why is the built-in implementation like this? Are these extra pprod and punit needed?

#### Mario Carneiro (Oct 08 2020 at 01:25):

It's because it was written by generic code that can handle many arguments to the constructors:

inductive treee
| niil : treee
| coons : treee → treee → treee

example (C T1 T2) : treee.below C (treee.coons T1 T2) = (
pprod (pprod (C T1) (treee.below C T1)) $pprod (pprod (C T2) (treee.below C T2))$
punit)


#### Adrián Doña Mateo (Oct 08 2020 at 09:11):

Oh, I see. Thank you very much!

Last updated: May 14 2021 at 22:15 UTC