Zulip Chat Archive

Stream: general

Topic: Concerns about `invertible` class


Oliver Nash (Jun 20 2020 at 15:29):

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 (Jun 20 2020 at 15:30):

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 (Jun 20 2020 at 15:31):

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 (Jun 20 2020 at 15:34):

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 (Jun 20 2020 at 15:35):

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 (Jun 20 2020 at 15:37):

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 (Jun 20 2020 at 15:38):

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 (Jun 20 2020 at 15:38):

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

Jalex Stark (Jun 20 2020 at 15:39):

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 (Jun 20 2020 at 15:39):

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 (Jun 20 2020 at 15:40):

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

Oliver Nash (Jun 20 2020 at 15:41):

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 (Jun 20 2020 at 15:41):

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 (Jun 20 2020 at 15:49):

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 (Jun 20 2020 at 16:50):

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 (Jun 20 2020 at 18:14):

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

Yury G. Kudryashov (Jun 20 2020 at 18:16):

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 (Jun 20 2020 at 18:17):

Yes absolutely, I see that.

Oliver Nash (Jun 20 2020 at 18:18):

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

Oliver Nash (Jun 20 2020 at 18:19):

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 (Jun 20 2020 at 18:21):

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 (Jun 20 2020 at 18:22):

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

Yury G. Kudryashov (Jun 20 2020 at 18:23):

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

Oliver Nash (Jun 20 2020 at 18:24):

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 (Jun 20 2020 at 18:24):

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 (Jun 20 2020 at 18:25):

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

Oliver Nash (Jun 20 2020 at 18:25):

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 (Jun 20 2020 at 18:27):

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

Yury G. Kudryashov (Jun 20 2020 at 18:31):

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 (Jun 20 2020 at 18:32):

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 (Jun 20 2020 at 18:33):

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 (Jun 20 2020 at 18:34):

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 (Jun 20 2020 at 18:34):

I don't care about computability.

Yury G. Kudryashov (Jun 20 2020 at 18:34):

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

Oliver Nash (Jun 20 2020 at 18:37):

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 (Jun 20 2020 at 18:37):

Hmm, well I can imagine other differences.

Yury G. Kudryashov (Jun 20 2020 at 18:45):

The theory of units has more simp lemmas etc.

Oliver Nash (Jun 20 2020 at 18:46):

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 (Jun 21 2020 at 04:28):

simp_rw will avoid the motive issue

Oliver Nash (Jun 22 2020 at 14:56):

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


Last updated: Dec 20 2023 at 11:08 UTC