Zulip Chat Archive

Stream: Is there code for X?

Topic: matrices over a ring are a ring


view this post on Zulip Aniruddh Agarwal (May 25 2020 at 22:38):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 22:39):

does apply_instance find it?

view this post on Zulip Aniruddh Agarwal (May 25 2020 at 22:40):

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

view this post on Zulip Alex J. Best (May 25 2020 at 22:40):

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

view this post on Zulip Mario Carneiro (May 25 2020 at 22:41):

ah, you are probably missing the decidable_eq assumption

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

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

view this post on Zulip Mario Carneiro (May 26 2020 at 03:18):

yes, I think

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

view this post on Zulip Mario Carneiro (May 26 2020 at 03:19):

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

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

view this post on Zulip Mario Carneiro (May 26 2020 at 03:19):

oh, the mathematician is wrong of course

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

view this post on Zulip Mario Carneiro (May 26 2020 at 03:20):

It's not, really

view this post on Zulip Mario Carneiro (May 26 2020 at 03:20):

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

view this post on Zulip Yury G. Kudryashov (May 26 2020 at 03:20):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 03:21):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 03:21):

that is, if you want to compute in a proof

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

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

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

view this post on Zulip Kenny Lau (May 26 2020 at 03:35):

maybe we need to modify norm_num again

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

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

view this post on Zulip Johan Commelin (May 26 2020 at 03:57):

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

view this post on Zulip Johan Commelin (May 26 2020 at 03:57):

Can we teach norm_num about repeated squaring?

view this post on Zulip Mario Carneiro (May 26 2020 at 03:57):

It already knows

view this post on Zulip Johan Commelin (May 26 2020 at 03:58):

Hmm, but why the pow_succ, in that case?

view this post on Zulip Mario Carneiro (May 26 2020 at 03:58):

norm_num only knows how to multiply numbers

view this post on Zulip Johan Commelin (May 26 2020 at 03:58):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 03:58):

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

view this post on Zulip Johan Commelin (May 26 2020 at 03:59):

So we need a simp-lemma pow_bit0?

view this post on Zulip Johan Commelin (May 26 2020 at 03:59):

Which is a first approximation to repeated squaring

view this post on Zulip Mario Carneiro (May 26 2020 at 03:59):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:00):

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

view this post on Zulip Johan Commelin (May 26 2020 at 04:00):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:00):

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

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:01):

maybe, but it might also make general use slower

view this post on Zulip Mario Carneiro (May 26 2020 at 04:01):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:02):

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

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

view this post on Zulip Johan Commelin (May 26 2020 at 04:03):

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:03):

no

view this post on Zulip Johan Commelin (May 26 2020 at 04:03):

Should there be?

view this post on Zulip Mario Carneiro (May 26 2020 at 04:04):

hard to say

view this post on Zulip Mario Carneiro (May 26 2020 at 04:04):

most simp lemmas seem to be useful in norm_num

view this post on Zulip Mario Carneiro (May 26 2020 at 04:04):

except possibly the ones about numbers

view this post on Zulip Johan Commelin (May 26 2020 at 04:05):

I mean the other way round

view this post on Zulip Johan Commelin (May 26 2020 at 04:05):

Some simp lemmas are maybe only useful for norm num

view this post on Zulip Johan Commelin (May 26 2020 at 04:05):

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

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

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:08):

If mul_assoc is not in the list, yes

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:10):

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

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

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

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

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

view this post on Zulip Mario Carneiro (May 26 2020 at 04:16):

It's still faster than rfl though

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

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

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