# Example: Safe Matrix Subscripting

Internally, a matrix of the dimension m by n is represented as an array of the size m*n. For matrix subscripting, we need to implement a function template of the following interface:

```fun{
a:t@ype
} matrix_get
{m,n:int}{i,j:nat | i < m; j < n}
(A: arrayref (a, m*n), col: int n, i: int i, j: int j): (a)
// end of [matrix_get]
```

Assume that the matrix is represented in the row-major style. Then the element indexed by i and j in the matrix is the element indexed by i*n + j in the array that represents the matrix, where i and j are natural numbers less than m and n, respectively. However, the following implementation fails to pass typechecking:

```implement
{a}(*tmp*)
matrix_get (A, n, i, j) = A[i*n+j] // it fails to typecheck!!!
```

The simple reason for this failure is due to the ATS constraint solver not being able to automatically verify that i*n+j is a natural number strictly less than m*n. An implementation of matrix_get that typechecks can be given as follows:

```implement
{a}(*tmp*)
matrix_get
{m,n}{i,j}
(A, n, i, j) = let
//
val (pf | _in_) = imul2 (i, n)
//
prval ((*void*)) = mul_elim(pf)
prval ((*void*)) = mul_nat_nat_nat(pf)
prval ((*void*)) = mul_gte_gte_gte{m-1-i,n}()
//
in
A[_in_+j]
end // end of [matrix_get]
```

where the functions called in the body of matrix_get are assigned the following interfaces:

```//
fun
imul2{i,j:int}
(int i, int j):<> [ij:int] (MUL(i, j, ij) | int ij)
//
prfun
mul_elim
{i,j:int}{ij:int} (pf: MUL(i, j, ij)): [i*j==ij] void
//
prfun
mul_nat_nat_nat
{i,j:nat}{ij:int} (pf: MUL(i, j, ij)): [ij >= 0] void
//
prfun
mul_gte_gte_gte
{m,n:int | m >= 0; n >= 0} ((*void*)): [m*n >= 0] void
//
```

Assume that m and n are natural numbers and i and j are natural numbers less than m and n, respectively. The proof code employed in the implementation of matrix_get to show i*n+j < m*n proves (m-1-i)*n >= 0, which clearly implies m*n >= i*n+n > i*n+j.

Note that there are a variety of proof functions declared in arith_prf.sats for helping prove theorems involving arithmetic operations. For examples of proof construction in ATS, please find the implementation of some of these proof functions in arith_prf.dats.

The entirety of the above presented code is available on-line.