module Data.Rational where
import Algebra
import Data.Bool.Properties as Bool
open import Function
open import Data.Integer as ℤ using (ℤ; ∣_∣; +_; -_)
open import Data.Integer.Divisibility as ℤDiv using (Coprime)
import Data.Integer.Properties as ℤ
open import Data.Nat.Divisibility as ℕDiv using (_∣_)
import Data.Nat.Coprimality as C
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Sum
import Level
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
using (_≡_; refl; cong; cong₂)
open P.≡-Reasoning
record ℚ : Set where
field
numerator : ℤ
denominator-1 : ℕ
isCoprime : True (C.coprime? ∣ numerator ∣ (suc denominator-1))
denominator : ℤ
denominator = + suc denominator-1
coprime : Coprime numerator denominator
coprime = toWitness isCoprime
infixl 7 _÷_
_÷_ : (numerator : ℤ) (denominator : ℕ)
{coprime : True (C.coprime? ∣ numerator ∣ denominator)}
{≢0 : False (ℕ._≟_ denominator 0)} →
ℚ
(n ÷ zero) {≢0 = ()}
(n ÷ suc d) {c} =
record { numerator = n; denominator-1 = d; isCoprime = c }
private
0/1 : ℚ
0/1 = + 0 ÷ 1
-½ : ℚ
-½ = - + 1 ÷ 2
infix 4 _≃_
_≃_ : Rel ℚ Level.zero
p ≃ q = numerator p ℤ.* denominator q ≡
numerator q ℤ.* denominator p
where open ℚ
≡⇒≃ : _≡_ ⇒ _≃_
≡⇒≃ refl = refl
≃⇒≡ : _≃_ ⇒ _≡_
≃⇒≡ {i = p} {j = q} =
helper (numerator p) (denominator-1 p) (isCoprime p)
(numerator q) (denominator-1 q) (isCoprime q)
where
open ℚ
helper : ∀ n₁ d₁ c₁ n₂ d₂ c₂ →
n₁ ℤ.* + suc d₂ ≡ n₂ ℤ.* + suc d₁ →
(n₁ ÷ suc d₁) {c₁} ≡ (n₂ ÷ suc d₂) {c₂}
helper n₁ d₁ c₁ n₂ d₂ c₂ eq
with Poset.antisym ℕDiv.poset 1+d₁∣1+d₂ 1+d₂∣1+d₁
where
1+d₁∣1+d₂ : suc d₁ ∣ suc d₂
1+d₁∣1+d₂ = ℤDiv.coprime-divisor (+ suc d₁) n₁ (+ suc d₂)
(C.sym $ toWitness c₁) $
ℕDiv.divides ∣ n₂ ∣ (begin
∣ n₁ ℤ.* + suc d₂ ∣ ≡⟨ cong ∣_∣ eq ⟩
∣ n₂ ℤ.* + suc d₁ ∣ ≡⟨ ℤ.abs-*-commute n₂ (+ suc d₁) ⟩
∣ n₂ ∣ ℕ.* suc d₁ ∎)
1+d₂∣1+d₁ : suc d₂ ∣ suc d₁
1+d₂∣1+d₁ = ℤDiv.coprime-divisor (+ suc d₂) n₂ (+ suc d₁)
(C.sym $ toWitness c₂) $
ℕDiv.divides ∣ n₁ ∣ (begin
∣ n₂ ℤ.* + suc d₁ ∣ ≡⟨ cong ∣_∣ (P.sym eq) ⟩
∣ n₁ ℤ.* + suc d₂ ∣ ≡⟨ ℤ.abs-*-commute n₁ (+ suc d₂) ⟩
∣ n₁ ∣ ℕ.* suc d₂ ∎)
helper n₁ d c₁ n₂ .d c₂ eq | refl with ℤ.cancel-*-right
n₁ n₂ (+ suc d) (λ ()) eq
helper n d c₁ .n .d c₂ eq | refl | refl with Bool.proof-irrelevance c₁ c₂
helper n d c .n .d .c eq | refl | refl | refl = refl
infix 4 _≟_
_≟_ : Decidable {A = ℚ} _≡_
p ≟ q with ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≟
ℚ.numerator q ℤ.* ℚ.denominator p
p ≟ q | yes pq≃qp = yes (≃⇒≡ pq≃qp)
p ≟ q | no ¬pq≃qp = no (¬pq≃qp ∘ ≡⇒≃)
infix 4 _≤_ _≤?_
data _≤_ : ℚ → ℚ → Set where
*≤* : ∀ {p q} →
ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤
ℚ.numerator q ℤ.* ℚ.denominator p →
p ≤ q
drop-*≤* : ∀ {p q} → p ≤ q →
ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤
ℚ.numerator q ℤ.* ℚ.denominator p
drop-*≤* (*≤* pq≤qp) = pq≤qp
_≤?_ : Decidable _≤_
p ≤? q with ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤?
ℚ.numerator q ℤ.* ℚ.denominator p
p ≤? q | yes pq≤qp = yes (*≤* pq≤qp)
p ≤? q | no ¬pq≤qp = no (λ { (*≤* pq≤qp) → ¬pq≤qp pq≤qp })
decTotalOrder : DecTotalOrder _ _ _
decTotalOrder = record
{ Carrier = ℚ
; _≈_ = _≡_
; _≤_ = _≤_
; isDecTotalOrder = record
{ isTotalOrder = record
{ isPartialOrder = record
{ isPreorder = record
{ isEquivalence = P.isEquivalence
; reflexive = refl′
; trans = trans
}
; antisym = antisym
}
; total = total
}
; _≟_ = _≟_
; _≤?_ = _≤?_
}
}
where
module ℤO = DecTotalOrder ℤ.decTotalOrder
refl′ : _≡_ ⇒ _≤_
refl′ refl = *≤* ℤO.refl
trans : Transitive _≤_
trans {i = p} {j = q} {k = r} (*≤* le₁) (*≤* le₂)
= *≤* (ℤ.cancel-*-+-right-≤ _ _ _
(lemma
(ℚ.numerator p) (ℚ.denominator p)
(ℚ.numerator q) (ℚ.denominator q)
(ℚ.numerator r) (ℚ.denominator r)
(ℤ.*-+-right-mono (ℚ.denominator-1 r) le₁)
(ℤ.*-+-right-mono (ℚ.denominator-1 p) le₂)))
where
open Algebra.CommutativeRing ℤ.commutativeRing
lemma : ∀ n₁ d₁ n₂ d₂ n₃ d₃ →
n₁ ℤ.* d₂ ℤ.* d₃ ℤ.≤ n₂ ℤ.* d₁ ℤ.* d₃ →
n₂ ℤ.* d₃ ℤ.* d₁ ℤ.≤ n₃ ℤ.* d₂ ℤ.* d₁ →
n₁ ℤ.* d₃ ℤ.* d₂ ℤ.≤ n₃ ℤ.* d₁ ℤ.* d₂
lemma n₁ d₁ n₂ d₂ n₃ d₃
rewrite *-assoc n₁ d₂ d₃
| *-comm d₂ d₃
| sym (*-assoc n₁ d₃ d₂)
| *-assoc n₃ d₂ d₁
| *-comm d₂ d₁
| sym (*-assoc n₃ d₁ d₂)
| *-assoc n₂ d₁ d₃
| *-comm d₁ d₃
| sym (*-assoc n₂ d₃ d₁)
= ℤO.trans
antisym : Antisymmetric _≡_ _≤_
antisym (*≤* le₁) (*≤* le₂) = ≃⇒≡ (ℤO.antisym le₁ le₂)
total : Total _≤_
total p q =
[ inj₁ ∘′ *≤* , inj₂ ∘′ *≤* ]′
(ℤO.total (ℚ.numerator p ℤ.* ℚ.denominator q)
(ℚ.numerator q ℤ.* ℚ.denominator p))