draft: separating pointed out of topological

[zstone1]

Motivation for this change

as mentioned in the zulip, I've been having issues with pointedness being required on topology, and the interaction with weak subspaces/weak topologies.

I have a variation of the subspace problem related to having Pointed be a requirement on Topological. I know this has come up before. But it seems fairly solvable in mathcomp 2. I have forgotten if there's a good reason to require Pointed. But I'm definitely finding good reason to separate them. I volunteer to go through and figure out which lemmas do/don't need it.

... Only problem is, weak_topologicalType needs a Pointed, which causes a bit of havoc. So A has to be nonempty, which causes one set of issues. But even if we know A is non-empty one must construct the PointedType directly. It's doable (I do it in cantor.v), but verbose and terrible. It's also dangerous because it's badly non-canonical, and exposing these types in lemma statements risks lots of weird incompatibilities with other people building different instances.

It came up again for me trying to define the space of continuous functions from sets A -> B as inheriting the product/uniform/compact-open topology from X -> Y via the weak topology.

So I'm experimenting with separating things into topological and ptopological. We rarely need the pointedness. Pretty much only when computing explicit convergence, such as in complete spaces. And once we're into normedtype.v we can safely assume it. This also sidesteps the issues with rings by just requiring ptopological when needed, which is only once!

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[zstone1]

@CohenCyril @affeldt-aist

This is both a breaking change, and a restructuring of the hierarchy for topology stuff. However, by the time topology and lmodule merge in normedtype.v, the change is invisible because the structurea are pointed anyway.

This is a significant simplification in defining topological spaces over potentially-empty sets, though. So I'm hoping this approach works for you. The only alternative I can think of is adding structures for non-empty sets, which seems like it just propagates the problem instead of solving it.

If this approach works for you guys, I'll clean it up and undraft it.

[CohenCyril]

Nice! I'm totally in favour of this new structure, but I would still encourage to preserve backward compat.
We could put the pointed structures in a module that we export by default with a warning making explicit that one should explicitly use Pointed.topologicalType or ptopologicalType (this could be done through notations if there is no module deprecation feature at hand CC @proux01), and indicate that the new default will be NonPointed.topologicalType in the future and we recommend people to import NonPointed (to prepare for the transition) when appropriate. In one or two revision we actually make NonPointed the default.

We should do the same for rings and probably a bunch of other things, so it would be nice to test the approach.

[CohenCyril]

The only alternative I can think of is adding structures for non-empty sets, which seems like it just propagates the problem instead of solving it.

I think we might have to do this anyhow at some point, but we can keep it for later.

[zstone1]

Yeah, backwards compatibility is usually worth the effort. This approach sounds feasible, but more than just the name of topologicalType changes. All the factories change too. I'll have to mess around with this a bit to see what my options are.

[proux01]

this could be done through notations if there is no module deprecation feature at hand CC @proux01)

Indeed, no module deprecation, we only have file deprecation since Coq 8.19 (prints a warning at require time).

[zstone1]

So I think the nicest approach to backwards compatability is to define

HB.structure Definition UnpointedFiltered (U : Type) := {T of Choice T & isFiltered U T}.
HB.structure Definition PointedFiltered (U : Type) := {T of Pointed T & isFiltered U T}.

and two scopes: unpointed_filters_scope and pointed_filters_scope. Then for each the structure we're edittingFiltered, Nbhs, Topological, etc, we put all their notations into the both scopes with the unpointed/pointed meanings. We also put the p variant notations into the unpointed_fileters_scope.

Defining separate modules with different definitions of Filtered is seems tougher because then there really are two hierarchies, and only one is ever in scope. So making T of Filtered U T backwards compatible seems pretty difficult. But just using the notation makes T of Filtered U T meaningless.

What would make this really seamless is an HB feature for multiple names for the same structure.

Module UnpointedFilters.
#[duplicate]
HB.structure Definition Filtered (U:Type) = { T of UnpointedFilter U T)
End UnpointedFilters.

which just replaces Filtered with UnpointedFilter whenever it sees that, and all the corresponding notations. Sadly, attempting anything like this right now produces a Structure topology_UnpointedFiltered contains the same mixins as Filtered error. When in fact that's exactly what I want. I suspect that without being able to give two names to the same structure/mixin, we can't ever be completely backwards compatible.

