BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1382
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Formalizing Constructive Real Analysis
AUTHOR:: Forester, Max B. 
DATE:: September 1993
PAGES:: 24
ABSTRACT::
This paper arises from a project with the Nuprl Proof Development System 
which involved formalizing parts of real analysis, up through the intermediate 
value theorem. Extensive development of the rational library was required as 
the real library was being built, resulting in the addition of about 125 
rational theorems. The real library now contains about 150 theorems and 
includes enough basic results that further extensions of the library should be 
quite feasible. This paper aims to illustrate how higher mathematics can be 
implemented in a system like Nuprl, and also to introduce system users to the 
library.
END:: CORNELLCS//TR93-1382
BODY::
Formalizing Constructive Real Analysis*
Max B. Forester
TR 93-1382
September 1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
tThis work supported by NSF grants CCR-9244739, CCR-9148222 and ONR grants
N0001 4-92-J-1 764, N0001 4-91 -J-41 23.
Forma1izi?g Co?structive R?ea?1 A?a1ysis*
Ma? B. Forester
Departi?ent of Coi?puter Science
Cornell University
*This work supported by NSF gra??ts CCR-9244739. CCR-914Q?222 aiid ONR grauts
N00014-92-J-1764, NO()O14?91-J-41 2:3
Formalizing Constructive Real Analysis
Afax B. Forester
Department of Computer 5cience
Cornell University
forester?cs. cornell. edu
Abstract
This paper arises from a project with the Nuprl Proof Development System
which involved formalizing parts of real analysis, up through the intermediate
value theorem. Extensive development of the rational library was required as
the real library was being built, resulting in the addition of about 125 rational
theorems. The real library now contains about 150 theorems and includes enough
basic results that further extensions of the library should be quite feasible. This
paper aims to illustrate how higher mathematics can be implemented in a system
like Nuprl, and also to introduce system users to the library.
1 Introduction
The first part of this paper is a guided tour through the real library with emphasis on
the definitions, a handful of useful theorems, and the proof of the intermediate value
theorem. Afterwards is a section giving detailed descriptions of the special-purpose
tactics that were written in conjunction with the rationals and the reals. Users interested
in developing theories in analysis should find both sections helpful.
2 Real Analysis in Nupri
2.1 Definitions
In formalizing real analysis we follow the development of Bishop ?l]. Real numbers are
represented by infinite sequences of rationals, which are required to converge at a certain
rate. We have
* ABS real
R == fx:SeqCQ)I (Vi:N+. Vj:N+. IxCi) - x(j)I < i/i + i/j)) ;;
and equality is given by
* ABS eqreal
r = s == Vn:N+. Ir(n) - s(n)I < 2/n ;;
2 HEAL ANALYSIS IN NUPRL
9
Some operations on reals are defined as follows:
* ABS radd
a + b == Ai.(a((2 * I))) + (b((2 * I))) ;;
* ABS rneg
--Ha == Ai.--H(a(i)) ;;
* ABS rsub
a - b == a + -b ;;
?Te identify the rationals with the subset of the reals represented by constant sequences.
* ABS realzat
a == Aj. a
The definition of muftiplication involves the canonical bound of a real number a, which is
an integer Ka such that for all n, Ka > I a(n) . ?Ve define Ka as the least integer greater
than laCi) + 2.
* ABS canon?ound
Ka == Ia(?).num + a(1).denl + 3 ;;
* ABS rmu1?en
a *g b == Ai.C(aCC2 * (Ka * i)))) * (bC(2 * (Ka * I)))))
* ABS rriiul
a * b == if laCi) < Ib(i)I then b *g a else a *g b ;;
The purpose of the case split is to ensure that the maximum of the canonical bounds of
a and b is used.
* ABS rmax
maifa,bJ == Ai.mazfcaci)),Cb(i))t ,,
* ABS rabsval
Ia == mazfa,-aJ ;;
* ABS pos
a > 0 == ?n:N+. lin < a(n) ;;
* ABS lt?
a < b == b - a > 0
* ABS gt?
a > b == b < a ;;
2 REAL ANALYSIS Th NUPRL
* ABS non?eg
a > 0 == (Vn:N+. -lin ? a(n)) ;;
* ABS ler
a < b == b - a > 0
* ABS ger
a > b == b ? a ;;
:3
We also define the following subsets of R. Notice that a positive real is a pair, consisting
of a real and a positive integer. This integer is the witness that the real is positive.
Nonzero reals are defined similarly.
* ABS real?pos
== r:R X r > 0
* ABS real?on?eg
R0+ == (r:RI r > Ol ;;
* ABS real?zero
R-0 == r:R x (n:N+I tIn < Ir(n)I) ;;
It is often convenient to think of positive reals as real numbers rather than as pairs,
and in Bishop this simplification is made with the understanding that witnesses are
always available when needed. Nupri's display mechanism easily adopts this style of
presentation by having a positive number and its first projection look the same. This
goes for nonzero reals as well.
* ABS rnum
a == a.t ;;
* ABS rwit
awit == a.2 ;;
The following two operations are defined on R-0 and R x R-0.
* ABS rinv
i/a == Ai.if i <z awit then i/a(a.wit?3) else tIaCCi * a.wit?2))
* ABS rdiv
a/b == a * i/b ;;
And finally,
* ABS interval
[a2b] == fr:RI (a < r A r ? b)t
* ABS continuous
f cont on [a,b] == 3w:R R. V?:R+. w(?) > 0 A
(Vx:[a,b]. Vy:[a,b]. Ii - yI < w() ?
I(f(x)) - (f(y))I < e') ;;
2 REAL ANALYSIS IN NUPRL
4
2.2 Well-Formedness and Eunctionality
Since JR is a proper subset of Seq(?) it is necessary to prove that the operations above
actually produce real numbers, In Nupri such ""well-formedness" proofs are generally
required and usually trivial. ?`ith the constructive reals. though. these proofs are any-
thing but routine, and in fact are the reason that the definitions are so complicated.
Thus the following theorems deserve to be mentioned:
* THM radd?wf
Va:R. Vb:R. a + b E JR
* THM rneg?wt
Va:R. -a E JR
* THM rsub?wf
Va:JR. Vb:JR. a - b E JR
* THM rea1?at?w?
Va:Q. a E JR
* THM rmu1?en??
Va:JR. Vb:JR. IbCl)I ? laCi) ? a *g b E JR
* THM rmu1?wt
Va:JR. Vb:R. a * b E JR
* THM rmax??f
Va:R. Vb:R. max(a,b) E JR
* THM rabsva1?vf
Va:JR. Ia E JR
* THM rinv?wf
Va:JR?0. i/a E JR
* THM rdiv?":'
Va:JR. Vb:R?0. aIb E R
Another concern is that functions are well defined with respect to real equality. That
is, they do not depend on the particular sequences representing their arguments. For
example, the canonical bound of a number is not functional.
* THM radd?unctiona1ity
Vai:R. Va2:JR. Vbi:R. Vb2:R. al = a2 ? bi = b2 ? al + bi = a2 + b2
* THM rneg?unctionaiity
Va:R. Vb:R. a = b ? -a = -b
2 REAL ANALYSIS IN NUPRL
* THM rsub?unctiona1ity
Val:R. Va2:R. Vbi:R. Vb2:R. al = a2 ? = b2 ? al - bi = a2 - b2
* THM rea1zat?unctiona1ity
Va:Q. Vb:Q. a = b ? a = b
This theorem is not quite as trivial as it looks --H the equality on the left is rational
equality whereas the one on the right is real equality.
* THM rmu1?unctiona1ity
Val:R. Va2:R. Vbl:R. Vb2:R. al = a2 ? bi = b2 ? al * bi = a2 * b2
* THM rmax?unctiona1ity
Val:R. Va2:R. VbI:R. Vb2:tR. al = a2 ? bi = b2 ? maifa1,b1? =
maxfa2 ,b2?
* THM rabsva1?unctiona1ity
Va:R. Vb:R. a = b ? a = Ibi
* THM rinv?unctiona1ity
Va:R?0. Vb:R?0. a = b ? i/a = i/b
* THM rdiv?unctiona1ity
Vai:R. Va2:R. Vbi:R?0 Vb2:R?0. ai = a2 ? bi = b2 ? al/bi = a2/b2
Similarly the order relations are well defined:
* THM pos?unctiona1ity
Va:R. Vb:R. a = b ? (a > 0 ?? b > 0)
* THM 1tnr?unctionaiity
Vai:R. Va2:R. Vbi:R. Vb2:R. al = a2 ? bi = b2 ? Cal < bi ??
a2 < b2)
* THM non?eg?unctiona1ity
Va:R. vb:R. a = b ? (a> 0 ?? b > 0)
* THM 1enr?unctiona1ity
Val:R. Va2:R. vbl:R. vb2:R. al = a2 ? bi = b2 ? Cal < bi ??
a2 < b2)
2 REAL ANALYSIS LY NUPRL
6
2.3 Some Theorems
The surprising thing about the definitions is that they can be thought of in a very
intuitive way. For instance, the following lemma says that two real numbers are equal if
and only if they have the same limit.
* THM eq?rea1flemma
Vx:R. Vy:R. x = y ?? (Vj:N+. ?&:N+. Vn:(N...). Ix(n) - y(n)I < 1/j)
This lemma is useful in showing that real equality is transitive, and thinking about real
equality in terms of limits makes this fact obvious. However. from the definition alone it
seems that transitivity does not hold --H if Ia(n) - bCn) I < 2/n and Ib(n) - c(n) I
< 2/n, surely I a(n) - c(n) I can be made to be greater than 2/n! The solution is that
the convergence rate in the definition of JR prevents this from happening (the proposed
arrangement disqualifies at least one of a, b, and c from being a real number).
Another characterization of real equality is
* THM eqnrealflemma2
Va:R. Vb:R. a = b ?? (Vi:N+. Vj :N+. Ia(i) - b(j) I < i/i + 1/j)
which says that if you confuse equal numbers a and b (that is, if you interchange aCi)
and b(i) for various i), the resulting sequence is a valid real number.
One fact that was especially useful in proving arithmetic properties is that any sub-
sequence of a real number is again a real number, equal to the first. Subsequences are
defined by composing a monotone function on N+ with the real (which is a function N+
* ABS monotone
mono(f) == Va:N+. Vb:N+. a < b ? f(a) < f(b) ;;
* THM rea1?subsequence
Vf:N+ N+. mono(f) ? CVa:R. Ai.a(fCi)) = a)
* THM rea1?ubsequence2
Vf:N+ N+. monoCf) ? CVa:R. (Ai.a(fCi))) E JR)
There are lemmas about the order relations which provide some more intuition. In
particular, a number is nonnegative if and only if its limit is, and positive if and only if
there is a 1/n that the sequence stays above from n on (which is a little stricter than
saying that the limit is positive).
* THM rea1?pos?emma
Va:R. a > 0 ?? C3N:N+. Vm:(&. . .?. 1/N < aCm))
* THM real?oniiegA emma
Va:R. a > 0 ?? (Vn:N+. ?N:N+. Vm:fN. . .?. -1/n < a(m))
Now for some more interesting results. For example, the nth element of a real actually
approximates the real to within 1/n.
2 REAL ANALYSIS LY NUPRL
* THM rat?approx
Va:R. Vn:N+. Ia - a(n)I ? I/n
Also, as one might expact, the rationals are dense in the reals.
* THM ratAense
Va:R. Vb:tF?. a < b ? (?q:Q. a < q A q < b)
The following fact is quite important and plays a significant role in the intermediate
value theorem. It is not true in general that a < 0 V a > 0 for real a, but given an
arbitrarily small positive epsilon we can do almost as well.
* THM pos?quasiAecidab1e
Va:R. V:R+. a < ? V a > 0
2.4 The Intermediate Value Theorem
Our implementation of the intermediate value theorem uses the bisection method, and
follows the proof outline given in an earlier system [31. The theorem is:
* THM ivt
Va:R. Vb:R. a < b ? (Vf:R R. f cont on [a,b] ?
f(b) > 0 ? -(:`(a)) > 0 ? (Ve:R+. ?c:[a,b]. If(c)I < ?))
The procedure is to let c be the midpoint of a and b, and decide if If(c) < e. If so
then we are done, and otherwise If(c) > 0 by pos?quasiAecidab1e. It follows easily
that either :`(c) > 0 or -(f(c)) > 0. In the former case consider the interval [c,b],
and in the latter, [a,c], and repeat the procedure on this new interval. To see that this
terminates, note that the diameter of the intervals goes to zero, and by continuity the
diameter of the range of f goes to zero as well. This range always includes both positive
and negative values, so eventually it lies wholly inside (-e, e).
The proof generating this algorithm is an induction proof with the following induction
hypothesis:
* ABS bisects
bisects(a; b; f; e; n) == (?c:[a,b]. I:'(c)I < e') V
C3a:[a,b]. 3P:Ea,b]. f3 - = 1/2n * b - a A
> 0 A -(f(o)) > 0) ;;
The proof that this holds for all n is interesting in that the base case and the induction
step are almost identical. The base case is the lemma bisectionstep, and in the
induction step we just instantiate this lemma on the appropriate sub-interval.
* THM bisectionstep
Va:R. Vb:R. a < b ? (V:':R R. :`(b) > 0 ? -(f(a)) > 0 ?
(V?:R+. bisects(a; b; f; ?; 1)))
2 REAL ANALYSIS LY NUPRL
s
* THM bisection?induction
Va:iR. Vb:R. a < b ? (V?:R JR. ?(b) > 0 ? -(f(a)) > 0 ?
CV?:IR+. Vn:N+. bisects(a; b; ?; ?; n)))
The lemma that tells us how many steps to take is
* THM ha1ving?to?ero
Va:R. Vb:IR. a > 0 ? (?n:N+. 1/2?n * b < a)
and together with continuity and the following lemma provide all that is necessary to
complete the proof.
* THM rabsva1across?ero
Va:R. Vb:R. b > 0 ? -a > 0 ? Ibi < Ib - a
Now we can look at the details, though perhaps some explanation is in order.
A Nuprl proof is a tree where each node has a numbered list of hypotheses and
declarations, a conclusion (or goal), and a tactic name. If a tactic succeeds in proving the
goal from the hypotheses then the node becomes a leaf. Otherwise the tactic generates
one or more subgoals which, if proven, are sufficient to justify the claim of the current
node. Thus the overall idea is to start with the statement of the theorem at the root
and gradually reduce it to trivialities by applying tactics.
In reading this proof, the easiest way to understand what the tactics do is probably
to just look past them and see what subgoals they generate.
* THM ivt
 Va:R. Vb:R. a < b ?
