One of the atomic types available in Nuprl is the type integer, called int. The availability of integers as an atomic type allows one to express a great deal of elementary number theory without much effort. The type int comes equipped with an induction form so that one can inductively define functions from integers to integers. In this section we illustrate how some number--theoretic predicates and functions can be defined in Nuprl and how number--theoretic theorems are stated.
We begin this section with an example of a simple theorem which will be proved in chapter 4; we use this theorem to review how one enters theorems in the system. The theorem asserts that for every pair of integers one can find an integer whose value is 0 if the first of the original pair of integers is less than the second and whose value is 1 if the first of the original pair of integers is not less that the second. In this statement there are a pair of quantifiers; the first is universal and the second is existential. Accordingly we need the definitions for universal quantifiers and existential quantifiers from figure . To state the theorm in Nuprl , one would first create a name and place for the theorem using the commands discussed in section 3.2. Then the theorem would be viewed and finally the text editor would be invoked by clicking R on the mouse in <main proof goal>. Once in the text editor the first symbols typed would be >>; after this the text of the theorem can be typed. At this stage the definition all2 is needed. We use it by first typing ; this will put the cursor in the command window with the I> prompt. Now one types all2 followed by a carriage return. The definition will be instantiated in the text editor. The appearance of the definition template will be all <var>,<var>:<type>.<prop>. The variables x and y can now be entered as the first two parameters, and int can be entered as the third parameter. The body of this universally quantified statement is an existentially quantified statement. The last parameter, <prop>, in the definition is instantiated by invoking the definition for some. The first two arguments of this quantifier can be filled in as before. The body of the inner quantified statement is a conjunction of the two conditions appearing in the statement of the theorem and can be expressed using the built--in relation < between integers and the definitions for conjunction and negation. The final appearance of the theorem is as follows.
>>all x,y:int. some z:int. (x<y => z=0) & (~x<y => z= 1)This is a theorem whose proof will embody some computational content; the existence proof will involve a procedure which computes z, given x and y.
The following definitions suggest what some standard number theory looks like in Nuprl . We first define the predicate divides using the (built--in) mod function.
divides(<n>:int,<m>:int) == ( <m> mod <n> = 0 in int)The next definition defines the predicate prime on integers.
prime(<n:int>) == (1 < <n>) & all k:int. ( (0 < k) & (<n> mod k = 0 in int) ) => (k=1 in int) | (k=<n> in int)Now these number--theoretic predicates can be used in conjunction with the logic definitions to state theorems in number theory in the following fashion.
>> all n:int. prime(n) | ~prime(n) >> all n:int. some p:int. n<p & prime(p)In stating number--theoretic propositions we come across our first examples of Nuprl theorems that have manifestly interesting computational content. The Nuprl system can extract the procedure from the proof. If we call the theorem t, then
\n.(term_of(t)(n))is a function which takes a natural number to a prime which is greater than it, where the function term_of is the system function that performs function extraction . Similarly the proof of the first theorem above will involve giving a decision procedure for primality.
Another interesting theorem one can state in Nuprl is the remainder theorem :
>>all x:int. all y: int. some q:int. some r:int. (y = (q*x + r) in int) & (0 <= r < x).We assume that the term (0 <= r < x) has been defined to have its usual meaning via a definition. Once again a proof would give rise to an algorithm for finding the quotient and remainder resulting from dividing two integers, and the corresponding function would be extracted by the system. This illustrates, in a very simple setting, the use of Nuprl as a program synthesis tool.