Introduction to Programming in ATS:
<<< PreviousTheorem-Proving in ATS/LFNext >>>

Example: Proving Distributivity of Multiplication

The distributivity of multiplication over addition means that the following equation holds 

m * (n1 + n2) = m * n1 + m * n2

for m, n1 and n2 ranging over integers. Clearly, a direct encoding of the equation is given by the following (proof) function interface: 

extern
prfun mul_distribute {m:int} {n1,n2:int} {p1,p2:int}
  (pf1: MUL (m, n1, p1), pf2: MUL (m, n2, p2)): MUL (m, n1+n2, p1+p2)
// end of [mul_distribute]

Plainly speaking, the encoding states that the product of m and (n1+n2) is p1+p2 if the product of m and n1 is p1 and the product of m and n2 is p2. An implementation of mul_distribute is given as follows: 

implement
mul_distribute
  {m} {n1,n2} {p1,p2} (pf1, pf2) = let
  prfun aux
    {m:nat}
    {n1,n2:int}
    {p1,p2:int}
    .<m>. (
    pf1: MUL (m, n1, p1), pf2: MUL (m, n2, p2)
  ) : MUL (m, n1+n2, p1+p2) =
    case+ (pf1, pf2) of
    | (MULbas (), MULbas ()) => MULbas ()
    | (MULind pf1, MULind pf2) => MULind (aux (pf1, pf2))
  // end of [aux]
in
  sif m >= 0 then
    aux (pf1, pf2)
  else let
    prval MULneg (pf1) = pf1
    prval MULneg (pf2) = pf2
  in
    MULneg (aux (pf1, pf2))
  end
end // end of [mul_distribute]

In essence, the inner function aux encodes a straighforward proof based on mathematical induction that establishes the following equation: 

m * (n1 + n2) = m * n1 + m * n2

for m ranging over natural numbers and n1 and n2 ranging over integers. The function mul_distribute can then be implemented immediately based on aux.

<<< PreviousHomeNext >>>
Constructing Proofs as Total FunctionsUpDatasorts