I			CVf:R			JR. f cont on [a,b] ? f(b) > 0 ? -Cf (a)) > 0 ?
(Vr:JR+. 3c:[a,b]. If(c)I < e))
BY UnivCD THENA Auto
1. a: JR
2. b: JR
3. a < b
4.			f: JR			R
5. f cont on
6. fcb) > 0
7. -(fCa)) > 0
8. ?:
 3c:La,b] If(c)I < ?
BY Unfold `continuous 5
5.
3w: JR JR. V:R+. w(?) > 0 A
(Vx:[a,b]. Vy:[a,b]. Ix - yI < w(e) ? I(f(x)) - (f(y))I < e)
2 REAL ANALYSIS IN NUPRL
 ?c:[a,b]. If(c)I < ?
BY D 5
THENM With `e' (D 6)
THENM D (-i)
THENA Auto
5 w: R JR
9. wCe) > 0
10. Vx:[a,b]. Vy:[a,b]. Ix - yI,? wC?) ? I(f(x)) - (f(y))I < ?
 ?c:[a,b] If(c)I < e:
BY Using [?b','b - a'] CFwdThruLemnia (halvi?gto?ero? [9])
THENM D (-1)
THENA Auto
11. n:
12. 1/2?n * b - a < w(?)
 2c:[a,b] If(c)I < e
BY InstLemma ?bisection4nduction' [`a' ;`b'; `f';'?';'n']
THENN Unfold cbisectsc (-i)
THENA Auto
9
13			C?c:Ea,b]. If(c)I < ) V
I (3a:La,b]. ?P:[a,b]. P - a = 1/2?n * b - a A
> 0 A -(f(Q)) > 0)
 ?c:[a,b]. If(c)I < ?
