Next: Computation Up: Proofs Previous: Predicate Logic

# Example from Elementary Number Theory

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            |
`----------------------------------------------------'
```

```,----------------------------------------------------,
|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)).
```

Next: Computation Up: Proofs Previous: Predicate Logic

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995