0 | module Algebra.Solver.CommutativeMonoid

  2 | import public Algebra.Monoid

  3 | import public Algebra.Solver.Prod

  4 | import Syntax.PreorderReasoning

  6 | %default total

  8 | public export

  9 | times : CommutativeMonoid a => Nat -> a -> a

 10 | times 0     x = neutral

 11 | times (S k) x = x <+> times k x

 13 | public export

 14 | data Expr : (a : Type) -> (as : List a) -> Type where

 15 |   Lit     : (x : a) -> Expr a as

 16 |   Var     : (x : a) -> Elem x as -> Expr a as

 17 |   Neutral : Expr a as

 18 |   Append  : Expr a as -> Expr a as -> Expr a as

 20 | public export

 21 | FromString a => FromString (Expr a as) where

 22 |   fromString = Lit . fromString

 24 | public export

 25 | Semigroup (Expr a as) where

 26 |   (<+>) = Append

 28 | public export

 29 | Monoid (Expr a as) where

 30 |   neutral = Neutral

 36 | public export

 37 | record Term (a : Type) (as : List a) where

 38 |   constructor T

 39 |   factor : a

 40 |   prod   : Prod a as

 42 | public export

 43 | append : CommutativeMonoid a => Term a as -> Term a as -> Term a as

 44 | append (T f1 p1) (T f2 p2) = T (f1 <+> f2) (mult p1 p2)

 46 | public export

 47 | normalize : CommutativeMonoid a => {as : List a} -> Expr a as -> Term a as

 48 | normalize (Lit x)      = T x one

 49 | normalize (Var x y)    = T neutral (fromVar y)

 50 | normalize Neutral      = T neutral one

 51 | normalize (Append x y) = append (normalize x) (normalize y)

 57 | public export

 58 | eval : CommutativeMonoid a => Expr a as -> a

 59 | eval (Lit x)      = x

 60 | eval (Var x y)    = x

 61 | eval Neutral      = neutral

 62 | eval (Append x y) = eval x <+> eval y

 64 | public export

 65 | eprod : CommutativeMonoid a => {as : List a} -> Prod a as -> a

 66 | eprod []                        = neutral

 67 | eprod {as = v :: vs} (exp :: x) = times exp v <+> eprod x

 69 | public export

 70 | eterm : CommutativeMonoid a => {as : List a} -> Term a as -> a

 71 | eterm (T f p) = f <+> eprod p

 77 | 0 p1324 :

 78 |      {auto _ : CommutativeMonoid a}

 79 |   -> {k,l,m,n : a}

 80 |   -> (k <+> l) <+> (m <+> n) === (k <+> m) <+> (l <+> n)

 81 | p1324 = Calc $

 82 |   |~ (k <+> l) <+> (m <+> n)

 83 |   ~~ ((k <+> l) <+> m) <+> n ... appendAssociative

 84 |   ~~ (k <+> (l <+> m)) <+> n ..< cong (<+>n) appendAssociative

 85 |   ~~ (k <+> (m <+> l)) <+> n ... cong (\x => (k <+> x) <+> n) appendCommutative

 86 |   ~~ ((k <+> m) <+> l) <+> n ... cong (<+>n) appendAssociative

 87 |   ~~ (k <+> m) <+> (l <+> n) ..< appendAssociative

 89 | 0 pone :

 90 |      {auto _ : CommutativeMonoid a}

 91 |   -> (as : List a)

 92 |   -> eprod {as} Prod.one === Prelude.neutral

 93 | pone []        = Refl

 94 | pone (v :: vs) = Calc $

 95 |   |~ neutral <+> eprod {as = vs} one

 96 |   ~~ neutral <+> neutral             ... cong (neutral <+>) (pone vs)

 97 |   ~~ neutral                         ... appendLeftNeutral

100 | 0 pvar :

101 |      {auto _ : CommutativeMonoid a}

102 |   -> (as : List a)

103 |   -> (e  : Elem x as)

104 |   -> eprod (fromVar {as} e) === x

105 | pvar (x :: vs) Here      = Calc $

106 |   |~ (x <+> neutral) <+> eprod {as = vs} one

107 |   ~~ (x <+> neutral) <+> neutral ... cong ((x <+> neutral) <+>) (pone vs)

108 |   ~~ x <+> neutral               ... appendRightNeutral

