Real.agda

-- http://www.cs.swan.ac.uk/~csetzer/articlesFromOthers/chiMing/chiMingChuangExtractionOfProgramsForExactRealNumberComputation.pdf
module Real where

open import Data.Product renaming (_×_ to _∧_)

infixl 9 ─ recip
infixl 4 _*_
infixl 3 _+_ _#_
infixl 2 ∣_∣
infix  0 _==_ _≤_ _<_

postulate
  ℝ     : Set
  0ʳ    : ℝ
  1ʳ    : ℝ
  _==_  : ℝ → ℝ → Set          {- equality           -}
  _<_   : ℝ → ℝ → Set          {- less than          -}
  _≤_   : ℝ → ℝ → Set          {- less than or equal -}
  ─     : ℝ → ℝ                {- negate             -}
  _#_   : ℝ → ℝ → Set          {- different          -}
  _+_   : ℝ → ℝ → ℝ            {- addition           -}
  _*_   : ℝ → ℝ → ℝ            {- multiplication     -}
  ∣_∣    : ℝ → ℝ                 {- absolute value     -}
  recip : (r : ℝ) → 0ʳ # r → ℝ {- multi. inverse     -}

  0<1   : 0ʳ < 1ʳ

  ─0    : ─ 0ʳ == 0ʳ
  ──x=x : {r : ℝ} → ─(─ r) == r
  ─R<0  : {r : ℝ} → 0ʳ < r → ─ r < 0ʳ

  refl==  : {r     : ℝ} → r == r
  symm==  : {r s   : ℝ} → r == s → s == r
  trans== : {r s t : ℝ} → r == s → s == t → r == t

  abs0           : ∣ 0ʳ ∣ == 0ʳ
  0≤∣x∣           : {r : ℝ} → 0ʳ ≤ ∣ r ∣
  ∣─x∣=∣x∣         : {r : ℝ} → ∣ ─ r ∣ == ∣ r ∣
  ∣xy∣=∣x∣∣y∣       : {r s : ℝ} → ∣ r * s ∣ == ∣ r ∣ * ∣ s ∣
  r∈[─n,n]→∣r∣≤n : {r s : ℝ} → (─ s ≤ r) ∧ (r ≤ s) → ∣ r ∣ ≤ s

  #less : {r s : ℝ} → r < s → r # s
  #symm : {r s : ℝ} → r # s → s # r
  0#sr  : {r s : ℝ} → 0ʳ # r → 0ʳ # s → 0ʳ # r * s

  trans≤        : {r s t : ℝ} → r ≤ s  → s ≤ t → r ≤ t
  a≤b<          : {r s   : ℝ} → r < s  → r ≤ s
  a≤b=          : {r s   : ℝ} → r == s → r ≤ s
  a≤b→b<c→a<c : {r s t : ℝ} → r ≤ s → s < t → r < t
  a<b→b≤c→a<c : {r s t : ℝ} → r < s → s ≤ t → r < t

  axiom+0  : {r     : ℝ} →      r + 0ʳ == r
  symm+    : {r s   : ℝ} →       r + s == s + r
  assoc+   : {r s t : ℝ} → r + (s + t) == (r + s) + t
  minus+   : {r s   : ℝ} →    ─(r + s) == (─ r) + (─ s)
  axiomx─x : {r     : ℝ} →   r + (─ r) == 0ʳ

  axiom*0  : {r     : ℝ} →      r * 0ʳ == 0ʳ
  axiom*1  : {r     : ℝ} →      r * 1ʳ == r
  a*─b=─ab : {r s   : ℝ} →     r * ─ s == ─ (r * s)
  symm*    : {r s   : ℝ} →       r * s == s * r
  assoc*   : {r s t : ℝ} → r * (s * t) == (r * s) * t
  distri*  : {r s t : ℝ} → r * (s + t) == r * s + r * t

  0<recip               : {r   : ℝ} → 0ʳ < r  → (p : 0ʳ # r) → 0ʳ < recip r p
  recip<0               : {r   : ℝ} → r  < 0ʳ → (p : 0ʳ # r) → recip r p < 0ʳ
  aa⁻¹=1                : {r   : ℝ} → (p : 0ʳ # r) → (r * recip r p) == 1ʳ
  x<y→1/y<1/x           : {r s : ℝ} → (p : 0ʳ # r) → (p′ : 0ʳ # s) → r < s
                        → recip s p′ < recip r p
  recipxy=recipx*recipy : {r s : ℝ} → (prs : 0ʳ # r * s)
                        → (p : 0ʳ # r) → (p′ : 0ʳ # s)
                        → recip (r * s) prs == recip r p * recip s p′
  recip==               : {r s : ℝ} → (p : 0ʳ # r) → (p′ : 0ʳ # s)
                        → r == s
                        → recip r p == recip s p′

  axiom<+       : {r s t : ℝ} → r < s → r + t < s + t
  axiom≤+       : {r s t : ℝ} → r ≤ s → r + t ≤ s + t

  axiom<*       : {r s t : ℝ} → r  < s → 0ʳ < t → r * t < s * t
  c≤0→a≤b→ac≤bc : {r s t : ℝ} → 0ʳ ≤ t → r  ≤ s → r * t ≤ s * t

  transfer==    : {P : ℝ → Set} → {r s : ℝ} → r == s → P r → P s

-- Some example numbers
2ʳ = 1ʳ + 1ʳ
3ʳ = 2ʳ + 1ʳ
4ʳ = 3ʳ + 1ʳ
5ʳ = 4ʳ + 1ʳ
6ʳ = 5ʳ + 1ʳ
7ʳ = 6ʳ + 1ʳ
8ʳ = 7ʳ + 1ʳ
9ʳ = 8ʳ + 1ʳ
─1ʳ = ─ 1ʳ
─2ʳ = ─ 2ʳ
─3ʳ = ─ 3ʳ
─4ʳ = ─ 4ʳ
─5ʳ = ─ 5ʳ
─6ʳ = ─ 6ʳ
─7ʳ = ─ 7ʳ
─8ʳ = ─ 8ʳ
─9ʳ = ─ 9ʳ

_-_ : ℝ → ℝ → ℝ
i - j = i + ─ j

postulate
  triangle      : {r s t : ℝ} → ∣ r - s ∣ ≤ ∣ r - t ∣ + ∣ t - s ∣

data Q : ℝ → Set where
  close0     : Q 0ʳ
  close1     : Q 1ʳ
  close─     : {r   : ℝ} → Q r → Q (─ r)
  close+     : {r s : ℝ} → Q r → Q s → Q (r + s)
  close*     : {r s : ℝ} → Q r → Q s → Q (r * s)
  closerecip : {r   : ℝ} → (p : 0ʳ # r) → Q r → Q (recip r p)

open import Data.Nat     using (ℕ; suc)
open import Data.Integer using (ℤ; +_; -[1+_])

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

{-
-- TODO: this axiom might be nice
thing : (r s : ℝ) → r == s → r ≡ s
thing r s reflᵣ = {!!}
-}

transfer==₂ : {P : ℝ → ℝ → Set} → {r s x y : ℝ} → r == s → x == y → P r x → P s y
transfer==₂ {_} {_} {s} {x} p₁ p₂ prx = transfer== p₂ (transfer== p₁ prx)

trans< : {r s t : ℝ} → r < s → s < t → r < t
trans< p₁ p₂ = a<b→b≤c→a<c p₁ (a≤b< p₂)

symm+0 : {r : ℝ} → 0ʳ + r == r
symm+0 = trans== (symm== symm+) axiom+0

0+n<1+n : {r : ℝ} → 0ʳ + r < 1ʳ + r
0+n<1+n = axiom<+ 0<1

n<n+1 : {r : ℝ} → r < r + 1ʳ
n<n+1 = transfer==₂ {_<_} symm+0 symm+ 0+n<1+n

1<2 : 1ʳ < 2ʳ
1<2 = n<n+1

0<2 : 0ʳ < 2ʳ
0<2 = trans< 0<1 1<2

{- Exponential functions of ℝ -}
exp : (r : ℝ) → (0ʳ # r) → ℤ → ℝ
exp x p (+ (suc 0))      = x
exp x p (+ (suc n))      = exp x p (+ n) * x
exp x p (-[1+ 0 ])       = recip x p
exp x p (-[1+ (suc n) ]) = exp x p -[1+ n ] * recip x p
exp x p (+ 0)            = 1ʳ

2^ : ℤ → ℝ {- 2^ n = 2ⁿ -}
2^ n = exp 2ʳ p n
  where
  p : 0ʳ # 2ʳ
  p = #less 0<2