**Matrix Representation
**For the purposes of this project, matrices will be represented by
lists of lists. To be more specific, a matrix will be a represented list in
which each element represents a row of the matrix. Each row in the
representation will be the list of elements in the corresponding row of the
matrix. The (i,j)-th element of a matrix is the j-th element in the i-th list in
the representation of the matrix.

Examples

a matrix with three rows and four columns and its representation

1 2 3 4

5 6 7 8 ((1 2 3 4) (5 6 7 8) (9 12 11 12))

9 10 11 12

a matrix with four rows and three columns and its representation

1 5 9

2 6 10 ((1 5 9) (2 6 10) (3 7 11) (4 8 12))

3 7 11

4 8 12

A matrix with *m* rows and *n* columns is said to
be an *m*-by-*n* matrix. This project will deal only with rectangular
matrices -- that is, matrices in which all rows have the same number of
elements. In an *m*-by-*n* matrix, all *m* rows contain exactly *n*
elements. The number of lists in the representation of a matrix is, of course,
the number of rows in the matrix. So, there are *m* lists in the
representation of an *m*-by-*n* matrix, and each of those lists has
exactly *n* elements.

By convention, we allow 0-by-0 matrices, but we do not
allow 0-by-*n* matrices or *n*-by-0 matrices where *n* is not
zero. That is, an *m*-by-*n* matrix exists if and only if neither *m*
nor *n* is zero or both *m* and *n* are zero.

A 0-by-0 matrix is represented by NIL (the empty list). One consequence of the convention that prohibits non-empty matrices with empty rows is that NIL cannot be a member of a non-empty list representing a matrix. However, the list ((NIL NIL) (NIL NIL) (NIL NIL)) represents a 3-by-2 matrix in which all elements have the value NIL. Any ACL2 atom or cons-pair can be an element of a matrix.

**Matrix Transpose
**The rows of a matrix are the columns of its transpose. That is,
the (j,i)-th element of the transpose of a matrix A is the (i,j)-th element of
A. In the above examples, the 3-by-4 matrix is the transpose of the 4-by-3
matrix, and vice versa.

**Requirements**

**matrix?**The formula (matrix? X) delivers something other than NIL if X represents a matrix and NIL if X does not represent a matrix.**num-rows**The formula (num-rows X) delivers the number of rows in the matrix represented by X.**num-cols**The formula (num-cols X) delivers the number of columns in the matrix represented by X.**transpose**The formula (transpose X) delivers the representation of the transpose of the matrix that X represents.

**Properties**

State the following theorems in ACL2 notation, and use "The Method" to
get ACL2 to prove at least one of them.

- The value delivered by (transpose X) is a matrix whenever X is a matrix.
- The number of rows in (transpose X) is the number of columns in X.
- The number of columns in (transpose X) is the number of rows in X.

**Performance**

Demonstrate that transpose can successfully deliver the transpose of a 400-by-400 matrix in a reasonable time (under a minute, say,
and you may be able to do much better than that), and of course without a
mechanical breakdown, such as a stack overflow.

Don't display the transpose of a large matrix. Just invoke the operation and extract a small piece to display. Don't enter the matrix by hand, either. Find some other way to generate the representation of a 400-by-400 matrix.

You may be interested to know that functions meeting the performance requirements can be written in either nested or tail recursive form. It is, of course, also possible to write functions in either nested or tail recursive form that fail to meet the performance requirements.