[ bug ] Fixed two bugs in Rational and simplified (#681)

Author: MatthewDaggitt

CHANGELOG.md

@@ -448,6 +448,22 @@ Non-backwards compatible changes
   `decSetoid` and `_==_` to be moved from `Data.(Char/String).Unsafe` to
   `Data.(Char/String).Properties`.
 
+####  Overhaul of `Data.Rational`
+
+* Many new operators have been added to `Data.Rational` including
+  addition, substraction, multiplication, inverse etc.
+
+* The existing operator `_÷_` has been renamed `_/_` and is now more liberal
+  as it now accepts non-coprime arguments (e.g. `+ 2 / 4`) which are then
+  normalised.
+
+* The old name `_÷_` has been repurposed to represent division between two
+  rationals.
+
+* The proofs `drop-*≤*`, `≃⇒≡` and `≡⇒≃` have been moved from `Data.Rational`
+  to `Data.Rational.Properties`.
+
+
 #### Changes in `Data.List`
 
 * In `Data.List.Membership.Propositional.Properties`:
@@ -497,9 +513,6 @@ Non-backwards compatible changes
 * The type `Coprime` and proof `coprime-divisor` have been moved from
   `Data.Integer.Divisibility` to `Data.Integer.Coprimality`.
 
-* The proofs `drop-*≤*`, `≃⇒≡` and `≡⇒≃` have been moved from `Data.Rational`
-  to `Data.Rational.Properties`.
-
 * The functions `fromMusical` and `toMusical` were moved from the `Codata` modules
   to the corresponding `Codata.Musical` modules.
 
@@ -1136,7 +1149,6 @@ Other minor additions
 
 * Added new functions to `Data.Rational`:
   ```agda
-  norm-mkℚ : (n : ℤ) (d : ℕ) → d ≢0 → ℚ
   -_       : ℚ → ℚ
   1/_      : (p : ℚ) → .{n≢0 : ∣ ℚ.numerator p ∣ ≢0} → ℚ
   _*_      : ℚ → ℚ → ℚ

src/Data/Rational.agda

@@ -23,26 +23,11 @@ open import Data.Nat.Properties public
   using (_≟_; _≤?_)
 
 ------------------------------------------------------------------------
--- Publicly re-export contents of core module
+-- Method for displaying rationals
 
 show : ℚ → String
 show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)
 
-------------------------------------------------------------------------------
--- Some constants
-
-0ℚ : ℚ
-0ℚ = + 0 ÷ 1
-
-1ℚ : ℚ
-1ℚ = + 1 ÷ 1
-
-½ : ℚ
-½ = + 1 ÷ 2
-
--½ : ℚ
--½ = - ½
-
 ------------------------------------------------------------------------
 -- Deprecated
 

src/Data/Rational/Base.agda

@@ -11,18 +11,15 @@ module Data.Rational.Base where
 open import Function using (id)
 open import Data.Integer as ℤ using (ℤ; ∣_∣; +_; -[1+_])
 open import Data.Nat.GCD
-open import Data.Nat.Divisibility as ℕDiv using (_∣_ ; divides ; ∣-antisym)
-open import Data.Nat.Coprimality as C using (Coprime; coprime?; Bézout-coprime)
+open import Data.Nat.Divisibility as ℕDiv using (divides; 0∣⇒≡0)
+open import Data.Nat.Coprimality as C using (Coprime; Bézout-coprime)
 open import Data.Nat as ℕ using (ℕ; zero; suc)
-import Data.Nat.Properties as ℕ
 open import Data.Product
-open import Data.Unit using (tt)
 open import Level using (0ℓ)
-open import Relation.Nullary.Decidable
-  using (True; False; toWitness)
+open import Relation.Nullary.Decidable using (False)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary using (Rel; Decidable; _⇒_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; subst; cong; cong₂; module ≡-Reasoning)
 
 open ≡-Reasoning
@@ -38,13 +35,17 @@ record ℚ : Set where
     denominator-1 : ℕ
     .isCoprime    : Coprime ∣ numerator ∣ (suc denominator-1)
 
+  denominatorℕ : ℕ
+  denominatorℕ = suc denominator-1
+
   denominator : ℤ
-  denominator = + suc denominator-1
+  denominator = + denominatorℕ
 
 open ℚ public using ()
   renaming
-  ( numerator   to ↥_
-  ; denominator to ↧_
+  ( numerator    to ↥_
+  ; denominator  to ↧_
+  ; denominatorℕ to ↧ₙ_
   )
 
 ------------------------------------------------------------------------
@@ -53,114 +54,97 @@ open ℚ public using ()
 infix 4 _≃_
 
 _≃_ : Rel ℚ 0ℓ
-p ≃ q = (↥ p ℤ.* ↧ q) ≡ (↥ q) ℤ.* (↧ p)
+p ≃ q = (↥ p ℤ.* ↧ q) ≡ (↥ q ℤ.* ↧ p)
 
 ------------------------------------------------------------------------
 -- Ordering of rationals
 
 infix 4 _≤_
 
-data _≤_ : ℚ → ℚ → Set where
+data _≤_ : Rel ℚ 0ℓ where
   *≤* : ∀ {p q} → (↥ p ℤ.* ↧ q) ℤ.≤ (↥ q ℤ.* ↧ p) → p ≤ q
 
 ------------------------------------------------------------------------
--- Two useful lemmas to help with constructing on rationals
---
--- normalize takes two natural numbers, say 6 and 21 and their gcd 3, and
--- returns them normalized as 2 and 7 and a proof that they are coprime
+-- Negation
+
+pattern +0       = + 0
+pattern +[1+_] n = + suc n
+
+-_ : ℚ → ℚ
+- mkℚ -[1+ n ] d prf = mkℚ +[1+ n ] d prf
+- mkℚ +0       d prf = mkℚ +0       d prf
+- mkℚ +[1+ n ] d prf = mkℚ -[1+ n ] d prf
+
+------------------------------------------------------------------------
+-- Constructing rationals
 
 infix 4 _≢0
 _≢0 : ℕ → Set
 n ≢0 = False (n ℕ.≟ 0)
 
--- introducing a notation for that nasty pattern
-pattern ⟨_&_∧_&_⟩ p eqp q eqq = GCD.is (divides p eqp , divides q eqq) _
-
-normalize : ∀ m n g .{m≢0 : m ≢0} .{n≢0 : n ≢0} .{g≢0 : g ≢0} → GCD m n g →
-            Σ[ p ∈ ℕ ] Σ[ q ∈ ℕ ] Coprime (suc p) (suc q) × m ℕ.* suc q ≡ n ℕ.* suc p
-normalize 0       n       g {m≢0 = ()} _
-normalize m       0       g {n≢0 = ()} _
-normalize m       n       0 {g≢0 = ()} _
-normalize (suc _) n       g          ⟨ 0     & ()    ∧ q     & n≡qg' ⟩
-normalize m       (suc _) g          ⟨ p     & m≡pg' ∧ 0     & () ⟩
-normalize(suc _)  (suc _) (suc g) G@(⟨ suc p & refl  ∧ suc q & refl ⟩)
-  = p , q , Bézout-coprime (Bézout.identity G) , (begin
-    (suc p ℕ.* suc g) ℕ.* suc q ≡⟨ ℕ.*-assoc (suc p) (suc g) (suc q) ⟩
-    suc p ℕ.* (suc g ℕ.* suc q) ≡⟨ cong (suc p ℕ.*_) (ℕ.*-comm (suc g) (suc q)) ⟩
-    suc p ℕ.* (suc q ℕ.* suc g) ≡⟨ ℕ.*-comm (suc p) _ ⟩
-    (suc q ℕ.* suc g) ℕ.* suc p ∎)
-
--- a version of gcd that returns a proof that the result is non-zero given
--- that one of the inputs is non-zero
-
-gcd≢0 : (m n : ℕ) {m≢0 : m ≢0} → Σ[ d ∈ ℕ ] GCD m n d × d ≢0
-gcd≢0 m  n {m≢0} with gcd m n
-... | (suc d , G)  = (suc d , G , tt)
-... | (0 , GCD.is (0|m , _) _) with ℕDiv.0∣⇒≡0 0|m
-...   | refl = contradiction m≢0 id
+-- A constructor for ℚ that takes two natural numbers, say 6 and 21,
+-- and returns them in a normalized form, e.g. say 2 and 7
 
-pattern +0       = + 0
-pattern +[1+_] n = + suc n
+normalize : ∀ m n .{m≢0 : m ≢0} .{n≢0 : n ≢0} → ℚ
+normalize (suc m) (suc n) with gcd (suc m) (suc n)
+... | zero  , GCD.is (1+m∣0 , _) _ = contradiction (0∣⇒≡0 1+m∣0) λ()
+... | suc g , G@(GCD.is (divides (suc p) refl , divides (suc q) refl) _)
+  = mkℚ (+ suc p) q (Bézout-coprime (Bézout.identity G))
 
-norm-mkℚ : (n : ℤ) (d : ℕ) → .{d≢0 : d ≢0} → ℚ
-norm-mkℚ +0       d {d≢0} = mkℚ +0 0 (C.sym (C.1-coprimeTo 0))
-norm-mkℚ -[1+ n ] d {d≢0} =
-  let (q , gcd , q≢0)      = gcd≢0 (suc n) d
-      (n′ , d′ , prf , eq) = normalize (suc n) d q {_} {d≢0} {q≢0} gcd
-  in mkℚ -[1+ n′ ] d′ prf
-norm-mkℚ +[1+ n ] d {d≢0} =
-  let (q , gcd , q≢0)      = gcd≢0 (suc n) d
-      (n′ , d′ , prf , eq) = normalize (suc n) d q {_} {d≢0} {q≢0} gcd
-  in mkℚ (+ suc n′) d′ prf
+-- A constructor for ℚ that (unlike mkℚ) automatically normalises it's
+-- arguments. See the constants section below for how to use this operator.
 
-------------------------------------------------------------------------------
--- Operations on rationals
+infixl 7 _/_
 
-infix  8 -_ 1/_
-infixl 7 _*_ _/_ _÷_
-infixl 6 _-_ _+_
-
--- unary negation
+_/_ : (n : ℤ) (d : ℕ) → .{d≢0 : d ≢0} → ℚ
+_/_ +0       d {d≢0} = mkℚ +0 0 (C.sym (C.1-coprimeTo 0))
+_/_ +[1+ n ] d {d≢0} =   normalize (suc n) d {_} {d≢0}
+_/_ -[1+ n ] d {d≢0} = - normalize (suc n) d {_} {d≢0}
 
--_ : ℚ → ℚ
-- mkℚ -[1+ n ] d prf = mkℚ +[1+ n ] d prf
-- mkℚ +0       d prf = mkℚ +0       d prf
-- mkℚ +[1+ n ] d prf = mkℚ -[1+ n ] d prf
+------------------------------------------------------------------------------
+-- Some constants
 
--- reciprocal: requires a proof that the numerator is not zero
+0ℚ : ℚ
+0ℚ = + 0 / 1
 
-1/_ : (p : ℚ) → .{n≢0 : ∣ ↥ p ∣ ≢0} → ℚ
-(1/ mkℚ +0 d prf) {()}
-1/ mkℚ +[1+ n ] d prf = mkℚ +[1+ d ] n (C.sym prf)
-1/ mkℚ -[1+ n ] d prf = mkℚ -[1+ d ] n (C.sym prf)
+1ℚ : ℚ
+1ℚ = + 1 / 1
 
--- multiplication
+½ : ℚ
+½ = + 1 / 2
 
-_*_ : ℚ → ℚ → ℚ
-mkℚ n₁ d₁ prf₁ * mkℚ n₂ d₂ prf₂ = norm-mkℚ (n₁ ℤ.* n₂) (suc d₁ ℕ.* suc d₂)
+-½ : ℚ
+-½ = - ½
 
--- division
+------------------------------------------------------------------------------
+-- Operations on rationals
 
-_÷_ : (numerator : ℤ) (denominator : ℕ)
-      .{coprime : True (coprime? ∣ numerator ∣ denominator)}
-      {≢0 : denominator ≢0} →
-      ℚ
-(n ÷ zero)  {≢0 = ()}
-(n ÷ suc d) {c} = mkℚ n d (toWitness c)
+infix  8 -_ 1/_
+infixl 7 _*_ _÷_
+infixl 6 _-_ _+_
 
 -- addition
 
 _+_ : ℚ → ℚ → ℚ
-mkℚ n₁ d₁ prf₁ + mkℚ n₂ d₂ prf₂ = norm-mkℚ
-  (n₁ ℤ.* (+[1+ d₂ ]) ℤ.+ n₂ ℤ.* (+[1+ d₂ ]))
-  (suc d₁ ℕ.* suc d₂)
+p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)
+
+-- multiplication
+
+_*_ : ℚ → ℚ → ℚ
+p * q = (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)
 
 -- subtraction
 
 _-_ : ℚ → ℚ → ℚ
 p - q = p + (- q)
 
--- division
+-- reciprocal: requires a proof that the numerator is not zero
+
+1/_ : (p : ℚ) → .{n≢0 : ∣ ↥ p ∣ ≢0} → ℚ
+1/ mkℚ +[1+ n ] d prf = mkℚ +[1+ d ] n (C.sym prf)
+1/ mkℚ -[1+ n ] d prf = mkℚ -[1+ d ] n (C.sym prf)
+
+-- division: requires a proof that the denominator is not zero
 
-_/_ : (p q : ℚ) → {n≢0 : ∣ ↥ q ∣ ≢0} → ℚ
-(p / q) {n≢0} = p * (1/_ q {n≢0})
+_÷_ : (p q : ℚ) → .{n≢0 : ∣ ↥ q ∣ ≢0} → ℚ
+(p ÷ q) {n≢0} = p * (1/_ q {n≢0})

src/Data/Rational/Properties.agda

@@ -9,19 +9,30 @@
 module Data.Rational.Properties where
 
 open import Function using (_∘_ ; _$_)
-open import Data.Integer as ℤ using (ℤ; ∣_∣; +_)
+open import Data.Integer as ℤ using (ℤ; ∣_∣; +_; -[1+_])
 open import Data.Integer.Coprimality using (coprime-divisor)
 import Data.Integer.Properties as ℤ
 open import Data.Rational.Base
 open import Data.Nat as ℕ using (ℕ; zero; suc)
-open import Data.Nat.Coprimality as C using (Coprime)
-open import Data.Nat.Divisibility
+import Data.Nat.Properties as ℕ
+open import Data.Nat.Coprimality as C using (Coprime; coprime?)
+open import Data.Nat.Divisibility hiding (/-cong)
+open import Data.Product using (_,_)
 open import Data.Sum
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P
-  using (_≡_; refl; sym; cong; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary using (Dec; yes; no; recompute)
-open import Relation.Nullary.Decidable using (True; fromWitness)
+open import Relation.Nullary.Decidable as Dec′ using (True; fromWitness)
+
+open import Algebra.FunctionProperties {A = ℚ} _≡_
+open import Algebra.FunctionProperties.Consequences.Propositional
+
+------------------------------------------------------------------------
+-- Helper lemmas
+
+private
+  recomputeCP : ∀ {n d} → .(Coprime n (suc d)) → Coprime n (suc d)
+  recomputeCP {n} {d-1} c = recompute (coprime? n (suc d-1)) c
 
 ------------------------------------------------------------------------
 -- Equality
@@ -36,30 +47,21 @@ open import Relation.Nullary.Decidable using (True; fromWitness)
 
   1+d₁∣1+d₂ : suc d₁ ∣ suc d₂
   1+d₁∣1+d₂ = coprime-divisor (+ suc d₁) n₁ (+ suc d₂)
-    (C.sym (recompute (C.coprime? ∣ n₁ ∣ (suc d₁)) c₁)) $
+    (C.sym (recomputeCP c₁)) $
     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₁ = coprime-divisor (+ suc d₂) n₂ (+ suc d₁)
-    (C.sym (recompute (C.coprime? ∣ n₂ ∣ (suc d₂)) c₂)) $
+    (C.sym (recomputeCP c₂)) $
     divides ∣ n₁ ∣ (begin
-      ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ cong ∣_∣ (P.sym eq) ⟩
+      ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ cong ∣_∣ (sym eq) ⟩
       ∣ n₁ ℤ.* + suc d₂ ∣  ≡⟨ ℤ.abs-*-commute n₁ (+ suc d₂) ⟩
       ∣ n₁ ∣ ℕ.* suc d₂    ∎)
 
-  fromWitness′ : ∀ {p} {P : Set p} {Q : Dec P} → .P → True Q
-  fromWitness′ {Q = Q} p = fromWitness (recompute Q p)
-
-  .c₁′ : True (C.coprime? ∣ n₁ ∣ (suc d₁))
-  c₁′ = fromWitness′ {P = Coprime ∣ n₁ ∣ (suc d₁)} c₁
-
-  .c₂′ : True (C.coprime? ∣ n₂ ∣ (suc d₂))
-  c₂′ = fromWitness′ {P = Coprime ∣ n₂ ∣ (suc d₂)} c₂
-
-  helper : (n₁ ÷ suc d₁) {c₁′} ≡ (n₂ ÷ suc d₂) {c₂′}
+  helper : mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂
   helper with ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁
   ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) (λ ()) eq
   ...   | refl = refl
@@ -86,9 +88,9 @@ drop-*≤* (*≤* pq≤qp) = pq≤qp
 ≤-refl = ≤-reflexive refl
 
 ≤-trans : Transitive _≤_
-≤-trans {i = mkℚ n₁ d₁ c₁} {j = mkℚ n₂ d₂ c₂} {k = mkℚ n₃ d₃ c₃} (*≤* eq₁) (*≤* eq₂)
+≤-trans {i = p@(mkℚ n₁ d₁ c₁)} {j = q@(mkℚ n₂ d₂ c₂)} {k = r@(mkℚ n₃ d₃ c₃)} (*≤* eq₁) (*≤* eq₂)
   = *≤* $ ℤ.*-cancelʳ-≤-pos (n₁ ℤ.* ℤ.+ suc d₃) (n₃ ℤ.* ℤ.+ suc d₁) d₂ $ begin
-  let sd₁ = ℤ.+ suc d₁; sd₂ = ℤ.+ suc d₂; sd₃ = ℤ.+ suc d₃ in
+  let sd₁ = ↧ p; sd₂ = ↧ q; sd₃ = ↧ r in
   (n₁  ℤ.* sd₃) ℤ.* sd₂  ≡⟨ ℤ.*-assoc n₁ sd₃ sd₂ ⟩
   n₁   ℤ.* (sd₃ ℤ.* sd₂) ≡⟨ cong (n₁ ℤ.*_) (ℤ.*-comm sd₃ sd₂) ⟩
   n₁   ℤ.* (sd₂ ℤ.* sd₃) ≡⟨ sym (ℤ.*-assoc n₁ sd₂ sd₃) ⟩
@@ -110,13 +112,11 @@ drop-*≤* (*≤* pq≤qp) = pq≤qp
   (↥ q ℤ.* ↧ p))
 
 _≤?_ : Decidable _≤_
-p ≤? q with (↥ p ℤ.* ↧ q) ℤ.≤? (↥ q ℤ.* ↧ p)
-... | yes pq≤qp = yes (*≤* pq≤qp)
-... | no ¬pq≤qp = no (λ { (*≤* pq≤qp) → ¬pq≤qp pq≤qp })
+p ≤? q = Dec′.map′ *≤* drop-*≤* ((↥ p ℤ.* ↧ q) ℤ.≤? (↥ q ℤ.* ↧ p))
 
 ≤-isPreorder : IsPreorder _≡_ _≤_
 ≤-isPreorder = record
-  { isEquivalence = P.isEquivalence
+  { isEquivalence = isEquivalence
   ; reflexive     = ≤-reflexive
   ; trans         = ≤-trans
   }