0 | module Algebra.Solver.Ring
  1 |
  2 | import public Data.List.Elem
  3 | import public Algebra.Group
  4 | import public Algebra.Ring
  5 | import public Algebra.Solver.Ops
  6 | import public Algebra.Solver.Product
  7 | import public Algebra.Solver.Sum
  8 | import Algebra.Solver.Semiring as SR
  9 | import Syntax.PreorderReasoning
 10 |
 11 | %hide SR.Expr
 12 |
 13 | %default total
 14 |
 15 | public export
 16 | data Expr : (a : Type) -> (as : List a) -> Type where
 17 |   ||| A literal. This should be a value known at compile time
 18 |   ||| so that it reduces during normalization.
 19 |   Lit  : (v : a) -> Expr a as
 20 |
 21 |   ||| A variabl. This is is for values not known at compile
 22 |   ||| time. In order to compare and merge variables, we need an
 23 |   ||| `Elem x as` proof.
 24 |   Var  : (x : a) -> Elem x as -> Expr a as
 25 |
 26 |   ||| Addition of two expressions.
 27 |   (+)  : (x,y : Expr a as) -> Expr a as
 28 |
 29 |   ||| Multiplication of two expressions.
 30 |   (*)  : (x,y : Expr a as) -> Expr a as
 31 |
 32 |   (-)  : Expr a as -> Expr a as -> Expr a as
 33 |
 34 | --------------------------------------------------------------------------------
 35 | --          Syntax
 36 | --------------------------------------------------------------------------------
 37 |
 38 | public export
 39 | fromInteger : Num a => Integer -> Expr a as
 40 | fromInteger = Lit . fromInteger
 41 |
 42 | ||| Like `Var` but takes the `Elem x as` as an auto implicit
 43 | ||| argument.
 44 | public export
 45 | var : {0 as : List a} -> (x : a) -> Elem x as => Expr a as
 46 | var x = Var x %search
 47 |
 48 | ||| Addition of variables. This is an alias for
 49 | ||| `var x + var y`.
 50 | public export
 51 | (.+.) :
 52 |      {0 as : List a}
 53 |   -> (x,y : a)
 54 |   -> {auto _ : Elem x as}
 55 |   -> {auto _ : Elem y as}
 56 |   -> Expr a as
 57 | (.+.) x y =var x + var y
 58 |
 59 | ||| Addition of variables. This is an alias for
 60 | ||| `x + var y`.
 61 | public export
 62 | (+.) :
 63 |      {0 as : List a}
 64 |   -> (x : Expr a as)
 65 |   -> (y : a)
 66 |   -> {auto _ : Elem y as}
 67 |   -> Expr a as
 68 | (+.) x y = x + var y
 69 |
 70 | ||| Addition of variables. This is an alias for
 71 | ||| `var x + y`.
 72 | public export
 73 | (.+) :
 74 |      {0 as : List a}
 75 |   -> (x : a)
 76 |   -> (y : Expr a as)
 77 |   -> {auto _ : Elem x as}
 78 |   -> Expr a as
 79 | (.+) x y = var x + y
 80 |
 81 | ||| Addition of variables. This is an alias for
 82 | ||| `var x + var y`.
 83 | public export
 84 | (.-.) :
 85 |      {0 as : List a}
 86 |   -> (x,y : a)
 87 |   -> {auto _ : Elem x as}
 88 |   -> {auto _ : Elem y as}
 89 |   -> Expr a as
 90 | (.-.) x y =var x - var y
 91 |
 92 | ||| Addition of variables. This is an alias for
 93 | ||| `x + var y`.
 94 | public export
 95 | (-.) :
 96 |      {0 as : List a}
 97 |   -> (x : Expr a as)
 98 |   -> (y : a)
 99 |   -> {auto _ : Elem y as}
