0 | module Algebra.Solver.Group

  2 | import Syntax.PreorderReasoning

  4 | import public Algebra.Group

  5 | import public Algebra.Solver.Ops

  6 | import public Data.List.Elem

  8 | %default total

 10 | public export

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

 12 |   Lit     : (lit : a) -> Expr a as

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

 14 |   Neutral : Expr a as

 15 |   Neg     : Expr a as -> Expr a as

 16 |   (<+>)   : Expr a as -> Expr a as -> Expr a as

 18 | public export

 19 | data Term : (a : Type) -> (as : List a) -> Type where

 20 |   TLit : (lit : a) -> Term a as

 21 |   TVar : (x : a) -> Elem x as -> Term a as

 22 |   TNeg : (x : a) -> Elem x as -> Term a as

 28 | public export %inline

 29 | (.+>) : (x : a) -> Expr a xs -> {auto p : Elem x xs} -> Expr a xs

 30 | (.+>) x y = Var x p <+> y

 32 | public export %inline

 33 | (<+.) : Expr a xs -> (x : a) -> {auto p : Elem x xs} -> Expr a xs

 34 | (<+.) x y = x <+> Var y p

 36 | public export %inline

 37 | (.+.) :

 38 |      (x,y : a)

 39 |   -> {auto p : Elem x xs}

 40 |   -> {auto q : Elem y xs}

 41 |   -> Expr a xs

 42 | (.+.) x y = Var x p <+> Var y q

 44 | public export %inline

 45 | var : (x : a) -> {auto p : Elem x xs} -> Expr a xs

 46 | var x = Var x p

 48 | public export %inline

 49 | neg : (x : a) -> {auto p : Elem x xs} -> Expr a xs

 50 | neg x = Neg $ var x

 60 | public export

 61 | eval :

 62 |      {z : a}

 63 |   -> {i : a -> a}

 64 |   -> {p : a -> a -> a}

 65 |   -> (0 g : Group a z i p)

 66 |   -> Expr a as

 67 |   -> a

 68 | eval g (Lit lit) = lit

 69 | eval g (Var x _) = x

 70 | eval g Neutral   = z

 71 | eval g (Neg x)   = i (eval g x)

 72 | eval g (x <+> y) = eval g x `p` eval g y

 75 | public export

 76 | eterm : (i : a -> a) -> Term a as -> a

 77 | eterm i (TLit lit) = lit

 78 | eterm i (TVar x y) = x

 79 | eterm i (TNeg x y) = i x

 82 | public export

 83 | elist :

 84 |      {z : a}

 85 |   -> {i : a -> a}

 86 |   -> {p : a -> a -> a}

 87 |   -> (0 g : Group a z i p)

 88 |   -> List (Term a as)

 89 |   -> a

 90 | elist g []        = z

 91 | elist g (x :: xs) = eterm i x `p` elist g xs

 98 | public export

 99 | negSng : (i : a -> a) -> Term a as -> Term a as

100 | negSng i (TLit lit) = TLit $ i lit

101 | negSng i (TVar x y) = TNeg x y

102 | negSng i (TNeg x y) = TVar x y

108 | public export

109 | negate : (i : a -> a) -> List (Term a as) -> List (Term a as) -> List (Term a as)

110 | negate i xs []        = xs

111 | negate i xs (y :: ys) = negate i (negSng i y :: xs) ys

115 | public export

116 | flatten : (i : a -> a) -> Expr a as -> List (Term a as)

117 | flatten _ (Lit lit) = [TLit lit]

118 | flatten _ (Var x y) = [TVar x y]

119 | flatten _ Neutral   = []

120 | flatten i (Neg x)   = negate i [] (flatten i x)

121 | flatten i (x <+> y) = flatten i x ++ flatten i y

124 | public export

125 | fuse :

126 |      {z   : a}

127 |   -> {i   : a -> a}

128 |   -> {p   : a -> a -> a}

129 |   -> (0 g : Group a z i p)

130 |   -> (isZ : (v : a) -> Maybe (v === z))

131 |   -> Term a as

132 |   -> Term a as

133 |   -> List (Term a as)

