0 | module Algebra.Solver.Semiring.Expr
  1 |
  2 | import public Data.List.Elem
  3 | import public Algebra.Semiring
  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 : Semiring 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 semiring.
 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.Semiring.Sum.normalize`.
 54 | ||| 2. The normal forms are compared for being identical.
 55 | ||| 3. Since in `Algebra.Solver.Semiring.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 | public export
 61 | data Expr : (a : Type) -> (as : List a) -> Type where
 62 |   ||| A literal. This should be a value known at compile time
 63 |   ||| so that it reduces during normalization.
 64 |   Lit   : (v : a) -> Expr a as
 65 |
 66 |   ||| A variabl. This is is for values not known at compile
 67 |   ||| time. In order to compare and merge variables, we need an
 68 |   ||| `Elem x as` proof.
 69 |   Var   : (x : a) -> Elem x as -> Expr a as
 70 |
 71 |   ||| Addition of two expressions.
 72 |   Plus  : (x,y : Expr a as) -> Expr a as
 73 |
 74 |   ||| Multiplication of two expressions.
 75 |   Mult  : (x,y : Expr a as) -> Expr a as
 76 |
 77 | ||| While this allows you to use the usual operators
 78 | ||| for addition and multiplication, it is often convenient
 79 | ||| to use related operators `.*.`, `.+.`, and similar when
 80 | ||| working with variables.
 81 | public export
 82 | Num a => Num (Expr a as) where
 83 |   (+) = Plus
 84 |   (*) = Mult
 85 |   fromInteger = Lit . fromInteger
 86 |
 87 | ||| Like `Var` but takes the `Elem x as` as an auto implicit
 88 | ||| argument.
 89 | public export
 90 | var : {0 as : List a} -> (x : a) -> Elem x as => Expr a as
 91 | var x = Var x %search
 92 |
 93 | --------------------------------------------------------------------------------
 94 | --          Syntax
 95 | --------------------------------------------------------------------------------
 96 |
 97 | export infixl 8 .+., .+, +.
 98 |
 99 | export infixl 9 .*., .*, *.
100 |
101 | ||| Addition of variables. This is an alias for
102 | ||| `var x + var y`.
103 | public export
104 | (.+.) :
105 |      {0 as : List a}
106 |   -> (x,y : a)
107 |   -> {auto _ : Elem x as}
108 |   -> {auto _ : Elem y as}
109 |   -> Expr a as
110 | (.+.) x y = Plus (var x) (var y)
111 |
112 | ||| Addition of variables. This is an alias for
113 | ||| `x + var y`.
114 | public export
115 | (+.) :
116 |      {0 as : List a}
117 |   -> (x : Expr a as)
118 |   -> (y : a)
119 |   -> {auto _ : Elem y as}
120 |   -> Expr a as
121 | (+.) x y = Plus x (var y)
122 |
123 | ||| Addition of variables. This is an alias for
124 | ||| `var x + y`.
125 | public export
126 | (.+) :
127 |      {0 as : List a}
128 |   -> (x : a)
129 |   -> (y : Expr a as)
130 |   -> {auto _ : Elem x as}
131 |   -> Expr a as
132 | (.+) x y = Plus (var x) y
133 |
134 | ||| Multiplication of variables. This is an alias for
135 | ||| `var x * var y`.
136 | public export
137 | (.*.) :
138 |      {0 as : List a}
139 |   -> (x,y : a)
140 |   -> {auto _ : Elem x as}
141 |   -> {auto _ : Elem y as}
142 |   -> Expr a as
143 | (.*.) x y = Mult (var x) (var y)
144 |
145 | ||| Multiplication of variables. This is an alias for
146 | ||| `var x * y`.
147 | public export
148 | (*.) :
149 |      {0 as : List a}
150 |   -> (x : Expr a as)
151 |   -> (y : a)
152 |   -> {auto _ : Elem y as}
153 |   -> Expr a as
154 | (*.) x y = Mult x (var y)
155 |
156 | ||| Multiplication of variables. This is an alias for
157 | ||| `x * var y`.
158 | public export
159 | (.*) :
160 |      {0 as : List a}
161 |   -> (x : a)
162 |   -> (y : Expr a as)
163 |   -> {auto _ : Elem x as}
164 |   -> Expr a as
165 | (.*) x y = Mult (var x) y
166 |
167 | --------------------------------------------------------------------------------
168 | --          Evaluation
169 | --------------------------------------------------------------------------------
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 : Semiring a => Expr a as -> a
176 | eval (Lit v)     = v
177 | eval (Var x y)   = x
178 | eval (Plus x y)  = eval x + eval y
179 | eval (Mult x y)  = eval x * eval y
180 |
181 | --------------------------------------------------------------------------------
182 | --          Proofs
183 | --------------------------------------------------------------------------------
184 |
185 | ||| Proof that addition of exponents is equivalent to multiplcation
186 | ||| of the two terms.
187 | export
188 | 0 ppow :
189 |      {auto _ : Semiring a}
190 |   -> (m,n : Nat)
191 |   -> (x   : a)
192 |   -> pow x (m + n) === pow x m * pow x n
193 | ppow 0     n x = sym multOneLeftNeutral
194 | ppow (S k) n x = Calc $
195 |   |~ x * pow x (plus k n)
196 |   ~~ x * (pow x k * pow x n) ... cong (x*) (ppow k n x)
197 |   ~~ (x * pow x k) * pow x n ... multAssociative
198 |