Zulip Chat Archive

Stream: new members

Topic: Course-of-values recursion

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

#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?

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

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