Invertible and data

Stream: maths

[Yury G. Kudryashov]

Motivated by @Michael Stoll 's #14986. Why do we carry data in docs#Invertible ? Should we turn docs#IsUnit into a typeclass instead?

[Yury G. Kudryashov]

Alternatively, we can turn IsUnit into a typeclass and treat [Invertible _] the same way we treat Decidable: only use it if we need a computable invOf.

[Johan Commelin]

I think it was done because there are examples where you can compute, and it is nice if it works in those examples. For example some localizations like $\Z[1/2]$, where 2 is invertible, but you don't have all rational numbers. Or $\Z/8\Z$ where 3, 5, 7 are their own multiplicative inverses.

[Johan Commelin]

So I think it is worth looking into your 2nd suggestion. Where we have a data-carrying class that is used sparingly, and prop-class that is used for almost all the theory.

[Adam Topaz]

I think there is no obvious overlap here: docs#Units is essentially a bundled docs#Invertible and docs#IsUnit is the associated prop.

[Edward van de Meent]

• docs#Units

[Adam Topaz]

yeah, sorry!

[Yury G. Kudryashov]

Adam Topaz said:

I think there is no obvious overlap here: docs#Units is essentially a bundled docs#Invertible and docs#IsUnit is the associated prop.

IsUnit x is the same as Nonempty (Invertible x). What I'm trying to say is that we use a typeclass with subsingleton data (Invertible) as an assumption in theorems that don't need the data, and this can lead to non-defeq diamonds.

[Yury G. Kudryashov]

Opened #17458

[Yury G. Kudryashov]

On Github, @Eric Wieser argues that we should migrate to (h : IsUnit _) instead.

[Eric Wieser]

At least in places where we don't actually want the data

[Yury G. Kudryashov]

My main argument pro [IsUnit _] is that people who don't care about fields of positive characteristic may want to apply theorems that require IsUnit (2 : K) without making another stop to prove it.

[Eric Wieser]

Is it 2 specifically that we care about?

[Yury G. Kudryashov]

I definitely have some examples for IsUnit (2 : K), incl. midpoint and #14986

[Yury G. Kudryashov]

I don't have other examples in mind right now.

[Yury G. Kudryashov]

Unless we want to generalize docs#mul_inv_cancel etc to [DivisionMonoid G] [IsUnit a]

[Yury G. Kudryashov]

Note: we already have it as @[simp] for Invertible a.

[Eric Wieser]

