0 | module Algebra.Solver.Sum
  1 |
  2 | import Algebra.Group
  3 | import Algebra.Ring
  4 | import Algebra.Solver.Product
  5 | import Syntax.PreorderReasoning
  6 |
  7 | %default total
  8 |
  9 | ||| Normalized arithmetic expression in a commutative
 10 | ||| ring (represented as an (ordered) sum of terms).
 11 | public export
 12 | data Sum : (a : Type) -> (as : List a) -> Type where
 13 |   Nil  : {0 as : List a} -> Sum a as
 14 |   (::) : {0 as : List a} -> Term a as -> Sum a as -> Sum a as
 15 |
 16 | parameters {0 a : Type}
 17 |            {as : List a}
 18 |            {z,o : a}
 19 |            {p,m : a -> a -> a}
 20 |            (0 r : Rig a z o p m)
 21 |            (isZ : (v : a) -> Maybe (v === z))
 22 |
 23 |   public export %inline
 24 |   (+) : a -> a -> a
 25 |   (+) = p
 26 |
 27 |   public export %inline
 28 |   (*) : a -> a -> a
 29 |   (*) = m
 30 |
 31 |   public export %inline
 32 |   eterm : Term a as -> a
 33 |   eterm = Product.eterm m o
 34 |
 35 |   ||| Evaluate a sum of terms.
 36 |   public export
 37 |   esum : Sum a as -> a
 38 |   esum []        = z
 39 |   esum (x :: xs) = eterm x + esum xs
 40 |
 41 | --------------------------------------------------------------------------------
 42 | --          Normalizer
 43 | --------------------------------------------------------------------------------
 44 |
 45 |   ||| Add two sums of terms.
 46 |   |||
 47 |   ||| The order of terms will be kept. If two terms have identical
 48 |   ||| products of variables, they will be unified by adding their
 49 |   ||| factors.
 50 |   public export
 51 |   add : Sum a as -> Sum a as -> Sum a as
 52 |   add []        ys                = ys
 53 |   add xs        []                = xs
 54 |   add (T m x :: xs) (T n y :: ys) = case compProd x y of
 55 |     LT => T m x :: add xs (T n y :: ys)
 56 |     GT => T n y :: add (T m x :: xs) ys
 57 |     EQ => T (m + n) y :: add xs ys
 58 |
 59 |   ||| Normalize a sum of terms by removing all terms with a
 60 |   ||| `zero` factor.
 61 |   public export
 62 |   normSum : Sum a as -> Sum a as
 63 |   normSum []           = []
 64 |   normSum (T f p :: y) = case isZ f of
 65 |     Just refl => normSum y
 66 |     Nothing   => T f p :: normSum y
 67 |
 68 |   ||| Multiplies a single term with a sum of terms.
 69 |   public export
 70 |   mult1 :  Term a as -> Sum a as -> Sum a as
 71 |   mult1 (T f p) (T g q :: xs) = T (f * g) (mult p q) :: mult1 (T f p) xs
 72 |   mult1 _       []            = []
 73 |
 74 |   ||| Multiplies two sums of terms.
 75 |   public export
 76 |   mult : Sum a as -> Sum a as -> Sum a as
 77 |   mult []        ys = []
 78 |   mult (x :: xs) ys = add (mult1 x ys) (mult xs ys)
 79 |
 80 |   --------------------------------------------------------------------------------
 81 |   --          Proofs
 82 |   --------------------------------------------------------------------------------
 83 |
 84 |   epr : Prod a as -> a
 85 |   epr = eprod m o
 86 |
 87 |   -- Adding two sums via `add` preserves the evaluation result.
 88 |   -- Note: `assert_total` in here is a temporary fix for idris issue #2954
 89 |   export
 90 |   0 padd : (x, y : Sum a as) -> esum x + esum y === esum (add x y)
 91 |   padd []            xs = r.plus.leftNeutral
 92 |   padd (x :: xs)     [] = r.plus.rightNeutral
 93 |   padd (T f x :: xs) (T g y :: ys) with (compProd x y) proof eq
 94 |     _ | LT = Calc $
 95 |       |~ (f * epr x + esum xs) + (g * epr y + esum ys)
 96 |       ~~ (f * epr x) + (esum xs + (g * epr y + esum ys))
 97 |         ..< r.plus.associative
 98 |       ~~ f * epr x + esum (add xs (T g y :: ys))
 99 |         ... cong (f * epr x +) (assert_total $ padd xs (T g y :: ys))
