# Zulip Chat Archive

## Stream: general

### Topic: arbitrary types for matrices

#### Chris Hughes (Jun 25 2019 at 12:16):

Currently the columns and rows of matrices can be indexed by an arbitrary fintype. However, the following two definitions in data.matrix are less general.

def row (w : m → α) : matrix m punit α | x y := w x def col (v : n → α) : matrix punit n α | x y := v y

I anticipate that it may be difficult to develop a more sophisticated matrix library in this generality, and that we should be generally be using `fin 1`

instead of `punit`

and `fin`

as part of the library. For example, if I want to concatenate matrices, the output type of this should probably be `fin (m + n)`

as opposed to `α ⊕ β`

or some arbitrary type with a proof it has the correct cardinality.

I also think the following two definitions should be made

@[reducible] def cvec (R : Type*) (m : ℕ) := matrix (fin m) (fin 1) R @[reducible] def rvec (R : Type*) (n : ℕ) := matrix (fin 1) (fin n) R

This is preferable to the current system where the canonical vectors are `fin n -> R`

, which aren't matrices, and can't be multiplied as easily.

Any comments?

#### Mario Carneiro (Jun 25 2019 at 12:20):

you could take an arbitrary element in a type, or an inhabited type

#### Chris Hughes (Jun 25 2019 at 12:29):

I don't follow.

#### Mario Carneiro (Jun 25 2019 at 12:30):

Ah, actually inhabited isn't even necessary

#### Mario Carneiro (Jun 25 2019 at 12:31):

You could simply generalize the type signature of row/col

#### Chris Hughes (Jun 25 2019 at 12:37):

I still don't follow. Where should I use this inhabited type?

#### Mario Carneiro (Jun 25 2019 at 12:49):

def row (w : m → α) : matrix m B α | x y := w x

#### Mario Carneiro (Jun 25 2019 at 12:50):

You can use `unique`

if you need to prove stuff about the sum of entries or something

#### Chris Hughes (Jun 25 2019 at 12:50):

Okay I could do that, but what about the more general question. Should I concatenate matrices on arbitrary types?

#### Mario Carneiro (Jun 25 2019 at 12:51):

That's tougher. I have serious reservations about doing anything nontrivial with dependent type families with nat args

#### Mario Carneiro (Jun 25 2019 at 12:52):

Something like the traditional type signature of vector append is DTT hell just waiting to happen

#### Keeley Hoek (Jun 25 2019 at 12:55):

`vector (n + m) = vector (m + n)`

and we're dead

#### Johan Commelin (Jun 25 2019 at 12:58):

One of the reasons why I pushed for matrices indexed by arbitrary types is so that we can have matrices indexed by a basis.

#### Johan Commelin (Jun 25 2019 at 12:59):

I think that might be a useful application to keep in mind when developing the library.

#### Johan Commelin (Jun 25 2019 at 13:00):

Even though we will soon have bases that are not sets, we still don't want bases to be indexed by `fin n`

all the time.

#### Reid Barton (Jun 25 2019 at 13:24):

I haven't thought about what the API ought to look like but I agree that in math it's quite often natural to consider matrices indexed by things other than `fin n`

.

#### Reid Barton (Jun 25 2019 at 13:26):

Though it doesn't qualify as "real math", problem A2 from last year's Putnam exam is a good example: a matrix whose rows and columns are indexed by the nonempty subsets of $\{1, 2, \ldots, n\}$.

#### Kevin Buzzard (Jun 25 2019 at 13:42):

Even though we will soon have bases that are not sets, we still don't want bases to be indexed by

`fin n`

all the time.

"Let ${e_1,e_2,\ldots,e_n}$ be a basis for $V\ldots$". Don't we say this all the time in 1st year algebra?

#### Chris Hughes (Jun 25 2019 at 13:43):

In maths it's always indexed by fin.

#### Bryan Gin-ge Chen (Jun 25 2019 at 13:51):

Lots of matrices in graph theory are indexed by elements of edge or vertex sets.

