Rob Lewis (Jan 27 2022 at 03:08):
The story of filters comes up quite a bit here, as an example of an abstraction that's not seen much in informal mathematics but is a huge help in formalization. The semilinear maps refactor could be seen as something similar. Are there other examples along these lines, in mathlib and/or other proof assistant libraries?
Yakov Pechersky (Jan 27 2022 at 03:14):
Does Eric's paper on scalar towers and the algebra typeclass infrastructure count?
Rob Lewis (Jan 27 2022 at 03:42):
I guess the fine-grained algebraic hierarchy could count, although it's not exactly what I had in mind. I was thinking more about definitions with at least some mathematical content that are used in the proof assistant to unify concepts that are "similar but different" informally.
Rob Lewis (Jan 27 2022 at 03:44):
E.g. filters unify a bunch of different kinds of limits, semilinear maps unify linear and conjugate-linear maps. In both cases we'd duplicate a lot of work without the generalization.
Yakov Pechersky (Jan 27 2022 at 04:12):
The use of finsupp as the underlying data model for polynomials, m_power_series, and other corners of the library? Manifolds with corners? High powered integrals and the rest of the measure library? Uniform spaces as the underlying data model to metric spaces?
Rob Lewis (Jan 27 2022 at 04:21):
Oh, uniform spaces are a great example of this! Thanks!
Rob Lewis (Jan 27 2022 at 04:22):
As are the high powered integrals, although that's a story I know less about.
Heather Macbeth (Jan 27 2022 at 04:24):
Yakov Pechersky said:
Manifolds with corners?
Good example ... to make it a bit less abstract, the fact that the whole differentiation library is written for differentiability wrt a (not necessarily open) set, which unifies the usual definition of differentiation with, among other things, the ad-hoc "left differentiable"/"right differentiable" from 1-variable calculus.
Bryan Gin-ge Chen (Jan 27 2022 at 04:36):
Does the use of order theory / lattices everywhere count?
Heather Macbeth (Jan 27 2022 at 04:38):
Yes -- for a specific example, perhaps the "Galois connection" idea
Rob Lewis (Jan 27 2022 at 04:41):
Another good one. I was actually thinking of that and wondering if it was written down anywhere. It's been pushed here for a long time, and I'm not sure if it has its origins from Isabelle via Johannes, Metamath via Mario, or...?
Yakov Pechersky (Jan 27 2022 at 04:51):
Another more basic, and likely pan theorem prover approach, is to use index types for collections as opposed to finite/countable/uncountable sets. I mean in products, sums, infima, etc.
Johan Commelin (Jan 27 2022 at 06:08):
I think Johannes was the one making a big push for Galois connections.
Patrick Massot (Jan 27 2022 at 08:36):
Filters are really in a league of their own in this category.
Patrick Massot (Jan 27 2022 at 08:37):
No mathematician would be surprised to learn that conjuguate-linear maps and linear maps can be unified, but almost no mathematician has heard of filters (except maybe very specific uses of ultrafilters)
Patrick Massot (Jan 27 2022 at 08:39):
The systematic use of Galois connection is of a different nature, but also nice. But I guess people who work in category-theory-heavy areas of maths wouldn't be surprised at all.
Patrick Massot (Jan 27 2022 at 08:39):
I don't see what Yakov means with "the use of finsupp as the underlying data model for polynomials, mv_power_series". I've never met another model of polynomials.
Ruben Van de Velde (Jan 27 2022 at 09:04):
I thought of global fields, but I don't know if those are used outside proof assistants
Alex J. Best (Jan 27 2022 at 09:04):
You could use lists as a data model for polynomials, or some sort of dictionary, interpreted right they could be equivalent to finsupp of course but are very different to how polynomials are represented in computer algebra systems
Patrick Massot (Jan 27 2022 at 09:11):
Exactly, we use the real world model, contrasting with computer algebra systems or anything using lists.
Kevin Buzzard (Jan 27 2022 at 09:20):
I have little to say beyond Patrick's post four above this one but I would also stress uniform spaces as something not taught at all in maths departments but which has made my understanding of completions much clearer. In fact for decades I've known that completeness is not a topological property (you can't talk about complete topological spaces) and yet that one can talk about complete topological groups (which are everywhere in nonarchimedean analysis) and I'd never understood why.
Anne Baanen (Jan 27 2022 at 10:58):
Maybe docs#power_basis counts? Normally you'd write "suppose the field K is equal to " instead of "suppose K has a basis over of the form .
Reid Barton (Jan 27 2022 at 11:11):
How about inductive types/propositions
Last updated: Aug 03 2023 at 10:10 UTC