BY D 13
THEN Auto 7. If the first disjunct holds then we're done. ti'
THEN RepeatMFor 4 CD (-1))
THENA Auto
13.
14.
15.			1/2?n * b - a
16.
17
a: Ea,b]
?: Ea,b]
fC?) > 0
-CfCa)) > 0
 ?c:[a,b] IfCc)I < E
BY With `P' CD 10)
THENM With `a' CD (-1))
ThENA Auto
2 REAL ANALYSIS IN NUPRL
10. n:
11 1/2?n * b - a < w(?)
12. Q:
13. t3: [a,b]
14. P - = 1/2?n * b - a
15 f(?) > 0
16. -(?(o)) > 0
17 IP - ol < w(?) ? I(f(P)) - (f(o))I ?
 ?c:[a,b] If(c)I < ?
BY Rewrite (\e. HigherC (RevHypc 14 e) e) 11
ThENM Assert Jf3 - Q = -
ThENM Rewrite (\e. Higherc (HypC (-1) e) e) (-2)
ThENM OnHyps [(-1);13] Thin
THENA Auto
I			_			? I(f(?)) - (f(o))I ?
I			1/2?n > 0
0
11			o:
12			?: [a,b]
13.			P - = 1/2?n * b			- a
14.			f(?) > 0
15			-(f(o)) > 0
16			IP - ol < w()			_
17.			P - o < w(e)
 p - = IP -