I think we might be missing the bigger picture on 14986; the result is also true (and I believe straightforward to prove with docs#QuadraticMap.toBilin) in free modules where 2 is not invertible

[Yury G. Kudryashov]

See https://github.com/leanprover-community/mathlib4/actions/runs/11195116893/job/31122394124 for a list of lemmas that assume [Invertible _] but never use invOf in the statement.

[Yury G. Kudryashov]

(there are other pending linters in the same PR, so you need to search for Invertible)

[Eric Wieser]

Yury G. Kudryashov said:

See https://github.com/leanprover-community/mathlib4/actions/runs/11195116893/job/31122394124 for a list of lemmas that assume [Invertible _] but never use invOf in the statement.

I think I would be in favor of changing all these to (h : IsUnit x) and using [Fact (IsUnit x)] on the one or two instances.

[Yury G. Kudryashov]

Why [IsUnit _] is worse?

[Eric Wieser]

I don't understand how this argument doesn't lead to us converting everything of type Prop into a typeclass

[Eric Wieser]

Maybe that really is a fine outcome, but I've definitely heard arguments that doing that for, say, Odd and Even would amount to an abuse of typeclass search.

[Violeta Hernández]

This smells like typeclass abuse to me too. It feels much more likely that we'll want to prove IsUnit from other available hypotheses, than being able to infer it from the structure of the argument.

[Yury G. Kudryashov]

What do you think about docs#MonoidAlgebra.Submodule.complementedLattice ?

[Yury G. Kudryashov]

UPD: it should assume NeZero.

[Yury G. Kudryashov]

Ignore my last 2 messages.

[Yury G. Kudryashov]

#17754 makes Maschke use IsUnit.

[Yury G. Kudryashov]

What should I do about IsUnit 2? Use Fact? Introduce a typeclass specifically for this?

[Yury G. Kudryashov]

I also see an assumption Invertible 3 in docs#WeierstrassCurve.exists_variableChange_isShortNF

[Yury G. Kudryashov]

See also docs#CategoryTheory.Linear.instEpiHSMulHomOfInvertible

[Yury G. Kudryashov]

It's an instance that assumes [Invertible r] but doesn't use data.

[Violeta Hernández]

I think it makes sense to use Fact for these "a specific number is invertible" predicates

[Eric Wieser]

I think that depends whether the instance you're using Fact on is data or a proof

[Eric Wieser]

If it's a proof, then Fact (IsUnit x) does indeed make the most sense. If it's data, then Invertible x is often better.

[Eric Wieser]

If your proof uses some auxiliary data along the way, use def aux [Invertible x] to define that data, then use IsUnit.nonempty_invertible to construct that instance mid-proof

[Yury G. Kudryashov]

Why Fact (IsUnit _) is better than [IsUnit _]?

[Yury G. Kudryashov]

(e.g., docs#IsClosed is a typeclass but we mostly use it as a predicate)

[Violeta Hernández]

Yury G. Kudryashov said:

Why Fact (IsUnit _) is better than [IsUnit _]?

I'll admit, I'm not sure. Why is Fact (IsPrime _) better than [IsPrime _]? Seems to be similar reasoning.

[Eric Wieser]

Does docs#Fact have anything to say?

[Violeta Hernández]

Yes, but I don't really get its reasoning. Is the issue just that Nat.prime would become a one-field structure instead of being def-eq to its definition?

[Violeta Hernández]

By that reasoning, IsUnit should probably not be a class either

[Eric Wieser]

Ah, I hadn't considered that (historic?) limitations around non-structure classes could have factored in here.

[Eric Wieser]

My rule of thumb would be "only use typeclasses for types"

[Violeta Hernández]

I don't think it's quite as simple as that, e.g. having docs#CharZero as a typeclass is definitely a good thing.

[Violeta Hernández]

I'd argue the same for docs#WellFoundedLT and docs#WellFoundedGT but maybe I'm biased since I'm the one who pushed for those :stuck_out_tongue:

[Violeta Hernández]

Oh wait, I misunderstood you as implying typeclasses should be type-valued rather than having type arguments

[Violeta Hernández]

I mostly agree with that rule of thumb.

[Violeta Hernández]

I'd like to point to the counterexample of the unbundled order classes like docs#IsRefl, docs#IsTrans, etc. I'd argue these are still good to have, but if anyone ever wants to refactor them out I don't think I'll be strongly opposed.

[Yury G. Kudryashov]

We have docs#NeZero docs#IsClosed

[Eric Wieser]

IsClosed I'd argue should be de-classified, NeZero I haven't thought about before.

[Michael Stoll]

NeZero seems to be helpful e.g. to avoid using PNat.

[Yury G. Kudryashov]

Do you suggest migrating to Fact (IsClosed _) whenever we need to assume IsClosed in an instance?

[Eric Wieser]

Yes, that's my claim

[Sébastien Gouëzel]

The reason we used IsClosed as a typeclass is to be able to obtain that quotients of normed spaces by closed subspaces are normed spaces. For instance, if you're in finite dimension, subspaces are automatically closed, so quotients are automatically normed spaces. If you want to get this fact for free using the Fact mechanism, then you need to register this as a global Fact instance, but if I remember correctly global Fact instances should be avoided if possible. So I see what we lose when going from [IsClosed ...] to [Fact (IsClosed ...)]. What do we gain?

[Eric Wieser]

Agreed that the alternative would be a few global instances of docs#Fact, but we have a number of those already

[Eric Wieser]

Flipping the question around; what do we lose if we make _every_ structure ... : Prop a class?

[Yaël Dillies]

In Lean 3, that would have caused a lot of frozen instance cache issues

[Floris van Doorn]

Yury G. Kudryashov said:

We have docs#NeZero docs#IsClosed

IsClosed is a class? :shock:

[Violeta Hernández]

RE NeZero, I've only ever come across NeZero 1 in my own applications, which arguably could be made into a OneNeZeroClass if we really wanted to.

[Yury G. Kudryashov]

NeZero is used, e.g., in our instances about Fin.

[Yury G. Kudryashov]

In many cases, NeZero (1 : R) can be replaced with Nontrivial R.

[Yury G. Kudryashov]

See docs#NeZero.one

[Yaël Dillies]

It's also used for measures, where a bunch of lemmas break for the zero measure

[Oliver Nash]

Also in low characteristic [NeZero (2 : R)]and [NeZero (3 : R)] are already useful (and one day we'll certainly get to [NeZero (5 : R)] and maybe higher). E.g., docs#EllipticCurve.ofJ_0_of_three_ne_zero

[Eric Wieser]

That looks like it could just take (h : 3 \ne 0) as an argument

[Matthew Ballard]

In these scenarios, I just want to avoid manually supplying a proof that something is not 0. Typeclass synthesis is one mechanism. If set up appropriately, autoparams could be another. Though NeZero didn’t get upstreamed for no reason.

[Eric Wieser]

My understanding is that NeZero got upstreamed because of Fin, and the decision was based on "this is what mathlib does" not "this is clearly the perfect solution"

[Eric Wieser]

NeZero is also somehow different because we have both the class and the non-class

[Matthew Ballard]

Sure, but if they had a better idea, they wouldn’t have.

I think the cost of flipping everything to classes is just performance.

[Matthew Ballard]

I would like

import Mathlib.Data.ZMod.Defs

instance (p : Nat) (hp : p.Prime := by norm_num) : Field (ZMod p) := sorry

#synth Field (ZMod 5)

to succeed

[Eric Wieser]

Enough to create an RFC for it?

[Sébastien Gouëzel]

If I recall correctly, having the possibility to run tactics for default arguments in typeclass inference was considered at the beginning of Lean 4, but it was discarded later because of added complexity and performance issues. Given how critical this is, I'm not sure the FRO is willing to revisit this.

[Matthew Ballard]

I think an RFC is fine but I would guess that as @Sébastien Gouëzel says: significant changes to typeclass synthesis are currently off the table

[Matthew Ballard]

I would also guess that the FRO considered something like this before upstreaming NeZero but I have no first-hand knowledge

[Jz Pan]

Now my PR #18531 of to elliptic curves is related to #17458... If IsUnit is a typeclass then this PR could be simplified a little bit (also with API changes).

[Kim Morrison]

Pinging that #17458 is marked awaiting-zulip based on this thread. It would be good to come to a decision here, and either close that PR or proceed with reviewing it.

[Yury G. Kudryashov]

+1 for ping

[Michael Stoll]

I've been using (and got to like) docs#NeZero quite consistently in the recent factor of rootsOfUnity. So I think a Prop- valued version of docs#Invertible makes sense. But I haven't followed this discussion very closely.

[Yury G. Kudryashov]

@Eric Wieser WDYT?

[Eric Wieser]

My stance is:

• IsUnit shouldn't be a class
• Invertible is mostly ok as is
• A new HasInverse x x_inv : Prop (which is to IsUnit as HasSum is to Summable) would ease some of the pain around Invertible.

[Yury G. Kudryashov]

In the examples where I suggest we assume [IsUnit a], we don't want to know a_inv.

[Eric Wieser]

Right, in those examples I am suggesting Fact (IsUnit a)

[Eric Wieser]

(and I am not proposing HasInverse should be a class)

[Yury G. Kudryashov]

Why Fact (IsUnit a) is better than class IsUnit (rarely used as a class)?

[Eric Wieser]

Should Summable be a class too? Should Prime?

[Yury G. Kudryashov]

Summable: AFAICT, we never need it to construct an instance. Prime: possibly (we use Fact (Nat.Prime p) very often).

[Eric Wieser]

Yury G. Kudryashov said:

Why Fact (IsUnit a) is better than class IsUnit (rarely used as a class)?

Here's one argument; if you make it a class, every caller has to think about whether to write (h : IsUnit a) or [IsUnit a]. If you use Fact, this choice is obvious

[Yury G. Kudryashov]

Makes sense, but didn't work for Nat.Prime... I don't see any system in (h : p.Prime) vs [Fact p.Prime]...

[Yury G. Kudryashov]

So, we should add instances for, e.g., [GroupWithZero G] {a : G} [NeZero a] : Fact (IsUnit a)?

[Eric Wieser]

Yury G. Kudryashov said:

AFAICT, we never need it to construct an instance.

I think "needed to construct an instance" is exactly the design problem that Fact is intended to solve.

So I think your argument might extend to "we should remove Fact", which is worthy of its own thread.

[Yury G. Kudryashov]

BTW, are discrimination trees good enough with Facts?

[Eric Wieser]

They should be fine, key (Fact X) = [Fact] ++ key X

[Yury G. Kudryashov]

Does it mean that we can use Fact (Predicate ...) instead of turning Predicate into a class without slowdown?

[Eric Wieser]

I think yes

[Eric Wieser]

(ignoring the negligable cost of the key having one more element)

[Yury G. Kudryashov]

Then I'll start migrating some [Invertible] assumptions to [Fact (IsUnit _)].

[Kim Morrison]

Yury G. Kudryashov said:

Does it mean that we can use Fact (Predicate ...) instead of turning Predicate into a class without slowdown?

While this is true, it also goes against our original plans to not use Fact as a general "let's have typeclass search do our proving" mechanism.

(Perhaps it is a feature, not a bug, that there is overhead to turning something into a class?)

[Kevin Buzzard]

With Nat.prime p there is never any proving; it literally is just a convenient way of saying "let p be a prime forever". So this is a great use of Fact as far as I can see.

[Eric Wieser]

My mental model was that Fact was only really intended to allow non-typeclasses into the assumptions of instances as instance [Fact (Predicate ..)] : _; which is compatible with Kim's comment which I think is objecting to it appearing in the conclusion as instance : Fact (Predicate ..).

[Eric Wieser]

(docs#Fact indicates a few such instances exist, but I think they're mostly for convenience rather than doing heavy lifting)

[Yury G. Kudryashov]

But we want to have at least the following instances for IsUnit _ (or `Fact (IsUnit _)1):

• [Group G] (a : G) : IsUnit a
• [Invertible a] : IsUnit a
• IsUnit 1
• [GroupWithZero G₀] (a : G₀) [NeZero a]
• [CommMonoid M] {a b : M} [IsUnit a] [IsUnit b] : IsUnit (a * b)
• [IsUnit a] (n : Nat) : IsUnit (a ^ n)
• [IsUnit (OfNat.ofNat n : R)] : IsUnit (OfNat.ofNat : Module.End R M) (this instance from #14986 and motivated this thread).

[Johan Commelin]

@Eric Wieser Maybe we should just try to make IsUnit a class. Your argument is that this puts us on a slippery slope. Maybe it does. But we're still deciding on a case-by-case basis. And Yury has some good arguments for wanting automation to kick in. TC is the best we have for this right now.

[Eric Wieser]

The examples above feel rather like

Kim Morrison said:

"let's have typeclass search do our proving"

I'm not sure that the fact some proposition can be deduced structurally is a sufficient argument for us to use typeclasses search to prove it; otherwise Differentiable and IsSquare would surely deserve the same treatment.

[Patrick Massot]

I find it sad that we can’t have “let’s have typeclass search do our proving”.

[Kevin Buzzard]

IIRC we tried this a bit in LTE with simple inequalities. We were working with L^p spaces with p<1 remembered as a Fact, and would occasionally get typeclass inference to prove things like q<p and p<1 implies q<1.

[Johan Commelin]

Yeah, we used it a lot. It did all sorts of multiplications of inequalities

[Johan Commelin]

Of course we didn't have gcongr back then

[Yakov Pechersky]

The situation is somewhat similar to docs#Ideal.IsPrime where that is a class. Sometimes IsPrime is passed as an explicit argument, and sometimes as a TC argument. And it has to be in TC access so that one can get an integral domain instance on the quotient ring.

[Yury G. Kudryashov]

Note that I explained that we may have reasonable IsUnit instances but I didn't find any instances that need to assume [IsUnit _], at least in this thread.

[Yury G. Kudryashov]

I guess, we can try to migrate some of those [Invertible _] to (h : IsUnit _) until we meet an instance, then come back to this discussion.

[Eric Wieser]

I think we should do that (and migrate to Fact (IsUnit _) where appropriate), then come back to this discussion once we know how many such Fact (IsUnit _)s there are which we want to de-Fact

[Jz Pan]

Yury G. Kudryashov said:

Note that I explained that we may have reasonable IsUnit instances but I didn't find any instances that need to assume [IsUnit _], at least in this thread.

https://github.com/leanprover-community/mathlib4/blob/3f45494422faa4e895db8a57b7a486dd9e0c2a5d/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean#L556-L563 in PR #18531. It is [Invertible ...] in current mathlib, but we plan to refactor it without requiring knowing what the exact inverse is.

[Eric Wieser]

My impression from that PR is that IsElliptic should perhaps also not be a class

[Yury G. Kudryashov]

I don't think that we'll have any instance implying IsUnit (_ - 1728).

[Violeta Hernández]

Just to be clear, what's the argument against having typeclass search take over every single structural predicate?

[Johan Commelin]

TC is already the most expensive part of building mathlib. I guess we should keep it in check a bit.
And probably going down that path would cause a net slowdown.

I would still love to have more invisible automation for these structural proofs though...

[Violeta Hernández]

Can we maybe make custom simp / aesop sets? And have an autoparam calling the relevant tactic

[Jz Pan]

Eric Wieser said:

My impression from that PR is that IsElliptic should perhaps also not be a class

Then each time you write j you need to provide a proof that the discriminant is invertible. Or fall back to current design: WeierstrassCurve vs EllipticCurve which I want to refactor. Or assign j a junk value when the discriminant is not invertible.

[Jz Pan]

I have already list the reason in that PR why current design is suboptimal: it requires copies of APIs between WeierstrassCurve and EllipticCurve.

[Jz Pan]

Yury G. Kudryashov said:

I don't think that we'll have any instance implying IsUnit (_ - 1728).

It is provided by haveI later in that file. That instance is used in another instance which does not require any other auxiliary inputs, and which is designed to be the public instance to use.