0 | module Algebra.Solver.Product
  1 |
  2 | import Algebra.Group
  3 | import Algebra.Ring
  4 | import public Data.List.Elem
  5 | import Syntax.PreorderReasoning
  6 |
  7 | %default total
  8 |
  9 | ||| A product of variables each represented by the exponent,
 10 | ||| to which it is raised.
 11 | |||
 12 | ||| When normalizing commutative arithmetic expressions, they often
 13 | ||| get converted to (sums of) products of variables
 14 | ||| (listed in index `as`), each raised to a certain
 15 | ||| exponent. This is the case for commutative monoids
 16 | ||| (a single product) as well as commutative (semi)rings
 17 | ||| (a sum of products).
 18 | |||
 19 | ||| Example: Assume the monoid in question is `(Bits8,(+),0)` (addition
 20 | |||          of 8-bit numbers). Assume further, that we have variables
 21 | |||          `[x,y,z]`. The expression `(x + x) + y + (z + z + z + z)` would
 22 | |||          then be represented as `[2,1,4]`
 23 | public export
 24 | data Prod : (a : Type) -> (as : List a) -> Type where
 25 |   Nil  : Prod a []
 26 |   (::) : (exp : Nat) -> Prod a xs -> Prod a (x :: xs)
 27 |
 28 | ||| Multiplying two products means adding all
 29 | ||| expontents pairwise.
 30 | public export
 31 | mult : Prod a as -> Prod a as -> Prod a as
 32 | mult []        []        = []
 33 | mult (x :: xs) (y :: ys) = (x + y) :: mult xs ys
 34 |
 35 | ||| We sort products by lexicographically comparing
 36 | ||| the exponents.
 37 | public export
 38 | compProd : Prod a as -> Prod a as -> Ordering
 39 | compProd []        []        = EQ
 40 | compProd (x :: xs) (y :: ys) = case compare x y of
 41 |   LT => LT
 42 |   GT => GT
 43 |   EQ => compProd xs ys
 44 |
 45 | ||| The neutral product where all exponents are zero.
 46 | public export
 47 | one : {as : List a} -> Prod a as
 48 | one {as = []}      = []
 49 | one {as = x :: xs} = 0 :: one
 50 |
 51 | ||| Convert a single variable to a product of variables.
 52 | public export
 53 | fromVar : {as : List a} -> Elem x as -> Prod a as
 54 | fromVar {as = x :: xs} Here      = 1 :: one
 55 | fromVar {as = x :: xs} (There y) = 0 :: fromVar y
 56 | fromVar {as = []} Here impossible
 57 | fromVar {as = []} (There y) impossible
 58 |
 59 | --------------------------------------------------------------------------------
 60 | --          Term
 61 | --------------------------------------------------------------------------------
 62 |
 63 | ||| A single term in a normalized arithmetic expressions.
 64 | |||
 65 | ||| This is a product of all variables each raised to
 66 | ||| a given power, multiplied with a constant factor (which is supposed
 67 | ||| to reduce during elaboration).
 68 | |||
 69 | ||| Example: Assume the monoid in question is `(Bits8,(+),0)` (addition
 70 | |||          of 8-bit numbers). Assume further, that we have variables
 71 | |||          `[x,y,z]`. The expression `3 + (x + x) + y + (z + z + z + z)` would
 72 | |||          then be represented as `T 3 [2,1,4]`
 73 | public export
 74 | record Term (a : Type) (as : List a) where
 75 |   constructor T
 76 |   factor : a
 77 |   prod   : Prod a as
 78 |
 79 | ||| Negates the constant factor in a term using the given negation function.
 80 | public export
 81 | negTerm : (neg : a -> a) -> Term a as -> Term a as
 82 | negTerm neg (T f p) = T (neg f) p
 83 |
 84 | namespace Term
 85 |
 86 |   ||| Multiplies two terms using the given function to multiply the
 87 |   ||| constant factors.
 88 |   public export
 89 |   mult : (p : a -> a -> a) -> Term a as -> Term a as -> Term a as
 90 |   mult p (T f1 p1) (T f2 p2) = T (p f1 f2) (mult p1 p2)
 91 |
 92 | --------------------------------------------------------------------------------
 93 | --          Evaluation
 94 | --------------------------------------------------------------------------------
 95 |
 96 | public export
 97 | times : (p : a -> a -> a) -> (n : a) -> Nat -> a -> a
 98 | times p n 0     x = n
 99 | times p n (S k) x = x `p` times p n k x
