real.tla

------------------------------ MODULE real ------------------------------- 

EXTENDS Naturals, Integers, Sequences, FiniteSets, FiniteSetsExt, NaturalsInduction

CONSTANT max

McNat == 0..max

(***********************************************************************)
(* Approximate sqrt(r)                                                  *)
(***********************************************************************)

\* approx ∈ ℝ → (ℤ → ℤ )
GenericApprox(f(_,_), n) == { k \in Nat : f(k, n) }

Sqrt(r, n) == GenericApprox(LAMBDA k, m: k * k <= r * (m * m), n)

Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y

\* approx(√ r, n) ≡ max({ k | k ∈ ℕ ∧ k² ≤ 2 * n² })
ApproxSqrt(r, n) == << Maximum(Sqrt(r, n)), n >>

(***********************************************************************)
(* Approximate exp(z)                                                  *)
(***********************************************************************)

Factorial[n \in Nat] == IF n = 0 THEN 1 ELSE n * Factorial[n-1]

SameDenominator(x, y) == CHOOSE k \in Nat : x * k = y

Pow(x,n) == FoldSet(LAMBDA y, acc:  x * acc, 1, 1..n)

TaylorSery(z, n) == LET fact_n == Factorial[n] IN
    FoldSet(LAMBDA x, acc:  Pow(z,x) * SameDenominator(Factorial[x], fact_n) + acc , 0, 0..n)

Exp(z, n) == GenericApprox(LAMBDA k, m: k <= TaylorSery(z,m), n)

ExpApprox(z, n) ==  << Maximum(Exp(z, n)), Factorial[n] >>


(***********************************************************************)
(* Reals Set                                                           *)
(***********************************************************************)

\* f(0) = 0
Q1(f) == f[0] = 0

\* ∀ m, ℤ \ ℕ ⟹ f(m) - f(n) 
Q2(f) == \A m \in Int \ Nat : f[m] = - f[-m]

Q3(f) == \E k \in Nat : \A m, n \in Nat \ {0} : (f[m + n] - f[m] - f[n]) <= k

Q(f) ==  f \in [Int -> Int] /\ Q1(f) /\ Q2(f) /\ Q3(f)

\* ℝ ≡ { f : f ∈ ℤ → ℤ ∧ Q1 ∧ Q2 ∧ Q3 }
Reals == { f \in [ Int -> Int ] : Q(f) }

Abs(x) == IF x < 0 THEN -x ELSE x

\* f = g ≡ ∃ k, k ∈ ℕ ∧ (∀ n, n ∈ ℕ ⟹ |f(n) - g(n)| ≤ k )
Equal(f, g) == f \in [Int -> Int] /\ g \in [Int -> Int] /\ \E k \in Nat : \A n \in Nat : Abs(f[n] - g[n]) <= k

AXIOM EquivRefl == \A f \in Reals : Equal(f, f)

AXIOM EquivSym == \A f, g \in Reals : Equal(f, g) = Equal(g, f)

AXIOM EquivTrans == \A f, g, h \in Reals : Equal(f, g) /\ Equal(g, h) => Equal(f, h)

LEMMA FunEquiv == \A f1 \in Reals: 
                    \A f2 \in  { f \in [ Int -> Int ] : Q1(f) /\ Q2(f)  } :
                    (\E k \in Nat : \A n \in Nat \ {0} : Abs(f1[n] - f2[n]) <= k)
                    => f2 \in Reals
<1> USE DEF Reals, Q, Q1, Q2, Q3, Abs
<1> SUFFICES ASSUME NEW f1 \in Reals, 
                    NEW f2 \in [ Int -> Int ],
                    Q1(f2),
                    Q2(f2),
                    NEW k \in Nat, 
                    \A n \in Nat \ {0} : Abs(f1[n] - f2[n]) <= k
             PROVE  f2 \in Reals
    OBVIOUS