BY BackThruLemma `eq?eal?ym
THENM BackThruLemma crabsval?ero
THENA Auto
BY Rewrite (\e. Higherc (HypC 13 e) e) 0
THENM BackThruflernnia rinul preserves?on?eg
ThENN Try (Fold Cle? 0)
THENM Try (BackmruLemma `lez?weakeningdtz')
THEN Auto
BY Rewrite (Higherc real?tozatC)
THENM BackThruLetnma cexponpreserves?on?eg
THEN Auto
THEN le?q?expand 0
10
3 TACTICS
3 Tactics
THENM Rewrite (Higherc qnd?evalC) 0
THEN Auto
11			Q:
12			?: [a,b]
13			fC4) > 0
14			-(f(Q)) > 0
15			IP - QI ? w(?) ?			- (fCQ))I ?
16.			IP - QI < "`Ce:)
			?c:[a,b] If(c)I < ?
BY FwdThruLemma `lejr?weakeningdt?' [16]
ThENM FwdThruHyp 15 [(-1)]
THENM OnHyps [(-2);16;15] Thin
ThENA Auto
15. I(f(?)) - (f(Q))I < ?
 ?c:[a,b] If(c)I < e:
BY With ??? CD 0)
THENM Rewrite (\e. Higherc (RevHypC 15 e) e) 0
ThENM BackThruLemma ?rabsval?across?ero
ThEN Auto
The following is a listing of the user defined tactics in the rational and real libraries to-
gether with illustrations of their use. Some do a fair amount of computation or rewriting
while others are basically macros for various sequences of tactics that show up repeat-
edly in the libraries. "Direct computation" tactics perform only term reduction and
unfolding and folding of definitions.
CaseSplit This tactic decomposes an ifthenelse term and rewrites the Boolean con-
dition to a proposition. From qabsvalie?q:
1. a: Q
 a < if (a.num * -a.den) <z (-a.num * a.den) then -a else a
BY CaseSplit 0
I 2. a.num * -a.den < -a.nwn * a.den
 a _ -a
2. -a.num * a.den ? a.num * -a.den
3 TACTICS
 a _ a
qnd?evalC This is a direct computation tactic that reduces a/b . num to a and a/b . den
to b. From eq?q?ef1:
1			xl: Z
2			x2: N+
 xl/x2.num * xl/x2.den = xl/x2.num * xl/x2.den
BY Rewrite (Higherc qnd?evalC) 0
 xl * x2 = xl * x2
expcn?nrollC This unrolls the definition of expon using direct computation.
* ABS expcn?en
expon?en == Af,a,n.if n =z 1 then a else (a * f(a)(n - 1))
* ABS expon
an == Y(expon?en)(a)(n) ;;
The effect is to replace a?n with if n =z 1 then a else (a * a?(n - 1)).
From exponpreservespos:
1 a: Q
2. 0. < a
3. n: Z
4. 1 < n
5. 0. < a?(n - 1)
 0. < a?n
BY Rewrite (Higherc expon?unrollC) 0
THENM CaseSplit 0
ThEN Auto
6. ?n = 1
 0. < (a * a?(n - 1))
lt?q?expand Converts a < b to a.num * b.den < b.num * a.den. le?q?expand and
eq?q?expand are similar. From lt?q?qmax:
3 TACTICS
1 a: Q
2 b: Q
3. a < b
 maxfa,bf = b E ?
BY Un?old Cqm?x? 0
THEN lt?q?expand 3
THENA Auto
1:3
3. a.num * b.den < b.num * a.den
 if (a.num * b.den) <z (b.niim * a.den) tilen b else a = b ?
qabsval?evalC This tactic rewrites absolute values of rational arithmetic expressions
to expressions with absolute values in the numerators. From rat?triangle:
1. a: Q
2. b: Q
3. c: Q
 Ia - cl < Ia - bi + Ib - cl
BY Rewrite (Higherc qabsval?evalC) 0
THENA Auto
THEN Try (BackThruLemma Cmul?eroitC)
THEN Auto
 la.num * c.den + -c.num * a.denl/(a.den * c.den) <
Ia.num * b.den + -b.num * a.denl/(a.den * b.den) +
lb.num * c.den + -c.num * b.denl/(b.den * c.den)
SAuto This is a version of the autotactic that tries calling AbSetMemEqTypeCD. It is
useful for handling membership goals of the form a = b E T where T is a set
type. From real?os?nc:
1 r: R
2 xl: N+
3 lixi <
 <r,x1>
BY Assert
THEN SAuto
 l/xl < lrCxl)l
r(xl)
E r:R x (n:N+I 1/n < Ir(n)I)
`i/il < IrCxl)l'
3 LACTICS
14
rat?to?intC Rewrites expressions of rational integers (rationals of the form a/i) to
integer expressions. In the example from canon?ound?property., the conclusion
is an equality between rationals.
1. a:
2. n:
3. a(i).den # 0
 IaCi).num + a(i).denl + 3 = Ia(i).num + a(i).denl + 1 + 2
