agda-stdlibの有理数をもっとがんばる

Rational.agda

------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational numbers
------------------------------------------------------------------------

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.Sign as Sign using (Sign)
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₂; subst)
open P.≡-Reasoning

------------------------------------------------------------------------
-- The definition

-- Rational numbers in reduced form. Note that there is exactly one
-- representative for every rational number. (This is the reason for
-- using "True" below. If Agda had proof irrelevance, then it would
-- suffice to use "isCoprime : Coprime numerator denominator".)

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

-- Constructs rational numbers. The arguments have to be in reduced
-- form.

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

  -- Note that the implicit arguments do not need to be given for
  -- concrete inputs:

  0/1 : ℚ
  0/1 = + 0 ÷ 1

  -½ : ℚ
  -½ = ℤ.- + 1 ÷ 2

------------------------------------------------------------------------
-- Equality

-- Equality of rational numbers.

infix 4 _≃_

_≃_ : Rel ℚ Level.zero
p ≃ q = numerator p ℤ.* denominator q ≡
        numerator q ℤ.* denominator p
  where open ℚ

-- _≃_ coincides with propositional equality.

≡⇒≃ : _≡_ ⇒ _≃_
≡⇒≃ 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

------------------------------------------------------------------------
-- Equality is decidable

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 ∘ ≡⇒≃)

------------------------------------------------------------------------
-- Conversions

-- Gives the sign. For zero the sign is arbitrarily chosen to be +.

sign : ℚ → Sign
sign = ℤ.sign ∘ ℚ.numerator

------------------------------------------------------------------------
-- Arithmetic

-- Negation.

infix 8 -_

-_ : ℚ → ℚ
- q = record { numerator = ℤ.- ℚ.numerator q
             ; denominator-1 = ℚ.denominator-1 q
             ; isCoprime = lemma (ℚ.numerator q) (suc (ℚ.denominator-1 q)) (ℚ.isCoprime q)
             }
  where
    ∣i∣≡∣-i∣ : ∀ i → ∣ i ∣ ≡ ∣ ℤ.- i ∣
    ∣i∣≡∣-i∣ ℤ.-[1+ n ] = refl
    ∣i∣≡∣-i∣ (+ zero) = refl
    ∣i∣≡∣-i∣ (+ suc n) = refl
    lemma : ∀ n d →
            True (C.coprime? ∣ n ∣ d) →
            True (C.coprime? ∣ ℤ.- n ∣ d)
    lemma n d cop rewrite ∣i∣≡∣-i∣ n = cop

