Leibniz OFE construction

[Kaptch]

Description

POC: OFE constructor that takes:

• Carrier: X: Type _;
• Distance: dist: Nat \to X \to X \to Prop, satisfying old distance axioms.

And returns a OFE that has X/\sim carrier, where x \sim y \iff \forall n. dist n x y and lifted distance.
It trivially satisfies old equiv_dist axiom, and is Leibniz.
Tested it on agreement, and it was relatively fast to fix downstream problems (~10 lines in total).

Updated summary

Made Agree a Leibniz OFE, on Agree A, equiv is now just =.

There is a generic construction in OFE.lean (QuotientO + mkQuotient, plus a little mk/lift/map wrapper API), then a Leibniz version of Agree on top of it. Agree API is the same, except that now it requires its type argument to be OFE even for the definition.
Once Agree is Leibniz, a bunch of cameras built on it are too, so I added the instances: View, Auth, and the lib ones (DFracAgree, ExclAuth, FracAuth). Plus two tiny fixes where the refactor changed how Agree values get constructed.
The only non-Leibniz (or Leibniz-preserving) OFEs/CMRAs are related to maps, and I'll do them in a separate PR shortly.

[markusdemedeiros]

Nice! Any reason why this touches views/agree?

[Kaptch]

I tested it on agreement, because it is one of a few algebras, which would be changed, if we move to a new definition of OFEs without equiv. Views were a collateral damage, there was minor case of looking past the interface of agreement.
But apart from minor nits in agreement-dependent algebras, nothing changes much. We never eliminate from algebras to Lean types, so there's no need for Quotient.lift in other parts of the project.
Morally, this example shows that changing equiv -> eq would not break agreement algebra, since we could provide the same interface.
I haven't tested it with other algebras with non-trivial equiv, but it should work fine.

[markusdemedeiros]

That's promising!

[Shreyas4991]

Setoid is a type class. We typically use instance instead of def.

[markusdemedeiros]

@Kaptch I'm a little confused as to why the type needs to be an OFE here, when the type did not need to be an OFE before. Isn't the point of the Agree quotient just to make it a set rather than a list?

[Kaptch]

Under [OFE \alpha] it should be isomorphic to Agree := { X : FiniteSet \alpha | X \neq \empty }
The reason I used this implementation is that I thought that making our version of FiniteSet seems to be redundant, given that it will be used only in Agree, and Mathlib has a version of FiniteSet with good API, so porting it would introduce duplication of one more chunk of Mathlib.
This version of Agree can be used with non-OFE types by giving them discrete metric.
Also, it was a good usecase for a more general quotient construction, which could be reused for some client OFEs if they also required implicit quotienting via Equiv.
That being said, I can redo it with finite sets instead, I have a simple version of FiniteSet somewhere, and can use that.

[markusdemedeiros]

I think you succeeded in showing that the general quotient construction works, but yes, it sounds like we should definitely avoid the extra OFE constraint.

[Kaptch]

Oki, I will think of a good way to do it then.

[Kaptch]

Instead of bringing finsets for one definition, quotiented lists in-place, and restored the old interface without the OFE obligation.

[markusdemedeiros]

Sounds great. Re-request when I can review it!

[markusdemedeiros]

Looks superb!