<1>2. PICK k1 \in Nat : \A m, n \in Nat \ {0} :
                                        f1[m + n] - f1[m] - f1[n] =< k1
    OBVIOUS
<1>3. Q3(f2)
    <2>. f1 \in [ Int -> Int ] /\ f2 \in [ Int -> Int ] OBVIOUS
    <2>1. WITNESS (k1 + 3*k) \in Nat
    <2>2. TAKE m, n \in Nat \ {0}
    <2>3. f2[m + n] <= f1[m + n] + Abs(f1[m + n] - f2[m + n]) OBVIOUS
    <2>4. @ <= f1[m] + f1[n] + k1 + k   BY <1>2
    <2>5. @ <= f2[m] + Abs(f1[m] - f2[m]) + f2[n] + Abs(f1[n] - f2[n]) + k1 + k OBVIOUS
    <2>6. @ <= f2[m] + k + f2[n] + k + k1 + k OBVIOUS
    <2>. HIDE DEF Abs
    <2>. \A x \in Int : Abs(x) \in Nat  BY DEF Abs
    <2>. f2[m + n] - f2[m] - f2[n] <= k1 + 3*k    BY <2>3, <2>4, <2>5, <2>6
    <2>. QED OBVIOUS
<1> QED BY <1>3                 


\*∀f · f ∈ R ⇒ ∃k · k ∈ N ∧ (∀m, n · m ∈ Z ∧ n ∈ Z ⇒ |f(m + n) − f(m) − f(n)| ≤ k)
LEMMA Q3bis == \A f \in Reals :
                    \E k \in Nat:
                         \A m, n \in Int:
                            Abs(f[m + n] - f[m] - f[n]) <= k
                             

THEOREM MyNatInduction ==
  ASSUME NEW P(_),
         P(1),
         \A n \in Nat \ {0} : P(n) => P(n+1)
  PROVE  \A n \in Nat \ {0} : P(n)

LEMMA SlopeCancel == 
                    ASSUME NEW f \in [ Int -> Int ],
                    NEW m \in Int,
                    NEW n \in Int,
                    Q1(f),
                    Q2(f),
                    NEW k \in Nat, 
                    \A m1, n1 \in Int:
                       Abs(f[m1 + n1] - f[m1] - f[n1]) =< k
                    
             PROVE Abs(f[m * n] - m * f[ n ]) <= Abs(m) * k
<1> USE DEF Reals, Q, Q1, Q2, Q3
<1> f \in [ Int -> Int ] OBVIOUS
<1> (m > 0) \/ (m = 0) \/ (m < 0) OBVIOUS
<1>a. CASE m > 0 
    <2>. m \in Nat \ {0} BY <1>a
    <2>2. DEFINE P(x) == Abs(f[x * n] - x * f[ n ]) <= Abs(x) * k
    <2>3. P(1)
        BY DEF Abs
    <2>4. ASSUME NEW x \in Nat, P(x)
            PROVE  P(x+1)
        <3>2. (Abs(f[x * n + n] - f[x * n] - f[n]) =< k) OBVIOUS
        <3>3. (Abs(f[x * n + n] - x * f[n] - f[n]) =<  Abs(x) * k + k) BY <2>4, <3>2
\*        <3>4.  @ = (Abs(f[(x + 1) * n] - (x + 1) * f[n]) =< Abs(x + 1) * k) OBVIOUS
        <3> QED BY <2>4
    <2>5. \A x \in Nat : P(x)
        <4> TAKE x \in Nat
        <4> HIDE DEF P
        <4> QED BY <2>3, <2>4, MyNatInduction
    <2>6. QED BY <1>a, <2>5 DEF Abs, Q, Q1, Q2
<1>b. CASE m = 0
    <2> QED BY <1>b DEF Reals, Abs, Q, Q1
<1>c. CASE m < 0
    <2> QED BY <1>c
<1>7. QED BY <1>a, <1>b, <1>c
===============================================