Concerns about `invertible` class

Stream: general

[Oliver Nash]

I'm looking guidance on when it is a good idea to use the invertible class. I am concerned that naive usage can set things up for the dreaded motive is not type correct error.

[Oliver Nash]

Specifically the "function" defined by "a ↦ ⅟a" pulls data from a typeclass instance and so is not really a function. I encountered this a couple of hours ago when I was considering modifying matrix.nonsing_inv to use invertible so that it was not necessary for the base type to carry a has_inv instance.

[Oliver Nash]

Here is the example:

import linear_algebra.nonsingular_inverse
import algebra.invertible

universes u v

namespace matrix
open_locale matrix
section bad_invertible

variables {n : Type u} [fintype n] [decidable_eq n]
variables {R : Type v} [comm_ring R]
variables (A : matrix n n R) [invertible A.det]
variables (B : matrix n n R) [invertible B.det]

/-- Bad definition: pulls data from a typeclass instance. -/
def nonsing_inv' : matrix n n R := ⅟(A.det) • adjugate A

lemma inverses_are_unique (h : A = B) :
  A.nonsing_inv' = B.nonsing_inv' :=
begin
  rw h, -- rewrite tactic failed, motive is not type correct
end

end bad_invertible
end matrix

[Oliver Nash]

Now the above is not a problem in the sense that inverses_are_unique is provable by other means but it still seems like nonsing_inv' would be a pretty horrible definition to make.

[Oliver Nash]

So I had a quick look for usage of invertible and I see that equivariant_projection in representation_theory.maschke uses it and, I think, will one day trigger the motive is not type correct error.

[Oliver Nash]

Am I missing the obvious and somehow this is all fine? Do others feel like invertible should come with guidance to stop it being a footgun?

[Jalex Stark]

Oliver Nash said:

Specifically the "function" defined by "a ↦ ⅟a" pulls data from a typeclass instance and so is not really a function.

i'm confused. isn't * a function which takes data from a typeclass, namely has_mul? does your objection also apply to this?

[Oliver Nash]

That same thought is in the back of my mind. I haven't bottomed out on it yet.

[Jalex Stark]

what do you want to be able to do with invertible that you can't "because it's not really a function"? (probably i will know the answer to this question after poking at your example for a few minutes)

[Sebastien Gouezel]

I don't think this is the indended use of the invertible typeclass: it is only there to provide (once and for all) invertibility of a few fixed elements in a ring. If you want to discuss invertibility of variables or complicated objects, is_unit should be used instead (if I understand correctly what the doc in invertible.lean says).

[Oliver Nash]

Aha, so perhaps I should just be reading the docs!

[Oliver Nash]

OK I see that now. I still think the fact that it has crept into equivariant_projection indicates there is potential for future problems.

[Reid Barton]

I think the main difference with has_mul (and this also goes for other things like is_ring_hom) is that invertible has a parameter which is a value, for which you are likely to want to reason about its equality to other values, while has_mul takes a type

[Oliver Nash]

Jalex Stark said:

what do you want to be able to do with invertible that you can't "because it's not really a function"? (probably i will know the answer to this question after poking at your example for a few minutes)

Sorry I missed this. The rw h in my example is the best example I can give.

In any case, I'm happy to leave this now. I recognise that there is already documentation not to use invertible in the way that I did in my example.

[Yury G. Kudryashov]

As far as I understand, non-typeclass version of ⅟(A.det) is def nonsing_inv' (A : matrix n n R) {u : units R} (hu : (u : R) = A.det) := ((u⁻¹ : units R) : R) • adjugate A

[Oliver Nash]

Thanks @Yury G. Kudryashov I think that's exactly what Sebastian was hinting me toward.

[Yury G. Kudryashov]

The only difference between these two approaches is that u : units R shows the problem explicitly. Note that while rw doesn't work dsimp [nonsing_inv']; simp only [h] should work.

[Oliver Nash]

Yes absolutely, I see that.

[Oliver Nash]

The fact that hu appears an explicit argument makes it clear that there is additional data to handle.

[Oliver Nash]

I have a little time now so I might see if it looks like it is worth changing the definition of matrix.nonsing_inv along these lines. It would suit something else I'd like to do.

[Yury G. Kudryashov]

What's wrong with invertible definition + subsingleton instance? AFAIR, this should be enough for simp to be able to rewrite h : A = B.

[Oliver Nash]

Perhaps nothing: I don't know anything about subsingletons!

[Yury G. Kudryashov]

[subsingleton α] means that α has at most one element.

[Oliver Nash]

I see, and from what you're saying simp will be smart enough to make use of this. However would rw still trigger the rewrite tactic failed, motive is not type correct error?

[Yury G. Kudryashov]

AFAIR, simp can unify two subsingletons automatically. If not, then @[congr] lemma nonsing_inv'_congr (h : A = B) : nonsing_inv' A = nonsing_inv' B should help.

[Yury G. Kudryashov]

Yes, rw won't work. For me the general rule is "if rw or simp doesn't work, try the other one".

[Oliver Nash]

Understood, this is really a great tutorial you are giving me. Thank you. I'm still reluctant to design something that will cause problems for rw though. Do you think I'm being too conservative?

[Oliver Nash]

Admittedly I haven't tried it yet but the approach via units seems more attractive.

[Yury G. Kudryashov]

How are you going to use this definition? If you want a user to explicitly prove that det A is invertible, then (u : units R) is a good approach. If you want Lean to automatically figure out that det A is invertible, then inv_of is better.

If you use (u : units R), then you'll need @[congr] lemma nonsing_inv'_congr {A B : matrix n n R} (h : A = B) {uA uB : units R} {hA : (uA : R) = det A} {hB : (uB : R) = det B} : nonsing_inv' A hA = nonsing_inv' B hB.

[Yury G. Kudryashov]

This should help simp go from nonsing_inv' A hA = nonsing_inv' B hB to A = B, not A = B and uA = uB.

[Oliver Nash]

I see, it's great to know that the congr decorator can make Lean consume a proof that inverses are unique in this way.

[Yury G. Kudryashov]

Another question is whether you want it to be computable. If not, then you can use hA : is_unit (det A), and get u from classical.choice.

[Oliver Nash]

I don't care about computability.

[Yury G. Kudryashov]

Note that @[congr] is used by simp but not congr and convert.

[Oliver Nash]

I plan to have the user provide proof that A.det is invertible so I guess I'll try the approach via units. I guess the advantage of the approach via is_unit over raw unit is that the user need only provide a single argument?

[Oliver Nash]

Hmm, well I can imagine other differences.

[Yury G. Kudryashov]

The theory of units has more simp lemmas etc.

[Oliver Nash]

I did see that is_unit is basically just a wrapper on top of it. I'm currently tinkering to see if I can get something sane with just unit.

[Yakov Pechersky]

simp_rw will avoid the motive issue

[Oliver Nash]

I explored various approaches for nonsing_inv and eventually settled on https://github.com/leanprover-community/mathlib/pull/3136