Cauchy sequences in metric spaces

[lowasser]

Gives us the ability to go back and forth between Cauchy sequences and Cauchy approximations, and their limits.

Naturally, this is going to be necessary for a lot of analysis built on series and sequences.

Depends on #1345.

[fredrik-bakke]

I'm not a fan of the prevalent use of let bindings here. One thing is to use them for the monad syntax we have been discussing, but here you're using them to formalize lemmas and to create aliases.

[lowasser]

I guess my understanding of the objective of the stylistic practice here is to encourage pulling out reusable lemmas and functions rather than reinventing logic repeatedly. I see and buy that, though as I work in this project I am becoming less convinced over time that that scales all that well. Many individual steps to proving theorems feel so narrow and specific that generating even a name for them as a lemma feels oppressively difficult. You can try to make them more general and get a better name as a result, but the work to apply the general case to the specific need often feels like as least as much work as the effort to prove the specific case from scratch without the lemma.

But separately, many of the the aliases in this PR give an easier-to-follow, shorter name to what would otherwise be a long function call -- let xm = map-cauchy-sequence-cauchy-approximation-Metric-Space M x m, for example, a case in which there aren't any lemmas or functions to pull out because it's already maximally reduced. Such aliases make the logic easier for me, at least, to follow and (especially) debug; they make the proof more closely resemble anything I'd write as a "traditional" proof in English. The case of let (ε'⁺@(ε' , _) , 2ε'<ε) = bound-double-le-ℚ⁺ ε⁺ could be done as ind or rec on the dependent pair type, but -- as with the do syntax we've discussed and that I think I've successfully convinced you is a positive development -- that'd result in gratuitously deep nesting that additionally separates the newly defined variables visually from their semantic relationship to ε⁺ (since ind-Sigma and rec-Sigma put the dependent pair after the entire lambda which uses the components).

I can find more steps to combine into more general lemmas and functions, and I see some examples in this PR where that shouldn't be too difficult. Combining map-cauchy-sequence-Metric-Space and modulus-of-convergence-cauchy-sequence-Metric-Space is a good example, though I'd have to think a bit about what to name that new function. But for many of the more alias-style usages in the lets, inlining feels as though it accomplishes nothing more than making the result harder to comprehend. I certainly claim that I could not have figured out how to write this without at least using the let versions as an intermediate step before inlining things.

[EgbertRijke]

I understand your sentiment, and I have seen from working with students that sensibly breaking down code into reusable lemmas is one of the hardest things for newcomers to learn.

On the other hand, it is a skill that is possible to learn, and I don't really believe in your scaling argument. In fact, I think the opposite is true. There are parts of the library that have been coded in less refactorable style, and in practice it has just been about impossible to do anything with it. Refactoring that code is an insurmountable task, probably worse that just formalizing it from scratch all anew. As a results, these parts of the code have been sitting in the library with low maintenance. Furthermore, these are often the parts of the library that take up the most time of the type checker. So I am a firm believer in breaking down everything into small, sensible, reusable lemmas.

On the other hand, if you have the sense that it hampers your progress, I'd rather have that you formalize in your preferred style. According to the rising sea model, eventually the code written in small reusable lemmas will catch up and these parts of the library will also be nicely refactored.

[lowasser]

I am willing to go ahead and trust that experience for the lemmas aspect; that comment has successfully moved me there.
I'm not sure I'm clear to what extent what you said just applies to the aliasing case, where I don't see a way to break out any lemma from e.g. let xm = map-cauchy-sequence-cauchy-approximation-Metric-Space M x m.

[EgbertRijke]

I think it is fine. I use let expressions too on rare occasions.

I also thought that I should add that I don't mean to say that the code you write, or any code from anyone that gets rewritten including my own, is bad code. It's normal that things get rewritten, and it's normal that after having formalized something once, later a better/new interesting approach comes along. We're not setting our formalization in stone, it changes all the time.

[fredrik-bakke]

It seems that a conclusion was reached on the use of let bindings here, is that correct? If so, we can move ahead and merge this PR I believe

[lowasser]

I believe I've eliminated all the let bindings here that seem reasonable: what remains are aliases for concision and pair decompositions.