generalize setUitv1, setU1itv, setDitv1{l,r}, and add similar lemmas

[t6s]

Motivation for this change

This PR does

• generalize setUitv1, setU1itv, setDitv1{l,r},
• add similar lemmas such as setUitv2, setDitv2, setDitvoo, etc.

#1848 (comment)

I am not confident about the names of two added lemmas: setDcitvy and setDcitvNy,
and want reviewers to suggest better ones if any.

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]

Since you have a doubt about the naming of setUitv2 and setDitv2,
what about setUitv_set2 and setDitv_set2?
It might make it clearer that the lemmas are about dealing with the (two) endpoints.

I observe that, when used, for example setU1itv, is mostly used to rewrite from
right to left and requires a boolean flag whose setting always requires a bit of
thought, which makes me wonder whether there isn't some improvement possible
in terms of usability, but I do not have any idea (but you already observed that issue
in he original PR).

Some lemmas that you add, specifically:

• setDitvoy
• setDitvNyo
• setDccitv
• setDcitvy
• setDcitvNy
  are not used in the PR. They are variations of two others,
  so that's almost enough a justification, but are they used
  in the original PR 1848?

[affeldt-aist]

One CI error is the following:

       > File "./reals/real_interval.v", line 61, characters 28-38:
       > Error: The reference ltrW_lteif was not found in the current environment.
       > Did you mean lt_leif?

Looking at MathComp's changelog, it looks like a MathComp 2.5.0 lemma.

[affeldt-aist]

And thanks for taking the time to extract these lemmas from the PR #1848, this helps a lot!

[affeldt-aist]

I am not confident about the names of two added lemmas: setDcitvy and setDcitvNy, and want reviewers to suggest better ones if any.

setDcitvy -> setD_cbnd_bndy

setDcitvNy -> setD_bndc_Nybnd

I think that we are using at several places the substring bnd when the interval bound is generalized.
That might look a bit long, but on the other hand setDcitvNy starts to become a bit unreadable
(I didn't spot the "c" on a first reading ^_^).

[t6s]

Thank you for reviewing!

Since you have a doubt about the naming of setUitv2 and setDitv2, what about setUitv_set2 and setDitv_set2? It might make it clearer that the lemmas are about dealing with the (two) endpoints.

Unlike setDcitvy and setDcitvNy, I am fine with setUitv2 and setDitv2. Have you found these names less clear? Then I do not hesitate to rename them to *_set2.

I observe that, when used, for example setU1itv, is mostly used to rewrite from right to left and requires a boolean flag whose setting always requires a bit of thought, which makes me wonder whether there isn't some improvement possible in terms of usability, but I do not have any idea (but you already observed that issue in he original PR).

One solution would be to introduce a "disjoint union" operator in classical_sets,
and use it to state the original version as a different lemmas.

Some lemmas that you add, specifically:

• setDitvoy
• setDitvNyo
• setDccitv
• setDcitvy
• setDcitvNy
  are not used in the PR. They are variations of two others,
  so that's almost enough a justification, but are they used
  in the original PR 1848?

I think some are used in PR 1848, but probably not all.
The others are indeed written down for symmetry and perfection.

Looking at MathComp's changelog, it looks like a MathComp 2.5.0 lemma.

I will fix this soon.

setDcitvy -> setD_cbnd_bndy
setDcitvNy -> setD_bndc_Nybnd

Thanks for suggestions. I will take these names.

[affeldt-aist]

Since you have a doubt about the naming of setUitv2 and setDitv2, what about setUitv_set2 and setDitv_set2? It might make it clearer that the lemmas are about dealing with the (two) endpoints.

Unlike setDcitvy and setDcitvNy, I am fine with setUitv2 and setDitv2. Have you found these names less clear? Then I do not hesitate to rename them to *_set2.

Sorry, I misread, but indeed I was bothered by the "2" suffix.
I think that the reason is that MathComp is using the "2" suffix in lemmas like:

lerN2: forall {R : porderedZmodType}, {mono -%R : x y /~ (x : R) <= (y : R)}

when some binary relation is involved. On the other hand, classical_sets.v
introduces set1 for singletons. So here since we are taking about a set with
two points, set2 looks clearer to me.

[t6s]

it has turned out that doing a disjoint union operator with a binary notation is not straightforward

Record disjoint_union {T : Type} (A B : set T) := { _ : [disjoint A & B] }.
Definition setЦ {T : Type} (A B : set T) (_ : disjoint_union A B) := A `|` B.
Coercion setЦ : disjoint_union >-> set.
Reserved Notation "A `Ц` B" (at level 52, left associativity).
Arguments setЦ {T}.
Notation "A `Ц` B" := (setЦ A B _) : classical_set_scope.

Section test.
Variables (T : Type) (A B : set T) (disjAB : [disjoint A & B]).
Let ab := Build_disjoint_union disjAB.
Check erefl : A `Ц` B = A `|` B.
Fail Lemma setЦC : A `Ц` B = B `Ц` A.
End test.