0 | module Algebra.Solver.Ring.Expr
  1 |
  2 | import public Data.List.Elem
  3 | import public Algebra.Ring
  4 | import Syntax.PreorderReasoning
  5 |
  6 | %default total
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          Natural Numbers
 10 | --------------------------------------------------------------------------------
 11 |
 12 | ||| Multiplies a value `n` times with itself. In case of `n`
 13 | ||| being zero, this returns `1`.
 14 | public export
 15 | pow : Ring a => a -> Nat -> a
 16 | pow x 0     = 1
 17 | pow x (S k) = x * pow x k
 18 |
 19 | --------------------------------------------------------------------------------
 20 | --          Expression
 21 | --------------------------------------------------------------------------------
 22 |
 23 | ||| Data type representing expressions in a commutative ring.
 24 | |||
 25 | ||| This is used to at compile time compare different forms of
 26 | ||| the same expression and proof that they evaluate to
 27 | ||| the same result.
 28 | |||
 29 | ||| An example:
 30 | |||
 31 | ||| ```idris example
 32 | ||| 0 binom1 : {x,y : Bits8} -> (x + y) * (x + y) === x * x + 2 * x * y + y * y
 33 | ||| binom1 = solve [x,y]
 34 | |||                ((x .+. y) * (x .+. y))
 35 | |||                (x .*. x + 2 *. x *. y + y .*. y)
 36 | ||| ```
 37 | |||
 38 | ||| @ a  the type used in the arithmetic expression
 39 | ||| @ as list of variables which don't reduce at compile time
 40 | |||
 41 | ||| In the example above, `x` and `y` are variables, while `2`
 42 | ||| is a literal known at compile time. To make working with
 43 | ||| variables more convenient (the have to be wrapped in data
 44 | ||| constructor `Var`, by using function `var` for instance),
 45 | ||| additional operators for addition, multiplication, and
 46 | ||| subtraction are provided.
 47 | |||
 48 | ||| In order to proof that two expressions evaluate to the
 49 | ||| same results, the following steps are taken at compile
 50 | ||| time:
 51 | |||
 52 | ||| 1. Both expressions are converted to a normal form via
 53 | |||    `Algebra.Solver.Ring.Sum.normalize`.
 54 | ||| 2. The normal forms are compared for being identical.
 55 | ||| 3. Since in `Algebra.Solver.Ring.Sum` there is a proof that
 56 | |||    converting an expression to its normal form does not
 57 | |||    affect the result when evaluating it, if the normal
 58 | |||    forms are identical, the two expressions must evaluate
 59 | |||    to the same result.
 60 | |||
 61 | ||| You can find several examples of making use of this
 62 | ||| in `Data.Prim.Integer.Extra`.
 63 | public export
 64 | data Expr : (a : Type) -> (as : List a) -> Type where
 65 |   ||| A literal. This should be a value known at compile time
 66 |   ||| so that it reduces during normalization.
 67 |   Lit   : (v : a) -> Expr a as
 68 |
 69 |   ||| A variabl. This is is for values not known at compile
 70 |   ||| time. In order to compare and merge variables, we need an
 71 |   ||| `Elem x as` proof.
 72 |   Var   : (x : a) -> Elem x as -> Expr a as
 73 |
 74 |   ||| Negates and expression.
 75 |   Neg   : Expr a as -> Expr a as
 76 |
 77 |   ||| Addition of two expressions.
 78 |   Plus  : (x,y : Expr a as) -> Expr a as
 79 |
 80 |   ||| Multiplication of two expressions.
 81 |   Mult  : (x,y : Expr a as) -> Expr a as
 82 |
 83 |   ||| Subtraction of two expressions.
 84 |   Minus : (x,y : Expr a as) -> Expr a as
 85 |
 86 | ||| While this allows you to use the usual operators
 87 | ||| for addition and multiplication, it is often convenient
 88 | ||| to use related operators `.*.`, `.+.`, and similar when
 89 | ||| working with variables.
 90 | public export
 91 | Num a => Num (Expr a as) where
 92 |   (+) = Plus
 93 |   (*) = Mult
 94 |   fromInteger = Lit . fromInteger
 95 |
 96 | public export
 97 | Neg a => Neg (Expr a as) where
 98 |   negate = Neg
 99 |   (-)    = Minus