[proux01]

I guess you don't want to declare two times the same structure. Unfortunately, HB currently doesn't offer any mechanism for this kind of renaming, the best solution as of today is to do it manually with notations and deprecation like https://github.com/math-comp/math-comp/blob/b622c1b3cc30ff33bd394f9abdf2105742bf0b4d/mathcomp/field/falgebra.v#L97-L98

[CohenCyril]

@zstone1 I do not see the problem in doing something like:

Module Unpointed.
#[export] HB.structure Definition Filtered (U:Type) = {T of Choice T & isFiltered U T}.
Module Exports. HB.exports. End Exports.
End Unpointed.
Export Unpointed.Exports.

Module Pointed.
#[export] HB.structure Definition Filtered (U:Type) = {T of Pointed T & isFiltered U T}.
Module Exports. HB.exports. End Exports.
End Pointed.
Export Pointed.Exports.

#[deprecated(note="...", since="...")]
Notation filteredType := Pointed.Filtered.type.
Notation pointedFilteredType := Pointed.Filtered.type.
Notation unpointedFilteredType := Unpointed.Filtered.type.

[zstone1]

Using the modules is fine for defining the hierarchy. One annoying issue is it doesn't put nbhs into scope because there are no top-level structures with isFiltered. That's easily fixed by adding a JustFiltered structure, though it's a bit awkward. The more substantive complexity is that all the lemmas rely on Pointed.Filtered given the notation you defined above. So Unpointed.Filtered isn't really usable. That's what I'm working through.

My ideal end state is to have definitions for #[short(type = filteredType)] HB.structure Definition Filtered which is unpointed, and #[short(type = pfilteredType)] HB.structure Definition PointedFiltered which is pointed. No modules. Likewise for all the other bits in the hierarchy: Nbhs, Topology, Uniform, PseudoMetric. So I don't really want to rewrite everything to use unpointedFilteredType, unpointedTopologicalType, etc, only to change it back later. That's why having two scopes works nicely: one for the "ideal end state" and one for "legacy state". Then if a user opens the legacy scope, HB handles the backwards compatibility because a Pointed.Filtered is also an Unpointed.Filtered.

I'm updating my draft with the modules as you suggested, and to have the two notations for filteredType in different scopes.

[zstone1]

I'm encountering an HB issue I don't understand. I keep getting seeing

join_UnpointedPseudoMetric_PseudoMetric_between_topology_JustPseudoMetric_and_UnpointedUniform_Uniform

appear in the goals, which breaks all the simple applys from the hints and seems to interfere with Filter inference. Any idea what this is, and why it keeps appearing? I just pushed the branch with the issue, you'll see an explicit call to simple apply on line 4990, which should just be handled by a hint. But fails. Note that apply works fine.

[proux01]

Sorry, I don't have enough time to get a closer look but either:

• the joins are unwanted and we should understand where they come from
• or (more probably) hints should be generalized like https://github.com/math-comp/analysis/blob/64bf98c0e7f13493766bb0cc4937bd94591fadc8/theories/constructive_ereal.v#L2627C1-L2627C85

[zstone1]

Coming back to this after many months, I'm not sure how much effort with trying to make this backwards compatible. My recollection is

• Several proposed hierarchy builder features would help such as namespacing/bundling/aliasing
• Use aliasing/modules/notation trickery gets us pretty far. But I end up needing factories for both structures, which is pretty unpleasant. We end up duplicating stuff anyway, which defeats the purpose a bit.

My guess is that it's not gonna be worth the effort in the end since the intention was to see if there was a nice way that we could replicate for ring. But looking at this now, a solution that will scale to Ring will probably involve some hierarchy builder support anyway. I've posted #1312 for the non-backwards compat solution

[proux01]

I agree it's probably not worth putting too much effort in backward compatibility considering how painful it currently is.
Probably the most reasonnable solution is to just mention in changelog that users that actually needed the pointed version should rename to *Pointed or something like that?

[zstone1]

I've updated #1312 with more explicit instructions, and a bit of additional cleanup.

[zstone1]

With #1312 merged, this is now redundant.