Introduction to Programming in ATS:
PrevChapter 12. Programming with Theorem-ProvingNext

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.

PrevHomeNext
Programming with Theorem-ProvingUpSpecifying with Enhanced Precision