134 | fuse g isZ (TLit lit) (TLit x) = case isZ (lit `p` x) of

135 |   Just _  => []

136 |   Nothing => [TLit $ lit `p` x]

137 | fuse g isZ (TLit lit) t        = case isZ lit of

138 |   Just _  => [t]

139 |   Nothing => [TLit lit, t]

140 | fuse g isZ (TVar x w) (TNeg y v) = case eqElem w v of

141 |   Just prf => []

142 |   Nothing  => [TVar x w, TNeg y v]

143 | fuse g isZ (TVar x w) t          = [TVar x w, t]

144 | fuse g isZ (TNeg x w) (TVar y v) = case eqElem w v of

145 |   Just prf => []

146 |   Nothing  => [TNeg x w, TVar y v]

147 | fuse g isZ (TNeg x w) t          = [TNeg x w, t]

152 | public export

153 | prepend :

154 |      {z   : a}

155 |   -> {i   : a -> a}

156 |   -> {p   : a -> a -> a}

157 |   -> (0 g : Group a z i p)

158 |   -> (isZ : (v : a) -> Maybe (v === z))

159 |   -> List (Term a as)

160 |   -> Term a as

161 |   -> List (Term a as)

162 | prepend g isZ []       (TLit x) = case isZ x of

163 |   Just p  => []

164 |   Nothing => [TLit x]

165 | prepend g isZ []        t       = [t]

166 | prepend g isZ (x :: xs) t       = fuse g isZ t x ++ xs

168 | public export

169 | merge :

170 |      {z : a}

171 |   -> {i : a -> a}

172 |   -> {p : a -> a -> a}

173 |   -> (0 g : Group a z i p)

174 |   -> (isZ : (v : a) -> Maybe (v === z))

175 |   -> List (Term a as)

176 |   -> List (Term a as)

177 | merge g isZ []        = []

178 | merge g isZ (x :: xs) = prepend g isZ (merge g isZ xs) x

180 | public export

181 | normalize :

182 |      {z   : a}

183 |   -> {i   : a -> a}

184 |   -> {p   : a -> a -> a}

185 |   -> (0 g : Group a z i p)

186 |   -> (isZ : (v : a) -> Maybe (v === z))

187 |   -> Expr a as

188 |   -> List (Term a as)

189 | normalize g isZ e = merge g isZ (flatten i e)

195 | 0 pnegSng :

196 |      Group a z i p

197 |   -> (s : Term a as)

198 |   -> i (eterm i s) === eterm i (negSng i s)

199 | pnegSng g (TLit lit) = Refl

200 | pnegSng g (TVar x y) = Refl

201 | pnegSng g (TNeg x y) = inverseInvolutory g

203 | 0 pnegate' :

204 |      (g  : Group a z i p)

205 |   -> (vs : List (Term a as))

206 |   -> (ws : List (Term a as))

207 |   -> i (elist g ws) `p` elist g vs === elist g (negate i vs ws)

208 | pnegate' g vs []        = Calc $

209 |   |~ p (i z) (elist g vs)

210 |   ~~ p z     (elist g vs) ... cong (`p` elist g vs) (inverseZero g)

211 |   ~~ elist g vs           ... g.leftNeutral

212 | pnegate' g vs (w :: ws) = Calc $

213 |   |~ i (eterm i w `p` elist g ws) `p` elist g vs

214 |   ~~ (i (elist g ws) `p` (i (eterm i w)) `p` elist g vs)

215 |      ... cong ( `p` elist g vs) (invertProduct g)

216 |   ~~ i (elist g ws) `p` (i (eterm i w) `p` elist g vs)

217 |      ..< g.associative

218 |   ~~ i (elist g ws) `p` (eterm i (negSng i w) `p` elist g vs)

219 |      ... cong (\v => i (elist g ws) `p` (v `p` elist g vs)) (pnegSng g w)

220 |   ~~ i (elist g ws) `p` elist g (negSng i w :: vs)

221 |      ... cong (i (elist g ws) `p`) Refl

222 |   ~~ elist g (negate i (negSng i w :: vs) ws)

223 |      ... pnegate' g (negSng i w :: vs) ws

