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

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

sqrt(<x:int>)== 1of(term_of(troot)(x)).

Thu Sep 14 08:45:18 EDT 1995