0 | module Algebra.Ring

  2 | import Algebra.Group

  3 | import Data.Nat

  4 | import Syntax.PreorderReasoning

  6 | %default total

  9 | public export

 10 | 0 LeftDistributive : (p,m : Op2 a) -> Type

 11 | LeftDistributive p m = {u,v,w : a} -> u `m` (v `p` w) === (u `m` v) `p` (u `m` w)

 14 | public export

 15 | 0 MultZeroLeftAbsorbs : (z : a) -> (m : Op2 a) -> Type

 16 | MultZeroLeftAbsorbs z m = {n : a} -> z `m` n === z

 19 | public export

 20 | 0 MinusAssociative : (p,sub : Op2 a) -> Type

 21 | MinusAssociative p sub = {u,v,w : a} -> u `p` (v `sub` w) === (u `p` v) `sub` w

 24 | public export

 25 | 0 ZeroMinus : (z : a) -> (p,sub : Op2 a) -> Type

 26 | ZeroMinus z p sub = {u : a} -> (z `sub` u) `p` u === z

 32 | public export

 33 | record Rig (a : Type) (z,o : a) (p,m : Op2 a) where

 34 |   constructor MkRig

 35 |   plus                : CommutativeMonoid a z p

 36 |   mult                : CommutativeMonoid a o m

 37 |   leftDistributive    : LeftDistributive p m

 38 |   multZeroLeftAbsorbs : MultZeroLeftAbsorbs z m

 40 | namespace Rig

 41 |   ||| Zero is an absorbing element of multiplication.

 42 |   export

 43 |   0 (.multZeroRightAbsorbs) : Rig a z o p m -> {x : a} -> x `m` z === z

 44 |   r.multZeroRightAbsorbs =

 45 |     Calc $

 46 |       |~ x `m` z

 47 |       ~~ z `m` x ... r.mult.commutative

 48 |       ~~ z       ... r.multZeroLeftAbsorbs

 50 |   ||| Multiplication is distributive with respect to addition.

 51 |   export

 52 |   0 (.rightDistributive) :

 53 |        Rig a z o p m

 54 |     -> {x,y,v : a}

 55 |     -> (y `p` v) `m` x === y `m` x `p` v `m` x

 56 |   r.rightDistributive =

 57 |     Calc $

 58 |       |~ (y `p` v) `m` x

 59 |       ~~ x `m` (y `p` v)         ... r.mult.commutative

 60 |       ~~ (x `m` y) `p` (x `m` v) ... r.leftDistributive

 61 |       ~~ y `m` x `p` x `m` v     ... cong (`p` x `m` v) r.mult.commutative

 62 |       ~~ y `m` x `p` v `m` x     ... cong (y `m` x `p`) r.mult.commutative

 66 | multZeroAbsorbs :

 67 |      Rig a z o p m

 68 |   -> {x,y : a}

 69 |   -> Either (x === z) (y === z)

 70 |   -> x `m` y === z

 71 | multZeroAbsorbs r (Left rfl) =

 72 |   Calc $

 73 |     |~ x `m` y

 74 |     ~~ z `m` y ... cong (`m` y) rfl

 75 |     ~~ z       ... r.multZeroLeftAbsorbs

 76 | multZeroAbsorbs r (Right rfl) =

 77 |   Calc $

 78 |     |~ x `m` y

 79 |     ~~ x `m` z ... cong (x `m`) rfl

 80 |     ~~ z       ... r.multZeroRightAbsorbs

 83 | 0 NatRig : Rig Nat 0 1 (+) (*)

 84 | NatRig =

 85 |   MkRig cmon_nat_plus cmon_nat_mult (multDistributesOverPlusRight  _ _ _) Refl

 91 | public export

 92 | record Ring (a : Type) (z,o : a) (p,m,sub : Op2 a) where

 93 |   constructor MkRing

 94 |   plusMon          : CommutativeMonoid a z p

 95 |   mult             : CommutativeMonoid a o m

 96 |   leftDistributive : LeftDistributive p m

 97 |   minusAssociative : MinusAssociative p sub

 98 |   zeroMinus        : ZeroMinus z p sub

101 | namespace Ring

102 |   export

103 |   0 (.plus) : Ring a z o p m sub -> AbelianGroup a z (z `sub`) p