100 |   -> Expr a as
101 | (-.) x y = x - var y
102 |
103 | ||| Addition of variables. This is an alias for
104 | ||| `var x + y`.
105 | public export
106 | (.-) :
107 |      {0 as : List a}
108 |   -> (x : a)
109 |   -> (y : Expr a as)
110 |   -> {auto _ : Elem x as}
111 |   -> Expr a as
112 | (.-) x y = var x - y
113 |
114 | ||| Multiplication of variables. This is an alias for
115 | ||| `var x * var y`.
116 | public export
117 | (.*.) :
118 |      {0 as : List a}
119 |   -> (x,y : a)
120 |   -> {auto _ : Elem x as}
121 |   -> {auto _ : Elem y as}
122 |   -> Expr a as
123 | (.*.) x y = var x * var y
124 |
125 | ||| Multiplication of variables. This is an alias for
126 | ||| `var x * y`.
127 | public export
128 | (*.) :
129 |      {0 as : List a}
130 |   -> (x : Expr a as)
131 |   -> (y : a)
132 |   -> {auto _ : Elem y as}
133 |   -> Expr a as
134 | (*.) x y = x * var y
135 |
136 | ||| Multiplication of variables. This is an alias for
137 | ||| `x * var y`.
138 | public export
139 | (.*) :
140 |      {0 as : List a}
141 |   -> (x : a)
142 |   -> (y : Expr a as)
143 |   -> {auto _ : Elem x as}
144 |   -> Expr a as
145 | (.*) x y = var x * y
146 |
147 | --------------------------------------------------------------------------------
148 | --          Evaluation
149 | --------------------------------------------------------------------------------
150 |
151 | namespace Eval
152 |   parameters {0 a : Type}
153 |              {as : List a}
154 |              {z,o : a}
155 |              {p,m,sub : a -> a -> a}
156 |              (0 r : Ring a z o p m sub)
157 |              (isZ : (v : a) -> Maybe (v === z))
158 |
159 |     public export %inline
160 |     (+) : a -> a -> a
161 |     (+) = p
162 |
163 |     public export %inline
164 |     (*) : a -> a -> a
165 |     (*) = m
166 |
167 |     public export %inline
168 |     (-) : a -> a -> a
169 |     (-) = sub
170 |
171 |     ||| Evaluation of expressions. This keeps the exact
172 |     ||| structure of the expression tree. For instance
173 |     ||| `eval $ x .*. (y .+. z)` evaluates to `x * (y + z)`.
174 |     public export
175 |     eval : Expr a as -> a
176 |     eval (Lit v)   = v
177 |     eval (Var x y) = x
178 |     eval (x + y)   = eval x + eval y
179 |     eval (x * y)   = eval x * eval y
180 |     eval (x - y)   = eval x - eval y
181 |
182 |     --------------------------------------------------------------------------------
183 |     --          Normalize
184 |     --------------------------------------------------------------------------------
185 |
186 |     public export
187 |     negate : Sum a as -> Sum a as
188 |     negate []            = []
189 |     negate (T f x :: xs) = T (z - f) x :: negate xs
190 |
191 |     ||| Normalizes an arithmetic expression to a sum of products.
192 |     public export
193 |     norm : Expr a as -> Sum a as
194 |     norm (Lit n)   = [T n one]
195 |     norm (Var x y) = [T o $ fromVar y]
196 |     norm (x + y)   = add r.rig isZ (norm x) (norm y)
197 |     norm (x * y)   = mult r.rig isZ (norm x) (norm y)
198 |     norm (x - y)   = add r.rig isZ (norm x) (negate $ norm y)
199 |
200 |     ||| Like `norm` but removes all `zero` terms.
201 |     public export
202 |     normalize : Expr a as -> Sum a as
203 |     normalize e = normSum r.rig isZ (norm e)
204 |
205 |     0 pneg : (s : Sum a as) -> esum r.rig isZ (negate s) === z - esum r.rig isZ s
206 |     pneg []            = sym r.minusSelf
207 |     pneg (T f x :: xs) = Calc $
208 |       |~ (z - f) * eprod m o x + esum (r .rig) isZ (negate xs)
209 |       ~~ (z - f) * eprod m o x + (z - esum (r .rig) isZ xs)
210 |         ... cong ((z - f) * eprod m o x +) (pneg xs)
211 |       ~~ (z - f * eprod m o x) + (z - esum (r .rig) isZ xs)
212 |         ... cong (+ (z - esum (r .rig) isZ xs)) r.multNegLeft
213 |       ~~ z - (esum (r .rig) isZ xs + f * eprod m o x)
214 |         ..< invertProduct r.plus.grp
215 |       ~~ z - (f * eprod m o x + esum r.rig isZ xs)
216 |         ... cong (z `sub`) r.plus.commutative
217 |
218 |     -- Evaluating an expression gives the same result as
219 |     -- evaluating its normalized form.
220 |     0 pnorm : (e : Expr a as) -> eval e === esum r.rig isZ (norm e)
221 |     pnorm (Lit n)   = Calc $
222 |       |~ n
223 |       ~~ n * o                        ..< r.mult.rightNeutral
224 |       ~~ n * eprod m o (one {as})     ..< cong (n *) (pone r.mult as)
225 |       ~~ n * eprod m o (one {as}) + z ..< r.plus.rightNeutral
226 |
227 |     pnorm (Var x y) = Calc $
228 |       |~ x
229 |       ~~ eprod m o (fromVar y)          ..< pvar r.mult as y
230 |       ~~ o * eprod m o (fromVar y)      ..< r.mult.leftNeutral
231 |       ~~ o * eprod m o (fromVar y) + z  ..< r.plus.rightNeutral
232 |
233 |     pnorm (x + y)   = Calc $
234 |       |~ eval x + eval y
235 |       ~~ esum r.rig isZ (norm x) + eval y
236 |          ... cong (+ eval y) (pnorm x)
237 |       ~~ esum r.rig isZ (norm x) + esum r.rig isZ (norm y)
238 |          ... cong (esum r.rig isZ (norm x) +) (pnorm y)
239 |       ~~ esum r.rig isZ (add r.rig isZ (norm x) (norm y))
240 |          ... padd r.rig isZ _ _
241 |
242 |     pnorm (x * y) = Calc $
243 |       |~ eval x * eval y
244 |       ~~ esum r.rig isZ (norm x) * eval y
245 |          ... cong (* eval y) (pnorm x)
246 |       ~~ esum r.rig isZ (norm x) * esum r.rig isZ (norm y)
247 |          ... cong (esum r.rig isZ (norm x) *) (pnorm y)
248 |       ~~ esum r.rig isZ (mult r.rig isZ (norm x) (norm y))
249 |          ... pmult r.rig isZ _ _
250 |
251 |     pnorm (x - y) = Calc $
252 |       |~ eval x - eval y
253 |       ~~ esum r.rig isZ (norm x) - eval y
254 |         ... cong (\v => v - eval y) (pnorm x)
255 |       ~~ esum r.rig isZ (norm x) - esum r.rig isZ (norm y)
256 |         ... cong (esum r.rig isZ (norm x) -) (pnorm y)
257 |       ~~ (esum r.rig isZ (norm x) + z) - esum r.rig isZ (norm y)
258 |         ..< cong (\v => v - esum r.rig isZ (norm y)) r.plus.rightNeutral
259 |       ~~ esum r.rig isZ (norm x) + (z - esum r.rig isZ (norm y))
260 |         ..< r.minusAssociative
261 |       ~~ esum r.rig isZ (norm x) + (esum r.rig isZ (negate $ norm y))
262 |         ..< cong (esum r.rig isZ (norm x) +) (pneg $ norm y)
263 |       ~~ esum r.rig isZ (add r.rig isZ (norm x) (negate (norm y)))
264 |         ... padd r.rig isZ _ _
265 |
266 |     -- Evaluating an expression gives the same result as
267 |     -- evaluating its normalized form.
268 |     0 pnormalize : (e : Expr a as) -> eval e === esum r.rig isZ (normalize e)
269 |     pnormalize e = Calc $
270 |       |~ eval e
271 |       ~~ esum r.rig isZ (norm e)                     ... pnorm e
272 |       ~~ esum r.rig isZ (normSum r.rig isZ (norm e)) ..< pnormSum r.rig isZ (norm e)
273 |
274 |     --------------------------------------------------------------------------------
275 |     --          Solver
276 |     --------------------------------------------------------------------------------
277 |
278 |     ||| Given a list `as` of variables and two arithmetic expressions
279 |     ||| over these variables, if the expressions are converted
280 |     ||| to the same normal form, evaluating them gives the same
281 |     ||| result.
282 |     |||
283 |     ||| This simple fact allows us to conveniently and quickly
284 |     ||| proof arithmetic equalities required in other parts of
285 |     ||| our code. For instance:
286 |     |||
287 |     ||| ```idris example
288 |     ||| 0 binom1 : {x,y : Bits8}
289 |     |||          -> (x + y) * (x + y) === x * x + 2 * x * y + y * y
290 |     ||| binom1 = solve [x,y]
291 |     |||                ((x .+. y) * (x .+. y))
292 |     |||                (x .*. x + 2 *. x *. y + y .*. y)
293 |     ||| ```
294 |     export
295 |     0 solve :
296 |          (e1,e2 : Expr a as)
297 |       -> {auto prf : normalize e1 === normalize e2}
298 |       -> eval e1 === eval e2
299 |     solve e1 e2 @{prf} = Calc $
300 |       |~ eval e1
301 |       ~~ esum r.rig isZ (normalize e1) ...(pnormalize e1)
302 |       ~~ esum r.rig isZ (normalize e2) ...(cong (esum r.rig isZ) prf)
303 |       ~~ eval e2                       ..<(pnormalize e2)
304 |