[Merged by Bors] - refactor: remove Sym2's global Prod setoid instance, use s(x, y) notation for unordered pairs

[kmill]

The Sym2 type used a global setoid instance on α × α so that ⟦(x, y)⟧ could stand for an unordered pair using standard Quotient syntax. This commit refactors Sym2 to not use Quotient and instead use its own s(x, y) notation. One benefit to this is that this notation produces a term with type Sym2 rather than Quotient.

The Fintype instance for Sym2 is in Mathlib.Data.Finset.Sym. We switch from using the one for Quotient because it does not require DecidableEq.

---

[eric-wieser]

I don't understand what the gain of moving from Quotient to Quot is here; it looks like it just makes less API available...

(I agree with the move of de-instancing the Setoid instance and the new notation)

[kmill]

I strongly believe that any type defined using a quotient needs to recapitulate part of the quotient API so that it can ensure that there is no API leak.

The big problem with using the Quotient or Quot APIs on a type that happens to be defined using them is that (1) they change the type of the term from (for example) Sym2 to Quotient, (2) they use the constructor Quotient.mk instead of Sym2.mk (again, changing the type), (3) they use non-informative Setoid.r for the relation rather than Sym2.Rel. With that last point, it's hard writing these Quotient relation terms yourself when there's no global Setoid instance.

I am not sure what the Quotient API gives us that the Quot API couldn't -- the main one is Quotient.eq, but in the long run I'm imagining quotients would be more convenient if Quot had lemmas that could take a class version of Equivalence. That way relations wouldn't unnecessarily get turned into their Setoid-bundled forms.

One other reason I switched from Quotient to Quot is to disable the ⟦(x, y)⟧ notation.

You'll notice that in practice we can still use Quotient API by passing in a setoid. There's even a place where I temporarily enable the Setoid instance to use it. Other places I switched to Quot where it was more convenient, and I added Sym2 versions of recursors just to keep the types nice. (There's also the small point that the Quot recursors are missing @[elab_as_elim], which needs to be fixed in core.)

[YaelDillies]

Why do we need this extra import?

[kmill]

It brings in Sym2.instFintype

[YaelDillies]

Hmm okay sure, but why do we suddenly need Sym2.instFintype here?

[YaelDillies]

Ah, is it because you can't use the Quotient instance anymore? Worth mentioning in the description.

[kmill]

It's less a "can't" and more a "the Sym2.instFintype one is better". It's true that the Quotient instance would have to be restated using a inferInstanceAs instance to get it to apply though.

(I mentioned it in the other comment, but fleshing out the Quot API with a typeclass version of Equivalence would mean we could take these Quotient instances and make them be nicer-to-use Quot instances.)

[eric-wieser]

Isn't that typeclass version HasEquiv?

[kmill]

No, that's a notation typeclass.

I mean this:

class IsEquivalence {α : Type*} (r : α → α → Prop) : Prop where
  equivalence : Equivalence r

[jcommelin]

I'm going to kick this on the queue. The diff has net size close to zero. Outside the API file on sym2, it really cleans up some type-mess. The file on sym2 itself now duplicates some Quotient API. Maybe that can be done in a better way in the future. But that doesn't have to block this PR.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style