[ new ] Perfect binary trees

libs/base/Data/Nat.idr

@@ -80,6 +80,28 @@ public export
 LT : Nat -> Nat -> Type
 LT left right = LTE (S left) right
 
+namespace LT
+
+  ||| LT is defined in terms of LTE which makes it annoying to use.
+  ||| This convenient view of allows us to avoid having to constantly
+  ||| perform nested matches to obtain another LT subproof instead of
+  ||| an LTE one.
+  public export
+  data View : LT m n -> Type where
+    LTZero : View (LTESucc LTEZero)
+    LTSucc : (lt : m `LT` n) -> View (LTESucc lt)
+
+  ||| Deconstruct an LT proof into either a base case or a further *LT*
+  export
+  view : (lt : LT m n) -> View lt
+  view (LTESucc LTEZero) = LTZero
+  view (LTESucc lt@(LTESucc _)) = LTSucc lt
+
+  ||| A convenient alias for trivial LT proofs
+  export
+  ltZero : Z `LT` S m
+  ltZero = LTESucc LTEZero
+
 public export
 GT : Nat -> Nat -> Type
 GT left right = LT right left
@@ -367,6 +389,14 @@ plusLteMonotoneLeft p q r p_lt_q
      rewrite plusCommutative p r in
      plusLteMonotoneRight p q r p_lt_q
 
+export
+plusLteMonotone : {m, n, p, q : Nat} -> m `LTE` n -> p `LTE` q ->
+                  (m + p) `LTE` (n + q)
+plusLteMonotone left right
+  = lteTransitive
+      (plusLteMonotoneLeft m p q right)
+      (plusLteMonotoneRight q m n left)
+
 zeroPlusLeftZero : (a,b : Nat) -> (0 = a + b) -> a = 0
 zeroPlusLeftZero 0 0 Refl = Refl
 zeroPlusLeftZero (S k) b _ impossible
@@ -482,6 +512,31 @@ minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
 minusPlusZero Z     _ = Refl
 minusPlusZero (S n) m = minusPlusZero n m
 
+export
+minusPos : m `LT` n -> Z `LT` minus n m
+minusPos lt = case view lt of
+  LTZero    => ltZero
+  LTSucc lt => minusPos lt
+
+export
+minusLteMonotone : {p : Nat} -> m `LTE` n -> minus m p `LTE` minus n p
+minusLteMonotone LTEZero = LTEZero
+minusLteMonotone {p = Z} prf@(LTESucc _) = prf
+minusLteMonotone {p = S p} (LTESucc lte) = minusLteMonotone lte
+
+export
+minusLtMonotone : m `LT` n -> p `LT` n -> minus m p `LT` minus n p
+minusLtMonotone mltn pltn = case view pltn of
+  LTZero => rewrite minusZeroRight m in mltn
+  LTSucc pltn => case view mltn of
+    LTZero => minusPos pltn
+    LTSucc mltn => minusLtMonotone mltn pltn
+
+public export
+minusPlus : (m : Nat) -> minus (plus m n) m === n
+minusPlus Z = irrelevantEq (minusZeroRight n)
+minusPlus (S m) = minusPlus m
+
 export
 plusMinusLte : (n, m : Nat) -> LTE n m -> (minus m n) + n = m
 plusMinusLte  Z     m    _   = rewrite minusZeroRight m in
@@ -642,10 +697,34 @@ sucMinR (S l) = cong S $ sucMinR l
 
 -- Algebra -----------------------------
 
-public export
-Semigroup Nat where
-  (<+>) = plus
+namespace Semigroup
 
-public export
-Monoid Nat where
-  neutral = Z
+  public export
+  [Additive] Semigroup Nat where
+    (<+>) = (+)
+
+  public export
+  [Multiplicative] Semigroup Nat where
+    (<+>) = (*)
+
+  public export
+  [Maximum] Semigroup Nat where
+    (<+>) = max
+
+  public export
+  [Minimum] Semigroup Nat where
+    (<+>) = min
+
+namespace Monoid
+
+  public export
+  [Additive] Monoid Nat using Semigroup.Additive where
+    neutral = 0
+
+  public export
+  [Multiplicative] Monoid Nat using Semigroup.Multiplicative where
+    neutral = 1
+
+  public export
+  [Maximum] Monoid Nat using Semigroup.Maximum where
+    neutral = 0

libs/contrib/Data/Monoid/Exponentiation.idr

