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]
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]
// 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 //
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.