## Stream: Is there code for X?

### Topic: matrices over a ring are a ring

#### Aniruddh Agarwal (May 25 2020 at 22:38):

I can't find the statement that matrices over a ring form a ring in mathlib

#### Mario Carneiro (May 25 2020 at 22:39):

does apply_instance find it?

#### Aniruddh Agarwal (May 25 2020 at 22:40):

I don't know what apply_instance is, but I'm looking it up now

#### Alex J. Best (May 25 2020 at 22:40):

https://leanprover-community.github.io/mathlib_docs/data/matrix/basic.html#matrix.ring

#### Mario Carneiro (May 25 2020 at 22:41):

ah, you are probably missing the decidable_eq assumption

#### Mario Carneiro (May 25 2020 at 22:42):

In mathlib you don't usually explicitly reference a proof that says that some type is a ring, you let typeclass inference find it for you and just use * and mul_add and so on without reference to this instance

#### Johan Commelin (May 26 2020 at 03:17):

Mario Carneiro said:

ah, you are probably missing the decidable_eq assumption

Do we want to keep that assumption?

yes, I think

#### Mario Carneiro (May 26 2020 at 03:18):

to a mathematician it's only ever instantiated at fin n so the decidable assumption is no problem

#### Mario Carneiro (May 26 2020 at 03:19):

also I imagine people might want to actually compute with the matrix type

#### Johan Commelin (May 26 2020 at 03:19):

Hmm... the reason we generalized to arbitrary fintypes is exactly because we could have random fintypes showing up as index type for a basis.

#### Mario Carneiro (May 26 2020 at 03:19):

oh, the mathematician is wrong of course

#### Johan Commelin (May 26 2020 at 03:20):

But is this implementation efficient for computations? I guess we'll want sparse_matrix and fast_matrix and whatever, once we start computing

It's not, really

#### Mario Carneiro (May 26 2020 at 03:20):

I think this is a function on fin n? That's got pretty poor access overhead

#### Yury G. Kudryashov (May 26 2020 at 03:20):

If you just want to compute a simple expression with $2\times 2$ matrices then any implementation is efficient.

#### Mario Carneiro (May 26 2020 at 03:21):

If you want to compute on $2\times 2$ matrices a it is better to have a good defeq and "force" the results using rfl

#### Mario Carneiro (May 26 2020 at 03:21):

that is, if you want to compute in a proof

#### Mario Carneiro (May 26 2020 at 03:22):

if you want to compute in #eval then anything is efficient but you will probably be looking at bigger matrices

#### Mario Carneiro (May 26 2020 at 03:27):

This seems to work fairly well:

import data.matrix.notation

def foo : matrix (fin 3) (fin 3) ℤ := ![![1,1,1],![1,0,1],![1,1,1]]

def to_list {α m n} (M : matrix (fin m) (fin n) α) : list (list α) :=
list.of_fn (λ i, list.of_fn (M i))

#eval to_list (foo ^ 10)


#### Mario Carneiro (May 26 2020 at 03:28):

I suspect it doesn't scale the way it should though because it doesn't cache intermediate values

#### Kenny Lau (May 26 2020 at 03:35):

maybe we need to modify norm_num again

#### Mario Carneiro (May 26 2020 at 03:41):

Looking at the contents of data.matrix.notation, it seems like there are enough simp lemmas that norm_num should Just Work

#### Mario Carneiro (May 26 2020 at 03:45):

Ah, simp gets stuck on the power operation. But still it gets pretty close:

import data.matrix.notation

def foo : matrix (fin 3) (fin 3) ℤ := ![![1,1,1],![1,0,1],![1,1,1]]

example : foo ^ 10 = ![![9136, 6688, 9136], ![6688, 4896, 6688], ![9136, 6688, 9136]] :=
by simp [pow_succ]; norm_num [foo]


#### Johan Commelin (May 26 2020 at 03:57):

@Mario Carneiro norm_num does cache intermediate results, does it?

#### Johan Commelin (May 26 2020 at 03:57):

Can we teach norm_num about repeated squaring?

#### Johan Commelin (May 26 2020 at 03:58):

Hmm, but why the pow_succ, in that case?

#### Mario Carneiro (May 26 2020 at 03:58):

norm_num only knows how to multiply numbers

#### Johan Commelin (May 26 2020 at 03:58):

It should compute foo ^ 2, foo ^ 4, foo ^ 8 and then foo ^ 8 * foo ^ 2.

#### Mario Carneiro (May 26 2020 at 03:58):

simp knows how to multply other things but it doesn't know repeated squaring

#### Johan Commelin (May 26 2020 at 03:59):

