Programmer-Centric Theorem-Proving

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] //

The interface for mylemma_main states that (m)2=p(n)2 implies (n)2=p(m2)2 for some natural number m2.

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) //

where EQINT is a dataprop declared as follows:

dataprop EQINT(int, int) = {x:int} EQINT(x, x)

Given two integers x and y, EQINT(x, y) simply means that x equals y. Also, the function eqint_make is assgined the interface below:

prfun eqint_make{x,y:int | x == y}((*void*)): EQINT (x, y)

Given an integer p, PRIME(p) means that p is a prime number. The following two proof functions are called in the above implementation of mylemma_main:

// 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) //

The proof function mylemma1 encodes a proposition stating that p divides n if p divides the square of n and p is also a prime number. I give no implementation of mylemma1 as I see the encoded proposition to be obviously true. Certainly, this is a kind of programmer-centric judgment.

One may find that the following declaration in the implementation of mylemma_main looks mysterious:

  prval EQINT() = pfeq_mm_pnn

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.