104 |   (.plus) (MkRing (MkCommutativeMonoid a c l) _ _ _ zm) =

105 |     MkAbelianGroup a c l zm

107 |   export

108 |   0 (.multZeroRightAbsorbs) : Ring a z o p m sub -> {x : a} -> x `m` z === z

109 |   r.multZeroRightAbsorbs =

110 |     leftInjective r.plus.grp $ Calc $

111 |       |~ (x `m` z) `p` (x `m` z)

112 |       ~~ x `m` (z `p` z)         ..< r.leftDistributive {u = x, v = z, w = z}

113 |       ~~ x `m` z                 ... cong (x `m`) r.plus.leftNeutral

114 |       ~~ (x `m` z) `p` z         ..< r.plus.rightNeutral

116 |   export

117 |   0 (.multZeroLeftAbsorbs) : Ring a z o p m sub -> {x : a} -> z `m` x === z

118 |   r.multZeroLeftAbsorbs = Calc $

119 |     |~ z `m` x

120 |     ~~ x `m` z ... r.mult.commutative

121 |     ~~ z       ... r.multZeroRightAbsorbs

123 |   export

124 |   0 (.rig) : Ring a z o p m sub -> Rig a z o p m

125 |   (.rig) r@(MkRing pm mult ld _ _) = MkRig pm mult ld r.multZeroLeftAbsorbs

127 |   export

128 |   0 (.minusSelf) : Ring a z o p m sub -> {x : a} -> x `sub` x === z

129 |   r.minusSelf = Calc $

130 |     |~ x `sub`x

131 |     ~~ (x `p` z) `sub` x ..< cong (`sub` x) r.plus.rightNeutral

132 |     ~~ x `p` (z `sub` x) ..< r.minusAssociative

133 |     ~~ z                 ... r.plus.rightInverse

135 |   export

136 |   0 (.minusIsPlusRight) :

137 |         Ring a z o p m sub

138 |     -> {x,y : a}

139 |     -> x `sub` y === x `p` (z `sub` y)

140 |   r.minusIsPlusRight = Calc $

141 |     |~ x `sub` y

142 |     ~~ (x `p` z) `sub` y ..< cong (`sub` y) r.plus.rightNeutral

143 |     ~~ x `p` (z `sub` y) ..< r.minusAssociative

145 |   export

146 |   0 (.minusIsPlusLeft) :

147 |         Ring a z o p m sub

148 |     -> {x,y : a}

149 |     -> x `sub` y === (z `sub` y) `p` x

150 |   r.minusIsPlusLeft = Calc $

151 |     |~ x `sub` y

152 |     ~~ x `p` (z `sub` y) ... r.minusIsPlusRight

153 |     ~~ (z `sub` y) `p` x ... r.plus.commutative

155 |   export

156 |   0 (.multNegRight) :

157 |        Ring a z o p m sub

158 |     -> {x,y : a}

159 |     -> x `m` (z `sub` y) === z `sub` (x `m` y)

160 |   r.multNegRight =

161 |     solveInverseLeft r.plus.grp $ Calc $

162 |       |~ (x `m` y) `p` (x `m` (z `sub` y))

163 |       ~~ x `m` ( y `p` (z `sub` y)) ..< r.leftDistributive

164 |       ~~ x `m` z                    ... cong (x `m`) r.plus.rightInverse

165 |       ~~ z                          ... r.multZeroRightAbsorbs

167 |   export

168 |   0 (.negMultNegRight) :

169 |        Ring a z o p m sub

170 |     -> {x,y : a}

171 |     -> z `sub` (x `m` (z `sub` y)) === x `m` y

172 |   r.negMultNegRight = Calc $

173 |     |~ z `sub` (x `m` (z `sub` y))

174 |     ~~ z `sub` (z `sub` (x `m` y))  ... cong (z `sub`) r.multNegRight

175 |     ~~ x `m` y                      ... inverseInvolutory r.plus.grp

177 |   export

178 |   0 (.multNegLeft) :

179 |        Ring a z o p m sub

180 |     -> {x,y : a}

181 |     -> (z `sub` x) `m` y === z `sub` (x `m` y)

182 |   r.multNegLeft = Calc $

