new factory for algebra of sets

[affeldt-aist]

Co-authored-by: @JeremyDubut
Co-authored-by: @AkihisaYamada

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

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

[affeldt-aist]

NB: The main issue is to find a better name instead of isAlgebraOfSetsD renamed

[affeldt-aist]

Despite the fact that symmetric difference is not yet exploited seriously, this PR already went through several eyes and since there is no disagreement we might as well merge it soon.

[affeldt-aist]

@t6s ping ?

[t6s]

Adding the symmetric difference will be useful, but the choice of laws looks a bit random. What about calling the symmetric difference "add?", ? being some appropriate letter for sets, and provide the ring laws? (mul = setI, opp = idfun)

[t6s]

setdiffA, setdiffC, set0diff, setdiff0, set1diff, setdiff1, setdiffBAC, etc. might be better? But I am not sure how to handle names like mul?Dl .

[affeldt-aist]

What about calling the symmetric difference "add?", ? being some appropriate letter for sets, and provide the ring laws? (mul = setI, opp = idfun)

what about setX for xor instead of sym_diff/add? sounds even more a propos

[affeldt-aist]

What about the last commit 9ef13c2 ?

sym_diff becomes setX for XOR (setX was not taken, the cartesian product is setM).
(It is true that add could be used instead of xor but setD is already taken by set difference...)
It also provides instantiations of commutative monoid and ring laws.

[t6s]

Looks good. The conflict with finset in the naming for direct products is fearsome, but I believe that that is already discussed when setM was introduced.

[t6s]

I cannot figure out how to approve this PR from the Android GitHub app.

[affeldt-aist]

Looks good. The conflict with finset in the naming for direct products is fearsome, but I believe that that is already discussed when setM was introduced.

Let us ping @CohenCyril on that.

[affeldt-aist]

@Tragicus and @proux01 were not upset by the use of setX, let's merge! ;-)

[CohenCyril]

As @t6s noted, setX was already taken here
https://github.com/math-comp/math-comp/blob/b174dacb24a4b5d44e71e3fe18d7a5ccd25a8b85/mathcomp/ssreflect/finset.v#L54-L55
and that setM being introduced despite the pre-established convention is probably young-me's fault 🤷

In order to avoid clashes when we re-unify, why not use Y as in "sYmmetric difference", since setY is unbound for now?

[t6s]

As @t6s noted, setX was already taken here
https://github.com/math-comp/math-comp/blob/b174dacb24a4b5d44e71e3fe18d7a5ccd25a8b85/mathcomp/ssreflect/finset.v#L54-L55
and that setM being introduced despite the pre-established convention is probably young-me's fault 🤷

In order to avoid clashes when we re-unify, why not use Y as in "sYmmetric difference", since setY is unbound for now?

setY seems to be nice; I do not come up with any common set operation beginning with "y" :)

What about doing a renaming PR? @affeldt-aist

[affeldt-aist]

so a new PR that turns setX into setY and renames setM into setX, let's do that
(by the way, using setY was also proposed by @proux01 and/or @Tragicus )