@@ -0,0 +1,83 @@
+module Data.Monoid.Exponentiation
+
+import Control.Algebra
+import Data.Nat.Views
+import Data.Num.Implementations
+import Syntax.PreorderReasoning
+
+%default total
+
+------------------------------------------------------------------------
+-- Implementations
+
+public export
+linear : Monoid a => a -> Nat -> a
+linear v Z = neutral
+linear v (S k) = v <+> linear v k
+
+public export
+modularRec : Monoid a => a -> HalfRec n -> a
+modularRec v HalfRecZ = neutral
+modularRec v (HalfRecEven _ acc) = let e = modularRec v acc in e <+> e
+modularRec v (HalfRecOdd _ acc) = let e = modularRec v acc in v <+> e <+> e
+
+public export
+modular : Monoid a => a -> Nat -> a
+modular v n = modularRec v (halfRec n)
+
+infixl 10 ^
+public export
+(^) : Num a => a -> Nat -> a
+(^) = modular @{Multiplicative}
+
+------------------------------------------------------------------------
+-- Properties
+
+-- Not using `MonoidV` because it's cursed
+export
+linearPlusHomo : (mon : Monoid a) =>
+  -- good monoid
+  (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
+  (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
+  -- result
+  (v : a) -> {m, n : Nat} ->
+  (linear v m <+> linear v n) === linear v (m + n)
+linearPlusHomo opAssoc neutralL v = go m where
+
+  go : (m : Nat) -> (linear v m <+> linear v n) === linear v (m + n)
+  go Z = neutralL
+  go (S m) = Calc $
+    |~ (v <+> linear v m) <+> linear v n
+    ~~ v <+> (linear v m <+> linear v n) ...( opAssoc )
+    ~~ v <+> (linear v (m + n))          ...( cong (v <+>) (go m) )
+
+export
+modularRecCorrect : (mon : Monoid a) =>
+    -- good monoid
+  (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
+  (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
+  -- result
+  (v : a) -> {n : Nat} -> (p : HalfRec n) ->
+  modularRec v p === linear v n
+modularRecCorrect opAssoc neutralL v acc = go acc where
+
+  aux : {m, n : Nat} -> (linear v m <+> linear v n) === linear v (m + n)
+  aux = linearPlusHomo opAssoc neutralL v
+
+  go : {n : Nat} -> (p : HalfRec n) -> modularRec v p === linear v n
+  go HalfRecZ = Refl
+  go (HalfRecEven k acc) = rewrite go acc in aux
+  go (HalfRecOdd k acc) = rewrite go acc in Calc $
+    |~ (v <+> linear v k) <+> linear v k
+    ~~ v <+> (linear v k <+> linear v k)  ...( opAssoc )
+    ~~ v <+> (linear v (k + k))           ...( cong (v <+>) aux )
+
+export
+modularCorrect : (mon : Monoid a) =>
+    -- good monoid
+  (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) ->
+  (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) ->
+  -- result
+  (v : a) -> {n : Nat} -> modular v n === linear v n
+modularCorrect opAssoc neutralL v
+  = modularRecCorrect opAssoc neutralL v (halfRec n)

libs/contrib/Data/Nat/Algebra.idr

@@ -5,11 +5,15 @@ import Data.Nat
 
 %default total
 
-public export
-SemigroupV Nat where
-  semigroupOpIsAssociative = plusAssociative
-
-public export
-MonoidV Nat where
-  monoidNeutralIsNeutralL = plusZeroRightNeutral
-  monoidNeutralIsNeutralR = plusZeroLeftNeutral
+namespace SemigroupV
+
+  public export
+  [Additive] SemigroupV Nat using Semigroup.Additive where
+    semigroupOpIsAssociative = plusAssociative
+
+namespace MonoidV
+
+  public export
+  [Additive] MonoidV Nat using Monoid.Additive SemigroupV.Additive where
+    monoidNeutralIsNeutralL = plusZeroRightNeutral
+    monoidNeutralIsNeutralR = plusZeroLeftNeutral

libs/contrib/Data/Nat/Exponentiation.idr

@@ -0,0 +1,83 @@
+module Data.Nat.Exponentiation
+
+import Data.Nat as Nat
+import Data.Monoid.Exponentiation as Mon
+import Data.Num.Implementations as Num
+import Data.Nat.Views
+import Data.Nat.Order
+import Decidable.Order
+import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Generic
+
+%default total
+
+public export
+pow : Nat -> Nat -> Nat
+pow = Mon.(^)
+
+public export
+lpow : Nat -> Nat -> Nat
+lpow = linear @{Nat.Monoid.Multiplicative}
+
+public export
+pow2 : Nat -> Nat
+pow2 = (2 ^)
+
+public export
+lpow2 : Nat -> Nat
+lpow2 = lpow 2
+
+export
+modularCorrect : (v : Nat) -> {n : Nat} ->
+                 pow v n === lpow v n
+modularCorrect
+   = Mon.modularCorrect
+     @{Nat.Monoid.Multiplicative}
+     (sym (multAssociative _ _ _))
+     (irrelevantEq $ multOneLeftNeutral _)
+
+export
+pow2Correct : {n : Nat} -> pow2 n === lpow2 n
+pow2Correct = modularCorrect 2
+
+export
+unfoldDouble : {0 n : Nat} -> (2 * n) === (n + n)
+unfoldDouble = irrelevantEq $ cong (n +) (plusZeroRightNeutral _)
+
+export
+unfoldLpow2 : lpow2 (S n) === (lpow2 n + lpow2 n)
+unfoldLpow2 = unfoldDouble
+
+export
+unfoldPow2 : pow2 (S n) === (pow2 n + pow2 n)
+unfoldPow2 = irrelevantEq $ Calc $
+  let mon : Monoid Nat; mon = Nat.Monoid.Multiplicative
+      lpow2 : Nat -> Nat; lpow2 = linear @{mon} 2 in
+  |~ pow2 (S n)
+  ~~ lpow2 (S n)       ...( pow2Correct )
+  ~~ lpow2 n + lpow2 n ...( unfoldLpow2 )
+  ~~ (pow2 n + pow2 n) ...( cong2 (+) (sym pow2Correct) (sym pow2Correct) )
+
+export
+lteLpow2 : {m : Nat} -> 1 `LTE` lpow2 m
+lteLpow2 {m = Z} = lteRefl
+lteLpow2 {m = S m} = CalcWith $
+  let ih = lteLpow2 {m} in
+  |~ 1
+  <~ 2                 ...( ltZero )
+  <~ lpow2 m + lpow2 m ...( plusLteMonotone ih ih )
+  ~~ lpow2 (S m)       ...( sym (unfoldLpow2) )
+
+export
+ltePow2 : {m : Nat} -> 1 `LTE` pow2 m
+ltePow2 = CalcWith $
+  |~ 1
+  <~ lpow2 m ...( lteLpow2 )
+  ~~ pow2 m  ...( sym pow2Correct )
+
+export
+pow2Increasing : {m : Nat} -> pow2 m `LT` pow2 (S m)
+pow2Increasing = CalcWith $
+  |~ S (pow2 m)
+  <~ pow2 m + pow2 m ...( plusLteMonotoneRight (pow2 m) 1 (pow2 m) ltePow2 )
+  ~~ pow2 (S m)      ...( sym unfoldPow2 )

libs/contrib/Data/Nat/Order/Properties.idr

@@ -34,10 +34,18 @@ export
 lteIsLTE : (a, b : Nat) -> a `lte` b = True -> a `LTE` b
 lteIsLTE  a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
 
+export
+ltIsLT : (a, b : Nat) -> a `lt` b = True -> a `LT` b
+ltIsLT  a = lteIsLTE (S a)
+
 export
 notlteIsNotLTE : (a, b : Nat) -> a `lte` b = False -> Not (a `LTE` b)
 notlteIsNotLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b))
 
+export
+notltIsNotLT : (a, b : Nat) -> a `lt` b = False -> Not (a `LT` b)
+notltIsNotLT a = notlteIsNotLTE (S a)
+
 
 export
 notlteIsLT : (a, b : Nat) -> a `lte` b = False -> b `LT` a

libs/contrib/Data/Num/Implementations.idr

@@ -0,0 +1,23 @@
+module Data.Num.Implementations
+
+%default total
+
+namespace Semigroup
+
+  public export
+  [Additive] Num a => Semigroup a
+    where (<+>) = (+)
+  public export
+  [Multiplicative] Num a => Semigroup a
+    where (<+>) = (*)
+
+namespace Monoid
+
+  public export
+  [Additive] Num a => Monoid a
+    using Semigroup.Additive
+    where neutral = 0
+  public export
+  [Multiplicative] Num a => Monoid a
+    using Semigroup.Multiplicative
+    where neutral = 1