0 | module Data.Monoid.Exponentiation
 1 |
 2 | import Data.Nat.Views
 3 | import Syntax.PreorderReasoning
 4 |
 5 | %default total
 6 |
 7 | ------------------------------------------------------------------------
 8 | -- Implementations
 9 |
10 | public export
11 | linear : Monoid a => a -> Nat -> a
12 | linear v Z = neutral
13 | linear v (S k) = v <+> linear v k
14 |
15 | public export
16 | modularRec : Monoid a => a -> HalfRec n -> a
17 | modularRec v HalfRecZ = neutral
18 | modularRec v (HalfRecEven _ acc) = let e = modularRec v acc in e <+> e
19 | modularRec v (HalfRecOdd _ acc) = let e = modularRec v acc in v <+> e <+> e
20 |
21 | public export
22 | modular : Monoid a => a -> Nat -> a
23 | modular v n = modularRec v (halfRec n)
24 |
25 | export infixr 10 ^
26 | public export
27 | (^) : Num a => a -> Nat -> a
28 | (^) = modular @{Multiplicative}
29 |
30 | ------------------------------------------------------------------------
31 | -- Properties
32 |
33 | -- Not using `MonoidV` because it's cursed
34 | export
35 | linearPlusHomo : (mon : Monoid a) =>
36 |   -- good monoid
37 |   (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
38 |   (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
39 |   -- result
40 |   (v : a) -> {m, n : Nat} ->
41 |   (linear v m <+> linear v n) === linear v (m + n)
42 | linearPlusHomo opAssoc neutralL v = go m where
43 |
44 |   go : (m : Nat) -> (linear v m <+> linear v n) === linear v (m + n)
45 |   go Z = neutralL
46 |   go (S m) = Calc $
47 |     |~ (v <+> linear v m) <+> linear v n
48 |     ~~ v <+> (linear v m <+> linear v n) ...( opAssoc )
49 |     ~~ v <+> (linear v (m + n))          ...( cong (v <+>) (go m) )
50 |
51 | export
52 | modularRecCorrect : (mon : Monoid a) =>
53 |     -- good monoid
54 |   (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
55 |   (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
56 |   -- result
57 |   (v : a) -> {n : Nat} -> (p : HalfRec n) ->
58 |   modularRec v p === linear v n
59 | modularRecCorrect opAssoc neutralL v acc = go acc where
60 |
61 |   aux : {m, n : Nat} -> (linear v m <+> linear v n) === linear v (m + n)
62 |   aux = linearPlusHomo opAssoc neutralL v
63 |
64 |   go : {n : Nat} -> (p : HalfRec n) -> modularRec v p === linear v n
65 |   go HalfRecZ = Refl
66 |   go (HalfRecEven k acc) = rewrite go acc in aux
67 |   go (HalfRecOdd k acc) = rewrite go acc in Calc $
68 |     |~ (v <+> linear v k) <+> linear v k
69 |     ~~ v <+> (linear v k <+> linear v k)  ...( opAssoc )
70 |     ~~ v <+> (linear v (k + k))           ...( cong (v <+>) aux )
71 |
72 | export
73 | modularCorrect : (mon : Monoid a) =>
74 |     -- good monoid
75 |   (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
76 |   (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
77 |   -- result
78 |   (v : a) -> {n : Nat} -> modular v n === linear v n
79 | modularCorrect opAssoc neutralL v
80 |   = modularRecCorrect opAssoc neutralL v (halfRec n)
81 |