0 | module Algebra.Ring
  1 |
  2 | import Syntax.PreorderReasoning
  3 |
  4 | %default total
  5 |
  6 | public export %inline %tcinline
  7 | neg : Neg a => a -> a
  8 | neg = negate
  9 |
 10 | ||| This interface is a witness that for a (primitive)
 11 | ||| integral type `a` the axioms of a commutative ring hold:
 12 | |||
 13 | ||| 1. `a` is an abelian group under addition:
 14 | |||    1. `+` is associative: `k + (m + n) = (k + m) + n` for all `k,m,n : a`.
 15 | |||    2. `+` is commutative: `m + n = n + m` for all `m,n : a`.
 16 | |||    3. 0 is the additive identity: `n + 0 = n` for all `n : a`.
 17 | |||    4. `neg n` is the additive inverse of `n`:
 18 | |||       `n + neg n = 0` for all `n : a`.
 19 | |||
 20 | ||| 2. `a` is a commutative monoid under multiplication:
 21 | |||    1. `*` is associative: `k * (m * n) = (k * m) * n` for all `k,m,n : a`.
 22 | |||    2. `*` is commutative: `m * n = n * m` for all `m,n : a`.
 23 | |||    3. 1 is the multiplicative identity: `n * 1 = n` for all `n : a`.
 24 | |||
 25 | ||| 3. Multiplication is distributive with respect to addition:
 26 | |||    `k * (m + n) = (k * m) + (k * n)` for all `k,m,n : a`.
 27 | |||
 28 | ||| 4. Subtraction syntax: `m - n = m + neg n` for all `m,n : a`.
 29 | public export
 30 | interface Neg a => Ring a where
 31 |   ||| Addition is associative.
 32 |   0 plusAssociative : {k,m,n : a} -> k + (m + n) === (k + m) + n
 33 |
 34 |   ||| Addition is commutative.
 35 |   0 plusCommutative : {m,n : a} -> m + n === n + m
 36 |
 37 |   ||| 0 is the additive identity.
 38 |   0 plusZeroLeftNeutral : {n : a} -> 0 + n === n
 39 |
 40 |   ||| `neg n` is the additive inverse of `n`.
 41 |   0 plusNegLeftZero : {n : a} -> neg n + n === 0
 42 |
 43 |   ||| Multiplication is associative.
 44 |   0 multAssociative : {k,m,n : a} -> k * (m * n) === (k * m) * n
 45 |
 46 |   ||| Multiplication is commutative.
 47 |   0 multCommutative : {m,n : a} -> m * n === n * m
 48 |
 49 |   ||| 1 is the multiplicative identity.
 50 |   0 multOneLeftNeutral : {n : a} -> 1 * n === n
 51 |
 52 |   ||| Multiplication is distributive with respect to addition.
 53 |   0 leftDistributive : {k,m,n : a} -> k * (m + n) === (k * m) + (k * n)
 54 |
 55 |   ||| `m - n` is just "syntactic sugar" for `m + neg n`.
 56 |   0 minusIsPlusNeg : {m,n : a} -> m - n === m + neg n
 57 |
 58 | --------------------------------------------------------------------------------
 59 | --          Proofs on Addition
 60 | --------------------------------------------------------------------------------
 61 |
 62 | ||| `n + 0 === n` for all `n : a`.
 63 | export
 64 | 0 plusZeroRightNeutral : Ring a => {n : a} -> n + 0 === n
 65 | plusZeroRightNeutral =
 66 |   Calc $
 67 |     |~ n + 0
 68 |     ~~ 0 + n ... plusCommutative
 69 |     ~~ n     ... plusZeroLeftNeutral
 70 |
 71 | ||| `n + neg n === 0` for all `n : a`.
 72 | export
 73 | 0 plusNegRightZero : Ring a => {n : a} -> n + neg n === 0
 74 | plusNegRightZero =
 75 |   Calc $
 76 |     |~ n + neg n
 77 |     ~~ neg n + n ... plusCommutative
 78 |     ~~ 0         ... plusNegLeftZero
 79 |
 80 | ||| `n - n === 0` for all `n : a`.
 81 | export
 82 | 0 minusSelfZero : Ring a => {n : a} -> n - n === 0
 83 | minusSelfZero =
 84 |   Calc $
 85 |     |~ n - n
 86 |     ~~ n + neg n ... minusIsPlusNeg
 87 |     ~~ 0         ... plusNegRightZero
 88 |
 89 | ||| Law of associativity for subtraction.
 90 | export
 91 | 0 plusMinusAssociative :
 92 |      {auto _ : Ring a}
 93 |   -> {k,m,n : a}
 94 |   -> k + (m - n) === (k + m) - n
 95 | plusMinusAssociative =
 96 |   Calc $
 97 |     |~ k + (m - n)
 98 |     ~~ k + (m + neg n) ..> cong (k+) minusIsPlusNeg
 99 |     ~~ (k + m) + neg n ..> plusAssociative