#### Reid Barton (Jun 25 2019 at 13:57):

The example I remember seeing in real math most recently was a $2^{n-1} \times 2^{n-1}$ matrix in which the rows were indexed by the basis elements of the exterior algebra of $k^{\oplus n}$ of even degree, and the columns were indexed by the basis elements of odd degree

#### Sebastien Gouezel (Jun 25 2019 at 13:57):

When doing representations it is also often indexed by the elements of a finite group (to construct the so-called "regular representation").

#### Alex J. Best (Jun 25 2019 at 14:13):

Ive not really thought about matrices indexed like this but there are many settings where this seems very natural in hindsight: Adjacency matrices of graphs or various intersection pairings in homology. Maybe this is a situation where type theory encourages us to make less arbitrary choices? After all the only reason I see for us to choose an order on the indices is to write the matrix on paper

#### Reid Barton (Jun 25 2019 at 14:20):

Or matrices for the differentials in cellular homology

#### Jeremy Avigad (Jun 25 2019 at 18:05):

AFAIK, the library with the most extensive linear algebra is SSReflect:

https://hal.inria.fr/hal-00805966/document

http://www.cs.cmu.edu/~amoertbe/papers/coqeal.pdf

Matrices are indexed by `fin n`

and lots of careful thought and subtlety is needed to cope with the usual DTT issues.

That is not to say that we can't do better with general index types. I don't know of anyone else who has tried it. Chris, do you see specific problems with the approach, or is it just a hunch that the added generality will hurt more than it will help?

#### Jeremy Avigad (Jun 25 2019 at 18:11):

By the way, the second paper promotes the "computational refinement" approach to computer algebra that Reid mentioned in an earlier post: start with the most natural mathematical definitions of your algebraic objects, use that as the theoretical reference, and then cook up better computational representations as needed. I agree that this is the right approach.

#### Kevin Buzzard (Jun 26 2019 at 10:24):

Does this general principle apply to glueing sheaves, or the Zassenhaus butterfly lemma? In The Rooster and The Butterfly, Assia argues that life is much easier if you make a large ambient group and make the groups you're interested in into subgroups of that group. However this does not feel to me like a natural mathematical definition. In glueing sheaves we've just run into an analogous issue -- we redefine "sheaf on U" to mean "sheaf on a larger space X containing every U we will ever care about". I understand the practical impliciations of making a mathematically weird definition which turns out to be a far more effective way of encoding the idea into type theory; indeed I tried to do it the "mathematically natural" way and it was very painful.

#### Chris Hughes (Jun 26 2019 at 10:31):

I think to be more accurate, "most natural mathematical definitions of your algebraic objects", should be substituted with "easiest definitions to write formal proofs with" in Jeremy's comment.

#### Mario Carneiro (Jun 26 2019 at 10:34):

I understand the practical impliciations of making a mathematically weird definition which turns out to be a far more effective way of encoding the idea into type theory; indeed I tried to do it the "mathematically natural" way and it was very painful.

In general, I think you have to be prepared to do this. Any time you decide "alright I'm going to rigidly transcribe this maths textbook" you find that it's actually really hard to stick to the plan, you end up with unidiomatic things, the proofs get bogged down and you generally have a bad time. I think that a little "formalization flexibility" is essential for effective use

#### Kevin Buzzard (Jun 26 2019 at 10:41):

"I think you have to be prepared to do this" -- here "this" is presumably "formalise in the way that Lean likes best" rather than "do it the mathematically natural way and endure the pain".

#### Mario Carneiro (Jun 26 2019 at 10:46):

Yes, although I would say that only about half of it is "what lean likes" and the other half is just general formalization stuff that you would need to do in any proof assistant

#### Kevin Buzzard (Jun 26 2019 at 10:58):

With the sheaf glueing thing I feel like if anyone wanted the mathematically natural way of doing it, they can go through the hell of formalising it themselves and then just prove it by using the DTT-natural proof.

Last updated: Aug 03 2023 at 10:10 UTC