In chapter 3 simple results about
integers were stated; now a simple number--theoretic
argument will be developed.
Our goal is to prove that every nonnegative
integer x has an integer square root, which we
define to be that
integer y such that 
.
From the proof we will derive
an integer square root function called sqrt.
The following Nuprl statement poses the computational problem that we want to solve.
>> all x:int. x>=0 => some y:int. y*y <= x < (y+1)*(y+1)
A proof of this statement in Nuprl must be constructive because the constructive connectives and quantifiers defined in chapter 3 are used to state the problem; hence the proof will implicitly contain a method for computing square roots. We will use the proof to define the square root function. Before looking at the formal proof, however, let us consider an informal constructive proof.
We clearly want to proceed by induction, because one
can build the root of x from a root y0 of x-1
by testing
whether 
If this inequality holds then y0 is also the root
of x; if it does not then 
is the root of
x. Therefore we
introduce x and then perform induction on
x (the Nuprl
rule for this being elim x).
Integer induction generally involves three proof obligations:
one for downward induction, to establish the result for negative
numbers, one for the base case, x=0, and one for the upward case of
the positive integers. For this proof the downward case is trivial
because x is assumed to be nonnegative.
The base case is also trivial
because for x=0 we must take y to be 0.
We are left with the upward induction
case, for which the induction assumption is
We know 0<x because we are in the upward case,
so we can prove 
That allows us to conclude that
We want to examine this y explicitly so that we can
compare 
to x, so we
choose y0 as a witness for the some quantifier.
(This will be done in Nuprl
by using elim.)
Once we have y0 we can do a case
analysis on whether or not 
.
We would like to invoke the ``trichotomy '' rule,
and then observe that the first case is impossible so that we only need to consider
In the first case y0 is the root and in the last case y0+1 is.
In the snapshots which follow the preceding informal argument is formalized in Nuprl . The first snapshot shows the result of the first introduction rule applied to the statement of the theorem.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |# top | |>> all x:int. x>=0 => some y:int. y*y<= x <(y+1)* | | (y+1) | | | |BY intro | | | |1# 1. x:(int) | | >> ( x>=0 => some y:int. y*y<= x <(y+1)*(y+1) ) | | | |2* >> (int) in U1 | `----------------------------------------------------'
The new h part of the rule shown in the next snapshot directs the refinement editor to label the new hypothesis with h. Recall that when x is an integer elim x is the refinement rule for induction.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |# top 1 | |1. x:(int) | |>> ( x>=0 => some y:int. y*y<= x <(y+1)*(y+1) ) | | | |BY elim x new h | | | |1# 1. x:(int) | | 2. x<0 | | 3. h:( x+1>=0 => some y:int. y*y<= x+1 <(y+1)* | | (y+1)) | | >> ( x>=0 => some y:int. y*y<= x <(y+1)*(y+1) ) | | | |2# 1. x:(int) | | >> ( 0>=0 => some y:int. y*y<= 0 <(y+1)*(y+1) ) | | | |3# 1. x:(int) | | 2. 0<x | | 3. h:( x-1>=0 => some y:int. y*y<= x-1 <(y+1)* | | (y+1)) | | >> ( x>=0 => some y:int. y*y<= x <(y+1)*(y+1) ) | `----------------------------------------------------'
We now introduce the fact that x-1>=0 in order to use the induction hypothesis.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |# top 1 3 1 | |1. x:(int) | |2. 0<x | |3. h:( x-1>=0 => some y:int. y*y<= x-1 <(y+1)*(y+1))| |4. (x>=0) | |>> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY seq x-1>=0 | | | |1* 1. x:(int) | | 2. 0<x | | 3. h:( x-1>=0 => some y:int. y*y<= x-1 <(y+1)* | | (y+1)) | | 4. (x>=0) | | >> x-1>=0 | | | |2# 1. x:(int) | | 2. 0<x | | 3. h:( x-1>=0 => some y:int. y*y<= x-1 <(y+1)* | | (y+1)) | | 4. (x>=0) | | 5. x-1>=0 | | >> (some y:int. y*y<= x <(y+1)*(y+1)) | `----------------------------------------------------'
In the next step we want to obtain the consequent of
hypothesis 3, the induction hypothesis. Since we know x-1>=0 the first subgoal
will be immediate.
The interesting part is subgoal 2, in which
the consequent is now available. (From now on we will
elide some of the hypotheses
by substituting ``... '' for them.
)
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |# top 1 3 1 2 | |1. x:(int) | |2. 0<x | |3. h:( x-1>=0 => some y:int. y*y<= x-1 <(y+1)*(y+1))| |4. (x>=0) | |5. x-1>=0 | |>> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY elim h new r | | | |1* 1...5. | | >> (x-1>=0) | | | |2# 1...5. | | 6. r:(some y:int. y*y<= x-1 <(y+1)*(y+1)) | | >> (some y:int. y*y<= x <(y+1)*(y+1)) | `----------------------------------------------------'
Now we choose a name, y0, for the witness of the existential quantifier in line 6. As a result we are also required to supply a name for the fact known about y0, namely hh.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |* top 1 3 1 2 2 | |1. x:(int) | |2. 0<x | |3. h:( x-1>=0 => some y:int. y*y<= x-1 <(y+1)*(y+1))| |4. (x>=0) | |5. x-1>=0 | |6. r:(some y:int. y*y<= x-1 <(y+1)*(y+1)) | |>> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY elim r new y0,hh | | | |1# 1...6. | | 7. y0:(int) | | 8. hh:( y0*y0<= x-1 <(y0+1)*(y0+1)) | | 9. r=<y0,hh> in (some y:int. y*y<= x-1 <(y+1)*(y+| | 1)) | | >> (some y:int. y*y<= x <(y+1)*(y+1)) | `----------------------------------------------------'
Now the sequence rule is used to introduce the formula needed for the case analysis.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |# top 1 3 1 2 2 1 | |1...7. | |8. hh:( y0*y0<= x-1 <(y0+1)*(y0+1)) | |9. r=<y0,hh> in (some y:int. y*y<= x-1 <(y+1)*(y+1))| |>> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY seq (y0+1)*(y0+1)<x | ~(y0+1)*(y0+1)<x | | | |1* 1...7. | | 8. hh:( y0*y0<= x-1 <(y0+1)*(y0+1)) | | 9. r=<y0,hh> in (some y:int. y*y<= x-1 <(y+1)*(y+| | 1)) | | >> (y0+1)*(y0+1)<x | ~(y0+1)*(y0+1)<x | `----------------------------------------------------'
The contradictory case follows.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |* top 1 3 1 2 2 1 2 1 1 | |1...9. | |10. (y0+1)*(y0+1)<x | ~(y0+1)*(y0+1)<x | |11. (y0+1)*(y0+1)<x | |12. (y0*y0<= x-1 ) | |13. ( x-1 <(y0+1)*(y0+1)) | |>> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY arith at U1 | `----------------------------------------------------'
Now comes the other part of the trichotomy analysis.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |# top 1 3 1 2 2 1 2 2 | |1...9. | |10. (y0+1)*(y0+1)<x | ~(y0+1)*(y0+1)<x | |11. ~(y0+1)*(y0+1)<x | |>> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY seq ( (y0+1)*(y0+1)=x in int ) | x<(y0+1)*(y0+1) | `----------------------------------------------------'
Now we conduct a case analysis. Only a few steps of each case are shown.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |# top 1 3 1 2 2 1 2 2 2 1 | |13. ( (y0+1)*(y0+1)=x in int ) | |>> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY intro (y0+1) | | | |1* 1...10. | | 11. ~(y0+1)*(y0+1)<x | | 12. ( (y0+1)*(y0+1)=x in int ) | x<(y0+1)*(y0+1) | | 13. ( (y0+1)*(y0+1)=x in int ) | | >> (y0+1) in (int) | `----------------------------------------------------'
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |* top 1 3 1 2 2 1 2 2 2 1 2 1 | |1...10. | |11. ~(y0+1)*(y0+1)<x | |12. ( (y0+1)*(y0+1)=x in int ) | x<(y0+1)*(y0+1) | |13. ( (y0+1)*(y0+1)=x in int ) | |>> ((y0+1)*(y0+1)<= x ) | | | |BY arith at U1 | `----------------------------------------------------'
Now we consider the other case, given by hypothesis 13 above.
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |* top 1 3 1 2 2 1 2 2 2 | | 1...9. | | 10. (y0+1)*(y0+1)<x | ~(y0+1)*(y0+1)<x | | 11. ~(y0+1)*(y0+1)<x | | 12. ( (y0+1)*(y0+1)=x in int ) | x<(y0+1)*(y0+1) | | 13. x<(y0+1)*(y0+1) | | >> (some y:int. y*y<= x <(y+1)*(y+1)) | | | |BY intro y0 | `----------------------------------------------------'
,----------------------------------------------------, |EDIT THM root | |----------------------------------------------------| |* top 1 3 1 2 2 1 2 2 2 2 2 | |1...11. | |12. ( (y0+1)*(y0+1)=x in int ) | x<(y0+1)*(y0+1) | |13. x<(y0+1)*(y0+1) | |>> ( y0*y0<= x <(y0+1)*(y0+1)) | | | |BY intro | `----------------------------------------------------'
Assuming that the theorem has been proved and is named root,
the term term_of(root) will
evaluate to
a function which takes an integer x and
a proof of
x>=0 and produces a proof of some y:int.(...). A proof of
the latter is a pair, the first element of which is
the integer square root of x.
Thus the
definition below of rootf, when instantiated
with a nonnegative integer
as its parameter, will evaluate to the integer square
root of the supplied integer.
The definition uses a defined function 1of which
returns the first element of a pair. Also, we supply
v.v as the proof of x>=0; since by definition
x>=0 is x<0=>void, a proof of it, if it is true,
can be any lambda term.
rootf(<x:int>) == 1of( term_of(root)(<x>)(\v.v) )This is a partial function on int because its domain is a subset of int. It is a total function from nonnegative integers to integers.
If we want a function which will return an integer value on all integer inputs, then the following theorem describes a reasonable choice.
>> all x:int. some y:int.
(x<0 => y=0 in int) & (x>=0 => y*y<=x<(y+1)*(y+1))
If this theorem is called troot then a
(total) square root function on int can be defined by
sqrt(<x:int>)== 1of(term_of(troot)(x)).