100 |
101 | ||| Like `Var` but takes the `Elem x as` as an auto implicit
102 | ||| argument.
103 | public export
104 | var : {0 as : List a} -> (x : a) -> Elem x as => Expr a as
105 | var x = Var x %search
106 |
107 | --------------------------------------------------------------------------------
108 | --          Syntax
109 | --------------------------------------------------------------------------------
110 |
111 | export infixl 8 .+., .+, +.
112 |
113 | export infixl 8 .-., .-, -.
114 |
115 | export infixl 9 .*., .*, *.
116 |
117 | ||| Addition of variables. This is an alias for
118 | ||| `var x + var y`.
119 | public export
120 | (.+.) :
121 |      {0 as : List a}
122 |   -> (x,y : a)
123 |   -> {auto _ : Elem x as}
124 |   -> {auto _ : Elem y as}
125 |   -> Expr a as
126 | (.+.) x y = Plus (var x) (var y)
127 |
128 | ||| Addition of variables. This is an alias for
129 | ||| `x + var y`.
130 | public export
131 | (+.) :
132 |      {0 as : List a}
133 |   -> (x : Expr a as)
134 |   -> (y : a)
135 |   -> {auto _ : Elem y as}
136 |   -> Expr a as
137 | (+.) x y = Plus x (var y)
138 |
139 | ||| Addition of variables. This is an alias for
140 | ||| `var x + y`.
141 | public export
142 | (.+) :
143 |      {0 as : List a}
144 |   -> (x : a)
145 |   -> (y : Expr a as)
146 |   -> {auto _ : Elem x as}
147 |   -> Expr a as
148 | (.+) x y = Plus (var x) y
149 |
150 | ||| Subtraction of variables. This is an alias for
151 | ||| `var x - var y`.
152 | public export
153 | (.-.) :
154 |      {0 as : List a}
155 |   -> (x,y : a)
156 |   -> {auto _ : Elem x as}
157 |   -> {auto _ : Elem y as}
158 |   -> Expr a as
159 | (.-.) x y = Minus (var x) (var y)
160 |
161 | ||| Subtraction of variables. This is an alias for
162 | ||| `x - var y`.
163 | public export
164 | (-.) :
165 |      {0 as : List a}
166 |   -> (x : Expr a as)
167 |   -> (y : a)
168 |   -> {auto _ : Elem y as}
169 |   -> Expr a as
170 | (-.) x y = Minus x (var y)
171 |
172 | ||| Subtraction of variables. This is an alias for
173 | ||| `var x - y`.
174 | public export
175 | (.-) :
176 |      {0 as : List a}
177 |   -> (x : a)
178 |   -> (y : Expr a as)
179 |   -> {auto _ : Elem x as}
180 |   -> Expr a as
181 | (.-) x y = Minus (var x) y
182 |
183 | ||| Multiplication of variables. This is an alias for
184 | ||| `var x * var y`.
185 | public export
186 | (.*.) :
187 |      {0 as : List a}
188 |   -> (x,y : a)
189 |   -> {auto _ : Elem x as}
190 |   -> {auto _ : Elem y as}
191 |   -> Expr a as
192 | (.*.) x y = Mult (var x) (var y)
193 |
194 | ||| Multiplication of variables. This is an alias for
195 | ||| `var x * y`.
196 | public export
197 | (*.) :
198 |      {0 as : List a}
199 |   -> (x : Expr a as)
200 |   -> (y : a)
201 |   -> {auto _ : Elem y as}
202 |   -> Expr a as
203 | (*.) x y = Mult x (var y)
204 |
205 | ||| Multiplication of variables. This is an alias for
206 | ||| `x * var y`.
207 | public export
208 | (.*) :
209 |      {0 as : List a}
210 |   -> (x : a)
211 |   -> (y : Expr a as)
212 |   -> {auto _ : Elem x as}
213 |   -> Expr a as
214 | (.*) x y = Mult (var x) y
215 |
216 | --------------------------------------------------------------------------------
217 | --          Evaluation
218 | --------------------------------------------------------------------------------
219 |
220 | ||| Evaluation of expressions. This keeps the exact
221 | ||| structure of the expression tree. For instance
222 | ||| `eval $ x .*. (y .+. z)` evaluates to `x * (y + z)`.
223 | public export
224 | eval : Ring a => Expr a as -> a
225 | eval (Lit v)     = v
226 | eval (Var x y)   = x
227 | eval (Neg v)     = neg $ eval v
228 | eval (Plus x y)  = eval x + eval y
229 | eval (Mult x y)  = eval x * eval y
230 | eval (Minus x y) = eval x - eval y
231 |
232 | --------------------------------------------------------------------------------
233 | --          Proofs
234 | --------------------------------------------------------------------------------
235 |
236 | ||| Proof that addition of exponents is equivalent to multiplcation
237 | ||| of the two terms.
238 | export
239 | 0 ppow :
240 |      {auto _ : Ring a}
241 |   -> (m,n : Nat)
242 |   -> (x   : a)
243 |   -> pow x (m + n) === pow x m * pow x n
244 | ppow 0     n x = sym multOneLeftNeutral
245 | ppow (S k) n x = Calc $
246 |   |~ x * pow x (plus k n)
247 |   ~~ x * (pow x k * pow x n) ... cong (x*) (ppow k n x)
248 |   ~~ (x * pow x k) * pow x n ... multAssociative
249 |