# [tlaplus] Re: tla+ source code for the example in "How to Write a 21st Century Proof"

Got it. Thank you very much.
On Wednesday, November 11, 2020 at 2:03:18 PM UTC-5 Leslie Lamport wrote:
The file dates from 2011, but the version of TLAPS on my machine (which is approximately the current one) still checks the proof.

I've tried to attach the file, but I get an unexplained error.  So I've copied it below.

Leslie

------------------------------ MODULE Calculus ------------------------------
EXTENDS Reals

OpenInterval(a, b) == {r \in Real : (a < r) /\ (r < b)}
ClosedInterval(a, b) == {r \in Real : (a \leq r) /\ (r \leq b)}
SetOfIntervals == {S \in SUBSET Real : \A x, y \in S : OpenInterval(x, y) \subseteq S}

RealFunction == UNION {[S -> Real] : S \in SUBSET Real}

AbsoluteValue(a) == IF a > 0 THEN a ELSE -a
OpenBall(a, e) == {x \in Real : e > AbsoluteValue(x-a)}
PositiveReal == {r \in Real : r > 0}

IsLimitAt(f, a, b) == (b \in Real) /\
\A e \in PositiveReal : \E d \in PositiveReal :
\A x \in OpenBall(a, d) \ {a} : f[x] \in OpenBall(b, e)

IsContinuousAt(f, a) == IsLimitAt(f, a, f[a])

IsContinuousOn(f, S) == \A x \in S : IsContinuousAt(f, x)

IsDerivativeAt(f, a, b) ==
\E e \in PositiveReal :
(OpenBall(a, e) \subseteq DOMAIN f)  /\
IsLimitAt([x \in OpenBall(a,e) \ {a} |-> (f[x] - f[a]) / (x - a)], a, b)
IsDifferentiableAt(f, a) == \E b \in Real : IsDerivativeAt(f, a, b)
IsDifferentiableOn(f, S) == \A x \in S : IsDifferentiableAt(f, x)

Derivative(f) == [x \in DOMAIN f |-> CHOOSE y : IsDerivativeAt(f, x, y)]

THEOREM Theorem1 == \A f \in RealFunction : \A a \in Real :
IsDifferentiableAt(f, a) => IsContinuousAt(f, a)

IsIncreasingOn(f, I) == \A x, y \in I : (x < y) => (f[x] < f[y])

THEOREM MeanValueTheorem ==
\A f \in RealFunction : \A a, b \in Real :
(    (a < b)
/\ IsContinuousOn(f, ClosedInterval(a, b))
/\ IsDifferentiableOn(f, OpenInterval(a, b)))
=> (\E x \in OpenInterval(a,b) :
Derivative(f)[x] = (f[b]-f[a])/(b-a))

PROPOSITION Fact1 == \A x \in Real : x - x = 0
PROPOSITION Fact2 == \A x, y \in Real : (x \leq y) <=> (x < y) \/ (x = y)
PROPOSITION Fact3 == \A x, y \in Real : x - y \in Real
PROPOSITION Fact4 == \A x, y \in Real : (x < y) <=> (y - x > 0)
PROPOSITION Fact5 == \A x, y \in Real : (y > 0) /\ (x / y > 0) => (x > 0)

COROLLARY Spivak == ASSUME NEW f \in RealFunction,
NEW I \in SetOfIntervals,
IsDifferentiableOn(f, I),
\A x \in I : Derivative(f)[x] > 0
PROVE  IsIncreasingOn(f, I)

<1>1. SUFFICES ASSUME NEW a \in I, NEW b \in I, a < b
PROVE  f[a] < f[b]
BY DEF IsIncreasingOn
<1>1a.    (OpenInterval(a, b) \subseteq I)
/\ (ClosedInterval(a, b) \subseteq I)
/\ (OpenInterval(a, b) \subseteq ClosedInterval(a, b))
<2>1. OpenInterval(a, b) \subseteq I
BY DEF SetOfIntervals
<2>2. ClosedInterval(a, b) = OpenInterval(a, b) \cup {a, b}
BY <1>1, Fact2  DEF ClosedInterval, OpenInterval, SetOfIntervals
<2>3. QED
BY <2>1, <2>2
<1>2. \E x \in OpenInterval(a, b) : Derivative(f)[x] = (f[b] - f[a]) / (b-a)
<2>1. IsDifferentiableOn(f, ClosedInterval(a, b))
BY <1>1a, <1>1 DEF IsDifferentiableOn
<2>2. IsContinuousOn(f, ClosedInterval(a, b))
<3>1. SUFFICES ASSUME NEW x \in ClosedInterval(a, b)
PROVE  IsContinuousAt(f, x)
BY DEF IsContinuousOn
<3>2. IsDifferentiableAt(f, x)
BY <2>1 DEF IsDifferentiableOn
<3>3. QED
BY <3>2, Theorem1  DEF ClosedInterval
<2>3. QED
BY <1>1, <1>1a, <2>1, <2>2, MeanValueTheorem
DEF SetOfIntervals, IsDifferentiableOn
<1>3. \A x \in OpenInterval(a, b) : Derivative(f)[x] > 0
BY <1>1a
<1>4. (f[b] - f[a]) / (b-a) > 0
<2>1. PICK x \in OpenInterval(a, b) :
Derivative(f)[x] = (f[b] - f[a]) / (b-a)
BY <1>2
<2>2. Derivative(f)[x] > 0
BY <2>1 DEF SetOfIntervals
<2>3. QED
BY <2>1, <2>2
<1>5. QED
<2>1. (a \in Real) /\ (b \in Real)
BY DEF SetOfIntervals
<2>2. (f[a] \in Real) /\ (f[b] \in Real)
<3>1. SUFFICES ASSUME NEW x \in Real,
IsDifferentiableAt(f, x)
PROVE  f[x] \in Real
BY <2>1 DEF IsDifferentiableOn
<3>2. \A e \in PositiveReal : x \in OpenBall(x, e)
BY Fact1  DEF OpenBall, PositiveReal, AbsoluteValue
<3>3. x \in DOMAIN f
BY <3>1, <3>2 DEF IsDifferentiableAt, IsDerivativeAt
<3>4. QED
BY <3>3 DEF IsDifferentiableAt, IsDerivativeAt, RealFunction
<2>3. (f[b] - f[a] \in Real) /\ (b - a \in Real)
BY <2>1, <2>2, Fact3
<2>4. f[b] - f[a] > 0
BY <1>1, <1>4, <2>1, <2>3, Fact4, Fact5
<2>5. QED
BY <2>2, <2>4, Fact4
=============================================================================
\* Modification History