search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
585 stars 237 forks source link

Lemmas for Positive, Negative, etc. and _+_ and _*_ for rationals #2496

Closed Taneb closed 1 month ago

Taneb commented 1 month ago

This is pulled out from my branch for real numbers

A discovered annoyance (bug?) is that *-monoˡ-≤-nonNeg corresponds to *-monoʳ-<-pos, not *-monoˡ-<-pos as one may expect. But I don't want to fix that in this PR

jamesmckinna commented 1 month ago

This is pulled out from my branch for real numbers

Looks good!

A discovered annoyance (bug?) is that *-monoˡ-≤-nonNeg corresponds to *-monoʳ-<-pos, not *-monoˡ-<-pos as one may expect. But I don't want to fix that in this PR

Yes, I think this is an(other) example of left/right being mixed up in the library, and at some point, we should rationalise (and correctly implement) our conventions. Cf. https://github.com/agda/agda-stdlib/issues/1436#issuecomment-1243841859 and #1579 etc.

See also #2193 ...

Taneb commented 1 month ago

all the lemmas are in Data.Rational.Properties: is there any relationship with/need for, any (additional) ones in Data.Rational.Unnormalised.Properties? (I've never been quite clear about the division of labour between the two...)

I'll admit I didn't do that simply out of laziness. But looking at it now, I don't think in this case doing it that way would be helpful.