private
  module Reduce where
    open import Data.Nat.GCD
    open import Data.Product
    open import Data.Unit

    reduce : ∀ m n → ℕ × ℕ
    reduce m n = Data.Product.map ℕDiv.quotient ℕDiv.quotient
                   (GCD.commonDivisor (proj₂ (gcd m n)))

    lemma-reduce₂≢0 : ∀ m n → n ≢ 0 → False (proj₂ (reduce m n) ℕ.≟ 0)
    lemma-reduce₂≢0 m n n≢0 with proj₂ (reduce m n) ℕ.≟ 0
    lemma-reduce₂≢0 m zero    n≢0 | yes p = n≢0 refl
    lemma-reduce₂≢0 m (suc n) n≢0 | yes p with gcd m (suc n)
    lemma-reduce₂≢0 m (suc n) n≢0 | yes p | _ , GCD.is (_ , ℕDiv.divides _ eq₂) _ rewrite p = n≢0 eq₂
    lemma-reduce₂≢0 m n       n≢0 | no ¬p = tt

    lemma-reduce-gcd1 : ∀ m n → uncurry GCD (reduce m n) 1
    lemma-reduce-gcd1 zero zero
      = GCD.is (ℕDiv.divides zero refl , ℕDiv.divides (suc zero) refl) (λ {d₁} → proj₂)
    lemma-reduce-gcd1 zero (suc n)
      = GCD.is (GCD.commonDivisor (lemma-reduce-gcd1 zero n)) (λ {d₁} → proj₂)
    lemma-reduce-gcd1 (suc m) zero
      = GCD.is (ℕDiv.divides (suc zero) refl , ℕDiv.divides zero refl) (λ {d₁} → proj₁)
    lemma-reduce-gcd1 (suc m) (suc n) with gcd (suc m) (suc n)
    lemma-reduce-gcd1 (suc m) (suc n) | zero , GCD.is (0∣Sm , 0∣Sn) _ with ℕDiv.0∣⇒≡0 0∣Sm
    lemma-reduce-gcd1 (suc m) (suc n) | zero , GCD.is (0∣Sm , 0∣Sn) _ | ()
    lemma-reduce-gcd1 (suc m) (suc n) | suc g , GCD.is (ℕDiv.divides q₁ eq₁ , ℕDiv.divides q₂ eq₂) greatest
      rewrite eq₁
            | eq₂
            = GCD.is (ℕDiv.1∣ q₁ , ℕDiv.1∣ q₂)
                (λ {d₁} →
                   λ {(d₁∣q₁ , d₁∣q₂)
                        → ℕDiv./-cong g
                          (subst (λ x → suc g ℕ.* d₁ ∣ x) (n≡n*1 (suc g))
                           (greatest
                            (subst (λ x → suc g ℕ.* d₁ ∣ x) (*-comm (suc g) q₁)
                             (ℕDiv.*-cong (suc g) d₁∣q₁)
                             ,
                             subst (λ x → suc g ℕ.* d₁ ∣ x) (*-comm (suc g) q₂)
                             (ℕDiv.*-cong (suc g) d₁∣q₂))))})
      where
        open import Data.Nat.Properties
        open import Algebra
        open CommutativeSemiring commutativeSemiring
        n≡n*1 : ∀ n → n ≡ n ℕ.* 1
        n≡n*1 n rewrite *-comm n 1 = sym (proj₂ +-identity n)

    gcd≡1→True-coprime : ∀ {m n} → GCD m n 1 → True (C.coprime? m n)
    gcd≡1→True-coprime {m} {n} gcd with C.coprime? m n
    gcd≡1→True-coprime gcd | yes p = tt
    gcd≡1→True-coprime gcd | no ¬p with ¬p (C.gcd-coprime gcd)
    gcd≡1→True-coprime gcd | no ¬p | ()

    lemma : ℕ → (d : ℕ) → d ≢ 0 → ℚ
    lemma n d d≢0 = uncurry (_÷_ ∘ +_) (reduce n d)
                      {gcd≡1→True-coprime (lemma-reduce-gcd1 n d)}
                      {lemma-reduce₂≢0 n d d≢0}

    infixl 7 _÷′_

    -- Constructs rational numbers with reduce.
    _÷′_ : (numerator : ℤ) (denominator : ℕ)
           {≢0 : False (ℕ._≟_ denominator 0)} →
           ℚ
    (n ÷′ zero) {()}
    n ÷′ suc d with ℤ.sign n
    n ÷′ suc d | Sign.- = - lemma ∣ n ∣ (suc d) (λ ())
    n ÷′ suc d | Sign.+ =   lemma ∣ n ∣ (suc d) (λ ())

-- Addition.

infixl 6 _+_

_+_ : ℚ → ℚ → ℚ
p + q = (ℚ.numerator p ℤ.* ℚ.denominator q ℤ.+
         ℚ.numerator q ℤ.* ℚ.denominator p) ÷′
        (suc (ℚ.denominator-1 p) ℕ.* suc (ℚ.denominator-1 q))
  where
    open Reduce

-- Subtraction.

infixl 6 _-_

_-_ : ℚ → ℚ → ℚ
p - q = p + - q

-- Multiplication.

infixl 7 _*_

_*_ : ℚ → ℚ → ℚ
p * q = (ℚ.numerator p ℤ.* ℚ.numerator q) ÷′
        (suc (ℚ.denominator-1 p) ℕ.* suc (ℚ.denominator-1 q))
  where
    open Reduce

-- Reciprocal.

infix 8 1/_

1/_ : (q : ℚ) {q≢0 : False (∣ ℚ.numerator q ∣ ℕ.≟ 0)} → ℚ
1/_ q {q≢0} = case sign q of λ
              { Sign.- → - (ℚ.denominator q ÷′ ∣ ℚ.numerator q ∣) {q≢0}
              ; Sign.+ →   (ℚ.denominator q ÷′ ∣ ℚ.numerator q ∣) {q≢0}
              }
  where
    open Reduce

-- Division.

infixl 7 _/_

_/_ : (p : ℚ) → (q : ℚ) {q≢0 : False (∣ ℚ.numerator q ∣ ℕ.≟ 0)} → ℚ
(p / q) {q≢0} = p * (1/ q) {q≢0}

------------------------------------------------------------------------
-- Ordering

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))