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