<div dir="ltr">Hi,<div><br></div><div>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 <a href="http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf">http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf</a>). Generally speaking, it contains a set of operations and properties like normalisation functions (in this case, the fraction-reducing functions) and representative selection functions.</div>
<div><br></div><div>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).</div>
<div><br></div><div>I hope it helps you.</div><div><br></div><div>Cheers,</div><div>Nuo</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">2014-03-11 4:38 GMT+00:00 Amr Sabry <span dir="ltr"><<a href="mailto:sabry@soic.indiana.edu" target="_blank">sabry@soic.indiana.edu</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I need some decent Rational library and since the current Data.Rational<br>
looks like it needs quite a bit of extension, I started writing a few<br>
small functions. I am getting stuck very quickly though. Here is a small<br>
example that should work:<br>
<br>
-- unary negation<br>
ℚ- : ℚ → ℚ<br>
ℚ- p with ℚ.numerator p | ℚ.denominator-1 p | toWitness (ℚ.isCoprime p)<br>
... | -[1+ n ] | d | c = (+ ℕ.suc n ÷ ℕ.suc d) {fromWitness {!!}}<br>
... | + 0 | d | _ = p<br>
... | + ℕ.suc n | d | c = (-[1+ n ] ÷ ℕ.suc d) {fromWitness {!!}}<br>
<br>
In the first line, c has type:<br>
<br>
c : {i : ℕ} → Σ (i ∣ ℕ.suc n) (λ x → i ∣ ℕ.suc d) → i ≡ 1<br>
<br>
The goal is:<br>
<br>
?0 : Coprime (ℕ.suc n) (ℕ.suc d)<br>
<br>
where Coprime is defined in Data.Nat.Coprimality as:<br>
<br>
Coprime m n = ∀ {i} → (i ∣ m) × (i ∣ n) → (i ≡ 1)<br>
<br>
As far as I can see, the type of the goal expands directly to the type<br>
of c and in fact, "giving" c to the hole works but then the file doesn't<br>
reload after that?<br>
<br>
Any suggestions? --Amr<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>