Zulip Chat Archive

Stream: Is there code for X?

Topic: Apply function N times


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

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

view this post on Zulip Kevin Buzzard (Jul 07 2020 at 19:41):

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

view this post on Zulip Jalex Stark (Jul 07 2020 at 19:41):

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

view this post on Zulip Jalex Stark (Jul 07 2020 at 19:41):

i think this is notation for iterate

view this post on Zulip Pedro Minicz (Jul 07 2020 at 19:41):

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

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

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

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

view this post on Zulip Kevin Buzzard (Jul 07 2020 at 19:44):

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

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

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

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

view this post on Zulip Pedro Minicz (Jul 07 2020 at 19:47):

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

view this post on Zulip Pedro Minicz (Jul 07 2020 at 19:47):

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

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

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

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

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

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

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

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

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