So we need a simp-lemma pow_bit0?

#### Johan Commelin (May 26 2020 at 03:59):

Which is a first approximation to repeated squaring

#### Mario Carneiro (May 26 2020 at 03:59):

norm_num also doesn't do common subexpression elimination before trying to evaluate

#### Mario Carneiro (May 26 2020 at 04:00):

simp can only set up the goal here as foo * foo * ... * foo in some associativity

#### Johan Commelin (May 26 2020 at 04:00):

But it should be able to set it up as something smarter

#### Mario Carneiro (May 26 2020 at 04:00):

not really, what expression should it produce that is better?

#### Johan Commelin (May 26 2020 at 04:01):

Mario Carneiro said:

norm_num also doesn't do common subexpression elimination before trying to evaluate

Would it help to teach norm_num about this?

#### Mario Carneiro (May 26 2020 at 04:01):

maybe, but it might also make general use slower

#### Mario Carneiro (May 26 2020 at 04:01):

Right now norm_num is mostly relying on simp to give it a clean input

#### Mario Carneiro (May 26 2020 at 04:02):

it would have to orchestrate more of the process in order to do these things

#### Mario Carneiro (May 26 2020 at 04:03):

Plus, with the code above simp will hand a term like foo * (foo * (foo * ...)) anyway so there is no CSE to be had

#### Johan Commelin (May 26 2020 at 04:03):

Is there a simp-set that's specifically for norm_num?

no

Should there be?

hard to say

#### Mario Carneiro (May 26 2020 at 04:04):

most simp lemmas seem to be useful in norm_num

#### Mario Carneiro (May 26 2020 at 04:04):

except possibly the ones about numbers

#### Johan Commelin (May 26 2020 at 04:05):

I mean the other way round

#### Johan Commelin (May 26 2020 at 04:05):

Some simp lemmas are maybe only useful for norm num

#### Johan Commelin (May 26 2020 at 04:05):

But you don't want them in a random simp call

#### Mario Carneiro (May 26 2020 at 04:05):

I suppose there are some lemmas that you probably don't want to use unless you are trying to normalize

#### Johan Commelin (May 26 2020 at 04:07):

But if simp only [pow_bit0] turns this into foo ^ 5 * foo ^ 5, then norm_num could apply CSE, right?

#### Mario Carneiro (May 26 2020 at 04:08):

If mul_assoc is not in the list, yes

#### Mario Carneiro (May 26 2020 at 04:10):

Also, maybe the CSE should be on the simp side; the internal function here is simplify.bottom_up or something like that, which calls a tactic on every subterm. It knows enough at that stage to potentially apply CSE, which is especially important if the term is dag-like and highly duplicated

#### Mario Carneiro (May 26 2020 at 04:10):

The lean side can't do much about dag-like terms

#### Johan Commelin (May 26 2020 at 04:11):

I imagine simp-lemmas that turn foo ^ 10 into

cache (foo * foo) *
( cache ( (foo * foo) * (foo * foo) ) *
(foo * foo) * (foo * foo) )


where cache := id is a wrapper that tells norm_num to store a result for later.

#### Mario Carneiro (May 26 2020 at 04:12):

maybe better to put the cache on both sides, indicating both which to cache and which to look in the cache for

#### Mario Carneiro (May 26 2020 at 04:14):

But keep in mind that norm_num still hasn't triggered at this point. Once it is reduced to a bunch of multiplies, simp[foo] unfolds it to literals, and then all the matrix simp lemmas trigger until it is a bunch of cells like

(… +
(… +
(… +
(… + (… + (1 + (1 + 1))) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1)))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1)))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1)))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))))))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1)))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) +
(1 + (1 + 1) + (1 + (1 + 1)) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))))) +
(1 + (1 + 1) + (1 + 1 + (1 + (1 + 1))) + (1 + (1 + 1) + (1 + 1 + (1 + (1 + 1)))) +
...


#### Mario Carneiro (May 26 2020 at 04:15):

It is only at this point that norm_num sees something with numerals that it can evaluate

#### Mario Carneiro (May 26 2020 at 04:16):

It's still faster than rfl though

#### Johan Commelin (May 26 2020 at 04:17):

I see, but still the cache thing might help, maybe? (And your suggestion of reusing cache to flag a look-up seems good.)

#### Mario Carneiro (May 26 2020 at 04:18):

I mean the optimal solution is just to do like Kenny says and bake matrix operations into norm_num

#### Mario Carneiro (May 26 2020 at 04:19):

which might not even be so bad if norm_num grows some extensibility

Last updated: May 16 2021 at 05:21 UTC