Introduction to Programming in ATS:
Prev	Chapter 11. Theorem-Proving in ATS/LF	Next

Constructing Proofs as Total Functions

Theorems are represented as types (or more accurately, props) in ATS/LF. For instance, the following prop states that integer multiplication is commutative:

{m,n:int}{p:int} MUL(m, n, p) -<prf> MUL(n, m, p)

Constructing a proof for a theorem in ATS/LF means implementing a total value (which is most likely to be a total function) of the type that is the encoding of the theorem in ATS/LF, where being total means being pure and terminating. Please note that this style of theorem-proving may seem rather peculiar to those who have never tried it before.

As a simple introductory example, let us first construct a proof function in ATS/LF that is given the following interface:

prfun mul_istot {m,n:int} (): [p:int] MUL(m, n, p)

The keyword prfun indicates that the interface is for a proof function (in contrast to a non-proof function). Note that mul_istot is declared to be of the following type (or more accurately, prop):

{m,n:int} () -<prf> [p:int] MUL(m, n, p)

which essentially states that integer multiplication is a total function: Given any two integers m and n, there exists an integer p such that m, n and p are related according to the structurally inductively defined relation MUL. The following code gives an implementation of mul_istot:

primplement
mul_istot{m,n}() = let
//
prfun istot
  {m:nat;n:int} .<m>. (): [p:int] MUL(m, n, p) =
  sif m > 0 then MULind(istot{m-1,n}()) else MULbas()
// end of [istot]
//
in
  sif m >= 0 then istot{m,n}() else MULneg(istot{~m,n}())
end // end of [mul_istot]

Note that the keyword primplement (instead of implement) initiates the implementation of a proof. The inner proof function istot encodes a proof showing that there exists an integer p for any given natural number m and integer n such that m, n and p are related (according to MUL). The keyword sif is used for forming a conditional (proof) expression in which the test is a static expression. The proof encoded by istot proceeds by induction on m; if m > 0 holds, then there exists an integer p1 such that m-1, n and p1 are related by induction hypothesis (on m-1) and thus m, n and p are related for p = p1+n according to the rule encoded by MULind; if m = 0, then m, n and p are related for p = 0. The proof encoded by the implementation of mul_istot goes like this: if m is a natural number, then the lemma proven by istot shows that m, n and some p are related; if m is negative, then the same lemma shows that ~m, n and p1 are related for some integer p1 and thus m, n and p are related for p = ~p1 according to the rule encoded by MULneg.

As another example of theorem-proving in ATS/LF, a proof function of the name mul_isfun is given as follows:

prfn mul_isfun
  {m,n:int}{p1,p2:int}
(
  pf1: MUL(m, n, p1), pf2: MUL(m, n, p2)
) : [p1==p2] void = let
  prfun isfun
    {m:nat;n:int}{p1,p2:int} .<m>.
  (
    pf1: MUL(m, n, p1), pf2: MUL(m, n, p2)
  ) : [p1==p2] void =
    case+ pf1 of
    | MULind(pf1prev) => let
        prval MULind(pf2prev) = pf2 in isfun (pf1prev, pf2prev)
      end // end of [MULind]
    | MULbas() => let
        prval MULbas() = pf2 in ()
      end // end of [MULbas]
  // end of [isfun]
in
  case+ pf1 of
  | MULneg(pf1nat) => let
      prval MULneg(pf2nat) = pf2 in isfun (pf1nat, pf2nat)
    end // end of [MULneg]
  | _ (*non-MULneg*) =>> isfun (pf1, pf2)
end // end of [mul_isfun]

The keyword prfn is used for defining a non-recursive proof function, and the keyword prval for introducing bindings that relate names to proof expressions, that is, expressions of prop-types. As far as pattern matching exhaustiveness is concerned, prval is equivalent to val+ (as proofs cannot contain any effects such as failures of pattern matching).

What mul_isfun proves is that the relation MUL is functional on its first two arguments: If m, n and p1 are related according to MUL and m, n and p2 are also related according to MUL, then p1 and p2 are equal. The statement is first proven by the inner proof function isfun under the assumption that m is a natural number, and then the assumption is dropped. Let us now take a look at the first matching clause in the body of isfun. If the clause is chosen, then pf1 matches the pattern MULind(pf1prev) and thus pf1prev is of the type MUL(m1, n1, q1) for some natural number m1 and integer n1 and integer p1 such that m=m1+1, n=n1, and p1=q1+n1. This means that pf2 must be of the form MULind(pf2prev) for some pf2prev of the type MUL(m2, n2, q2) such that m2+1=m, n2=n and p2=q2+n2. By calling isfun on pf1prev and pf2prev, which amounts to invoking the induction hypothesis on m-1, we establish q1=q2, which implies p1=p2. The second matching clause in the body of isfun can be readily understood, which corresponds to the base case in the inductive proof encoded by isfun.

Prev	Home	Next
Theorem-Proving in ATS/LF	Up	Example: Distributivity of Multiplication