arbitrary types for matrices

Stream: general

[Chris Hughes]

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]

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

[Chris Hughes]

I don't follow.

[Mario Carneiro]

Ah, actually inhabited isn't even necessary

[Mario Carneiro]

You could simply generalize the type signature of row/col

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

You can use unique if you need to prove stuff about the sum of entries or something

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Keeley Hoek]

vector (n + m) = vector (m + n) and we're dead

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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]

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]

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]

In maths it's always indexed by fin.

[Bryan Gin-ge Chen]

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

[Reid Barton]

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]

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]

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]

Or matrices for the differentials in cellular homology

[Jeremy Avigad]

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]

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]

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]

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]

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]

"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]

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]

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.