Apply function N times

Stream: Is there code for X?

[Pedro Minicz]

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]

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]

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

[Jalex Stark]

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

[Jalex Stark]

i think this is notation for iterate

[Pedro Minicz]

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

[Kevin Buzzard]

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]

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]

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]

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

[Pedro Minicz]

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]

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]

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]

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

[Pedro Minicz]

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

[Pedro Minicz]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kyle Miller]

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]

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

[Pedro Minicz]

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