BY Rewrite (Higherc ratfto?intC) 0
THEN Auto
intftoratC Rewrites integer expressions to rational ones.
RAuto Like SAuto except that if it gets stuck on a membership goal it will try to unfold
the type subterm. It is useful for goals like a = b E IR where the type needs
unfolding. From rat?zero ft oreal ?zero:
2
3.
4.
5.
BY RAuto
 i/n < IaCn) I
a: Q
a.num ? 0
0 < Ia
n:
lin < a
= <a,n> E R-0
PosHD Decomposes a hypothesis of the form a > 0 and obtains a witness, although it
sometimes must be used with the tactic Unnide. From rea1?posaemma:
a: R
a>O
1.
2.
BY PosHD 2
THEN Unhide
THENA Auto
Vm:fN. . .J. tIN < a(m)
2. n:
3. i/n < a(n)
 ?N:N+. Vm:(N. . .?. i/N < a(m)
3 TACTICS
15
PosCD This takes a term as an argument to be used as a witness for a goal of the form
a > 0. From rflegA'unctiona1ity?wrtdtr:
1. a: tR
2. b: tF?
3. n:
4. i/fl < (b -
 (-a - -b) > 0
BY PosOD )?)
ThENA Auto
 lIn < (-a - -b) Cn)
rnw?eva1C This tactic is similar to qnd?eva1C except that it takes pairs which are
nonzero reals. In this example from pos?quasiAecidab1e the term e in the
conclusion is actually a display for rnumCe), which becomes rnum(<?i ,n>) after
CD 2) is applied.
1. a: R
2. e:
 a < ? V a > 0
