[Agda] Data.Rational

[Amr Sabry]

Oh I am developing and testing using 2.3.3. --Amr

Mateusz Kowalczyk <fuuzetsu at fuuzetsu.co.uk> wrote:

> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda