Printing specialized notations

[zstone1]

Notations like {within A, continuous f} that specialize a common one (E.G. continuous f) don't print correctly. For a full list,

{within A, continuous f} prints as continuous f { uniform A , F --> f } prints as F --> f { uniform , F --> f } prints as F --> f { ptws , F --> f } prints as F --> f { 'uniform' A , F --> f } prints as F --> f

This is particularly unpleasant when proving facts like { uniform , F --> f } -> { ptws , F --> f } that print as , F --> f -> , F --> f

[affeldt-aist]

This commit https://github.com/math-comp/analysis/pull/752/commits/b4230f9a0d02c068f3c457c0eed74ac6dd988c9b might be a solution for the case {within A, continuous f}. Can you confirm? (I used the lemma itv_continuous_inj_le in realfun.v for testing but a quick look at other lemmas seems to indicate that it works.)

[zstone1]

Yeah, I'm seeing it work well. There are a couple interesting consequences of this approach:

1. If (f : subspace A -> T) in the first place, then continuous f and {within A, continuous f} print differently. The first uses (Phantom (subspace_filteredType A) x)) and the second uses Phantom (subspace A) x. You can see in

   Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) :
   {within A, continuous f} -> continuous (f : subspace A -> subspace B).
   Proof.
   move=> /=.

   after simplifications they are identical. Perhaps that's fine, or even desirable?

2. This avoids Coq ever having to unify f : T -> U and f : subspace A -> U. I was having problems defining mixins for continuity because of this. My naive attempt was

   IsContinuous {T U : topologicalTypes} (f : T -> U) { cts : continuous f}

   And then mix in into IsFun as

   ContinuousFun {T U : topologicalTypes} A B = { f of IsFun T U A B f & IsContinuous (subspace A) U f}

   This compiled, but I couldn't use it in practice. Coq (or HB?) couldn't determine that f : subspace A -> U and f : T -> U were really the same thing. The notation may sidestep the issue entirely.

[affeldt-aist]

Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) :
  {within A, continuous f} -> continuous (f : subspace A -> subspace B).
Proof.
move=> /=.

after simplifications they are identical. Perhaps that's fine, or even desirable?

I am not sure. On the one hand I would say that it is ok because it seems uncommon to me to rely on the stability of an explicit type constraint and because favoring one notation over the other should lead to a more uniform presentation of definitions and lemmas. On the other hand, they look identical but that may be misleading because exact does not conclude the proof...

[CohenCyril]

after simplifications they are identical. Perhaps that's fine, or even desirable?

I think it's better than before, but not ideal. Maybe we should have {witin A >-> B, continuous f} to specify the target subspace as well?

[CohenCyril]

(and by the way, it feels a bit weird to restrict ourselves to subspace topologies, maybe we could generalize the notation to support both subspace topologies and arbitrary topologies, just some thoughs)

[zstone1]

There are a lot of places where this notation will be used, and a lot of different use cases and requirements we've encountered. So I'd like to start by just outlining the desirable features of any new notations here. Please add any I've missed.

1. Working with single topologies Sometimes we have a space T: topologicalType, but only want to consider it only under a different topology. An example is intermediate value theorem, where f : R -> R , but we only care about subspace [a,b]. Another possible example is using the Sogenfrey line to define "right continuity", where we just don't care about left limits of distributions.

   • It should be minimally invasive to specify which topology we want.
   • We should be able to easily check the topology during a proof
   • It needs to be optional, so if there is only one "obvious" topology we don't need to declare it

2. Working with multiple topologies This problem occurs when you need two topologies on the same set. An example of this is Ascoli's theorem, relating pointwise convergence to uniform convergence.

   • We need to be able to (visually) distinguish between statements like (F --> f) in both topologies during a proof.

3. Beyond continuity We will need to distinguish between topologies for lots of properties, not just convergence and continuity. For example, differentiability in a certain topology.

   • We should have an approach that will work generically across predicates

[CohenCyril]

The solution I have had in mind for a long time is "two-way displays". Today displays are an additional parameter that we add to structures (e.g. ordered types or measurable types) that we use to decide which notation is to be used (hence the name "display"). The design pattern to make them also available to the elaborator to decide which instance to use (that's why I call it "two-way") is too complicated to handle by hand. It would be a nice addition to HB though.

PS: Also it is not yet implemented because, thanks to coq-elpi, there might be better design patterns than before to get them, but I didn't have a chance to test how they scale to mathcomp...