abstractions in proof assistants

Stream: general

[Rob Lewis]

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]

Does Eric's paper on scalar towers and the algebra typeclass infrastructure count?

[Rob Lewis]

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]

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]

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]

Oh, uniform spaces are a great example of this! Thanks!

[Rob Lewis]

As are the high powered integrals, although that's a story I know less about.

[Heather Macbeth]

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]

Does the use of order theory / lattices everywhere count?

[Heather Macbeth]

Yes -- for a specific example, perhaps the "Galois connection" idea

[Rob Lewis]

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]

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]

I think Johannes was the one making a big push for Galois connections.

[Patrick Massot]

Filters are really in a league of their own in this category.

[Patrick Massot]

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]

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]

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]

I thought of global fields, but I don't know if those are used outside proof assistants

[Alex J. Best]

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]

Exactly, we use the real world model, contrasting with computer algebra systems or anything using lists.

[Kevin Buzzard]

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]

Maybe docs#power_basis counts? Normally you'd write "suppose the field K is equal to $\mathbb{Q}(\alpha)$" instead of "suppose K has a basis over $\mathbb{Q}$ of the form $1, \alpha, \alpha^2, ...$.

[Reid Barton]

How about inductive types/propositions