geometric group theory

Stream: LftCM22

[Jim Fowler]

As a first project for myself, I would like to turn groups into metric_spaces via the word metric.

[Jim Fowler]

An initial attempt is at
https://github.com/kisonecat/word-metric/blob/main/src/word_metric.lean

[Jim Fowler]

But there are various things I do not understand: in https://github.com/kisonecat/word-metric/blob/main/src/word_metric.lean#L12-L30 I define enat' := with_top nat to avoid using part_enat, but surely there is a better way to tell Lean that enat' is well-ordered.

[Jim Fowler]

Also emetric_spaces use ennreal but all the code I wrote using with_top nat, so it would be nice if there were a not too painful way to wrap these functions to translate enat to ennreal.

[Jim Fowler]

And I am doing a lot of terrible things with unfold.

[Oliver Nash]

This is great, thanks for doing it! With regard to the enat pain, IIUC @Yury G. Kudryashov is currently in the process of carrying out a refactor that should resolve your issues.

[Oliver Nash]

See e.g., https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/enat.20pain/near/287893054

[Oliver Nash]

(Judging from #15245 this refactor is currently underway.)

[Yury G. Kudryashov]

@Laurent Bartholdi is also interested in this metric.

[Yury G. Kudryashov]

I'm going to add enat := with_top nat with basic lemmas in the next few days.