Theorems are represented as types (or more accurately, props) in ATS/LF. For instance, the following prop states that integer multiplication is commutative:
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:
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): 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]
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]
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.