tla+ source code for the example in "How to Write a 21st Century Proof"

[William Mitchell Jr]

I am an undergraduate student working on a senior project on TLAPS. I am working through the example in "How to Write a 21st Century Proof." Can someone please post the source code for the pretty-printed version in the appendix? I am trying to illustrate the process of starting with a prose proof, structuring it, coding it in TLA+, then using the TLAPS in the TLA+ Toolbox.

Thanks,

William

[Leslie Lamport]

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

\* Last modified Tue Sep 27 23:29:24 PDT 2011 by lamport

\* Created Sat Aug 13 11:38:21 PDT 2011 by lamport

[William Mitchell Jr]

Got it. Thank you very much.