[Agda] Data.Rational

[Li Nuo]

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>:

> 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
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140311/f97347d8/attachment.html