
   0 | module Algebra.Solver.Semigroup
   1 | 
   2 | import Syntax.PreorderReasoning
   3 | 
   4 | import public Algebra.Group
   5 | import public Algebra.Solver.Ops
   6 | import public Data.List1
   7 | 
   8 | %default total
   9 | 
  10 | ||| Tree representing an algebraic expression in a semigroup 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 binary operation of the monoid
  30 |   (<+>)   : Expr a as -> Expr a as -> Expr a as
  31 | 
  32 | ||| An `Expr a as` is normalized to a sequence of terms of type
  33 | ||| `List (Term a as)`.
  34 | public export
  35 | data Term : (a : Type) -> (as : List a) -> Type where
  36 |   TLit : (lit : a) -> Term a as
  37 |   TVar : (x : a) -> Elem x as -> Term a as
  38 | 
  39 | --------------------------------------------------------------------------------
  40 | --          Syntax
  41 | --------------------------------------------------------------------------------
  42 | 
  43 | ||| Alias for `var` that uses an auto-implicit proof of `Elem x xs`.
  44 | public export %inline
  45 | var : (x : a) -> {auto p : Elem x xs} -> Expr a xs
  46 | var x = Var x p
  47 | 
  48 | ||| Alias for `var x <+> y`
  49 | public export %inline
  50 | (.+>) : (x : a) -> Expr a xs -> {auto p : Elem x xs} -> Expr a xs
  51 | (.+>) x y = Var x p <+> y
  52 | 
  53 | ||| Alias for `x <+> var y`
  54 | public export %inline
  55 | (<+.) : Expr a xs -> (x : a) -> {auto p : Elem x xs} -> Expr a xs
  56 | (<+.) x y = x <+> Var y p
  57 | 
  58 | ||| Alias for `var x .+. var y`
  59 | public export %inline
  60 | (.+.) :
  61 |      (x,y : a)
  62 |   -> {auto p : Elem x xs}
  63 |   -> {auto q : Elem y xs}
  64 |   -> Expr a xs
  65 | (.+.) x y = Var x p <+> Var y q
  66 | 
  67 | --------------------------------------------------------------------------------
  68 | --          Evaluation
  69 | --------------------------------------------------------------------------------
  70 | 
  71 | ||| Evaluates an expression over the given monoid.
  72 | ||| Note: The idea is to use this function at compile-time to
  73 | |||       convert the expression we evaluate to the corresponding
  74 | |||       Idris expression.
  75 | public export
  76 | eval : {p : a -> a -> a} -> (0 s : Semigroup a p) -> Expr a as -> a
  77 | eval s (Lit lit) = lit
  78 | eval s (Var x _) = x
  79 | eval s (x <+> y) = eval s x `p` eval s y
  80 | 
  81 | ||| Evaluates a single term.
  82 | public export
  83 | eterm : Term a as -> a
  84 | eterm (TLit lit) = lit
  85 | eterm (TVar x y) = x
  86 | 
  87 | ||| Evaluates a list of terms over the given Semigroup.
  88 | public export
  89 | elist :
  90 |      {p : a -> a -> a}
  91 |   -> (0 s : Semigroup a p)
  92 |   -> (t : Term a as)
  93 |   -> List (Term a as)
  94 |   -> a
  95 | elist s v []        = eterm v
  96 | elist s v (x :: xs) = eterm v `p` elist s x xs
  97 | 
  98 | ||| Evaluates a non-empty list of terms over the given Semigroup.
  99 | public export
 100 | elist1 : {p : a -> a -> a} -> (0 s : Semigroup a p) -> List1 (Term a as) -> a
 101 | elist1 s (h ::: t) = elist s h t
 102 | 
 103 | --------------------------------------------------------------------------------
 104 | --          Normalization
 105 | --------------------------------------------------------------------------------
 106 | 
 107 | ||| Flattens an expression into a list of terms
 108 | public export
 109 | flatten : Expr a as -> List1 (Term a as)
 110 | flatten (Lit lit) = TLit lit ::: []
 111 | flatten (Var x y) = TVar x y ::: []
 112 | flatten (x <+> y) = flatten x ++ flatten y
 113 | 
 114 | ||| Prepends a single term in front of a list of terms.
 115 | ||| This will remove terms that evaluate to zero and
 116 | ||| fuse neighbouring literals.
 117 | public export
 118 | prepend :
 119 |      {p   : a -> a -> a}
 120 |   -> (0 s : Semigroup a p)
 121 |   -> List1 (Term a as)
 122 |   -> Term a as
 123 |   -> List1 (Term a as)
 124 | prepend s (TLit x ::: xs) (TLit y) = TLit (y `p` x) ::: xs
 125 | prepend s (x      ::: xs) y        = y ::: x :: xs
 126 | 
 127 | public export
 128 | merge :
 129 |      {p : a -> a -> a}
 130 |   -> (0 s : Semigroup a p)
 131 |   -> (t : Term a as)
 132 |   -> List (Term a as)
 133 |   -> List1 (Term a as)
 134 | merge s t []        = t ::: []
 135 | merge s t (x :: xs) = prepend s (merge s x xs) t
 136 | 
 137 | public export
 138 | merge1 :
 139 |      {p : a -> a -> a}
 140 |   -> (0 s : Semigroup a p)
 141 |   -> List1 (Term a as)
 142 |   -> List1 (Term a as)
 143 | merge1 s (t ::: ts) = merge s t ts
 144 | 
 145 | public export
 146 | normalize : {p : _} -> (0 s : Semigroup a p) -> Expr a as -> List1 (Term a as)
 147 | normalize s e = merge1 s (flatten e)
 148 | 
 149 | --------------------------------------------------------------------------------
 150 | --          Proofs
 151 | --------------------------------------------------------------------------------
 152 | 
 153 | 0 pelist :
 154 |      (s  : Semigroup a p)
 155 |   -> (v  : Term a as)
 156 |   -> (w  : Term a as)
 157 |   -> (vs : List (Term a as))
 158 |   -> (ws : List (Term a as))
 159 |   -> elist s v vs `p` elist s w ws === elist s v (vs ++ w :: ws)
 160 | pelist s v w []        ws = Refl
 161 | pelist s v w (x :: xs) ws = Calc $
 162 |   |~ (eterm v `p` elist s x xs) `p` elist s w ws
 163 |   ~~ eterm v `p` (elist s x xs `p` elist s w ws)
 164 |      ..< s.associative
 165 |   ~~ eterm v `p` elist s x (xs ++ (w :: ws))
 166 |      ... cong (eterm v `p`) (pelist s x w xs ws)
 167 | 
 168 | 0 pelist1 :
 169 |      (s  : Semigroup a p)
 170 |   -> (vs : List1 (Term a as))
 171 |   -> (ws : List1 (Term a as))
 172 |   -> elist1 s vs `p` elist1 s ws === elist1 s (vs ++ ws)
 173 | pelist1 s (v ::: vs) (w ::: ws) = pelist s v w vs ws
 174 | 
 175 | 0 pflatten :
 176 |      (s : Semigroup a p)
 177 |   -> (e : Expr a as)
 178 |   -> eval s e === elist1 s (flatten e)
 179 | pflatten s (Lit lit) = Refl
 180 | pflatten s (Var x y) = Refl
 181 | pflatten s (x <+> y) = Calc $
 182 |   |~ eval s x `p` eval s y
 183 |   ~~ elist1 s (flatten x) `p` eval s y
 184 |      ... cong (`p` eval s y) (pflatten s x)
 185 |   ~~ elist1 s (flatten x) `p` elist1 s (flatten y)
 186 |      ... cong (elist1 s (flatten x) `p`) (pflatten s y)
 187 |   ~~ elist1 s (flatten x ++ flatten y)
 188 |      ... pelist1 s (flatten x) (flatten y)
 189 | 
 190 | 0 pprepend :
 191 |      (s   : Semigroup a p)
 192 |   -> (ts  : List1 (Term a as))
 193 |   -> (t   : Term a as)
 194 |   -> eterm t `p` elist1 s ts === elist1 s (prepend s ts t)
 195 | pprepend s (TLit lit ::: [])      (TLit x)   = Refl
 196 | pprepend s (TLit lit ::: t :: ts) (TLit x)   = s.associative
 197 | pprepend s (TLit lit ::: ts)      (TVar x y) = Refl
 198 | pprepend s (TVar x y ::: ts)      (TLit lit) = Refl
 199 | pprepend s (TVar x y ::: ts)      (TVar z w) = Refl
 200 | 
 201 | 0 pmerge :
 202 |      (s   : Semigroup a p)
 203 |   -> (t   : Term a as)
 204 |   -> (ts  : List (Term a as))
 205 |   -> elist s t ts === elist1 s (merge s t ts)
 206 | pmerge s t []        = Refl
 207 | pmerge s t (x :: xs) = Calc $
 208 |   |~ eterm t `p` elist s x xs
 209 |   ~~ eterm t `p` elist1 s (merge s x xs)
 210 |      ... cong (eterm t `p`) (pmerge s x xs)
 211 |   ~~ elist1 s (prepend s (merge s x xs) t)
 212 |      ... pprepend s (merge s x xs) t
 213 | 
 214 | 0 pmerge1 :
 215 |      (s   : Semigroup a p)
 216 |   -> (ts  : List1 (Term a as))
 217 |   -> elist1 s ts === elist1 s (merge1 s ts)
 218 | pmerge1 s (t ::: ts) = pmerge s t ts
 219 | 
 220 | 0 pnormalize :
 221 |      (s   : Semigroup a p)
 222 |   -> (e   : Expr a as)
 223 |   -> eval s e === elist1 s (normalize s e)
 224 | pnormalize s e = Calc $
 225 |   |~ eval s e
 226 |   ~~ elist1 s (flatten e)            ... pflatten s e
 227 |   ~~ elist1 s (merge1 s $ flatten e) ... pmerge1 s (flatten e)
 228 | 
 229 | --------------------------------------------------------------------------------
 230 | --          Solver
 231 | --------------------------------------------------------------------------------
 232 | 
 233 | export
 234 | 0 solve :
 235 |      (s     : Semigroup a p)
 236 |   -> (e1,e2 : Expr a as)
 237 |   -> {auto prf : normalize s e1 === normalize s e2}
 238 |   -> eval s e1 === eval s e2
 239 | solve s e1 e2 = Calc $
 240 |   |~ eval s e1
 241 |   ~~ elist1 s (normalize s e1) ... pnormalize s e1
 242 |   ~~ elist1 s (normalize s e2) ... cong (elist1 s) prf
 243 |   ~~ eval s e2                 ..< pnormalize s e2
 244 |