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
|
module Reals where
-- (a set with properties of) the reals
data ℝ : Set where
r0 : ℝ
r1 : ℝ
_+_ : ℝ → ℝ → ℝ
-- equality
data _==_ : ℝ → ℝ → Set where
AXrefl== : ∀ {r} → r == r
AXsymm== : ∀ {r s} → r == s → s == r
AXtrans== : ∀ {r s t} → r == s → s == t → r == t
AX+0 : ∀ {r} → (r + r0) == r
AXsymm+ : ∀ {r s} → (r + s) == (s + r)
AX+== : ∀ {r s t} → r == s → (r + t) == (s + t)
THM0+ : {r : ℝ} → r == (r0 + r)
THM0+ = AXsymm== (AXtrans== AXsymm+ AX+0)
-- AXsymm+ AX+0 r0 + r == r + r0 and r + r0 == r
-- AXtrans== so r0 + r == r
-- AXsymm== so r == r0 + r
THM0+alt : {r : ℝ} → r == (r0 + r)
THM0+alt {r} = AXsymm== {r0 + r} {r} ((AXtrans== {r0 + r} {r + r0} {r}) (AXsymm+ {r0} {r}) (AX+0 {r}))
-- strict partial ordering
data _<_ : ℝ → ℝ → Set where
AXtrans<<< : ∀ {r s t} → r < s → s < t → r < t
AX<=< : ∀ {r s t} → r < s → s == t → r < t
AX=<< : ∀ {r s t} → r == s → s < t → r < t
AX0<1 : r0 < r1
AX+<< : ∀ {r s t} → r < s → (r + t) < (s + t)
THM<+1 : {r : ℝ} → r < (r + r1)
THM<+1 = AX<=< (AX=<< THM0+ (AX+<< AX0<1)) AXsymm+
-- AX0<1 0 < 1
-- AX<+ % so 0 + r < 1 + r
-- AX=<< lem0+ % so r < 1 + r
-- AX<=< % AXsymm+ so r < r + 1
|
