[Agda] Data.Rational

[Sergei Meshveliani]

On Tue, 2014-03-11 at 14:28 +0100, Andreas Abel wrote:
> 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).
> > [..]


>> Here in this case,
>> it reduces the complexity of checking coprime property all through 
>> which is unnecessary when doing operations on fractions


I do not precisely follow the subject. But I would note for any
occasion: 

if one needs to compute efficiently with fractions, then a good
tactic is to cancel each fraction to coprime as earlier as possible.
  
If one does not follow this rule, then computation will remain
theoretically correct, but for most practicable examples it will become
somewhat hundreds of times more expensive (the size of intermediate
denominators in a loop will explode).

This feature does not depend on the choice a programming language or
programming technique.

As to the below example of            ℚ- : ℚ → ℚ,
its main part is a matter of proving 

 -- (1)
 lemma :  {m d : ℕ}  →  Coprime ∣ - (+ m) ∣ d  →  Coprime ∣ (+ m) ∣ d

And I think, it is by applying  PropositionalEquality.subst  for  
(\x -> Coprime x d)
 
with using the identity   ∣ - x ∣ ≡ ∣ x ∣   for  x : ℤ

(for absolute value). This latter identity can be taken from
Data.Integer.

Probably, the lemmata like (1) need to be in Standard library.

Regards,

------
Sergei


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