# 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 `subsingleton`

s!

#### 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 `subsingleton`

s 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 `unit`

s 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 `unit`

s. 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: May 14 2021 at 07:19 UTC