100 |     ~~ (k + m) - n     ..< minusIsPlusNeg
101 |
102 | ||| We can solve equations involving addition.
103 | export
104 | 0 solvePlusRight :
105 |      {auto _ : Ring a}
106 |   -> {k,m,n : a}
107 |   -> k + m === n
108 |   -> k === n - m
109 | solvePlusRight prf =
110 |   Calc $
111 |     |~ k
112 |     ~~ k + 0        ..< plusZeroRightNeutral
113 |     ~~ k + (m - m)  ..< cong (k +) minusSelfZero
114 |     ~~ (k + m) - m  ..> plusMinusAssociative
115 |     ~~ n - m        ..> cong (\x => x - m) prf
116 |
117 | ||| We can solve equations involving addition.
118 | export
119 | 0 solvePlusLeft :
120 |      {auto _ : Ring a}
121 |   -> {k,m,n : a}
122 |   -> k + m === n
123 |   -> m === n - k
124 | solvePlusLeft prf =
125 |   solvePlusRight $ Calc $
126 |     |~ m + k
127 |     ~~ k + m ... plusCommutative
128 |     ~~ n     ... prf
129 |
130 | ||| Addition from the left is injective.
131 | export
132 | 0 plusLeftInjective : Ring a => {k,m,n : a} -> k + n === m + n -> k === m
133 | plusLeftInjective prf =
134 |   Calc $
135 |     |~ k
136 |     ~~ (m + n) - n ..> solvePlusRight prf
137 |     ~~ m + (n - n) ..< plusMinusAssociative
138 |     ~~ m + 0       ..> cong (m +) minusSelfZero
139 |     ~~ m           ..> plusZeroRightNeutral
140 |
141 | ||| Addition from the right is injective.
142 | export
143 | 0 plusRightInjective : Ring a => {k,m,n : a} -> n + k === n + m -> k === m
144 | plusRightInjective prf =
145 |   plusLeftInjective $
146 |     Calc $
147 |       |~ k + n
148 |       ~~ n + k  ... plusCommutative
149 |       ~~ n + m  ... prf
150 |       ~~ m + n  ... plusCommutative
151 |
152 | ||| From `m + n === 0` follows that `n` is the
153 | ||| additive inverse of `m`.
154 | export
155 | 0 solvePlusNegRight :
156 |      {auto _ : Ring a}
157 |   -> {m,n : a}
158 |   -> m + n === 0
159 |   -> n === neg m
160 | solvePlusNegRight prf =
161 |   plusRightInjective (trans prf (sym plusNegRightZero))
162 |
163 | ||| From `m + n === 0` follows that `m` is the
164 | ||| additive inverse of `n`.
165 | export
166 | 0 solvePlusNegLeft :
167 |      {auto _ : Ring a}
168 |   -> {m,n : a}
169 |   -> m + n === 0
170 |   -> m === neg n
171 | solvePlusNegLeft prf =
172 |   solvePlusNegRight $ Calc $
173 |     |~ n + m
174 |     ~~ m + n ... plusCommutative
175 |     ~~ 0     ... prf
176 |
177 | ||| From `m + n === m` follows `n === 0`.
178 | export
179 | 0 solvePlusZeroRight :  Ring a => {m,n : a} -> m + n === m -> n === 0
180 | solvePlusZeroRight prf =
181 |     Calc $
182 |       |~ n
183 |       ~~ m - m ... solvePlusLeft prf
184 |       ~~ 0     ... minusSelfZero
185 |
186 | ||| From `n + m === m` follows `n === 0`.
187 | export
188 | 0 solvePlusZeroLeft :  Ring a => {m,n : a} -> n + m === m -> n === 0
189 | solvePlusZeroLeft prf =
190 |     solvePlusZeroRight $ Calc $
191 |       |~ m + n
192 |       ~~ n + m ... plusCommutative
193 |       ~~ m     ... prf
194 |
195 | ||| Negation is involutory.
196 | export
197 | 0 negInvolutory : Ring a => {n : a} -> neg (neg n) === n
198 | negInvolutory = sym $ solvePlusNegLeft plusNegRightZero
199 |
200 | ||| From `neg n === 0` follows `n === 0`.
201 | export
202 | 0 solveNegZero : Ring a => {n : a} -> neg n === 0 -> n === 0
203 | solveNegZero prf =
204 |   Calc $
205 |     |~ n
206 |     ~~ n + 0     ..< plusZeroRightNeutral
207 |     ~~ n + neg n ..< cong (n +) prf
208 |     ~~ 0         ..> plusNegRightZero
209 |
210 | ||| `neg 0 === 0`
211 | export
212 | 0 negZero : Ring a => neg {a} 0 === 0
213 | negZero = solveNegZero negInvolutory
214 |
215 | export
216 | 0 negDistributes : Ring a => {m,n : a} -> neg (m + n) === neg m + neg n
217 | negDistributes =
218 |   sym $ solvePlusNegLeft $ Calc $
219 |   |~ (neg m + neg n) + (m + n)
220 |   ~~ (neg m + neg n) + (n + m) ... cong ((neg m + neg n) +) plusCommutative
221 |   ~~ ((neg m + neg n) + n) + m ... plusAssociative
222 |   ~~ (neg m + (neg n + n)) + m ..< cong (+m) plusAssociative
223 |   ~~ (neg m + 0) + m           ... cong (\x => neg m + x + m) plusNegLeftZero
224 |   ~~ neg m + m                 ... cong (+m) plusZeroRightNeutral
225 |   ~~ 0                         ... plusNegLeftZero
226 |
227 | --------------------------------------------------------------------------------
228 | --          Proofs on Multiplication
229 | --------------------------------------------------------------------------------
230 |
231 | ||| `n * 1 === n` for all `n : a`.
232 | export
233 | 0 multOneRightNeutral : Ring a => {n : a} -> n * 1 === n
234 | multOneRightNeutral =
235 |   Calc $
236 |     |~ n * 1
237 |     ~~ 1 * n ... multCommutative
238 |     ~~ n     ... multOneLeftNeutral
239 |
240 | ||| Zero is an absorbing element of multiplication.
241 | export
242 | 0 multZeroRightAbsorbs : Ring a => {n : a} -> n * 0 === 0
243 | multZeroRightAbsorbs =
244 |   solvePlusZeroRight $ Calc $
245 |     |~ (n * 0) + (n * 0)
246 |     ~~ n * (0 + 0)       ..< leftDistributive
247 |     ~~ n * 0             ..> cong (n *) plusZeroLeftNeutral
248 |
249 |
250 | ||| Zero is an absorbing element of multiplication.
251 | export
252 | 0 multZeroLeftAbsorbs : Ring a => {n : a} -> 0 * n === 0
253 | multZeroLeftAbsorbs =
254 |   Calc $
255 |     |~ 0 * n
256 |     ~~ n * 0 ... multCommutative
257 |     ~~ 0     ... multZeroRightAbsorbs
258 |
259 | ||| Zero is an absorbing element of multiplication.
260 | export
261 | 0 multZeroAbsorbs :
262 |      {auto _ : Ring a}
263 |   -> {m,n : a}
264 |   -> Either (m === 0) (n === 0)
265 |   -> m * n === 0
266 | multZeroAbsorbs (Left rfl) =
267 |   Calc $
268 |     |~ m * n
269 |     ~~ 0 * n ... cong (*n) rfl
270 |     ~~ 0     ... multZeroLeftAbsorbs
271 |
272 | multZeroAbsorbs (Right rfl) =
273 |   Calc $
274 |     |~ m * n
275 |     ~~ m * 0 ... cong (m*) rfl
276 |     ~~ 0     ... multZeroRightAbsorbs
277 |
278 | ||| `m * (-n) = - (m * n)`.
279 | export
280 | 0 multNegRight : Ring a => {m,n : a} -> m * neg n === neg (m * n)
281 | multNegRight =
282 |   solvePlusNegRight $ Calc $
283 |      |~ m * n + m * neg n
284 |      ~~ m * (n + neg n)   ..< leftDistributive
285 |      ~~ m * 0             ..> cong (m *) plusNegRightZero
286 |      ~~ 0                 ..> multZeroRightAbsorbs
287 |
288 | ||| `- (m * (-n)) = m * n`.
289 | export
290 | 0 negMultNegRight : Ring a => {m,n : a} -> neg (m * neg n) === m * n
291 | negMultNegRight =
292 |   Calc $
293 |     |~ neg (m * neg n)
294 |     ~~ neg (neg (m * n)) ... cong neg multNegRight
295 |     ~~ m * n             ... negInvolutory
296 |
297 | ||| `(- m) * n = - (m * n)`.
298 | export
299 | 0 multNegLeft : Ring a => {m,n : a} -> neg m * n === neg (m * n)
300 | multNegLeft =
301 |   Calc $
302 |     |~ neg m * n
303 |     ~~ n * neg m   ... multCommutative
304 |     ~~ neg (n * m) ... multNegRight
305 |     ~~ neg (m * n) ... cong neg multCommutative
306 |
307 | ||| `- ((-m) * n) = m * n`.
308 | export
309 | 0 negMultNegLeft : Ring a => {m,n : a} -> neg (neg m * n) === m * n
310 | negMultNegLeft =
311 |   Calc $
312 |     |~ neg (neg m * n)
313 |     ~~ neg (neg (m * n)) ... cong neg multNegLeft
314 |     ~~ m * n             ... negInvolutory
315 |
316 | ||| Multiplication with `(-1)` is negation.
317 | export
318 | 0 multMinusOneRight : Ring a => {n : a} -> n * neg 1 === neg n
319 | multMinusOneRight =
320 |   Calc $
321 |     |~ n * neg 1
322 |     ~~ neg (n * 1) ... multNegRight
323 |     ~~ neg n       ... cong neg multOneRightNeutral
324 |
325 | ||| Multiplication with `(-1)` is negation.
326 | export
327 | 0 multMinusOneLeft : Ring a => {n : a} -> neg 1 * n === neg n
328 | multMinusOneLeft =
329 |   Calc $
330 |     |~ neg 1 * n
331 |     ~~ neg (1 * n) ... multNegLeft
332 |     ~~ neg n       ... cong neg multOneLeftNeutral
333 |
334 | ||| Multiplication of two negations removes negations.
335 | export
336 | 0 negMultNeg : Ring a => {m,n : a} -> neg m * neg n === m * n
337 | negMultNeg =
338 |   Calc $
339 |     |~ neg m * neg n
340 |     ~~ neg (m * neg n)   ... multNegLeft
341 |     ~~ neg (neg (m * n)) ... cong neg multNegRight
342 |     ~~ m * n             ... negInvolutory
343 |
344 | ||| Multiplication is distributive with respect to addition.
345 | export
346 | 0 rightDistributive :
347 |      {auto _ : Ring a}
348 |   -> {k,m,n : a}
349 |   -> (m + n) * k === m * k + n * k
350 | rightDistributive =
351 |   Calc $
352 |     |~ (m + n) * k
353 |     ~~ k * (m + n)       ... multCommutative
354 |     ~~ (k * m) + (k * n) ... leftDistributive
355 |     ~~ m * k + k * n     ... cong (+ k * n) multCommutative
356 |     ~~ m * k + n * k     ... cong (m * k +) multCommutative
357 |
358 | export
359 | 0 multPlusSelf : Ring a => {m,n : a} -> m * n + m === m * (n + 1)
360 | multPlusSelf =
361 |   Calc $
362 |     |~ m * n + m
363 |     ~~ m * n + m * 1 ..< cong (m*n +) multOneRightNeutral
364 |     ~~ m * (n + 1)   ..< leftDistributive
365 |
366 | --------------------------------------------------------------------------------
367 | --          Implementations
368 | --------------------------------------------------------------------------------
369 |
370 | unsafeRefl : a === b
371 | unsafeRefl = believe_me (Refl {x = a})
372 |
373 | export
374 | Ring Bits8 where
375 |   plusAssociative     = unsafeRefl
376 |   plusCommutative     = unsafeRefl
377 |   plusZeroLeftNeutral = unsafeRefl
378 |   plusNegLeftZero     = unsafeRefl
379 |   multAssociative     = unsafeRefl
380 |   multCommutative     = unsafeRefl
381 |   multOneLeftNeutral  = unsafeRefl
382 |   leftDistributive    = unsafeRefl
383 |   minusIsPlusNeg      = unsafeRefl
384 |
385 | export
386 | Ring Bits16 where
387 |   plusAssociative     = unsafeRefl
388 |   plusCommutative     = unsafeRefl
389 |   plusZeroLeftNeutral = unsafeRefl
390 |   plusNegLeftZero     = unsafeRefl
391 |   multAssociative     = unsafeRefl
392 |   multCommutative     = unsafeRefl
393 |   multOneLeftNeutral  = unsafeRefl
394 |   leftDistributive    = unsafeRefl
395 |   minusIsPlusNeg      = unsafeRefl
396 |
397 | export
398 | Ring Bits32 where
399 |   plusAssociative     = unsafeRefl
400 |   plusCommutative     = unsafeRefl
401 |   plusZeroLeftNeutral = unsafeRefl
402 |   plusNegLeftZero     = unsafeRefl
403 |   multAssociative     = unsafeRefl
404 |   multCommutative     = unsafeRefl
405 |   multOneLeftNeutral  = unsafeRefl
406 |   leftDistributive    = unsafeRefl
407 |   minusIsPlusNeg      = unsafeRefl
408 |
409 | export
410 | Ring Bits64 where
411 |   plusAssociative     = unsafeRefl
412 |   plusCommutative     = unsafeRefl
413 |   plusZeroLeftNeutral = unsafeRefl
414 |   plusNegLeftZero     = unsafeRefl
415 |   multAssociative     = unsafeRefl
416 |   multCommutative     = unsafeRefl
417 |   multOneLeftNeutral  = unsafeRefl
418 |   leftDistributive    = unsafeRefl
419 |   minusIsPlusNeg      = unsafeRefl
420 |
421 | export
422 | Ring Int8 where
423 |   plusAssociative     = unsafeRefl
424 |   plusCommutative     = unsafeRefl
425 |   plusZeroLeftNeutral = unsafeRefl
426 |   plusNegLeftZero     = unsafeRefl
427 |   multAssociative     = unsafeRefl
428 |   multCommutative     = unsafeRefl
429 |   multOneLeftNeutral  = unsafeRefl
430 |   leftDistributive    = unsafeRefl
431 |   minusIsPlusNeg      = unsafeRefl
432 |
433 | export
434 | Ring Int16 where
435 |   plusAssociative     = unsafeRefl
436 |   plusCommutative     = unsafeRefl
437 |   plusZeroLeftNeutral = unsafeRefl
438 |   plusNegLeftZero     = unsafeRefl
439 |   multAssociative     = unsafeRefl
440 |   multCommutative     = unsafeRefl
441 |   multOneLeftNeutral  = unsafeRefl
442 |   leftDistributive    = unsafeRefl
443 |   minusIsPlusNeg      = unsafeRefl
444 |
445 | export
446 | Ring Int32 where
447 |   plusAssociative     = unsafeRefl
448 |   plusCommutative     = unsafeRefl
449 |   plusZeroLeftNeutral = unsafeRefl
450 |   plusNegLeftZero     = unsafeRefl
451 |   multAssociative     = unsafeRefl
452 |   multCommutative     = unsafeRefl
453 |   multOneLeftNeutral  = unsafeRefl
454 |   leftDistributive    = unsafeRefl
455 |   minusIsPlusNeg      = unsafeRefl
456 |
457 | export
458 | Ring Int64 where
459 |   plusAssociative     = unsafeRefl
460 |   plusCommutative     = unsafeRefl
461 |   plusZeroLeftNeutral = unsafeRefl
462 |   plusNegLeftZero     = unsafeRefl
463 |   multAssociative     = unsafeRefl
464 |   multCommutative     = unsafeRefl
465 |   multOneLeftNeutral  = unsafeRefl
466 |   leftDistributive    = unsafeRefl
467 |   minusIsPlusNeg      = unsafeRefl
468 |
469 | export
470 | Ring Int where
471 |   plusAssociative     = unsafeRefl
472 |   plusCommutative     = unsafeRefl
473 |   plusZeroLeftNeutral = unsafeRefl
474 |   plusNegLeftZero     = unsafeRefl
475 |   multAssociative     = unsafeRefl
476 |   multCommutative     = unsafeRefl
477 |   multOneLeftNeutral  = unsafeRefl
478 |   leftDistributive    = unsafeRefl
479 |   minusIsPlusNeg      = unsafeRefl
480 |
481 | export
482 | Ring Integer where
483 |   plusAssociative     = unsafeRefl
484 |   plusCommutative     = unsafeRefl
485 |   plusZeroLeftNeutral = unsafeRefl
486 |   plusNegLeftZero     = unsafeRefl
487 |   multAssociative     = unsafeRefl
488 |   multCommutative     = unsafeRefl
489 |   multOneLeftNeutral  = unsafeRefl
490 |   leftDistributive    = unsafeRefl
491 |   minusIsPlusNeg      = unsafeRefl
492 |