almost everywhere equality

[hoheinzollern]

Motivation for this change

Adds notations and generalization for almost everywhere equality and related lemmas.
This is part of the split of PR #1506

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• 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 preferentially merged 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]

In the interest of PR #1506 , I think that it is fine to merge (ae_eqe_mul2l is almost a duplicate, we may want to produce the theory for \bar R functions but we will come back soon to this topic anyway (@jmmarulang, @hoheinzollern)).

[hoheinzollern]

Oops, mistake when force pushing

[hoheinzollern]

I think this PR is almost ready for merging, and should be merged before #1606
One thing to note in this PR: the new notation \forall x ae mu, P x overlaps with the already available {ae mu, P}.
The first looks a bit more general, but in practice P is forced to be a forall quantified statement, making them equivalent.
I would argue for keeping only one, following the principle of least surprise (two notations for essentially the same thing).
What do you say @affeldt-aist @CohenCyril @proux01 @t6s ?

Edit: I swapped notations in my original comment.

[t6s]

I have a similar feeling about \near and {near , but not understood why these two are kept. I want to know a pointer to some previous discussion if any.

[affeldt-aist]

I have a similar feeling about \near and {near , but not understood why these two are kept. I want to know a pointer to some previous discussion if any.

I was about the make the same comment about near notations. There are sometimes two ways to write the same thing but Coq will actually print one of them so it will feel better to remove the one that is not printed by default. If you have a concrete example in mind we could try a PR trying to remove a notation to see the potential gain more clearly.

[hoheinzollern]

I added a commit that removes the duplicated notation, and again a similar one on PR #1606 that removes its usage on the theory of essential supremum.

[CohenCyril]

I added a commit that removes the duplicated notation, and again a similar one on PR #1606 that removes its usage on the theory of essential supremum.

This is not a duplication, please do not remove it...

The purpose is the same as the \in notation, most of the time one can write \forall x \near F, P x, but sometimes one has a definition of the form Q := forall x, P x and the only way to relativise the definition is to write {near F, Q}.

It should be documented that the priority should be given to the \forall x \near ... notation, since it is way more readable, and the {near F, ...} is dedicated to relativisation.

[affeldt-aist]

The purpose is the same as the \in notation, most of the time one can write \forall x \near F, P x,

You mean "the same as the \near notation" or are you thinking of \forall x \in F, P x?
In other words, are you thinking of having whenever possible \forall x \foo F, P x
(with foo = {in, near, ae, whatnot}) to help uniformizing the library?

[CohenCyril]

The purpose is the same as the \in notation, most of the time one can write \forall x \near F, P x,

You mean "the same as the \near notation" or are you thinking of \forall x \in F, P x? In other words, are you thinking of having whenever possible \forall x \foo F, P x (with foo = {in, near, ae, whatnot}) to help uniformizing the library?

I originally meant the "same as the {in } vs \in notations": you can write either of forall x, x \in A -> P x and {in A, forall x, P x}, and the latter was designed to relativise universally quantified definitions. I reused the same trick for "locally", "near" and "ae", but the basic principle is the same.

But indeed we could also introduce \forall x \in A in mathcomp it would avoid the repeat of the bound variable.
Moreover I still dream of getting rid of the backslash before forall.

[hoheinzollern]

OK, I understand the reasoning, thanks for the explanations. My main concern is that the notation is not stable and one (especially newcomers) may be surprised when they see something like this:

Section test_notation.
Context d (T : measurableType d) (R : realType) (P : T -> Prop) (mu : measure T R).

Check \forall x \ae mu, P x.
(* 1: Prints: \forall x \ae mu, P x : Prop *)
Check {ae mu, forall x, P x}.
(* 2: Prints: \forall x \ae mu, P x : Prop *)
Definition Q := forall x, P x.
Check {ae mu, Q}.
(* 3: Prints: {ae mu, Q} : Prop *)

End test_notation.

So test nr. 2 uses one notation and prints the other, which is undesirable. From a quick grep of the use of {ae, all of its instances are non-relativised statements (i.e. they contain an explicit forall inside). Perhaps those should use the \forall x \ae mu notation, or else the statements should be relativised. We should have a proper explanation for this and be consistent in the use of notation. If you agree, then I'll keep both notations, add an explanation in the headers, and then (perhaps separately) align all previous instances of {ae.

More long term, having an uniform {ae, near, in, etc notation with \forall equivalents seems very desirable.

[CohenCyril]

On the one hand, non "stable" notations are pervasive in mathcomp, starting with m.+1 <= n. And it is built-in in notations that what is printed is often not what one wrote (e.g. map f s gets rendered [seq f x | x <- s]). The printed notation should also be the canonical way to display / input something (at least when no additional type-inference information is needed), so it somehow improves discoverability that notations input in the "wrong" way get printed another way.
On the other hand it is confusing for users, in the absence of in-line documentation. I think this should be added to the list of meta-data that we must be able to link with a notation: all alternative notations and their human readable documentation.

[affeldt-aist]

The example of map f s reminds me of the last entry in the FAQ of MathComp-Analysis about the image notation:
https://github.com/math-comp/analysis/wiki/FAQ

Shall we expand a bit this FAQ entry too then?

[affeldt-aist]

I have adjusted the FAQ entry for image in MathComp-Analysis and added one in MathComp:

https://github.com/math-comp/math-comp/wiki/FAQ

https://github.com/math-comp/analysis/wiki/FAQ

[t6s]

Suggestions:

• In mathcomp wiki, add "Why does image f s prints as [seq f x | x in s]?" (in the same QA entry as that for map)
• In analysis wiki, note that image associated with @` is from classical_sets, and different from fintype.image

[affeldt-aist]

DONE. By the way, @t6s you don't have the rights to edit the wiki?

[affeldt-aist]

Is it ok to merge? I think that none of us qualifies as an non-conflicting reviewer ^_^ but we did add documentation pieces where appropriate going beyond the scope of the PR.

[t6s]

DONE. By the way, @t6s you don't have the rights to edit the wiki?

I suspect not. I could not find an edit button.