@@ -8,6 +8,11 @@ import org.scalacheck.{Arbitrary, Cogen, Prop}
8
8
import org .scalacheck .Prop ._
9
9
10
10
import cats .kernel .instances .all ._
11
+ import algebra .ring .Signed
12
+ import algebra .ring .CommutativeRing
13
+ import algebra .ring .TruncatedDivision
14
+ import algebra .ring .AdditiveCommutativeGroup
15
+ import algebra .ring .GCDRing
11
16
12
17
@ deprecated(" Provided by cats.kernel.laws" , since = " 2.7.0" )
13
18
object OrderLaws {
@@ -114,6 +119,105 @@ trait OrderLaws[A] extends Laws {
114
119
}
115
120
)
116
121
122
+ def signed (implicit A : Signed [A ]) = new OrderProperties (
123
+ name = " signed" ,
124
+ parent = Some (order(A .order)),
125
+ " abs non-negative" -> forAll((x : A ) => A .sign(A .abs(x)) != Signed .Negative ),
126
+ " signum returns -1/0/1" -> forAll((x : A ) => A .signum(A .abs(x)) <= 1 ),
127
+ " signum is sign.toInt" -> forAll((x : A ) => A .signum(x) == A .sign(x).toInt),
128
+ " ordered group" -> forAll { (x : A , y : A , z : A ) =>
129
+ A .order.lteqv(x, y) ==> A .order.lteqv(A .additiveCommutativeMonoid.plus(x, z),
130
+ A .additiveCommutativeMonoid.plus(y, z)
131
+ )
132
+ },
133
+ " triangle inequality" -> forAll { (x : A , y : A ) =>
134
+ A .order.lteqv(A .abs(A .additiveCommutativeMonoid.plus(x, y)), A .additiveCommutativeMonoid.plus(A .abs(x), A .abs(y)))
135
+ }
136
+ )
137
+
138
+ def signedAdditiveCommutativeGroup (implicit signedA : Signed [A ], A : AdditiveCommutativeGroup [A ]) = new DefaultRuleSet (
139
+ name = " signedAdditiveAbGroup" ,
140
+ parent = Some (signed),
141
+ " abs(x) equals abs(-x)" -> forAll { (x : A ) =>
142
+ signedA.abs(x) ?== signedA.abs(A .negate(x))
143
+ }
144
+ )
145
+
146
+ // more a convention: as GCD is defined up to a unit, so up to a sign,
147
+ // on an ordered GCD ring we require gcd(x, y) >= 0, which is the common
148
+ // behavior of computer algebra systems
149
+ def signedGCDRing (implicit signedA : Signed [A ], A : GCDRing [A ]) = new DefaultRuleSet (
150
+ name = " signedGCDRing" ,
151
+ parent = Some (signedAdditiveCommutativeGroup),
152
+ " gcd(x, y) >= 0" -> forAll { (x : A , y : A ) =>
153
+ signedA.isSignNonNegative(A .gcd(x, y))
154
+ },
155
+ " gcd(x, 0) === abs(x)" -> forAll { (x : A ) =>
156
+ A .gcd(x, A .zero) ?== signedA.abs(x)
157
+ }
158
+ )
159
+
160
+ def truncatedDivision (implicit ring : CommutativeRing [A ], A : TruncatedDivision [A ]) = new DefaultRuleSet (
161
+ name = " truncatedDivision" ,
162
+ parent = Some (signed),
163
+ " division rule (tquotmod)" -> forAll { (x : A , y : A ) =>
164
+ A .isSignNonZero(y) ==> {
165
+ val (q, r) = A .tquotmod(x, y)
166
+ x ?== ring.plus(ring.times(y, q), r)
167
+ }
168
+ },
169
+ " division rule (fquotmod)" -> forAll { (x : A , y : A ) =>
170
+ A .isSignNonZero(y) ==> {
171
+ val (q, r) = A .fquotmod(x, y)
172
+ x ?== ring.plus(ring.times(y, q), r)
173
+ }
174
+ },
175
+ " |r| < |y| (tmod)" -> forAll { (x : A , y : A ) =>
176
+ A .isSignNonZero(y) ==> {
177
+ val r = A .tmod(x, y)
178
+ A .order.lt(A .abs(r), A .abs(y))
179
+ }
180
+ },
181
+ " |r| < |y| (fmod)" -> forAll { (x : A , y : A ) =>
182
+ A .isSignNonZero(y) ==> {
183
+ val r = A .fmod(x, y)
184
+ A .order.lt(A .abs(r), A .abs(y))
185
+ }
186
+ },
187
+ " r = 0 or sign(r) = sign(x) (tmod)" -> forAll { (x : A , y : A ) =>
188
+ A .isSignNonZero(y) ==> {
189
+ val r = A .tmod(x, y)
190
+ A .isSignZero(r) || (A .sign(r) ?== A .sign(x))
191
+ }
192
+ },
193
+ " r = 0 or sign(r) = sign(y) (fmod)" -> forAll { (x : A , y : A ) =>
194
+ A .isSignNonZero(y) ==> {
195
+ val r = A .fmod(x, y)
196
+ A .isSignZero(r) || (A .sign(r) ?== A .sign(y))
197
+ }
198
+ },
199
+ " tquot" -> forAll { (x : A , y : A ) =>
200
+ A .isSignNonZero(y) ==> {
201
+ A .tquotmod(x, y)._1 ?== A .tquot(x, y)
202
+ }
203
+ },
204
+ " tmod" -> forAll { (x : A , y : A ) =>
205
+ A .isSignNonZero(y) ==> {
206
+ A .tquotmod(x, y)._2 ?== A .tmod(x, y)
207
+ }
208
+ },
209
+ " fquot" -> forAll { (x : A , y : A ) =>
210
+ A .isSignNonZero(y) ==> {
211
+ A .fquotmod(x, y)._1 ?== A .fquot(x, y)
212
+ }
213
+ },
214
+ " fmod" -> forAll { (x : A , y : A ) =>
215
+ A .isSignNonZero(y) ==> {
216
+ A .fquotmod(x, y)._2 ?== A .fmod(x, y)
217
+ }
218
+ }
219
+ )
220
+
117
221
class OrderProperties (
118
222
name : String ,
119
223
parent : Option [RuleSet ],
0 commit comments