
   0 | module Algebra.Solver.Monoid
   1 | 
   2 | import Syntax.PreorderReasoning
   3 | 
   4 | import public Algebra.Group
   5 | import public Algebra.Solver.Ops
   6 | import public Data.List.Elem
   7 | 
   8 | %default total
   9 | 
  10 | ||| Tree representing an algebraic expression in a monoid structure.
  11 | |||
  12 | ||| The idea here is to represent algebraic expressions as an `Expr a as`,
  13 | ||| where `a` is the type we operate on and `as` is a list of known
  14 | ||| variables. Such an `Expr a as` can then be normalized using function
  15 | ||| `normalize`. We proof in this module, that the result of evaluating an
  16 | ||| expression is not affected by normalization. Hence, if two expressions
  17 | ||| `e1` and `e2` have the same normalized representation, the results
  18 | ||| of evaluating the two (`eval e1` and `eval e2`) are propositionally
  19 | ||| equal. This is, what function `solve` is used for.
  20 | public export
  21 | data Expr : (a : Type) -> (as : List a) -> Type where
  22 |   ||| A literal value known at compile time. Use this if you want
  23 |   ||| values known at runtime to unify.
  24 |   Lit     : (lit : a) -> Expr a as
  25 | 
  26 |   ||| A variable from the given list of variables.
  27 |   Var     : (x : a) -> Elem x as -> Expr a as
  28 | 
  29 |   ||| Represents the neutral element of the monoid
  30 |   Neutral : Expr a as
  31 | 
  32 |   ||| Represents the binary operation of the monoid
  33 |   (<+>)   : Expr a as -> Expr a as -> Expr a as
  34 | 
  35 | ||| An `Expr a as` is normalized to a sequence of terms of type
  36 | ||| `List (Term a as)`.
  37 | public export
  38 | data Term : (a : Type) -> (as : List a) -> Type where
  39 |   TLit : (lit : a) -> Term a as
  40 |   TVar : (x : a) -> Elem x as -> Term a as
  41 | 
  42 | --------------------------------------------------------------------------------
  43 | --          Syntax
  44 | --------------------------------------------------------------------------------
  45 | 
  46 | ||| Alias for `var` that uses an auto-implicit proof of `Elem x xs`.
  47 | public export %inline
  48 | var : (x : a) -> {auto p : Elem x xs} -> Expr a xs
  49 | var x = Var x p
  50 | 
  51 | ||| Alias for `var x <+> y`
  52 | public export %inline
  53 | (.+>) : (x : a) -> Expr a xs -> {auto p : Elem x xs} -> Expr a xs
  54 | (.+>) x y = Var x p <+> y
  55 | 
  56 | ||| Alias for `x <+> var y`
  57 | public export %inline
  58 | (<+.) : Expr a xs -> (x : a) -> {auto p : Elem x xs} -> Expr a xs
  59 | (<+.) x y = x <+> Var y p
  60 | 
  61 | ||| Alias for `var x .+. var y`
  62 | public export %inline
  63 | (.+.) :
  64 |      (x,y : a)
  65 |   -> {auto p : Elem x xs}
  66 |   -> {auto q : Elem y xs}
  67 |   -> Expr a xs
  68 | (.+.) x y = Var x p <+> Var y q
  69 | 
  70 | --------------------------------------------------------------------------------
  71 | --          Evaluation
  72 | --------------------------------------------------------------------------------
  73 | 
  74 | ||| Evaluates an expression over the given monoid.
  75 | ||| Note: The idea is to use this function at compile-time to
  76 | |||       convert the expression we evaluate to the corresponding
  77 | |||       Idris expression.
  78 | public export
  79 | eval :
  80 |      {z : a}
  81 |   -> {p : a -> a -> a}
  82 |   -> (0 m : Monoid a z p)
  83 |   -> Expr a as
  84 |   -> a
  85 | eval m (Lit lit) = lit
  86 | eval m (Var x _) = x
  87 | eval m Neutral   = z
  88 | eval m (x <+> y) = eval m x `p` eval m y
  89 | 
  90 | ||| Evaluates a single term.
  91 | public export
  92 | eterm : Term a as -> a
  93 | eterm (TLit lit) = lit
  94 | eterm (TVar x y) = x
  95 | 
  96 | ||| Evaluates a list of terms over the given monoid.
  97 | public export
  98 | elist :
  99 |      {z : a}
 100 |   -> {p : a -> a -> a}
 101 |   -> (0 m : Monoid a z p)
 102 |   -> List (Term a as)
 103 |   -> a
 104 | elist m []        = z
 105 | elist m (x :: xs) = eterm x `p` elist m xs
 106 | 
 107 | --------------------------------------------------------------------------------
 108 | --          Normalization
 109 | --------------------------------------------------------------------------------
 110 | 
 111 | ||| Flattens an expression into a list of terms
 112 | public export
 113 | flatten : Expr a as -> List (Term a as)
 114 | flatten (Lit lit) = [TLit lit]
 115 | flatten (Var x y) = [TVar x y]
 116 | flatten Neutral   = []
 117 | flatten (x <+> y) = flatten x ++ flatten y
 118 | 
 119 | ||| Tries to fuse two neighbouring terms
 120 | public export
 121 | fuse :
 122 |      {z   : a}
 123 |   -> {p   : a -> a -> a}
 124 |   -> (0 m : Monoid a z p)
 125 |   -> (isZ : (v : a) -> Maybe (v === z))
 126 |   -> Term a as -> Term a as -> List (Term a as)
 127 | fuse m isZ (TLit lit) (TLit x) = case isZ (lit `p` x) of
 128 |   Just _  => []
 129 |   Nothing => [TLit $ lit `p` x]
 130 | fuse m isZ (TLit lit) t        = case isZ lit of
 131 |   Just _  => [t]
 132 |   Nothing => [TLit lit, t]
 133 | fuse m isZ x          y        = [x,y]
 134 | 
 135 | ||| Prepends a single term in front of a list of terms.
 136 | ||| This will remove terms that evaluate to zero and
 137 | ||| fuse neighbouring literals.
 138 | public export
 139 | prepend :
 140 |      {z   : a}
 141 |   -> {p   : a -> a -> a}
 142 |   -> (0 m : Monoid a z p)
 143 |   -> (isZ : (v : a) -> Maybe (v === z))
 144 |   -> List (Term a as)
 145 |   -> Term a as
 146 |   -> List (Term a as)
 147 | prepend m isZ [] (TVar x p) = [TVar x p]
 148 | prepend m isZ [] (TLit x)   = case isZ x of
 149 |   Just p  => []
 150 |   Nothing => [TLit x]
 151 | prepend m isZ (x :: xs) t = fuse m isZ t x ++ xs
 152 | 
 153 | public export
 154 | merge :
 155 |      {z : a}
 156 |   -> {p : a -> a -> a}
 157 |   -> (0 m : Monoid a z p)
 158 |   -> (isZ : (v : a) -> Maybe (v === z))
 159 |   -> List (Term a as)
 160 |   -> List (Term a as)
 161 | merge m isZ []        = []
 162 | merge m isZ (x :: xs) = prepend m isZ (merge m isZ xs) x
 163 | 
 164 | public export
 165 | normalize :
 166 |      {z   : a}
 167 |   -> {p   : a -> a -> a}
 168 |   -> (0 m : Monoid a z p)
 169 |   -> (isZ : (v : a) -> Maybe (v === z))
 170 |   -> Expr a as
 171 |   -> List (Term a as)
 172 | normalize m isZ e = merge m isZ (flatten e)
 173 | 
 174 | --------------------------------------------------------------------------------
 175 | --          Proofs
 176 | --------------------------------------------------------------------------------
 177 | 
 178 | 0 pelist :
 179 |      (m : Monoid a z p)
 180 |   -> (vs,ws : List (Term a as))
 181 |   -> elist m vs `p` elist m ws === elist m (vs ++ ws)
 182 | pelist m []        ws = m.leftNeutral
 183 | pelist m (v :: vs) ws = Calc $
 184 |   |~ (eterm v `p` elist m vs) `p` elist m ws
 185 |   ~~ eterm v `p` (elist m vs `p` elist m ws)
 186 |      ..< m.associative
 187 |   ~~ eterm v `p` elist m (vs ++ ws)
 188 |      ... cong (eterm v `p`) (pelist m vs ws)
 189 | 
 190 | 0 pflatten :
 191 |      (m : Monoid a z p)
 192 |   -> (e : Expr a as)
 193 |   -> eval m e === elist m (flatten e)
 194 | pflatten m (Lit lit) = sym m.rightNeutral
 195 | pflatten m (Var x y) = sym m.rightNeutral
 196 | pflatten m Neutral   = Refl
 197 | pflatten m (x <+> y) = Calc $
 198 |   |~ eval m x `p` eval m y
 199 |   ~~ elist m (flatten x) `p` eval m y
 200 |      ... cong (`p` eval m y) (pflatten m x)
 201 |   ~~ elist m (flatten x) `p` elist m (flatten y)
 202 |      ... cong (elist m (flatten x) `p`) (pflatten m y)
 203 |   ~~ elist m (flatten x ++ flatten y)
 204 |      ... pelist m (flatten x) (flatten y)
 205 | 
 206 | 0 pfuse :
 207 |      (m : Monoid a z p)
 208 |   -> (isZ : (v : a) -> Maybe (v === z))
 209 |   -> (t1,t2 : Term a as)
 210 |   -> eterm t1 `p` eterm t2 === elist m (fuse m isZ t1 t2)
 211 | pfuse m isZ (TLit lit) (TLit x) with (isZ $ lit `p` x)
 212 |   pfuse m isZ (TLit lit) (TLit x) | Just prf = prf
 213 |   pfuse m isZ (TLit lit) (TLit x) | Nothing  = sym $ m.rightNeutral
 214 | 
 215 | pfuse m isZ (TLit lit) (TVar x y) with (isZ lit)
 216 |   pfuse m isZ (TLit lit) (TVar x y) | Just prf = Calc $
 217 |     |~ lit `p` x
 218 |     ~~ z `p` x ... cong (`p` x) prf
 219 |     ~~ x       ... m.leftNeutral
 220 |     ~~ x `p` z ..< m.rightNeutral
 221 |   pfuse m isZ (TLit lit) (TVar x y) | Nothing  =
 222 |     cong (lit `p`) $ sym m.rightNeutral
 223 | 
 224 | pfuse m isZ (TVar x y) (TLit lit) = cong (x `p`) $ sym m.rightNeutral
 225 | pfuse m isZ (TVar x y) (TVar w v) = cong (x `p`) $ sym m.rightNeutral
 226 | 
 227 | 0 pprepend :
 228 |      (m   : Monoid a z p)
 229 |   -> (isZ : (v : a) -> Maybe (v === z))
 230 |   -> (ts  : List (Term a as))
 231 |   -> (t   : Term a as)
 232 |   -> eterm t `p` elist m ts === elist m (prepend m isZ ts t)
 233 | pprepend m isZ [] (TVar x y) = Refl
 234 | pprepend m isZ [] (TLit lit) with (isZ lit)
 235 |   pprepend m isZ [] (TLit lit) | Nothing  = Refl
 236 |   pprepend m isZ [] (TLit lit) | Just prf = Calc $
 237 |     |~ lit `p` z
 238 |     ~~ z `p` z   ... cong (`p` z) prf
 239 |     ~~ z         ... m.leftNeutral
 240 | pprepend m isZ (x :: xs) t = Calc $
 241 |   |~ eterm t `p` (eterm x `p` elist m xs)
 242 |   ~~ (eterm t `p` eterm x) `p` elist m xs
 243 |      ... m.associative
 244 |   ~~ elist m (fuse m isZ t x) `p` elist m xs
 245 |      ... cong (`p` elist m xs) (pfuse m isZ t x)
 246 |   ~~ elist m (fuse m isZ t x ++ xs)
 247 |      ... pelist m (fuse m isZ t x) xs
 248 | 
 249 | 0 pmerge :
 250 |      (m   : Monoid a z p)
 251 |   -> (isZ : (v : a) -> Maybe (v === z))
 252 |   -> (ts  : List (Term a as))
 253 |   -> elist m ts === elist m (merge m isZ ts)
 254 | pmerge m isZ []        = Refl
 255 | pmerge m isZ (x :: xs) = Calc $
 256 |    |~ eterm x `p` elist m xs
 257 |    ~~ eterm x `p` elist m (merge m isZ xs)
 258 |       ... cong (eterm x `p`) (pmerge m isZ xs)
 259 |    ~~ elist m (prepend m isZ (merge m isZ xs) x)
 260 |       ... pprepend m isZ (merge m isZ xs) x
 261 | 
 262 | 0 pnormalize :
 263 |      (m   : Monoid a z p)
 264 |   -> (isZ : (x : a) -> Maybe (x === z))
 265 |   -> (e   : Expr a as)
 266 |   -> eval m e === elist m (normalize m isZ e)
 267 | pnormalize m isZ e = Calc $
 268 |   |~ eval m e
 269 |   ~~ elist m (flatten e)               ... pflatten m e
 270 |   ~~ elist m (merge m isZ $ flatten e) ... pmerge m isZ (flatten e)
 271 | 
 272 | --------------------------------------------------------------------------------
 273 | --          Solver
 274 | --------------------------------------------------------------------------------
 275 | 
 276 | export
 277 | 0 solve :
 278 |      (m     : Monoid a z p)
 279 |   -> (isZ   : (x : a) -> Maybe (x === z))
 280 |   -> (e1,e2 : Expr a as)
 281 |   -> {auto prf : normalize m isZ e1 === normalize m isZ e2}
 282 |   -> eval m e1 === eval m e2
 283 | solve m isZ e1 e2 = Calc $
 284 |   |~ eval m e1
 285 |   ~~ elist m (normalize m isZ e1) ... pnormalize m isZ e1
 286 |   ~~ elist m (normalize m isZ e2) ... cong (elist m) prf
 287 |   ~~ eval m e2                    ..< pnormalize m isZ e2
 288 |