Zulip Chat Archive

Stream: general

Topic: Concerns about `invertible` class


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip Oliver Nash (Jun 20 2020 at 15:40):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Oliver Nash (Jun 20 2020 at 18:14):

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

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Jun 20 2020 at 18:17):

Yes absolutely, I see that.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Jun 20 2020 at 18:22):

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

view this post on Zulip Yury G. Kudryashov (Jun 20 2020 at 18:23):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip Oliver Nash (Jun 20 2020 at 18:27):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Oliver Nash (Jun 20 2020 at 18:34):

I don't care about computability.

view this post on Zulip Yury G. Kudryashov (Jun 20 2020 at 18:34):

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

view this post on Zulip 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?

view this post on Zulip Oliver Nash (Jun 20 2020 at 18:37):

Hmm, well I can imagine other differences.

view this post on Zulip Yury G. Kudryashov (Jun 20 2020 at 18:45):

The theory of units has more simp lemmas etc.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jun 21 2020 at 04:28):

simp_rw will avoid the motive issue

view this post on Zulip 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: May 14 2021 at 07:19 UTC