[nmolinamounier]

Motivation for this change

Fixes #758 by adding extra display arguments to topologies, in the same way as orders in math-comp.

A new type filter_display is added in filter.v, and every topology is associated with an instance of filter_display, which can be used in notations for proper display.

Since it is common to define specific topologies in terms of more generic ones, with_fdisp d' T has the same topology as T, but with display d'.

This PR requires changing every single definition involving a filtered type to add a display argument, hence its very large footprint.

Notations have been intentionally left out of this PR for ease of review, and will be addressed by a future PR.

Checklist

• appended entries in the relevant sections of CHANGELOG_UNRELEASED.md
• Finish header docs

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are likely to be merged as they are into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

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

[affeldt-aist]

Suggested change

	move=> FF; split.
	move=> FF; split.

[affeldt-aist]

Suggested change

	Context (d : fdisp_t).
	Context (V : topologicalType d) (S : pred V) (U : subChoiceType S).
	Context d (V : topologicalType d) (S : pred V) (U : subChoiceType S).

[affeldt-aist]

Could you check for trailing spaces? (It looks your PR is introducing a few.)

Regarding the order of declaration of displays, it looks like you put all the displays at the beginning of the type signature. An alternative could be to put the display just before the first type that uses it. I have the vague memory that we already discussed this in a meeting. Do you remember @proux01 ?

Maybe we do not need to indicate the type of displays in type signatures. This is an advantage of using Context instead of Variable. Displays are already noisy enough in themselves and their type is often not informative.

[affeldt-aist]

Maybe we need to update the documentation. For example, d.-nbhs in filter.v, d.-cluster, etc. in compact.v, .-sub in subspace.v, .-open, etc. in topology_structure.v, also in connected.v, etc.

[affeldt-aist]

(If it is possible, maybe several PRs introducing the notations incrementally could help organizing the work (including documentation, changelog, and review).)

[affeldt-aist]

:> -> : ?

[affeldt-aist]

:> -> :?

[affeldt-aist]

Shouldn't :> be :? I think that :> is rather used for equalities, as in a = b :> T. (I only commented on two occurrences but there are more.)

[nmolinamounier]

Shouldn't :> be :? I think that :> is rather used for equalities, as in a = b :> T. (I only commented on two occurrences but there are more.)

They are different, : remains in the resulting term whereas :> is truly volatile, which is what we want for a parse-only notation. An alternative is to specify the desired type with an implicit argument, but that is the same as using :>.

[affeldt-aist]

Shouldn't :> be :? I think that :> is rather used for equalities, as in a = b :> T. (I only commented on two occurrences but there are more.)

They are different, : remains in the resulting term whereas :> is truly volatile, which is what we want for a parse-only notation. An alternative is to specify the desired type with an implicit argument, but that is the same as using :>.

Is this documented somewhere? If not, it is maybe worth at least a comment in the code, as I don't see this usage mentioned in eqtype.v. (But I might just have missed the documentation: I remember that Zachary already used it in this way.)

[nmolinamounier]

Shouldn't :> be :? I think that :> is rather used for equalities, as in a = b :> T. (I only commented on two occurrences but there are more.)

They are different, : remains in the resulting term whereas :> is truly volatile, which is what we want for a parse-only notation. An alternative is to specify the desired type with an implicit argument, but that is the same as using :>.

Is this documented somewhere? If not, it is maybe worth at least a comment in the code, as I don't see this usage mentioned in eqtype.v. (But I might just have missed the documentation: I remember that Zachary already used it in this way.)

Yes, here in the Rocq manual.

[affeldt-aist]

Ah, I didn't know. I assumed this was coming from ssreflect which always had a similar syntax for equality. No documentation issue then.

[affeldt-aist]

supremum_fdisp is maybe missing from the changelog

(prod_fdisp maybe also)

[affeldt-aist]

Regarding the order of declaration of displays, it looks like you put all the displays at the beginning of the type signature. An alternative could be to put the display just before the first type that uses it. I have the vague memory that we already discussed this in a meeting. Do you remember @proux01 ?

Here for example the displays are not put at the beginning of the type signature:

HB.mixin Record isPath {d} {i : bpTopologicalType d} 
    {d'} {T : topologicalType d'} (x y : T) (f : i -> T) 
    & isContinuous d i d' T f := {

(other occurrences in landau.v)

[nmolinamounier]

You're looking at a recent commit, I'm changing them to be before the relevant type because that's what mathcomp does for orders.

[nmolinamounier]

I am soon going to rename fdisp_t to filter_display, unless anyone has a better suggestion. Additionally, I'll use the following rule of thumb to determine when and how to declare a new display:

1. If a type/type former has a canonical/natural topology (e.g. product, sigT, nat, bool), then it has default display. Custom displays are reserved for type aliases.
2. If a type alias has a custom display, the display takes the same arguments as the type alias.