183 |     |~ (z `sub` x) `m` y

184 |     ~~ y `m` (z `sub` x) ... r.mult.commutative

185 |     ~~ z `sub` (y `m` x) ... r.multNegRight

186 |     ~~ z `sub` (x `m` y) ... cong (z `sub`) r.mult.commutative

188 |   export

189 |   0 (.negMultNegLeft) :

190 |        Ring a z o p m sub

191 |     -> {x,y : a}

192 |     -> z `sub` ((z `sub` x) `m` y) === x `m` y

193 |   r.negMultNegLeft = Calc $

194 |     |~ z `sub` ((z `sub` x) `m` y)

195 |     ~~ z `sub` (z `sub` (x `m` y))  ... cong (z `sub`) r.multNegLeft

196 |     ~~ x `m` y                      ... inverseInvolutory r.plus.grp

198 |   export

199 |   0 (.multMinusOneRight) :

200 |        Ring a z o p m sub

201 |     -> {x : a}

202 |     -> x `m` (z `sub` o) === z `sub` x

203 |   r.multMinusOneRight = Calc $

204 |     |~ x `m` (z `sub` o)

205 |     ~~ z `sub` x `m` o  ... r.multNegRight

206 |     ~~ z `sub` x        ... cong (z `sub`) r.mult.rightNeutral

208 |   export

209 |   0 (.multMinusOneLeft) :

210 |        Ring a z o p m sub

211 |     -> {x : a}

212 |     -> (z `sub` o) `m` x === z `sub` x

213 |   r.multMinusOneLeft = Calc $

214 |     |~ (z `sub` o) `m` x

215 |     ~~ x `m` (z `sub` o) ... r.mult.commutative

216 |     ~~ z `sub` x         ... r.multMinusOneRight

218 |   export

219 |   0 (.negMultNeg) :

220 |        Ring a z o p m sub

221 |     -> {x,y : a}

222 |     -> (z `sub` x) `m` (z `sub` y) === x `m` y

223 |   r.negMultNeg = Calc $

224 |     |~ (z `sub` x) `m` (z `sub` y)

225 |     ~~ z `sub` (x `m` (z `sub` y)) ... r.multNegLeft

226 |     ~~ z `sub` (z `sub` (x `m` y)) ... cong (z `sub`) r.multNegRight

227 |     ~~ x `m` y                     ... inverseInvolutory r.plus.grp

233 | unsafeRefl : a === b

234 | unsafeRefl = believe_me (Refl {x = a})

237 | 0 ring_bits8 : Ring Bits8 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

238 | ring_bits8 = MkRing plus_bits8.cmon mult_bits8 unsafeRefl unsafeRefl unsafeRefl

241 | 0 ring_bits16 : Ring Bits16 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

242 | ring_bits16 = MkRing plus_bits16.cmon mult_bits16 unsafeRefl unsafeRefl unsafeRefl

245 | 0 ring_bits32 : Ring Bits32 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

246 | ring_bits32 = MkRing plus_bits32.cmon mult_bits32 unsafeRefl unsafeRefl unsafeRefl

249 | 0 ring_bits64 : Ring Bits64 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

250 | ring_bits64 = MkRing plus_bits64.cmon mult_bits64 unsafeRefl unsafeRefl unsafeRefl

253 | 0 ring_int8 : Ring Int8 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

254 | ring_int8 = MkRing plus_int8.cmon mult_int8 unsafeRefl unsafeRefl unsafeRefl

257 | 0 ring_int16 : Ring Int16 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

258 | ring_int16 = MkRing plus_int16.cmon mult_int16 unsafeRefl unsafeRefl unsafeRefl

261 | 0 ring_int32 : Ring Int32 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

262 | ring_int32 = MkRing plus_int32.cmon mult_int32 unsafeRefl unsafeRefl unsafeRefl

265 | 0 ring_int64 : Ring Int64 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

266 | ring_int64 = MkRing plus_int64.cmon mult_int64 unsafeRefl unsafeRefl unsafeRefl

269 | 0 ring_integer : Ring Integer 0 1 Prelude.(+) Prelude.(*) Prelude.(-)

270 | ring_integer = MkRing plus_integer.cmon mult_integer unsafeRefl unsafeRefl unsafeRefl