225 | 0 pnegate :

226 |      (g  : Group a z i p)

227 |   -> (ws : List (Term a as))

228 |   -> i (elist g ws) === elist g (negate i [] ws)

229 | pnegate g ws = Calc $

230 |   |~ i (elist g ws)

231 |   ~~ i (elist g ws) `p` z               ..< g.rightNeutral

232 |   ~~ i (elist g ws) `p` elist {as} g [] ... Refl

233 |   ~~ elist g (negate i [] ws)           ... pnegate' g [] ws

235 | 0 pelist :

236 |      (g : Group a z i p)

237 |   -> (vs,ws : List (Term a as))

238 |   -> elist g vs `p` elist g ws === elist g (vs ++ ws)

239 | pelist g []        ws = g.leftNeutral

240 | pelist g (v :: vs) ws = Calc $

241 |   |~ (eterm i v `p` elist g vs) `p` elist g ws

242 |   ~~ eterm i v `p` (elist g vs `p` elist g ws)

243 |      ..< g.associative

244 |   ~~ eterm i v `p` elist g (vs ++ ws)

245 |      ... cong (eterm i v `p`) (pelist g vs ws)

247 | 0 pflatten :

248 |      (g : Group a z i p)

249 |   -> (e : Expr a as)

250 |   -> eval g e === elist g (flatten i e)

251 | pflatten g (Lit lit) = sym g.rightNeutral

252 | pflatten g (Var x y) = sym g.rightNeutral

253 | pflatten g Neutral   = Refl

254 | pflatten g (Neg x)   = Calc $

255 |   |~ i (eval g x)

256 |   ~~ i (elist g (flatten i x))           ... cong i (pflatten g x)

257 |   ~~ elist g (negate i [] (flatten i x)) ... pnegate g (flatten i x)

258 | pflatten g (x <+> y) = Calc $

259 |   |~ eval g x `p` eval g y

260 |   ~~ elist g (flatten i x) `p` eval g y

261 |      ... cong (`p` eval g y) (pflatten g x)

262 |   ~~ elist g (flatten i x) `p` elist g (flatten i y)

263 |      ... cong (elist g (flatten i x) `p`) (pflatten g y)

264 |   ~~ elist g (flatten i x ++ flatten i y)

265 |      ... pelist g (flatten i x) (flatten i y)

267 | 0 lemma : (g : Group a z i p) -> {x,y : a} -> x `p` y === x `p` (y `p` z)

268 | lemma g = cong (x `p`) $ sym g.rightNeutral

270 | 0 pfuse :

271 |      (g : Group a z i p)

272 |   -> (isZ : (v : a) -> Maybe (v === z))

273 |   -> (t1,t2 : Term a as)

274 |   -> eterm i t1 `p` eterm i t2 === elist g (fuse g isZ t1 t2)

275 | pfuse g isZ (TLit lit) (TLit x)   with (isZ $ lit `p` x)

276 |   pfuse g isZ (TLit lit) (TLit x) | Just prf   = prf

277 |   pfuse g isZ (TLit lit) (TLit x) | Nothing    = sym $ g.rightNeutral

278 | pfuse g isZ (TLit lit) (TVar x y) with (isZ lit)

279 |   pfuse g isZ (TLit lit) (TVar x y) | Just prf = Calc $

280 |     |~ lit `p` x

281 |     ~~ z `p` x ... cong (`p` x) prf

282 |     ~~ x       ... g.leftNeutral

283 |     ~~ x `p` z ..< g.rightNeutral

284 |   pfuse g isZ (TLit lit) (TVar x y) | Nothing = lemma g

285 | pfuse g isZ (TLit lit) (TNeg x y) with (isZ lit)

286 |   pfuse g isZ (TLit lit) (TNeg x y) | Just prf = Calc $

287 |     |~ lit `p` i x

288 |     ~~ z `p` i x ... cong (`p` i x) prf

289 |     ~~ i x       ... g.leftNeutral

290 |     ~~ i x `p` z ..< g.rightNeutral

291 |   pfuse g isZ (TLit lit) (TNeg x y) | Nothing = lemma g

