0 | module Algebra.Solver.Semiring.Prod
 1 |
 2 | import Algebra.Solver.Semiring.Expr
 3 | import public Algebra.Solver.Prod
 4 | import Algebra.Solver.Semiring.Util
 5 |
 6 | %default total
 7 |
 8 | ||| Evaluate products of variables each raised to
 9 | ||| given exponent.
10 | |||
11 | ||| Every arithmetic expression in a commutative ring
12 | ||| can be represented as a sum of products of the variables
13 | ||| each raised by an exponent and multiplied by a constant
14 | ||| factor. For instance, expression `x + x * (y + z + z)`
15 | ||| gets normalized to `x + x * y + 2 * x * z`.
16 | public export
17 | eprod : Semiring a => {as : List a} -> Prod a as -> a
18 | eprod {as = []}      []        = 1
19 | eprod {as = x :: xs} (e :: es) = pow x e * eprod es
20 |
21 | --------------------------------------------------------------------------------
22 | --          Proofs
23 | --------------------------------------------------------------------------------
24 |
25 | ||| Proof that `one` evaluates to 1.
26 | export
27 | 0 pone : Semiring a => (as : List a) -> eprod (one {as}) === 1
28 | pone []        = Refl
29 | pone (x :: xs) = Calc $
30 |   |~ 1 * eprod (one {as = xs})
31 |   ~~ 1 * 1                     ... cong (1 * ) (pone xs)
32 |   ~~ 1                         ... multOneRightNeutral
33 |
34 | ||| Proof that `fromVar x` evaluates to `x`.
35 | export
36 | 0 pvar :
37 |      {auto _ : Semiring a}
38 |   -> (as : List a)
39 |   -> (e  : Elem x as)
40 |   -> eprod (fromVar {as} e) === x
41 | pvar (x :: vs) Here      = Calc $
42 |   |~ (x * 1) * eprod (one {as = vs})
43 |   ~~ (x * 1) * 1                     ... cong ((x*1) *) (pone vs)
44 |   ~~ x * 1                           ... multOneRightNeutral
45 |   ~~ x                               ... multOneRightNeutral
46 |
47 | pvar (v :: vs) (There y) = Calc $
48 |   |~ 1 * eprod (fromVar {as = vs} y)
49 |   ~~ 1 * x                           ... cong (1*) (pvar vs y)
50 |   ~~ x                               ... multOneLeftNeutral
51 |
52 | pvar [] Here impossible
53 | pvar [] (There y) impossible
54 |
55 | ||| Proof that evaluation of a multiplication of products
56 | ||| is the same as multiplying the results of evaluating each
57 | ||| of them.
58 | export
59 | 0 pmult :
60 |      {auto _ : Semiring a}
61 |   -> (p,q : Prod a as)
62 |   -> eprod (mult p q) === eprod p * eprod q
63 | pmult []        []        = sym multOneLeftNeutral
64 | pmult {as = h :: t} (x :: xs) (y :: ys) = Calc $
65 |   |~ pow h (x + y) * eprod (mult xs ys)
66 |   ~~ (pow h x * pow h y) * eprod (mult xs ys)
67 |      ... cong (* eprod (mult xs ys)) (ppow x y h)
68 |   ~~ (pow h x * pow h y) * (eprod xs * eprod ys)
69 |      ... cong ((pow h x * pow h y) *) (pmult xs ys)
70 |   ~~ (pow h x * eprod xs) * (pow h y * eprod ys)
71 |      ... Util.m1324
72 |