Introduction to Programming in ATS:
PrevChapter 11. Theorem-Proving in ATS/LFNext

Example: Commutativity of Multiplication

The commutativity of multiplication means that the following equation holds 

m * n = n * m

for m and n ranging over integers. A direct encoding of this equation is given by the following (proof) function interface: 

//
prfun
mul_commute{m,n:int}{p:int}(MUL(m, n, p)): MUL(n, m, p)
//

An implementation of mul_commute is given as follows: 

primplmnt
mul_commute
  {m,n}{p}(pf0) = let
//
prfun
auxnat
{m:nat}
{p:int} .<m>.
(
pf: MUL(m, n, p)
) : MUL(n, m, p) =
(
  case+ pf of
  | MULbas() => mul_nx0_0{n}()
  | MULind(pf1) =>
      mul_distribute(auxnat(pf1), mul_nx1_n{n}())
    // end of [MULind]
) (* end of [auxnat] *)
//
in
//
sif
m >= 0
then auxnat(pf0)
else let
  prval MULneg(pf1) = pf0 in mul_neg_2(auxnat(pf1))
end // end of [else]
//
end // end of [mul_commute]

where the following proof functions are called: 

//
prfun
mul_nx0_0{n:int}(): MUL(n, 0, 0) // n * 0 = 0
//
prfun
mul_nx1_n{n:int}(): MUL(n, 1, n) // n * 1 = n
//
prfun
mul_neg_2
  {m,n:int}{p:int}(MUL(m,n,p)): MUL(m,~n,~p) // m*(~n) = ~(m*n)
//

The inner function auxnat encodes a straighforward proof based on mathematical induction that establishes the following equation: 

m * n = n * m

for m ranging over natural numbers and n ranging over integers. The function mul_commute can then be implemented immediately based on auxnat.

PrevHomeNext
Example: Distributivity of MultiplicationUpAlgebraic Datasorts