refactor(group_theory/perm/basic): Redefine pow in terms of iterate

[YaelDillies]

Before, equiv.perm inherited the default pow. This changes it to a custom one using function.iterate.

Unfortunately, this changes the defeq as function.iterate is left recursive while npow_rec is right recursive. See Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60nat.2Eiterate.60.20vs.20.60stream.2Eiterate.60

---

Match leanprover-community/mathlib4#1388

[eric-wieser]

Can you do the same thing for function.End? module.End etc would be good too, but as those aren't "simpler" than perm they can wait to a follow-up.

[eric-wieser]

Did you consider changing the defeq of function.iterate or npow_rec? If such a change is seamless, it might be the easier solution...

[YaelDillies]

I remember lengthy discussions about why nat.iterate is tail-recursive. The answer is basically computation, so we're not really allowed to change it. Changing the defeq for npow_rec wouldn't help much. It would only have helped if it had been different in the first place.

[YaelDillies]

Done function.End. monoid_hom.End looks harder to get to because of import cycles (I would need algebra.hom.iterate, which imports group_theory.group_action.opposite which imports group_theory.group_action.defs).

[eric-wieser]

I remember lengthy discussions about why nat.iterate is tail-recursive.

That would be great to have in the commit message if yo ucan find it

Changing the defeq for npow_rec wouldn't help much.

Why not? Does too much stuff depend on the current definition?

[YaelDillies]

Yes exactly. Many proofs rely on the current defeq.

Here is the discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60nat.2Eiterate.60.20vs.20.60stream.2Eiterate.60

[YaelDillies]

Well, I guess not that many in the end 😄

[eric-wieser]

Changing the defeq for npow_rec wouldn't help much.

I realized on Zulip that it wouldn't help at all; this relies on function application commuting with recursors definitionally, which it does not.

[eric-wieser]

Done function.End. monoid_hom.End looks harder to get to because of import cycles (I would need algebra.hom.iterate, which imports group_theory.group_action.opposite which imports group_theory.group_action.defs).

Can we compromise on adding a TODO comment at the top of algebra.hom.iterate?

[urkud]

Note that if we go forward with this refactor, the monoid structure on category_theory.End (Group.of G) will be no longer defeq to monoid.End.monoid. I don't know whether we ever rely on this defeq.

[kim-em]

Could we abandon this as a mathlib3 PR, and make any desired changes after the port?

[YaelDillies]

I don't know. This is pretty short, self-contained and ready.

[eric-wieser]

Note that if we go forward with this refactor, the monoid structure on category_theory.End (Group.of G) will be no longer defeq to monoid.End.monoid. I don't know whether we ever rely on this defeq.

Is this fixable?

[YaelDillies]

Isn't the fix exactly what my TODO says, but for category_theory.End?
https://github.com/leanprover-community/mathlib/blob/64d3c00834e0c0364814b656ddceb77f04e5bd9d/src/algebra/hom/iterate.lean#L24-L26

[urkud]

No, it isn't. category_theory deals with non-necessarily concrete categories. Even if we're talking about concrete categories, we can't insert nat.iterate inside an unknown bundled homomorphism. The only way to fix it I can see is to add npow data to the category_theory.category signature. I don't think that we want to do this. IMHO, it's better to deal with a non-definitional equality in a visible argument than to have it in typeclass instances.