0 | module Algebra.Solver.Monoid
 1 |
 2 | import Algebra.Monoid
 3 | import Syntax.PreorderReasoning
 4 |
 5 | %default total
 6 |
 7 | public export
 8 | data Expr : (a : Type) -> Type where
 9 |   Var     : (x : a) -> Expr a
10 |   Neutral : Expr a
11 |   Append  : Expr a -> Expr a -> Expr a
12 |
13 | public export
14 | Semigroup (Expr a) where
15 |   (<+>) = Append
16 |
17 | public export
18 | Monoid (Expr a) where
19 |   neutral = Neutral
20 |
21 | public export
22 | eval : LMonoid a => Expr a -> a
23 | eval (Var x)      = x
24 | eval Neutral      = neutral
25 | eval (Append x y) = eval x <+> eval y
26 |
27 | --------------------------------------------------------------------------------
28 | --          Sum
29 | --------------------------------------------------------------------------------
30 |
31 | public export
32 | esum : LMonoid a => List a -> a
33 | esum []       = neutral
34 | esum (h :: t) = h <+> esum t
35 |
36 | public export
37 | normalize : Expr a -> List a
38 | normalize (Var x)      = x :: []
39 | normalize Neutral      = []
40 | normalize (Append x y) = normalize x ++ normalize y
41 |
42 | --------------------------------------------------------------------------------
43 | --          Proofs
44 | --------------------------------------------------------------------------------
45 |
46 | 0 psum :
47 |      {auto _ : LMonoid a}
48 |   -> (xs,ys : List a)
49 |   -> esum (xs ++ ys) === esum xs <+> esum ys
50 | psum []        ys = sym appendLeftNeutral
51 | psum (x :: xs) ys = Calc $
52 |   |~ x <+> esum (xs ++ ys)
53 |   ~~ x <+> (esum xs <+> esum ys) ... cong (x <+>) (psum xs ys)
54 |   ~~ (x <+> esum xs) <+> esum ys ... appendAssociative
55 |
56 |
57 | 0 pnorm : LMonoid a => (e : Expr a) -> eval e === esum (normalize e)
58 | pnorm (Var x)      = sym appendRightNeutral
59 | pnorm Neutral      = Refl
60 | pnorm (Append x y) = Calc $
61 |   |~ eval x <+> eval y
62 |   ~~ esum (normalize x) <+> eval y
63 |      ... cong (<+> eval y) (pnorm x)
64 |   ~~ esum (normalize x) <+> esum (normalize y)
65 |      ... cong (esum (normalize x) <+>) (pnorm y)
66 |   ~~ esum (normalize x ++ normalize y)
67 |      ..< psum (normalize x) (normalize y)
68 |
69 | --------------------------------------------------------------------------------
70 | --          Solver
71 | --------------------------------------------------------------------------------
72 |
73 | export
74 | 0 solve :
75 |      {auto _ : LMonoid a}
76 |   -> (e1,e2 : Expr a)
77 |   -> {auto prf : normalize e1 === normalize e2}
78 |   -> eval e1 === eval e2
79 | solve e1 e2 = Calc $
80 |   |~ eval e1
81 |   ~~ esum (normalize e1) ... pnorm e1
82 |   ~~ esum (normalize e2) ... cong esum prf
83 |   ~~ eval e2             ..< pnorm e2
84 |
85 | --------------------------------------------------------------------------------
86 | --          Example
87 | --------------------------------------------------------------------------------
88 |
89 | 0 solverExample : {x,y,z : String}
90 |                 -> x ++ ((y ++ "") ++ z) === ("" ++ x) ++ (y ++ z)
91 | solverExample =
92 |   solve
93 |     (Var x <+> ((Var y <+> Neutral) <+> Var z))
94 |     ((Neutral <+> Var x) <+> (Var y <+> Var z))
95 |