109 |   ~~ x                           ... appendRightNeutral

111 | pvar (v :: vs) (There y) = Calc $

112 |   |~ neutral <+> eprod (fromVar y)

113 |   ~~ eprod (fromVar y)             ... appendLeftNeutral

114 |   ~~ x                             ... pvar vs y

116 | pvar [] Here impossible

117 | pvar [] (There y) impossible

119 | 0 ptimes :

120 |      {auto _ : CommutativeMonoid a}

121 |   -> (m,n : Nat)

122 |   -> (x : a)

123 |   -> times m x <+> times n x === times (m + n) x

124 | ptimes 0     n x = appendLeftNeutral

125 | ptimes (S k) n x = Calc $

126 |   |~ (x <+> times k x) <+> times n x

127 |   ~~ x <+> (times k x <+> times n x) ..< appendAssociative

128 |   ~~ x <+> times (k + n) x           ... cong (x <+>) (ptimes k n x)

131 | 0 ppm :

132 |      {auto _ : CommutativeMonoid a}

133 |   -> (e1,e2 : Prod a as)

134 |   -> eprod e1 <+> eprod e2 === eprod (mult e1 e2)

135 | ppm []        []        = appendRightNeutral

136 | ppm {as = v :: vs} (m :: xs) (n :: ys) = Calc $

137 |   |~ (times m v <+> eprod xs) <+> (times n v <+> eprod ys)

138 |   ~~ (times m v <+> times n v) <+> (eprod xs <+> eprod ys)

139 |      ... p1324

140 |   ~~ (times m v <+> times n v) <+> eprod (mult xs ys)

141 |      ... cong ((times m v <+> times n v) <+>) (ppm xs ys)

142 |   ~~ times (m + n) v <+> eprod (mult xs ys)

143 |      ... cong (<+> eprod (mult xs ys)) (ptimes m n v)

146 | 0 pappend :

147 |      {auto _ : CommutativeMonoid a}

148 |   -> (e1,e2 : Term a as)

149 |   -> eterm e1 <+> eterm e2 === eterm (append e1 e2)

150 | pappend (T f p) (T g q) = Calc $

151 |   |~ (f <+> eprod p) <+> (g <+> eprod q)

152 |   ~~ (f <+> g) <+> (eprod p <+> eprod q) ... p1324

153 |   ~~ (f <+> g) <+> eprod (mult p q)      ... cong ((f <+> g) <+>) (ppm p q)

155 | 0 pnorm :

156 |      {auto _ : CommutativeMonoid a}

157 |   -> (e : Expr a as)

158 |   -> eval e === eterm (normalize e)

159 | pnorm (Lit x) = Calc $

160 |   |~ x

161 |   ~~ x <+> neutral        ..< appendRightNeutral

162 |   ~~ x <+> eprod {as} one ..< cong (x <+>) (pone as)

164 | pnorm (Var x y) = Calc $

165 |  |~ x

166 |  ~~ eprod (fromVar y)             ..< pvar as y

167 |  ~~ neutral <+> eprod (fromVar y) ..< appendLeftNeutral

169 | pnorm Neutral = Calc $

170 |   |~ neutral

171 |   ~~ neutral <+> neutral        ..< appendRightNeutral

172 |   ~~ neutral <+> eprod {as} one ..< cong (neutral <+>) (pone as)

174 | pnorm (Append x y) = Calc $

175 |   |~ eval x <+> eval y

176 |   ~~ eterm (normalize x) <+> eval y

177 |      ... cong (<+> eval y) (pnorm x)

178 |   ~~ eterm (normalize x) <+> eterm (normalize y)

179 |      ... cong (eterm (normalize x) <+>) (pnorm y)

180 |   ~~ eterm (append (normalize x) (normalize y))

181 |      ... pappend (normalize x) (normalize y)

188 | 0 solve :

189 |      {auto _ : CommutativeMonoid a}

190 |   -> (as : List a)

191 |   -> (e1,e2 : Expr a as)

192 |   -> {auto prf : normalize e1 === normalize e2}

193 |   -> eval e1 === eval e2

194 | solve _ e1 e2 = Calc $

195 |   |~ eval e1

196 |   ~~ eterm (normalize e1) ... pnorm e1

197 |   ~~ eterm (normalize e2) ... cong eterm prf

198 |   ~~ eval e2              ..< pnorm e2