1

How to add two rational.. I was trying this but this is not correct. As I am unable to prove that coprime part.

open import Data.Rational
open import Data.Integer
open import Data.Nat

_add_ : ℚ -> ℚ -> ℚ
x add y = (nx Data.Integer.* dy Data.Integer.+ dx Data.Integer.* ny) ÷
          (dx′ Data.Nat.* dy′)
  where
    nx = ℚ.numerator x
    dx = ℚ.denominator x
    dx′ = ℕ.suc (ℚ.denominator-1 x)

    ny = ℚ.numerator y
    dy = ℚ.denominator y
    dy′ = ℕ.suc (ℚ.denominator-1 y)
0

1 Answer 1

4

You need to simplify (nx * dy + dx * ny) / (dx * dy) to ensure its numerator and denominator are coprimes.

The following code shows you the core of the solution by simplifying a pair of natural numbers x and suc y-1 (i.e. a non-zero y). Extending it to handle the signs of the numerator should be an easy exercise. The heavy lifting is done by Data.Nat.Coprimality.Bézout-coprime.

open import Data.Nat
open import Data.Nat.GCD
open import Data.Nat.Coprimality hiding (sym)
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Nat.Divisibility
open import Data.Empty

record Simp (x : ℕ) (y : ℕ) : Set where
  constructor MkSimp
  field
    x′ y′ : ℕ
    eq-prf : x * y′ ≡ x′ * y
    coprime-prf : Coprime x′ y′

1+≢*0 : ∀ x y → suc x ≢ y * 0
1+≢*0 x zero ()
1+≢*0 x (suc y) = 1+≢*0 x y

simp : ∀ x y-1 → Simp x (suc y-1)
simp x y-1 with Bézout.lemma x (suc y-1)
simp x y-1 | Bézout.result 0 (GCD.is (_ , divides y′ y-eq) _) _ = ⊥-elim (1+≢*0 y-1 y′ y-eq)
simp x y-1 | Bézout.result (suc d-1) (GCD.is (divides x′ x-eq , divides y′ y-eq) _) bézout = MkSimp x′ y′ eq-prf (Bézout-coprime bézout′)
  where
    y = suc y-1
    d = suc d-1

    bézout′ : Bézout.Identity d (x′ * d) (y′ * d)
    bézout′ = subst₂ (Bézout.Identity d) x-eq y-eq bézout

    open Relation.Binary.PropositionalEquality.≡-Reasoning
    open import Data.Nat.Properties.Simple

    eq-prf : x * y′ ≡ x′ * y
    eq-prf = begin
      x * y′         ≡⟨ cong (λ z → z * y′) x-eq ⟩
      x′ * d * y′    ≡⟨ *-assoc x′ d y′ ⟩
      x′ * (d * y′)  ≡⟨ sym (cong (_*_ x′) (*-comm y′ d)) ⟩
      x′ * (y′ * d)  ≡⟨ sym (cong (_*_ x′) y-eq)  ⟩
      x′ * y         ∎
2
  • Thanks a lot :) but can you explain simp function little bit more please.
    – ajayv
    Jul 8, 2015 at 6:44
  • @ajayv: My recommendation is to leave the signature of simp, but delete the right-hand side, so you're just left with simp x y-1 | Bézout.result d (GCD.is (divides x′ x-eq , divides y′ y-eq) greatest) bézout = ?, then keep checking the goal-and-context (C-c C-, in Emacs) as you add more of my code -- that should show you what you need to prove at various points and which bit does what.
    – Cactus
    Jul 8, 2015 at 6:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.