matrices over a ring are a ring

Stream: Is there code for X?

[Aniruddh Agarwal]

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

[Mario Carneiro]

does apply_instance find it?

[Aniruddh Agarwal]

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

[Alex J. Best]

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

[Mario Carneiro]

ah, you are probably missing the decidable_eq assumption

[Mario Carneiro]

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]

Mario Carneiro said:

ah, you are probably missing the decidable_eq assumption

Do we want to keep that assumption?

[Mario Carneiro]

yes, I think

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

oh, the mathematician is wrong of course

[Johan Commelin]

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

[Mario Carneiro]

It's not, really

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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]

that is, if you want to compute in a proof

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kenny Lau]

maybe we need to modify norm_num again

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

Can we teach norm_num about repeated squaring?

[Mario Carneiro]

It already knows

[Johan Commelin]

Hmm, but why the pow_succ, in that case?

[Mario Carneiro]

norm_num only knows how to multiply numbers

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

So we need a simp-lemma pow_bit0?

[Johan Commelin]

Which is a first approximation to repeated squaring

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

maybe, but it might also make general use slower

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

no

[Johan Commelin]

Should there be?

[Mario Carneiro]

hard to say

[Mario Carneiro]

most simp lemmas seem to be useful in norm_num

[Mario Carneiro]

except possibly the ones about numbers

[Johan Commelin]

I mean the other way round

[Johan Commelin]

Some simp lemmas are maybe only useful for norm num

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

If mul_assoc is not in the list, yes

[Mario Carneiro]

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]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

It's still faster than rfl though

[Johan Commelin]

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]

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

[Mario Carneiro]

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