Z3: express linear algebra properties

Question

I would like to prove properties of expressions involving matrices and vectors (potentially large size, but size is fixed).

For example I want to prove that the outcome of an expression is a diagonal matrix or a triangular matrix, or it is positive definite, ...

To that end I'd like encode well known properties and identities from linear algebra, such as:

||x + y|| <= ||x|| + ||y||
(A * B) * C = A * (B * C)
det(A+B) = det(A) + det(B)
Tr(zA) = z * Tr(A)
(I + AB) ^ (-1) = I - A(I + BA) ^ (-1) * B
...

I have attempted to implement this in Z3. But even for simple properties it returns unknown or times out. I've tried with array theory and quantifiers.

I'd like know if this problem can be solved with an SMT solver or is it not suited for these kind of problems? Could you give a hint by giving a small example?

Answer 1

You can certainly use Z3 to do this.

I have constructed a small example here, which defines the identity matrix and what it means to be a diagonal matrix, and then proves that the identity matrix is diagonal.

So, it is definitely possible to do this kind of work in Z3. Though you may find you have a better time using a tool built on top of Z3 that has more interactive proving features, such as Dafny or F*.