0 | module Algebra.Solver.Semigroup
 1 |
 2 | import Algebra.Semigroup
 3 | import Data.List1
 4 | import Syntax.PreorderReasoning
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | data Expr : (a : Type) -> Type where
10 |   Var    : (x : a) -> 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 | eval : LSemigroup a => Expr a -> a
19 | eval (Var x)    = x
20 | eval (Append x y) = eval x <+> eval y
21 |
22 | --------------------------------------------------------------------------------
23 | --          Sum
24 | --------------------------------------------------------------------------------
25 |
26 | public export
27 | esum' : LSemigroup a => a -> List a -> a
28 | esum' v []       = v
29 | esum' v (h :: t) = v <+> esum' h t
30 |
31 | public export
32 | esum : LSemigroup a => List1 a -> a
33 | esum (v ::: vs) = esum' v vs
34 |
35 | public export
36 | normalize : Expr a -> List1 a
37 | normalize (Var x)      = x ::: []
38 | normalize (Append x y) = normalize x ++ normalize y
39 |
40 | --------------------------------------------------------------------------------
41 | --          Proofs
42 | --------------------------------------------------------------------------------
43 |
44 | 0 psum' :
45 |      {auto _ : LSemigroup a}
46 |   -> (x,y   : a)
47 |   -> (xs,ys : List a)
48 |   -> esum' x (xs ++ (y :: ys)) === esum' x xs <+> esum' y ys
49 | psum' x y []        ys = Refl
50 | psum' x y (v :: vs) ys = Calc $
51 |   |~ x <+> esum' v (vs ++ (y :: ys))
52 |   ~~ x <+> (esum' v vs <+> esum' y ys) ... cong (x <+>) (psum' v y vs ys)
53 |   ~~ (x <+> esum' v vs) <+> esum' y ys ... appendAssociative
54 |
55 | 0 psum :
56 |      {auto _ : LSemigroup a}
57 |   -> (xs,ys : List1 a)
58 |   -> esum (xs ++ ys) === esum xs <+> esum ys
59 | psum (x ::: xs) (y ::: ys) = psum' x y xs ys
60 |
61 | 0 pnorm : LSemigroup a => (e : Expr a) -> eval e === esum (normalize e)
62 | pnorm (Var x)      = Refl
63 | pnorm (Append x y) = Calc $
64 |   |~ eval x <+> eval y
65 |   ~~ esum (normalize x) <+> eval y
66 |      ... cong (<+> eval y) (pnorm x)
67 |   ~~ esum (normalize x) <+> esum (normalize y)
68 |      ... cong (esum (normalize x) <+>) (pnorm y)
69 |   ~~ esum (normalize x ++ normalize y)
70 |      ..< psum (normalize x) (normalize y)
71 |
72 | --------------------------------------------------------------------------------
73 | --          Solver
74 | --------------------------------------------------------------------------------
75 |
76 | export
77 | 0 solve :
78 |      {auto _ : LSemigroup a}
79 |   -> (e1,e2 : Expr a)
80 |   -> {auto prf : normalize e1 === normalize e2}
81 |   -> eval e1 === eval e2
82 | solve e1 e2 = Calc $
83 |   |~ eval e1
84 |   ~~ esum (normalize e1) ... pnorm e1
85 |   ~~ esum (normalize e2) ... cong esum prf
86 |   ~~ eval e2             ..< pnorm e2
87 |