/
Rational.agda
53 lines (35 loc) · 1.12 KB
/
Rational.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
open import Agda.Builtin.Nat
renaming ( Nat to ℕ
; _<_ to boolltℕ
; _+_ to _+ℕ_
; _-_ to _-ℕ_
; _*_ to _*ℕ_)
open import Natural renaming (_≤_ to _≤ℕ_)
open import Integer
renaming ( _≤_ to _≤ℤ_
; _+_ to _+ℤ_
; _-_ to _-ℤ_
; _*_ to _*ℤ_
; abs to absℤ )
open import common
data ℚ : Set where
quotient : ℤ → ℕ⁺ → ℚ
recip : ℕ⁺ → ℚ
recip n = quotient (wpos 1) n
rat : ℤ → ℚ
rat a = quotient a (csuc 0)
infixl 4 _≤_
infixl 6 _+_ _-_
infixl 7 _*_
_≤_ : ℚ → ℚ → Set
quotient a n ≤ quotient b m = a *ℤ pos m ≤ℤ b *ℤ pos n
_+_ : ℚ → ℚ → ℚ
quotient a n + quotient b m = quotient (a *ℤ pos m +ℤ b *ℤ pos n) (n *ℕ⁺ m)
_-_ : ℚ → ℚ → ℚ
quotient a n - quotient b m = quotient a n + quotient (wpos 0 -ℤ b) m
_*_ : ℚ → ℚ → ℚ
quotient a n * quotient b m = quotient (a *ℤ b) (n *ℕ⁺ m)
abs : ℚ → ℚ
abs (quotient a sn) = quotient (absℤ a) sn
-- half = quotient (wpos 1) (csuc 1)
-- third = quotient (wpos 1) (csuc 2)