[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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

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

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


--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9eff360c-c658-4954-b33f-ca8679113c8an%40googlegroups.com.