|
1 | 1 | package cats.algebra.laws
|
2 | 2 |
|
3 |
| -import cats.algebra.ring.{CommutativeRing, Signed, TruncatedDivision} |
| 3 | +import cats.algebra.ring.{ |
| 4 | + AdditiveCommutativeGroup, |
| 5 | + CommutativeRing, |
| 6 | + GCDRing, |
| 7 | + Signed, |
| 8 | + TruncatedDivision |
| 9 | +} |
4 | 10 | import cats.kernel._
|
5 | 11 | import org.scalacheck.{Arbitrary, Cogen, Prop}
|
6 | 12 | import org.scalacheck.Prop._
|
@@ -30,7 +36,37 @@ trait SignedTests[A] extends OrderTests[A] {
|
30 | 36 | "abs non-negative" -> forAll((x: A) => A.sign(A.abs(x)) != Signed.Negative),
|
31 | 37 | "abs never less than" -> forAll((x: A) => A.order.gteqv(A.abs(x), x)),
|
32 | 38 | "signum returns -1/0/1" -> forAll((x: A) => A.signum(A.abs(x)) <= 1),
|
33 |
| - "signum is sign.toInt" -> forAll((x: A) => A.signum(x) == A.sign(x).toInt) |
| 39 | + "signum is sign.toInt" -> forAll((x: A) => A.signum(x) == A.sign(x).toInt), |
| 40 | + "linear order" -> forAll { (x: A, y: A, z: A) => |
| 41 | + A.order.lteqv(x, y) ==> A.order.lteqv(A.additiveCommutativeMonoid.plus(x, z), |
| 42 | + A.additiveCommutativeMonoid.plus(y, z) |
| 43 | + ) |
| 44 | + }, |
| 45 | + "triangle inequality" -> forAll { (x: A, y: A) => |
| 46 | + A.order.lteqv(A.abs(A.additiveCommutativeMonoid.plus(x, y)), A.additiveCommutativeMonoid.plus(A.abs(x), A.abs(y))) |
| 47 | + } |
| 48 | + ) |
| 49 | + |
| 50 | + def signedAdditiveCommutativeGroup(implicit signedA: Signed[A], A: AdditiveCommutativeGroup[A]) = new DefaultRuleSet( |
| 51 | + name = "signedAdditiveAbGroup", |
| 52 | + parent = Some(signed), |
| 53 | + "abs(x) equals abs(-x)" -> forAll { (x: A) => |
| 54 | + signedA.abs(x) ?== signedA.abs(A.negate(x)) |
| 55 | + } |
| 56 | + ) |
| 57 | + |
| 58 | + // more a convention: as GCD is defined up to a unit, so up to a sign, |
| 59 | + // on an ordered GCD ring we require gcd(x, y) >= 0, which is the common |
| 60 | + // behavior of computer algebra systems |
| 61 | + def signedGCDRing(implicit signedA: Signed[A], A: GCDRing[A]) = new DefaultRuleSet( |
| 62 | + name = "signedGCDRing", |
| 63 | + parent = Some(signedAdditiveCommutativeGroup), |
| 64 | + "gcd(x, y) >= 0" -> forAll { (x: A, y: A) => |
| 65 | + signedA.isSignNonNegative(A.gcd(x, y)) |
| 66 | + }, |
| 67 | + "gcd(x, 0) === abs(x)" -> forAll { (x: A) => |
| 68 | + A.gcd(x, A.zero) ?== signedA.abs(x) |
| 69 | + } |
34 | 70 | )
|
35 | 71 |
|
36 | 72 | def truncatedDivision(implicit ring: CommutativeRing[A], A: TruncatedDivision[A]) = new DefaultRuleSet(
|
|
0 commit comments