0 | module Data.Nat.Exponentiation
 1 |
 2 | import Data.Nat as Nat
 3 | import Data.Nat.Properties
 4 | import Data.Monoid.Exponentiation as Mon
 5 | import Syntax.PreorderReasoning
 6 | import Syntax.PreorderReasoning.Generic
 7 |
 8 | %default total
 9 |
10 | public export
11 | pow : Nat -> Nat -> Nat
12 | pow = Mon.(^)
13 |
14 | public export
15 | lpow : Nat -> Nat -> Nat
16 | lpow = linear @{Monoid.Multiplicative}
17 |
18 | public export
19 | pow2 : Nat -> Nat
20 | pow2 = (2 ^)
21 |
22 | public export
23 | lpow2 : Nat -> Nat
24 | lpow2 = lpow 2
25 |
26 | export
27 | modularCorrect : (v : Nat) -> {n : Nat} ->
28 |                  pow v n === lpow v n
29 | modularCorrect
30 |    = Mon.modularCorrect
31 |      @{Monoid.Multiplicative}
32 |      (sym (multAssociative _ _ _))
33 |      (irrelevantEq $ multOneLeftNeutral _)
34 |
35 | export
36 | pow2Correct : {n : Nat} -> pow2 n === lpow2 n
37 | pow2Correct = modularCorrect 2
38 |
39 | export
40 | unfoldLpow2 : lpow2 (S n) === (lpow2 n + lpow2 n)
41 | unfoldLpow2 = unfoldDouble
42 |
43 | export
44 | unfoldPow2 : pow2 (S n) === (pow2 n + pow2 n)
45 | unfoldPow2 = irrelevantEq $ Calc $
46 |   let mon : Monoid Nat; mon = Monoid.Multiplicative
47 |       lpow2 : Nat -> Nat; lpow2 = linear @{mon} 2 in
48 |   |~ pow2 (S n)
49 |   ~~ lpow2 (S n)       ...( pow2Correct )
50 |   ~~ lpow2 n + lpow2 n ...( unfoldLpow2 )
51 |   ~~ (pow2 n + pow2 n) ...( cong2 (+) (sym pow2Correct) (sym pow2Correct) )
52 |
53 | export
54 | lteLpow2 : {m : Nat} -> 1 `LTE` lpow2 m
55 | lteLpow2 {m = Z} = reflexive
56 | lteLpow2 {m = S m} = CalcWith $
57 |   let ih = lteLpow2 {m} in
58 |   |~ 1
59 |   <~ 2                 ...( ltZero )
60 |   <~ lpow2 m + lpow2 m ...( plusLteMonotone ih ih )
61 |   ~~ lpow2 (S m)       ...( sym (unfoldLpow2) )
62 |
63 | export
64 | ltePow2 : {m : Nat} -> 1 `LTE` pow2 m
65 | ltePow2 = CalcWith $
66 |   |~ 1
67 |   <~ lpow2 m ...( lteLpow2 )
68 |   ~~ pow2 m  ...( sym pow2Correct )
69 |
70 | export
71 | pow2Increasing : {m : Nat} -> pow2 m `LT` pow2 (S m)
72 | pow2Increasing = CalcWith $
73 |   |~ S (pow2 m)
74 |   <~ pow2 m + pow2 m ...( plusLteMonotoneRight (pow2 m) 1 (pow2 m) ltePow2 )
75 |   ~~ pow2 (S m)      ...( sym unfoldPow2 )
76 |