[Agda] Data.Rational

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Sun Mar 23 16:42:29 CET 2014


On 23/03/14 15:29, Amr Sabry wrote:
> Thank you all for your responses. My take is that there are probably
> many many ways of implementing rationals and some might be significantly
> better than others. There is however not even a baseline implementation
> in the current library for simple operations on the rationals. Using the
> always-normalized approach that was started in the library, I
> implemented the basic operations on rationals (unary negation,
> reciprocal, addition, multiplication, and hence trivially subtraction
> and division). It's not much but it's start. I am attaching the code in
> case someone spots obvious improvements and/or problems. If everything
> looks reasonable, I'd be happy to push to the library. Thanks. --Amr
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

Hi,

On Agda 2.3.2.1 I get the following type error

/tmp/Rat.agda:25,1-51,16
Left hand side gives too many arguments to a function of type
{m n g : ℕ} →
{False (n ℕ≟ 0)} →
{False (g ℕ≟ 0)} →
GCD m n g →
Σ-syntax ℕ (λ p → Σ-syntax ℕ (λ q → Coprime p q × False (q ℕ≟ 0)))
when checking that the clause
normalize {m} {n} {ℕ.suc g} {_} {_} G with Bézout.identity G
normalize {m} {.0} {ℕ.suc g} {()} {_}
  (GCD.is (divides p m≡pg' , divides 0 refl) _)
  | _
normalize {m} {n} {ℕ.suc g} {_} {_}
  (GCD.is (divides p m≡pg' , divides (ℕ.suc q) n≡qg') _)
  | Bézout.+- x y eq
  = p ,
    ℕ.suc q ,
    Bézout-coprime {p} {ℕ.suc q} {g}
    (Bézout.+- x y
     (begin
      ℕ.suc g ℕ+ y ℕ* (ℕ.suc q ℕ* ℕ.suc g) ≡⟨
      cong (λ h → ℕ.suc g ℕ+ y ℕ* h) (sym n≡qg') ⟩
      ℕ.suc g ℕ+ y ℕ* n ≡⟨ eq ⟩
      x ℕ* m ≡⟨ cong (λ h → x ℕ* h) m≡pg' ⟩ (x ℕ* (p ℕ* ℕ.suc g) ∎)))
    , tt
normalize {m} {n} {ℕ.suc g} {_} {_}
  (GCD.is (divides p m≡pg' , divides (ℕ.suc q) n≡qg') _)
  | Bézout.-+ x y eq
  = p ,
    ℕ.suc q ,
    Bézout-coprime {p} {ℕ.suc q} {g}
    (Bézout.-+ x y
     (begin
      ℕ.suc g ℕ+ x ℕ* (p ℕ* ℕ.suc g) ≡⟨
      cong (λ h → ℕ.suc g ℕ+ x ℕ* h) (sym m≡pg') ⟩
      ℕ.suc g ℕ+ x ℕ* m ≡⟨ eq ⟩
      y ℕ* n ≡⟨ cong (λ h → y ℕ* h) n≡qg' ⟩
      (y ℕ* (ℕ.suc q ℕ* ℕ.suc g) ∎)))
    , tt
has type
{m n g : ℕ} →
{False (n ℕ≟ 0)} →
{False (g ℕ≟ 0)} →
GCD m n g →
Σ-syntax ℕ (λ p → Σ-syntax ℕ (λ q → Coprime p q × False (q ℕ≟ 0)))


I also advise against leaving trailing whitespace in the file like you
seem to have done. Lastly, I think the function names don't really fit
in with the rest of the standard lib, maybe they should be though about
more?

Thanks

-- 
Mateusz K.


More information about the Agda mailing list