[Agda] Data.Rational

[Andreas Abel]

Such a development would also be welcome for the standard library...

On 11.03.2014 11:43, Li Nuo wrote:
> Hi,
>
> I think you can use an alternative approach to make the definition
> simpler. You could define the setoid version (namely fractions which
> doesn't have to be reduced) and use what we call "definable quotient
> structure" to relate the setoid definition with the normal form
> definition (which you can find here
> http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf). Generally
> speaking, it contains a set of operations and properties like
> normalisation functions (in this case, the fraction-reducing functions)
> and representative selection functions.
>
> The advantage of it is to lift functions in a more systematic way,
> benefiting from "quotients" without "quotient types". Here in this case,
> it reduces the complexity of checking coprime property all through which
> is unnecessary when doing operations on fractions（It is only needed if
> we want to check whether they are normal form fractions i.e. reduced
> fractions).
>
> I hope it helps you.
>
> Cheers,
> Nuo
>
>
> 2014-03-11 4:38 GMT+00:00 Amr Sabry <sabry at soic.indiana.edu
> <mailto:sabry at soic.indiana.edu>>:
>
>     Hi,
>
>     I need some decent Rational library and since the current Data.Rational
>     looks like it needs quite a bit of extension, I started writing a few
>     small functions. I am getting stuck very quickly though. Here is a small
>     example that should work:
>
>     -- unary negation
>     ℚ- : ℚ → ℚ
>     ℚ- p with ℚ.numerator p | ℚ.denominator-1 p | toWitness (ℚ.isCoprime p)
>     ... | -[1+ n ] | d | c = (+ ℕ.suc n ÷ ℕ.suc d) {fromWitness {!!}}
>     ... | + 0 | d | _ = p
>     ... | + ℕ.suc n | d | c = (-[1+ n ] ÷ ℕ.suc d) {fromWitness {!!}}
>
>     In the first line, c has type:
>
>        c  : {i : ℕ} → Σ (i ∣ ℕ.suc n) (λ x → i ∣ ℕ.suc d) → i ≡ 1
>
>     The goal is:
>
>        ?0 : Coprime (ℕ.suc n) (ℕ.suc d)
>
>     where Coprime is defined in Data.Nat.Coprimality as:
>
>        Coprime m n = ∀ {i} → (i ∣ m) × (i ∣ n) → (i ≡ 1)
>
>     As far as I can see, the type of the goal expands directly to the type
>     of c and in fact, "giving" c to the hole works but then the file doesn't
>     reload after that?
>
>     Any suggestions? --Amr
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/