Course-of-values recursion

Stream: new members

[Adrián Doña Mateo]

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]

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]

Oh, I see. Thank you very much!