BY New [`e'i ;C?J] CD 2)
THEN Rewrite CHigherc rnw?eva1C) 0
2 e'i: R
3 n: El > 0
 a < 1 V a > 0
rea1?app1y?eva1C This direct computation tactic takes a real expression applied to
a natural number, and "distributes" the application inside the expression ac-
cording to the definitions of the operations involved. The operations it knows
about are radd, rneg, rsub, real rat, rmulgen, rmax and rabsval. From
radd?reserves?os:
1. a: R
2. b: R
3. c: R
4. N: N+
5. Vm:(N. . .?. l/N < Cb - a) Cm)
 ?N:N+ Vm:?N. . .?. tIN < Cb + c - a + c)Cm)
3 TACTICS
BY With ?N' (D 0)
ThENM Rewrite (HigherO real?apply?evalC) 5
ThENM Rewrite (Higherc real?apply?evalC) 0
THENA Auto
16
5. Vm:?N. .J. i/& ? b(2 * m) - a(2 *
 Vm:fN. o+1.
lIN < b(2 * (2 *			+ c(2 * (2 * m)) - a(2 * (2 * m)) +
c(2 * ( 2 *
real?toj'atC Rewrites expressions of reals which are constant sequences to rational
expressions.
rat?tozealC Rewrites rational expressions to real expressions, but does not recognize
qinv or qdiv. The reason for this is that rinv and rdiv must be given nonzero
reals, requiringwitnesses. Inthisexamplefromhalving?to?ero theconclusion is
arationalexpression. Itgets convertedtoarealexpression andthen is decomposed
so that it matches hypothesis 7.
1. a: JR
2. b: JR
3. a > 0
4. 0 < a
5. q: Q
6. n:
7. lin < (q -
8. q < a
9. r: Q
10. b < r
11. b > 0
 0 < q
BY Rewrite (Higherc ratftoj'ealC) 0
THENN Unfold cft?c 0
THENM PosCD )?J
ThEN Auto
rat?toJreal?witnessC Sameas rat?to?ealCexcept that it handles qinvand qdiv. It
takes anatural numberto be used as a witness for all instances ofrinvand rdiv.
This tactic does not get used in the library so we have a cooked up example:
1. a: Q
2. b: Q
3. c: Q
A LACTICCODE
4. c.num ? 0
5. n:
 -Ia + b - (1/c *			= -c - (b + c * a)
BY Rewrite (rat?toreal?witnessC )7)) 0
ThENA SAuto
I  <c,7> = <c,7> E R-0
I  0 < 7
 -Ia + b -			* b) = -c - (b + c * a)
A Tactic Code
The tactics described above? together with some special-purpose lemmas to which they
refer.
* ML casesplit
let CaseSplit =
\i.(if Ci=O) then
(ItmenElsecases 0
THENM RW boolfto?propC (-i)
THENA Auto)
else
(IfThenElseCases i
THENN RW bool?to?propC
THENA Auto))
* ML qnd?eval
let qndevalc = UnfoldsTopc ``qnumer qdenom'
ANDThENC AddrC [1] (UnfoldTopc cqfluflL?)
ANDThENC (pi1?evalC ORELSEC pi2?evalC)
* ML expon?unroll
let expon?inrollC =
FwdMacroC exponJinrollc
(UnioldO cexpon
ANDThENC Higherc YUnrollC
ANDThENC UnfoldO `expon?en'
ANDThENC ReduceC
ANDThENC FoldO ?expon?en'
ANDTHENC FoldO `expon'
A LACTIC CODE
a?n?
* ML expandAefs
let lt?q?expand =
\i. (Unfold `lt?q' I
THEN RWH (Lemmac Cassert?of?qlt?w?) I)
let le?q?expand =
\i. (Unfold `le?q' I
THEN Unfold `qie' I
THEN RWH (LemmaC `assert?of?bnot') I
THENM RWH (Lemmac `assert?of?qlt?rw') I)
let eq?q?expand =
\i. (Unfold `eqq' I
THEN Unfold `eqzat' I
THEN RWH (LemmaC `assert?of?eq?Int')
I)
* ML qabsval?eval
let qabsval?evalC =
Repeatc (UnfoldsC ``qdlv qinv qsub qneg qmul qadd'')
ANDTHENC Higherc qnd?evalC
ANDTHENC LemmaC qabsvalfto?Iabsval'
ANDTHENC Higherc qnd?evalC
ANDTHENC aepeatc (FoldsC ``qadd qmul qneg qsub qinv qdlv'')
is
For readability, different notations have been used in the foflowing theorems. a. is the
rational number a/i.
* THM rI?eq?q
Va:Z. Vb:Z. a. =? b. ?? a = b
* THM rI?t?q
Va:Z. Vb:Z. a. <? b. ?? a < b
* THN rIAe?q
Va:Z. Vb:Z. a. <Q b. ?? a ? b
* THM rI?qnegfto?Inus
Va:Z. -(a.) = (-a). E Q
A TACTIC CODE
* THM ri?qadd?to?add
Va:Z. Vb:Z. a. +? b. = (a + b). ?
* THM ri?qsub?to?sub
Va:Z. Vb;Z. a. ? b. = (a - b). ?
* THM ri?qmul?to?ul
Va:Z. Vb:Z. a. *? b. = (a * b). ?
* THM ri?qabsval?toAabsval
Va:Z. Ia. = lal. E Q
* ML collect?umer
let collectnumerC -
TryC
(SweepUpc (Firstc (map LemmaC eriqneg;to?in115 riqaddftoadd
ri?qsub?to?ub ri?qmul?to?ul ri?qabsval?to?absval' C))
* ML convertrel
let convertrelC =
TryC
(Firstc (map LemmaC ``rieqq ri2tq ri2e?qcC)
* ML ratfto?nt
7. rat?toAntC
If a term is of the form
expi R exp2
where expi and exp2 are arithmetic expressions of rational
integers, and ? is eq?q, lt?q, or le?q, ratftoAntC will
convert it to an equivalent integer expression.
7.
let
ratftoAntC =
HigherO collectnumerC
ANDThENC convertrelC
19
* ML spread?umer
let spread?umerC =
TryC
(SweepDnc (Firstc (map RevLemmaC ``riqnegtoJninus riqaddtoadd
ri?qsub?to?ub ri?qmul?to?ul ri?qabsval?torabsval
A TACTIC CODE
* ML rev?convertrel
let rev?convertrelO =
TryC
(FirstC
(map RevLemmaC ``rieqq riltq rjqeqtt)
* ML intftorat
let int?toratC =
rev?convertrelC
ANDTHENC Higherc spread?umerC
* ML posA
let RAuto = Auto THEN
\p.((if isequalfterm (concl p) then
(UnfoldAtAddr [1] 0 THEN SAuto)
else Id) p)
let PosHD = \i.(Untold `pos' I
THEN Unfold `exists?q' I
THEN AbSetHD I)
let PosOD t = Unfold `pos' 0
THEN Unfold `exIsts?q' 0
THEN (Refine `dependent?et?emberFormatIon'
Emkftevel?exp?arg(mkdevel?exp['I' ,O]);
mkterm?arg t;
mk?var?arg `mephistopheles5]
THENL EAddHiddenLabel `aux' ;AddHiddenLabel `main';
Try (Reduce 0) THEN RAuto THEN SlAuto
THEN Thin (-1) 1)
* ML rnw?eva1
let rnvevalC = UnfoldsTopC ``mum rwit''
ANDTHENC (pi1?evalC ORELSEC pi2?evalC)
* ML real?apply?eval
let radd?evalC =
SimpleMacroC `radd?evalC
`a +r b n? `(a (2 * n)) + (b (2 * n))' ``radd'
20
A TACTIC CODE
let rneg?evalC =
SimpleMacroC `rneg?evalC
-an `-Can)' C??eg
let rrnax?valC =
SimpleMacroC rmax?evalC?
`maxfa,bJ n' `rnaxf(a n),(b n)J' ?(rmaxc
let rmul?en?evalC =
SimpleMacroC ?rmul?en?evalC
`a * b n' `((a (2 * (Ka * n)))
* (b (2 * (Ka * n))))' ??rmul?en
let rsub?evalC =
MacroC `rsub?evalC
(AllO [Un?oldC `rsub';raddevalC;AddrC [2] rneg?evalC])
a -r b n'
(Un?oldC (qsub() `a (2 * n) - b (2 *
let rabsval?evalC =
MacroC rabsval?evalC
(AllC [tJn?oldC ?rabsvalC ;rmaxevalC;AddrC [2] rnegevalC])
`Ia n'
(UnfoldC `qabsval') `Ia ni'
let real?apply?evalC =
(SweepDnC
(FirstO
[rabsval?evalC;rmax?evalC;rmul?en?evalC;
rsub?evalC;rneg?evalC;radd?evalC])
ANDThENC TryC (UnfoldC treal?atC
ANDThENC ReduceC))
Again we use some more visible notation. a is the real number Ai . a.
* THM rr?qaddfto?add
Va:Q. Vb:Q. (a +? b) = a +R b E R
* THM rr?qnegftoZneg
Va:Q. (-a) = -(a) E R
* THM rr?qsubfto?sub
Va:Q. Vb:Q. (a -Q b) = a R b' E R
A TACTIC CODE
* THM rr?qmul?tormul
Va:Q. Vb:Q. (a *q b) = a *J? b E ?
* THM rr?qinvftorinv
Va:Q?0 Vn:N+. (i/a) = i/<a.,n> E IR
* THM rr?qdiv?tordiv
Va:Q. Vb;??0. Vn:N+. (a + b) = a/<b.,n> E R
* THM rr?qabsval?torabsval
Va:Q. lal = Ia. E R
* THM rr?eqreal
Va:Q. Vb:Q. a =? b ?? a =R b
* THM rratr
Va:Q. Vb:Q. a <? b ?? a <R b
* THM rriler
Va:Q. Vb:Q. a <Q b ?? a <R b
* THM rr?pos
Va:Q. 0 <Q a ?? a > 0
* THM rr??on?eg
Va:Q. 0 ?q a ?? a > 0
* ML collect
let collectC =
TryC
(Sweepupc (FirstC (map RevLemmaC `rr?qnegftorneg
rr?qadd?toradd rr?subfto?sub rr?qinv?torinv
rr?qmul?to?mul rr?qdiv?tordiv rr?qabsval?torabsval
* ML convert
let conveftC =
TryC
(Firstc (map ?evLemmaC t(rr?eq?eal rr?tz rrAe? rr?pos
rr?on?eg?')
REFERENCES
* ML real?to?at
let real?toratC =
Higherc collectc
ANDTHENC convertC
23
* ML disseminate
let disseminateC =
Tryc
(SweepDnc (FirstC (map LemmaC c(rrqflegftorfleg rrqaddftoradd
rr?qsub?torsub rr?qmulfto?mul rr?qabsval?tc?absval' C))
let
disseminate?itnessC n =
TryC
(SweepDnc ((FirstC (map Lemmac rr4negtorneg rrqaddftozadd
rr?qsub?tozsub rr?qmulftozmul rr?qabsval?torabsval
ORELSEC (LemmaWjthC [C?J ,n] `rr?qinv?tozinv')
ORELSEC (LemmaWithC [C?) ,n] `rr?qdiv?tordiv'))
* ML rev?convert
let rev?convertC =
TryC
(FirstO (map Lemmac c???eqreal rr?pos rr?on?eg rr?tz
rrde?' C)
* ML ratfto?eal
let rat?torealC =
rev?convertC
ANDTHENC Higherc disseminateC
let rat?to?eal?witnessC n =
rev?ccnveftC
ANDTHENC HigherC (disseminate?vitnessC n)
References
[11 E. Bishop. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967.
REFERENCES
[2] D. 5. Bridges. Constructive Functional Analysis. Pitman, London, 1979.
[3] F. Brown, J. Chirimar and D. J. Howe. unpublished Nupri libraries.
[4]
24
J. Chirimar and D. J. Howe. Implementing Constructive Real Analysis: A Prelimi-
nary Report. In Symposium on Constructivity in Computer Science, Lecture Notes
in Computer Science, Springer V&lag, 1991.
[5] R. L. Constable. et al. Implementing ;?athematics with the Nuprl Proof Develop-
ment System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.
[6] ?V. M. Farmer and F. J. Thayer, Two Computer-Supported Proofs in Nietric Space
Topology, Notices of the Ai?S, Nov 1991, Vol. 38, number 9, pp. 1133--H1138.
[7] J. Harrison, Constructing the real numbers in Higher Order Logic.
[8] J. Harrison and L. Thery, Extending the HOL theorem prover with a Computer
Algebra System to Reason about the Reals.
[9] J. T. Udding, A Theory of Real Numbers and its Presentation in AUTOMATH,
Vo1. I--HIll, Master's Thesis, Eindhoven University of Technology, 1980.
