[Merged by Bors] - feat(data/sym2) Defining the symmetric square (unordered pairs)

[kmill]

This adds a type for the symmetric square of a type, which is the quotient of the cartesian square by permutations. These are also known as unordered pairs.

Additionally, this provides some definitions and lemmas for equalities, functoriality, membership, and a relationship between symmetric relations and terms of the symmetric square.

I preferred sym2 over unordered_pairs out of a combination of familiarity and brevity, but I could go either way for naming.

---

[fpvandoorn]

Thank you for your pull request!

Do you have a particular use case for this file already? Generally you get a much better library if you work towards a particular goal, and add things that you need (and lemmas similar to those) than if you just start writing a library without a goal in mind.

For example, are mem and vmem both useful?

[kmill]

Thank you for reviewing my PR @fpvandoorn!

Do you have a particular use case for this file already? Generally you get a much better library if you work towards a particular goal, and add things that you need (and lemmas similar to those) than if you just start writing a library without a goal in mind.

For example, are mem and vmem both useful?

I hope this PR didn't look quite so aimless! This library came from some work dealing with graphs over the last few weeks, and I figured I would try a PR with this before attempting the rest. Some of the lemmas in this file, though, are purely for well-definedness/uniqueness purposes to prove the definition is good, in that I think they let you work with each definition without expanding them.

The mem versus vmem thing is for computability reasons, and there's a part of the graph library that might or might not use vmem in the end. (Given a vertex and an incident edge, how do you get the vertex opposite the edge? If edges are terms of sym2 over the vertex type, and incidence is recorded with vmem, then you can compute that opposite vertex. Otherwise one needs additional assumptions.)

[kmill]

I just added documentation pointing to from_rel, which is sort of the reason behind this PR.

I also added a lemma I forgot to include, from_rel_irreflexive, which is that from_rel of a symmetric relation has no diagonal elements iff the relation is irreflexive. This has applications for simple graphs, and it makes use of is_diag. Hopefully it is OK adding it to this PR this time.

[fpvandoorn]

I hope this PR didn't look quite so aimless! This library came from some work dealing with graphs over the last few weeks, and I figured I would try a PR with this before attempting the rest.

That's good! I also thought that this could be useful for graph theory.

Some of the lemmas in this file, though, are purely for well-definedness/uniqueness purposes to prove the definition is good, in that I think they let you work with each definition without expanding them.

That's indeed a good think to aim for!

The mem versus vmem thing is for computability reasons, and there's a part of the graph library that might or might not use vmem in the end. (Given a vertex and an incident edge, how do you get the vertex opposite the edge? If edges are terms of sym2 over the vertex type, and incidence is recorded with vmem, then you can compute that opposite vertex. Otherwise one needs additional assumptions.)

Yeah, vmem might be useful for computable functions.

Btw, the linter complains that it wants you to add an instance [inhabited \a] : inhabited (sym2 \a).

I just added documentation pointing to from_rel, which is sort of the reason behind this PR.

I also added a lemma I forgot to include, from_rel_irreflexive, which is that from_rel of a symmetric relation has no diagonal elements iff the relation is irreflexive. This has applications for simple graphs, and it makes use of is_diag. Hopefully it is OK adding it to this PR this time.

So for simple graphs isn't it easier to work with the type of unordered pairs where the two components are unequal (so the irreflexivity is built in)?
Though maybe this is better: make "simple graphs with loops" the basic object, and have a special class of simple graphs in those.

[kmill]

Btw, the linter complains that it wants you to add an instance [inhabited \a] : inhabited (sym2 \a).

Ok, I'll look into that. I was going to ask how to deal with this linter warning.

So for simple graphs isn't it easier to work with the type of unordered pairs where the two components are unequal (so the irreflexivity is built in)?
Though maybe this is better: make "simple graphs with loops" the basic object, and have a special class of simple graphs in those.

I've found it to be really hard to say what's better than what when defining graphs, since people use them for all sorts of things (and as for me, I tend to use multigraphs exclusively, or sometimes simple graphs allowing loops). Perhaps it's worth defining a symmetric square with deleted diagonal, but at least {x : sym2 α // ¬is_diag x} is equivalent.

[jcommelin]

Looks good to me! Some minor stylistic issues, but I think after that this is ready for merging.
@fpvandoorn Do you have further comments?

[fpvandoorn]

Looking good, including all additions.

Feel free to merge it after incorporating my comments (or let someone else do it if you're unsure).

bors d+

[bors]

✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[fpvandoorn]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Run tests and docs
• Lint mathlib
• Build mathlib

[kim-em]

Oops, we probably shouldn't leave import tactic in files going into mathlib. I'll clean this up elsewhere.