100 |
101 | public export
102 | eprod : {as : _} -> (p : a -> a -> a) -> (n : a) -> Prod a as -> a
103 | eprod                p n []         = n
104 | eprod {as = v :: vs} p n (exp :: x) = times p n exp v `p` eprod p n x
105 |
106 | ||| Evaluate a term using the given monoid.
107 | public export
108 | eterm : {as : List a} -> (p : a -> a -> a) -> (n : a) -> Term a as -> a
109 | eterm p n (T f prod) = f `p` eprod p n prod
110 |
111 | --------------------------------------------------------------------------------
112 | --          Monoid Proofs
113 | --------------------------------------------------------------------------------
114 |
115 | ||| A utility proof that is used several times internally
116 | export
117 | 0 lemma1324 :
118 |      CommutativeSemigroup a p
119 |   -> {k,l,m,n : a}
120 |   -> (k `p` l) `p` (m `p` n) === (k `p` m) `p` (l `p` n)
121 | lemma1324 c = Calc $
122 |   |~ (k `p` l) `p` (m `p` n)
123 |   ~~ ((k `p` l) `p` m) `p` n ... c.associative
124 |   ~~ (k `p` (l `p` m)) `p` n ..< cong (`p` n) c.associative
125 |   ~~ (k `p` (m `p` l)) `p` n ... cong (\x => (k `p` x) `p` n) c.commutative
126 |   ~~ ((k `p` m) `p` l) `p` n ... cong (`p` n) c.associative
127 |   ~~ (k `p` m) `p` (l `p` n) ..< c.associative
128 |
129 | ||| A utility proof that is used several times internally
130 | export
131 | 0 lemma213 :
132 |      CommutativeSemigroup a p
133 |   -> {k,m,n : a}
134 |   -> k `p` (m `p` n) === m `p` (k `p` n)
135 | lemma213 c = Calc $
136 |   |~ k `p` (m `p` n)
137 |   ~~ (k `p` m) `p` n ... c.associative
138 |   ~~ (m `p` k) `p` n ... cong (`p` n) c.commutative
139 |   ~~ m `p` (k `p` n) ..< c.associative
140 |
141 | export
142 | 0 ptimes :
143 |      CommutativeMonoid a z p
144 |   -> (m,n : Nat)
145 |   -> (x : a)
146 |   -> times p z m x `p` times p z n x === times p z (m + n) x
147 | ptimes c 0     n x = c.leftNeutral
148 | ptimes c (S k) n x = Calc $
149 |   |~ (x `p` times p z k x) `p` times p z n x
150 |   ~~ x `p` (times p z k x `p` times p z n x) ..< c.associative
151 |   ~~ x `p` (times p z (k + n) x)             ... cong (p x) (ptimes c k n x)
152 |
153 | export
154 | 0 peprod :
155 |      CommutativeMonoid a z p
156 |   -> (e1,e2 : Prod a as)
157 |   -> eprod p z e1 `p` eprod p z e2 === eprod p z (mult e1 e2)
158 | peprod                c []        []        = c.rightNeutral
159 | peprod {as = v :: vs} c (m :: xs) (n :: ys) = Calc $
160 |   |~ (times p z m v `p` eprod p z xs) `p` (times p z n v `p` eprod p z ys)
161 |   ~~ (times p z m v `p` times p z n v) `p` (eprod p z xs `p` eprod p z ys)
162 |      ... lemma1324 c.csgrp
163 |   ~~ (times p z m v `p` times p z n v) `p` (eprod p z (mult xs ys))
164 |      ... cong (p (times p z m v `p` times p z n v)) (peprod c xs ys)
165 |   ~~ times p z (m + n) v `p` eprod p z (mult xs ys)
166 |      ... cong (`p` eprod p z (mult xs ys)) (ptimes c m n v)
167 |
168 | export
169 | 0 pappend :
170 |      CommutativeMonoid a z p
171 |   -> (e1,e2 : Term a as)
172 |   -> eterm p z e1 `p` eterm p z e2 === eterm p z (mult p e1 e2)
173 | pappend c (T f v) (T g w) = Calc $
174 |   |~ (f `p` eprod p z v) `p` (g `p` eprod p z w)
175 |   ~~ (f `p` g) `p` (eprod p z v `p` eprod p z w)
176 |      ... lemma1324 c.csgrp
177 |   ~~ (f `p` g) `p` eprod p z (mult v w)
178 |      ... cong ((f `p` g) `p`) (peprod c v w)
179 |
180 | ||| Proof that `Prod.one` evaluates to `neutral`
181 | export
182 | 0 pone :
183 |      CommutativeMonoid a z p
184 |   -> (as : List a)
185 |   -> eprod p z {as} Product.one === z
186 | pone c []        = Refl
187 | pone c (v :: vs) = Calc $
188 |   |~ z `p` eprod p z {as = vs} one
189 |   ~~ z `p` z                       ... cong (z `p`) (pone c vs)
190 |   ~~ z                             ... c.leftNeutral
191 |
192 | ||| Proof that for `e : Elem x as`, `fromVar e` evaluates to `x`.
193 | export
194 | 0 pvar :
195 |      CommutativeMonoid a z p
196 |   -> (as : List a)
197 |   -> (e  : Elem x as)
198 |   -> eprod p z (fromVar {as} e) === x
199 | pvar c (x :: vs) Here      = Calc $
200 |   |~ (x `p` z) `p` eprod p z {as = vs} one
201 |   ~~ (x `p` z) `p` z                       ... cong ((x `p` z) `p`) (pone c vs)
202 |   ~~ x `p` z                               ... c.rightNeutral
203 |   ~~ x                                     ... c.rightNeutral
204 |
205 | pvar c (v :: vs) (There y) = Calc $
206 |   |~ z `p` eprod p z (fromVar y)
207 |   ~~ eprod p z (fromVar y)                 ... c.leftNeutral
208 |   ~~ x                                     ... pvar c vs y
209 |
210 | pvar c [] Here impossible
211 | pvar c [] (There y) impossible
212 |
213 | --------------------------------------------------------------------------------
214 | --          Ordering Proofs
215 | --------------------------------------------------------------------------------
216 |
217 | Uninhabited (LT = EQ) where
218 |   uninhabited _ impossible
219 |
220 | Uninhabited (GT = EQ) where
221 |   uninhabited _ impossible
222 |
223 | export
224 | 0 pcompNat : (x,y : Nat) -> (compare x y === EQ) -> x === y
225 | pcompNat 0 0         prf = Refl
226 | pcompNat (S k) (S j) prf = cong S $ pcompNat k j prf
227 | pcompNat Z (S k) Refl impossible
228 | pcompNat (S k) Z Refl impossible
229 |
230 | export
231 | 0 pcompProd :
232 |      (x,y : Prod a as)
233 |   -> (compProd x y === EQ)
234 |   -> x === y
235 | pcompProd []        []        prf = Refl
236 | pcompProd (x :: xs) (y :: ys) prf with (compare x y) proof eq
237 |   _ | EQ = cong2 (::) (pcompNat x y eq) (pcompProd xs ys prf)
238 |   _ | LT = absurd prf
239 |   _ | GT = absurd prf
240 | pcompProd []        (_ :: _)  Refl impossible
241 | pcompProd (_ :: _)  []        Refl impossible
242 |
243 | --------------------------------------------------------------------------------
244 | --          Ring Proofs
245 | --------------------------------------------------------------------------------
246 |
247 | ||| Proof that evaluation of a multiplication of products
248 | ||| is the same as multiplying the results of evaluating each
249 | ||| of them.
250 | export
251 | 0 pmult :
252 |      Rig a z o p m
253 |   -> (x,y : Prod a as)
254 |   -> eprod m o (mult x y) === eprod m o x `m` eprod m o y
255 | pmult r               []        []        = sym r.mult.leftNeutral
256 | pmult r {as = h :: t} (x :: xs) (y :: ys) = Calc $
257 |   |~ times m o (x + y) h `m` eprod m o (mult xs ys)
258 |   ~~ (times m o x h `m` times m o y h) `m` eprod m o (mult xs ys)
259 |      ..< cong (`m` eprod m o (mult xs ys)) (ptimes r.mult x y h)
260 |   ~~ (times m o x h `m` times m o y h) `m` (eprod m o xs `m` eprod m o ys)
261 |      ... cong ((times m o x h `m` times m o y h) `m`) (pmult r xs ys)
262 |   ~~ (times m o x h `m` eprod m o xs) `m` (times m o y h `m` eprod m o ys)
263 |     ... lemma1324 r.mult.csgrp
264 |