Nat.repeat vs Nat.iterate

Stream: mathlib4

[Yuyang Zhao]

Why do we have both docs#Nat.repeat and docs#Nat.iterate ?

[Eric Wieser]

It looks like Mathlib/Init/Data/Nat/Lemmas.lean is an ad-hoc port, which is probably why it has left this mess behind

[Ruben Van de Velde]

No, we already had both in lean 3 core

[Ruben Van de Velde]

Oh, but docs3#nat.repeat and docs#Nat.repeat don't match

[Ruben Van de Velde]

The new repeat was probably added with no concern for what existed in mathlib 3. Maybe it's worth filling an issue about

[Eric Wieser]

Eric Wieser said:

It looks like Mathlib/Init/Data/Nat/Lemmas.lean is an ad-hoc port

I've started a re-port at #5782

[Eric Wieser]

This now gives a panic‽

[Eric Wieser]

Ran into this again today. Should we delete docs#Nat.iterate, or should we file a bug against core to restore the old meaning of repeat?

[Yaël Dillies]

I have a slight preference for Nat.repeat since it means repeat f n.succ a is defeq to f _.

[Mario Carneiro]

The other definition is tail recursive though, which is important

[Mario Carneiro]

we can fix that using a csimp lemma though

[Eric Rodriguez]

does Lean have TCO?

[Yury G. Kudryashov]

There is a @[csimp] for Nat.repeat in the core.

[Yury G. Kudryashov]

And repeatTR is defined the same way as Nat.iterate.

[Yury G. Kudryashov]

I like the name iterate but I'm OK with migrating to repeat.

[Yaël Dillies]

I think iterate is a better name mathematically.

[Yury G. Kudryashov]

OTOH, we can redefine Nat.iterate to be as Nat.repeat.

[Yury G. Kudryashov]

And move some lemmas about it (in the Nat.repeat spelling) to Std4.

[Jz Pan]

Sorry to ping this thread again...

Yury G. Kudryashov said:

OTOH, we can redefine Nat.iterate to be as Nat.repeat.

msybe just abbrev Nat.iterate to Nat.repeat.

There is only one difference of them: Nat.iterate also works for Prop. Do we have such use case?