pattern for rewriting Boolean (in)equalities

[affeldt-aist]

Motivation for this change

These patterns were introduced by @CohenCyril in mathcomp-analysis and proved useful @thery .
They do not seem to be that useful in mathcomp itself but they could benefit to other users.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

[ybertot]

LGTM, but

• It feels that users will rarely use these, because it takes too much remembering that these pattern exist.
• This suggests that the "RHS" notation should be usable to denote the right-hand side of equalities and inequalities alike. How would that be possible? It seems that one would need to be able to define "multi-patterns" (disjunctions of patterns), in the same way that we already define multi-rules. On the surface, it seems an easy thing to define, but digging more deeply, it feels that providing this together with extensibility (as in extending multi-rules) is quite hard actually.

[ybertot]

Another issue I have with this PR is that it corrects some spacing problems which are independent from the subject in the title. It is too bad that these corrections will be forgotten if this PR is not incorporated.

[CohenCyril]

• This suggests that the "RHS" notation should be usable to denote the right-hand side of equalities and inequalities alike. How would that be possible?

I tried at some point and failed: this was too ambiguous, e.g. for which r would RHS match y in r x y?
Even if we narrow r down to a few symbols (e.g. through some for of table, e.g. canonical projections),
many goals containing _ <= _ also contain _ = _, if we are not more precise than just RHS how do we specify?
The ad-hoc solution here is to tailor customized patterns for the most frequently used...

Like many things in ssr most people will not use it until they really feel the need, and that's when they must be able find them through documentation. Maybe we should rewrite a mathcomp local addentum to https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html for that purpose?

[affeldt-aist]

The topic was discussed during the last mathcomp-dev meeting, see https://github.com/math-comp/math-comp/wiki/Minutes-April-06-2022.
After the meeting @gares figured out a way based on @CohenCyril 's idea:

Notation LEFT symb := (X in symb X _)%pattern.

with the following comment: "one still needs to put in %pattern scope some notations for the usual infix symbols."

Should it come as a replacement or an addition?

[CohenCyril]

Should it come as a replacement or an addition?

I would vote for "as an addition"

[gares]

I guess one needs to make the scope explicit around symb as well. And test it a little, since I did not do it very carefully.

[thery]

a pity we can't write [LEFT <=] and [LEFT =]

[thery]

should it not be eqbLHS?

[affeldt-aist]

for the sake of consistency indeed, but eqLHS is free and shorter; if we enforce consistency to have eqbLHS then we could think of using eqLHS instead of LHS and that does not seem a good idea given than it is used very often

[thery]

my poor brain prefers consistency 😉

[thery]

I would prefer eqLHS to be a synonymous of LHS and is there a need for leqLHS and ltnLHS or is this captured by leLHS and ltLHS?

[affeldt-aist]

The last push force added leqLHS, etc. They seem quite useful. As for adding eqLHS as a synonymous of LHS, it looks like it better be an addition to Coq's ssrmatching.v. Should we PR this to Coq?

[gares]

I think you can if you add these notations in the pattern scope (not as infix, just as atoms).

[thery]

I am pretty bad at notation I tried to add
Notation "LEFT <=" := (X in X <= _)%pattern (at level 10).
and it broke everything 🙈

[gares]

I'm not on my pc

Notation "<=" := leq : symb_scope.
Notation "LEFT f" := (X in f%symb X _)%pattern.

[affeldt-aist]

I would vote for "as an addition"

Then we can maybe merge this one for now and issue for the more general pattern (it might require some testing).

[thery]

I have tried

Notation "<=" := leq : symb_scope.
Delimit Scope symb_scope with symb.
Notation "'LEFT' f" := (X in f%symb X _)%pattern (at level 10).
Goal 1 <= 2 .

and I get a
Unknown interpretation for notation "<=".
for the <= in the goal.

[CohenCyril]

I think we need to create a new nonterminal (a.k.a. custom entry) for that otherwise we will screw up the main parser.

[thery]

ok this works

Declare Custom Entry symb.
Notation "<=" := leq (in custom symb at level 0).
Notation "'LEFT' f" := (X in f X _)%pattern (f in custom symb, at level 10).
Goal 1 <= 2 .
rewrite -[LEFT <=](addn1).