I have so far presented several formal proofs in ATS. However, constructing such formal proofs is at most a secondary issue in ATS. If I compare ATS with theorem-proving systems such as Isabelle and Coq, I would like to state emphatically that the design for theorem-proving in ATS takes a fundamentally different view of theorem-proving. In particular, theorem-proving in ATS does not take a foundational approach that establishes the validity of a theorem by reducing it to the validity of a minimal set of axioms and rules. Instead, theorem-proving in ATS is mostly done in a semi-formal manner and its primary purpose is to greatly diminish the chance of a programmer making use of incorrect assumptions or claims. In this regard, theorem-proving in ATS is rather similar to contructing informal paper-and-pencil proofs (in mathematics and elsewhere). I refer to this style of theorem-proving in ATS as being programmer-centric. In order to allow the reader to obtain a more concrete feel as to what this style of theorem-proving is like, I present in the rest of this section a simple but telling example of programmer-centric theorem-proving.
Suppose we are to prove that the square of any rational number cannot equal 2. Note that this statement is a bit weaker than the one stating that the square root of 2 is irrational as the latter assumes the very existence of the square root of 2. Let us first sketch an informal proof as follows.
Suppose (m/n)2=2 for some positive numbers m and n. Clearly, this means (m)2=2(n)2, implying m being an even number. Let m=2m2. We have (2m2)2=2(n)2, implying (n/m2)2=2. Clearly, m > n > m2 holds. If we assume that m is the least positive number satisfying (m/n)2=2 for some n, then a contradiction is reached as n satisfies the same property. Therefore, there is no rational number whose square equals 2. Clearly, this proof still holds if the number 2 is replaced with another prime number.
The primary argument in the above informal proof can be encoded in ATS as follows:
// extern prfun mylemma_main {m,n,p:int | m*m==p*n*n}(PRIME(p)): [m2:nat | n*n==p*m2*m2] void // primplmnt mylemma_main {m,n,p}(pfprm) = let prval pfeq_mm_pnn = eqint_make{m*m,p*n*n}() prval () = square_is_nat{m}() prval () = square_is_nat{n}() prval () = lemma_PRIME_param(pfprm) prval pfmod1 = lemma_MOD0_intr{m*m,p,n*n}() prval pfmod2 = mylemma1{m,p}(pfmod1, pfprm) prval [m2:int] EQINT() = lemma_MOD0_elim(pfmod2) prval EQINT() = pfeq_mm_pnn prval () = __assert{p}{p*m2*m2,n*n}() where { extern prfun __assert{p:pos}{x,y:int | p*x==p*y}(): [x==y] void } (* end of [where] *) // end of [prval] in #[m2 | ()] end // end of [mylemma_main] //
Given two integers m and p, MOD0(m,p) means that m equals the product of p and q for some natural number q. This meaning is encoded into the following two proof functions:
// prfun lemma_MOD0_intr{m,p,q:nat | m==p*q}(): MOD0(m, p) // prfun lemma_MOD0_elim{m,p:int}(MOD0(m, p)): [q:nat] EQINT(m, p*q) //
// prfun lemma_PRIME_param{p:int}(PRIME(p)): [p >= 2] void // prfun mylemma1{n,p:int}(MOD0(n*n, p), PRIME(p)): MOD0(n, p) //
One may find that the following declaration in the implementation of mylemma_main looks mysterious:
Note that pfeq_mm_pnn is of the prop EQINT(m*m, p*(n*n)). Also, m equaling p*m2 for some natural number m2 is available when the above declaration is typechecked. This means that the equality between (p*m2)2 and p*(n)2 is added into the current store of (static) assumptions after the above declaration is typechecked.Please find on-line the entirety of an encoded proof showing that there exists no rational number whose square equals 2.