293 | pfuse g isZ (TVar x y) (TNeg w v) with (eqElem y v)

294 |   pfuse g isZ (TVar x y) (TNeg x y) | Just Refl = g.rightInverse

295 |   pfuse g isZ (TVar x y) (TNeg w v) | Nothing   = lemma g

296 | pfuse g isZ (TVar x y) (TLit lit) = lemma g

297 | pfuse g isZ (TVar x y) (TVar w v) = lemma g

299 | pfuse g isZ (TNeg x y) (TVar w v) with (eqElem y v)

300 |   pfuse g isZ (TNeg x y) (TVar x y) | Just Refl = g.leftInverse

301 |   pfuse g isZ (TNeg x y) (TVar w v) | Nothing = lemma g

302 | pfuse g isZ (TNeg x y) (TNeg w v) = lemma g

303 | pfuse g isZ (TNeg x y) (TLit lit) = lemma g

305 | 0 pprepend :

306 |      (g   : Group a z i p)

307 |   -> (isZ : (v : a) -> Maybe (v === z))

308 |   -> (ts  : List (Term a as))

309 |   -> (t   : Term a as)

310 |   -> eterm i t `p` elist g ts === elist g (prepend g isZ ts t)

311 | pprepend g isZ [] (TVar x y) = Refl

312 | pprepend g isZ [] (TNeg x y) = Refl

313 | pprepend g isZ [] (TLit lit) with (isZ lit)

314 |   pprepend g isZ [] (TLit lit) | Nothing  = Refl

315 |   pprepend g isZ [] (TLit lit) | Just prf = Calc $

316 |     |~ lit `p` z

317 |     ~~ z `p` z   ... cong (`p` z) prf

318 |     ~~ z         ... g.leftNeutral

319 | pprepend g isZ (x :: xs) t = Calc $

320 |   |~ eterm i t `p` (eterm i x `p` elist g xs)

321 |   ~~ (eterm i t `p` eterm i x) `p` elist g xs

322 |      ... g.associative

323 |   ~~ elist g (fuse g isZ t x) `p` elist g xs

324 |      ... cong (`p` elist g xs) (pfuse g isZ t x)

325 |   ~~ elist g (fuse g isZ t x ++ xs)

326 |      ... pelist g (fuse g isZ t x) xs

328 | 0 pmerge :

329 |      (g   : Group a z i p)

330 |   -> (isZ : (v : a) -> Maybe (v === z))

331 |   -> (ts  : List (Term a as))

332 |   -> elist g ts === elist g (merge g isZ ts)

333 | pmerge g isZ []        = Refl

334 | pmerge g isZ (x :: xs) = Calc $

335 |    |~ eterm i x `p` elist g xs

336 |    ~~ eterm i x `p` elist g (merge g isZ xs)

337 |       ... cong (eterm i x `p`) (pmerge g isZ xs)

338 |    ~~ elist g (prepend g isZ (merge g isZ xs) x)

339 |       ... pprepend g isZ (merge g isZ xs) x

341 | 0 pnormalize :

342 |      (g   : Group a z i p)

343 |   -> (isZ : (x : a) -> Maybe (x === z))

344 |   -> (e   : Expr a as)

345 |   -> eval g e === elist g (normalize g isZ e)

346 | pnormalize g isZ e = Calc $

347 |   |~ eval g e

348 |   ~~ elist g (flatten i e)               ... pflatten g e

349 |   ~~ elist g (merge g isZ $ flatten i e) ... pmerge g isZ (flatten i e)

356 | 0 solve :

357 |      (g     : Group a z i p)

358 |   -> (isZ   : (x : a) -> Maybe (x === z))

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

360 |   -> {auto prf : normalize g isZ e1 === normalize g isZ e2}

361 |   -> eval g e1 === eval g e2

362 | solve g isZ e1 e2 = Calc $

363 |   |~ eval g e1

364 |   ~~ elist g (normalize g isZ e1) ... pnormalize g isZ e1

365 |   ~~ elist g (normalize g isZ e2) ... cong (elist g) prf

366 |   ~~ eval g e2                    ..< pnormalize g isZ e2