100 |     _ | GT = Calc $
101 |       |~ (f * epr x + esum xs) + (g * epr y + esum ys)
102 |       ~~ g * epr y + ((f * epr x + esum xs) + esum ys)
103 |          ..< lemma213 r.plus.csgrp
104 |       ~~ g * epr y + esum (add (T f x :: xs) ys)
105 |          ... cong (g * epr y  +) (assert_total $ padd (T f x :: xs) ys)
106 |     _ | EQ = case pcompProd x y eq of
107 |          Refl => Calc $
108 |            |~ (f * epr x + esum xs) + (g * epr x + esum ys)
109 |            ~~ (f * epr x + g * epr x) + (esum xs + esum ys)
110 |              ... lemma1324 r.plus.csgrp
111 |            ~~ (f + g) * epr x + (esum xs + esum ys)
112 |              ..< cong ( + (esum xs + esum ys)) r.rightDistributive
113 |            ~~ (f + g) * epr x + esum (add xs ys)
114 |              ... cong ((f + g) * epr x +) (padd xs ys)
115 |
116 |   -- Small utility lemma
117 |   0 psum0 : {x,y,v : a} -> x === y -> x === z * v + y
118 |   psum0 {x} {y} {v} prf = Calc $
119 |     |~ x
120 |     ~~ y         ... prf
121 |     ~~ z + y     ..< r.plus.leftNeutral
122 |     ~~ z * v + y ..< cong (+ y) r.multZeroLeftAbsorbs
123 |
124 |   -- Multiplying a sum with a term preserves the evaluation result.
125 |   0 pmult1 :
126 |        (v : a)
127 |     -> (q : Prod a as)
128 |     -> (s : Sum a as)
129 |     -> esum (mult1 (T v q) s) === (v * epr q) * esum s
130 |   pmult1 v q []            = sym r.multZeroRightAbsorbs
131 |   pmult1 v q (T f x :: xs) = Calc $
132 |     |~ (v * f) * epr (mult q x) + esum (mult1 (T v q) xs)
133 |     ~~ (v * f) * (epr q * epr x) + esum (mult1 (T v q) xs)
134 |       ..< cong (\x => ((v * f) * x) + esum (mult1 (T v q) xs)) (peprod r.mult q x)
135 |     ~~ (v * epr q ) * (f * epr x) + esum (mult1 (T v q) xs)
136 |       ..< cong ( + esum (mult1 (T v q) xs)) (lemma1324 r.mult.csgrp)
137 |     ~~ (v * epr q ) * (f * epr x) + (v * epr q ) * esum xs
138 |       ...  cong (((v * epr q ) * (f * epr x)) +) (pmult1 v q xs)
139 |     ~~ (v * epr q) * (f * epr x + esum xs)
140 |       ..< r.leftDistributive
141 |
142 |   -- Multiplying two sums of terms preserves the evaluation result.
143 |   export
144 |   0 pmult : (x,y : Sum a as) -> esum x * esum y === esum (mult x y)
145 |   pmult []            y = r.multZeroLeftAbsorbs
146 |   pmult (T f x :: xs) y = Calc $
147 |     |~ (f * epr x + esum xs) * esum y
148 |     ~~ (f * epr x) * esum y + esum xs * esum y
149 |       ... r.rightDistributive
150 |     ~~ (f * epr x) * esum y + esum (mult xs y)
151 |       ... cong ((f * epr x) * esum y +) (pmult xs y)
152 |     ~~ esum (mult1 (T f x) y) + esum (mult xs y)
153 |       ..< cong ( + esum (mult xs y)) (pmult1 f x y)
154 |     ~~ esum (add (mult1 (T f x) y) (mult xs y))
155 |       ... padd (mult1 (T f x) y) (mult xs y)
156 |
157 |   -- Removing zero values from a sum of terms does not
158 |   -- affect the evaluation result.
159 |   export
160 |   0 pnormSum : (s : Sum a as) -> esum (normSum s) === esum s
161 |   pnormSum []           = Refl
162 |   pnormSum (T f y :: ys) with (isZ f)
163 |     _ | Nothing   = Calc $
164 |       |~ f * epr y + esum (normSum ys)
165 |       ~~ f * epr y + esum ys ... cong ((f * epr y) +) (pnormSum ys)
166 |
167 |     _ | Just refl = Calc $
168 |       |~ esum (normSum ys)
169 |       ~~ esum ys               ... pnormSum ys
170 |       ~~ z + esum ys           ..< r.plus.leftNeutral
171 |       ~~ z * epr y + esum ys ..< cong (+ esum ys) r.multZeroLeftAbsorbs
172 |       ~~ f * epr y + esum ys ..< cong (\x => x * epr y + esum ys) refl
173 |