forked from sabry/agda-stdlib
/
Real.agda
88 lines (76 loc) · 3.54 KB
/
Real.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
module Data.Real where
open import Data.Sum
open import Data.Rational as ℚ using (ℚ; -_ ; _*_; _÷suc_;
_-_; _+_; ∣_∣; decTotalOrder; _≤_; *≤* ; _≤?_; _÷_; ≡⇒≃)
open import Data.Rational.Properties using (ℚabs₂;
+-red₂; triang; ℚ≤lem; _⁻¹; ℚ≤-abs₁; ℚ≤-abs₂)
renaming (-swap to ℚ-swap; _+-mono_ to _ℚ+-mono_)
open import Data.Integer as ℤ using (ℤ; +_ ; -[1+_])
open import Data.Nat as ℕ using (ℕ; suc; zero; _≤?_)
open import Data.Nat.Properties.Simple using (+-right-identity)
open import Relation.Binary.Core using (Rel; IsEquivalence)
import Level
open import Relation.Nullary.Core
open import Relation.Binary using (module DecTotalOrder)
open import Relation.Binary.PropositionalEquality as P using
(_≡_; refl; subst; cong; cong₂)
open import Data.Product
import Relation.Binary.PreorderReasoning as Pre
--Constructible Real numbers as described by Bishop
--A real number is defined to be a sequence along
--with a proof that the sequence is regular
record ℝ : Set where
constructor Real
field
f : ℕ -> ℚ
reg : {n m : ℕ} -> ∣ f n - f m ∣ ≤ (suc n)⁻¹ + (suc m)⁻¹
------------------------------------------------------------------------
-- Equality of real numbers.
infix 4 _≃_
_≃_ : Rel ℝ Level.zero
x ≃ y = {n : ℕ} -> ∣ ℝ.f x n - ℝ.f y n ∣ ≤ (suc n)⁻¹ + (suc n)⁻¹
-- Proof that this is an equivalence relation-------------------
--This lemma ((2.3) in Constructive Analysis) gives us a
--useful way to show equality
postulate Bishopslem : {x y : ℝ} ->
({j : ℕ} -> ∃ λ Nⱼ -> ({m : ℕ} ->
∣ ℝ.f x (Nⱼ ℕ.+ m) - ℝ.f y (Nⱼ ℕ.+ m) ∣ ≤ (suc j)⁻¹))
-> (x ≃ y)
isEquivalence : IsEquivalence _≃_
isEquivalence = record {
refl = λ {x} -> refl≃ {x} ;
sym = λ {x}{y} -> sym≃ {x}{y};
trans = λ {a}{b}{c} -> trans≃ {a}{b}{c}
}
where
--reflexitivity
refl≃ : {x : ℝ} -> (x ≃ x)
refl≃ {x} = ℝ.reg x
--symmetry
sym≃ : {x y : ℝ} -> (x ≃ y -> y ≃ x)
sym≃ {x}{y} x≃y = λ {n} ->
subst (λ a -> a ≤ (suc n)⁻¹ ℚ.+ (suc n)⁻¹)
(ℚabs₂ (ℝ.f x n) (ℝ.f y n)) (x≃y {n})
--transitivity
trans≃ : {x y z : ℝ} -> (x ≃ y) -> (y ≃ z) -> (x ≃ z)
trans≃ {x}{y}{z} x≃y y≃z = Bishopslem {x}{z} (λ {j} ->
Nⱼ {j} , λ {n} -> (begin
∣ ℝ.f x (Nⱼ {j} ℕ.+ n) - ℝ.f z (Nⱼ {j} ℕ.+ n) ∣
∼⟨ triang (ℝ.f x (Nⱼ {j} ℕ.+ n)) (ℝ.f y (Nⱼ {j} ℕ.+ n)) (ℝ.f z (Nⱼ {j} ℕ.+ n)) ⟩
∣ ℝ.f x (Nⱼ {j} ℕ.+ n) - ℝ.f y (Nⱼ {j} ℕ.+ n) ∣ +
∣ ℝ.f y (Nⱼ {j} ℕ.+ n) - ℝ.f z (Nⱼ {j} ℕ.+ n) ∣
∼⟨ (x≃y {Nⱼ {j} ℕ.+ n}) ℚ+-mono (y≃z {Nⱼ {j} ℕ.+ n}) ⟩
((suc (Nⱼ {j} ℕ.+ n))⁻¹ ℚ.+ (suc (Nⱼ {j} ℕ.+ n))⁻¹) ℚ.+
((suc (Nⱼ {j} ℕ.+ n))⁻¹ ℚ.+ (suc (Nⱼ {j} ℕ.+ n))⁻¹)
∼⟨ ((ℚ≤lem {Nⱼ {j}} {n}) ℚ+-mono (ℚ≤lem {Nⱼ {j}} {n}))
ℚ+-mono
((ℚ≤lem {Nⱼ {j}} {n}) ℚ+-mono (ℚ≤lem {Nⱼ {j}} {n})) ⟩
((suc (Nⱼ {j}))⁻¹ ℚ.+ (suc (Nⱼ {j}))⁻¹) ℚ.+
((suc (Nⱼ {j}))⁻¹ ℚ.+ (suc (Nⱼ {j}))⁻¹)
∼⟨ ≈->≤ (+-red₂ j) ⟩
((suc j)⁻¹ ∎) ))
where
open DecTotalOrder ℚ.decTotalOrder using ()
renaming (reflexive to ≈->≤; trans to ≤trans; isPreorder to ℚisPreorder)
open Pre record {isPreorder = ℚisPreorder}
Nⱼ = λ {j} -> suc ((suc (j ℕ.+ j) ℕ.+ (suc (j ℕ.+ j))))