Stream: Is there code for X?

Topic: Apply function N times

Pedro Minicz (Jul 07 2020 at 19:38):

Is there a function with the type ℕ → (α → α) → α → α that applied the second argument to the third the amount of times given? Also, why does Lean call the induction principle of a given type rec, e.g. nat.rec, I'd expect rec to refer to the given recursor. Does Lean generate the recursor, if so, under which name?

Kevin Buzzard (Jul 07 2020 at 19:40):

There is, because I was told about it at Xena last Thursday. We ended up making an int one, which took an int and an equiv :-) I only half remember the name -- was it docs#nat.iterate ?

Kevin Buzzard (Jul 07 2020 at 19:41):

Aah, it's function.swap applied to nat.iterate :-)

Jalex Stark (Jul 07 2020 at 19:41):

variables (α : Type) (f : α → α) (n : ℕ)
#check f^[n]


Jalex Stark (Jul 07 2020 at 19:41):

i think this is notation for iterate

Pedro Minicz (Jul 07 2020 at 19:41):

Yes! There is also docs#nat.repeat, which is also cool.

Kevin Buzzard (Jul 07 2020 at 19:42):

I don't understand your question about nat.rec though. nat.rec is exactly what I thought computer scientists called the recursor for nat. Because Prop = Sort 0, the recursor can also be used as the induction principle.

Kyle Miller (Jul 07 2020 at 19:43):

It's interesting that nat.iterate has that argument order. If it were @Pedro Minicz's, then it would be the map from Lean's naturals to Church-encoded naturals.

Pedro Minicz (Jul 07 2020 at 19:43):

A distinction between the recursor and the induction principle is usually made (at least where I've read), Coq and HoTT book do that distinction at least.

Kevin Buzzard (Jul 07 2020 at 19:44):

But I think they have more elaborate set-ups with Prop.

Pedro Minicz (Jul 07 2020 at 19:44):

In book HoTT the recursor is the non-dependent version of the induction principle (and the induction principle is what Lean calls rec).

Kevin Buzzard (Jul 07 2020 at 19:45):

nat.rec : Π {C : ℕ → Sort u}, C 0 → (Π (n : ℕ), C n → C n.succ) → Π (n : ℕ), C n


I was taught as a mathematician that one defines things by recursion and proves them by induction. Induction is inherently dependent. Sort u is precisely Lean's way of saying "Type or Prop, I don't care".

Pedro Minicz (Jul 07 2020 at 19:45):

I believe Coq's Prop is about the same as Lean's. In book HoTT there is no impredicative universe, so the distinction between the induction principle and the recursor does not necessarily have to do with Sort.

Pedro Minicz (Jul 07 2020 at 19:47):

I'd expect Lean to generate a recursor of with the type ℕ → α → (α → α) → α for nat.

Pedro Minicz (Jul 07 2020 at 19:47):

Which, of course, is just an specialization of nat.rec.

Pedro Minicz (Jul 07 2020 at 19:49):

Just checked, I was mistaken, Coq does not make such distinction. I guess book HoTT just left an impression on me.

Kevin Buzzard (Jul 07 2020 at 19:49):

It seems to me that nat.rec is one function which covers everything. It would not surprise me at all if there were specialised versions which cover more specialised use cases.

Kevin Buzzard (Jul 07 2020 at 19:50):

I think that when one makes a new inductive type, Lean generates a constant for the type, a constant for each constructor, and then a constant for the recursor (aka the eliminator). An algorithm then generates a bunch of helper functions, but each of these have definitions which depend on these undefined constants.

Kevin Buzzard (Jul 07 2020 at 19:53):

inductive mynat
| zero : mynat
| succ : mynat → mynat

#print prefix mynat -- about 20 things

-- these have no definitions

#print mynat
#print mynat.zero
#print mynat.succ
#print mynat.rec

-- everything else has a definition

#print mynat.rec_on


All you need is mynat.rec and then you can make anything else you need by yourself.

Pedro Minicz (Jul 07 2020 at 20:25):

Indeed. Coq defines a few recursors because of its universes. I mistook the distinction that book HoTT makes for it.

Kyle Miller (Jul 07 2020 at 20:28):

Pedro Minicz said:

Which, of course, is just an specialization of nat.rec.

Working through this to understand it better, it looks like you get nat.repeat with reordered arguments. That's interesting.

def nat.repeat' : α → (ℕ → α → α) → ℕ → α := @nat.rec (λ n, α)


Pedro Minicz (Jul 07 2020 at 20:50):

Indeed. If you want to go deeper into lambda calculus you can also compare it to Church encoded natural numbers.

Pedro Minicz (Jul 07 2020 at 20:51):

What is described as the "recursor" on book HoTT is I believe always (almost) equivalent to the Church encoded version of the type.

Last updated: May 07 2021 at 19:12 UTC