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