0 | module Algebra.Semiring
  1 |
  2 | import Data.Nat
  3 | import Syntax.PreorderReasoning
  4 |
  5 | %default total
  6 |
  7 | ||| This interface is a witness that for a
  8 | ||| numeric type `a` the axioms of a commutative semiring hold:
  9 | |||
 10 | ||| 1. `a` is a commutative monoid under addition:
 11 | |||    1. `+` is associative: `k + (m + n) = (k + m) + n` for all `k,m,n : a`.
 12 | |||    2. `+` is commutative: `m + n = n + m` for all `m,n : a`.
 13 | |||    3. 0 is the additive identity: `n + 0 = n` for all `n : a`.
 14 | |||
 15 | ||| 2. `a` is a commutative monoid under multiplication:
 16 | |||    1. `*` is associative: `k * (m * n) = (k * m) * n` for all `k,m,n : a`.
 17 | |||    2. `*` is commutative: `m * n = n * m` for all `m,n : a`.
 18 | |||    3. 1 is the multiplicative identity: `n * 1 = n` for all `n : a`.
 19 | |||
 20 | ||| 3. Multiplication is distributive with respect to addition:
 21 | |||    `k * (m + n) = (k * m) + (k * n)` for all `k,m,n : a`.
 22 | |||
 23 | public export
 24 | interface Num a => Semiring a where
 25 |   ||| Addition is associative.
 26 |   0 plusAssociative : {k,m,n : a} -> k + (m + n) === (k + m) + n
 27 |
 28 |   ||| Addition is commutative.
 29 |   0 plusCommutative : {m,n : a} -> m + n === n + m
 30 |
 31 |   ||| 0 is the additive identity.
 32 |   0 plusZeroLeftNeutral : {n : a} -> 0 + n === n
 33 |
 34 |   ||| Multiplication is associative.
 35 |   0 multAssociative : {k,m,n : a} -> k * (m * n) === (k * m) * n
 36 |
 37 |   ||| Multiplication is commutative.
 38 |   0 multCommutative : {m,n : a} -> m * n === n * m
 39 |
 40 |   ||| 1 is the multiplicative identity.
 41 |   0 multOneLeftNeutral : {n : a} -> 1 * n === n
 42 |
 43 |   ||| Multiplication is distributive with respect to addition.
 44 |   0 leftDistributive : {k,m,n : a} -> k * (m + n) === (k * m) + (k * n)
 45 |
 46 |   ||| Zero is an absorbing element of multiplication.
 47 |   0 multZeroLeftAbsorbs : {n : a} -> 0 * n === 0
 48 |
 49 | --------------------------------------------------------------------------------
 50 | --          Proofs on Addition
 51 | --------------------------------------------------------------------------------
 52 |
 53 | ||| `n + 0 === n` for all `n : a`.
 54 | export
 55 | 0 plusZeroRightNeutral : Semiring a => {n : a} -> n + 0 === n
 56 | plusZeroRightNeutral =
 57 |   Calc $
 58 |     |~ n + 0
 59 |     ~~ 0 + n ... plusCommutative
 60 |     ~~ n     ... plusZeroLeftNeutral
 61 |
 62 | --------------------------------------------------------------------------------
 63 | --          Proofs on Multiplication
 64 | --------------------------------------------------------------------------------
 65 |
 66 | ||| `n * 1 === n` for all `n : a`.
 67 | export
 68 | 0 multOneRightNeutral : Semiring a => {n : a} -> n * 1 === n
 69 | multOneRightNeutral =
 70 |   Calc $
 71 |     |~ n * 1
 72 |     ~~ 1 * n ... multCommutative
 73 |     ~~ n     ... multOneLeftNeutral
 74 |
 75 | ||| Zero is an absorbing element of multiplication.
 76 | export
 77 | 0 multZeroRightAbsorbs : Semiring a => {n : a} -> n * 0 === 0
 78 | multZeroRightAbsorbs =
 79 |   Calc $
 80 |     |~ n * 0
 81 |     ~~ 0 * n ... multCommutative
 82 |     ~~ 0     ... multZeroLeftAbsorbs
 83 |
 84 | ||| Zero is an absorbing element of multiplication.
 85 | export
 86 | multZeroAbsorbs :
 87 |      {auto _ : Semiring a}
 88 |   -> (m,n : a)
 89 |   -> Either (m === 0) (n === 0)
 90 |   -> m * n === 0
 91 | multZeroAbsorbs m n (Left rfl) =
 92 |   Calc $
 93 |     |~ m * n
 94 |     ~~ 0 * n ... cong (*n) rfl
 95 |     ~~ 0     ... multZeroLeftAbsorbs
 96 |
 97 | multZeroAbsorbs m n (Right rfl) =
 98 |   Calc $
 99 |     |~ m * n
100 |     ~~ m * 0 ... cong (m*) rfl
101 |     ~~ 0     ... multZeroRightAbsorbs
102 |
103 | ||| Multiplication is distributive with respect to addition.
104 | export
105 | 0 rightDistributive :
106 |      {auto _ : Semiring a}
107 |   -> {k,m,n : a}
108 |   -> (m + n) * k === m * k + n * k
109 | rightDistributive =
110 |   Calc $
111 |     |~ (m + n) * k
112 |     ~~ k * (m + n)       ... multCommutative
113 |     ~~ (k * m) + (k * n) ... leftDistributive
114 |     ~~ m * k + k * n     ... cong (+ k * n) multCommutative
115 |     ~~ m * k + n * k     ... cong (m * k +) multCommutative
116 |
117 | --------------------------------------------------------------------------------
118 | --          Implementations
119 | --------------------------------------------------------------------------------
120 |
121 | export
122 | Semiring Nat where
123 |   plusAssociative = Nat.plusAssociative _ _ _
124 |   plusCommutative = Nat.plusCommutative _ _
125 |   plusZeroLeftNeutral = Nat.plusZeroLeftNeutral _
126 |   multAssociative = Nat.multAssociative _ _ _
127 |   multCommutative = Nat.multCommutative _ _
128 |   multOneLeftNeutral = Nat.multOneLeftNeutral _
129 |   leftDistributive = multDistributesOverPlusRight _ _ _
130 |   multZeroLeftAbsorbs = Refl
131 |