[ 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
@@ -443,8 +473,9 @@ multOneLeftNeutral right = plusZeroRightNeutral right
 
 export
 multOneRightNeutral : (left : Nat) -> left * 1 = left
-multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left
-
+multOneRightNeutral left =
+  rewrite multCommutative left 1 in
+  multOneLeftNeutral left
 
 -- Proofs on minus
 
@@ -482,6 +513,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 +698,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/Binary.idr

@@ -0,0 +1,42 @@
+module Data.Binary
+
+import Data.Nat
+import Data.Nat.Properties
+import Data.Binary.Digit
+import Syntax.PreorderReasoning
+
+%default total
+
+||| Bin represents binary numbers right-to-left.
+||| For instance `4` can be represented as `OOI`.
+||| Note that representations are not unique: one may append arbitrarily
+||| many Os to the right of the representation without changing the meaning.
+public export
+Bin : Type
+Bin = List Digit
+
+||| Conversion from lists of bits to natural number.
+public export
+toNat : Bin -> Nat
+toNat = foldr (\ b, acc => toNat b + 2 * acc) 0
+
+||| Successor function on binary numbers.
+||| Amortised constant time.
+public export
+suc : Bin -> Bin
+suc [] = [I]
+suc (O :: bs) = I :: bs
+suc (I :: bs) = O :: (suc bs)
+
+||| Correctness proof of `suc` with respect to the semantics in terms of Nat
+export
+sucCorrect : {bs : Bin} -> toNat (suc bs) === S (toNat bs)
+sucCorrect {bs = []} = Refl
+sucCorrect {bs = O :: bs} = Refl
+sucCorrect {bs = I :: bs} = Calc $
+  |~ toNat (suc (I :: bs))
+  ~~ toNat (O :: suc bs) ...( Refl )
+  ~~ 2 * toNat (suc bs)  ...( Refl )
+  ~~ 2 * S (toNat bs)    ...( cong (2 *) sucCorrect )
+  ~~ 2 + 2 * toNat bs    ...( unfoldDoubleS )
+  ~~ S (toNat (I :: bs)) ...( Refl )

libs/contrib/Data/Binary/Digit.idr

@@ -0,0 +1,21 @@
+module Data.Binary.Digit
+
+%default total
+
+||| This is essentially Bool but with names that are easier
+||| to understand
+public export
+data Digit : Type where
+  O : Digit
+  I : Digit
+
+||| Translation to Bool
+public export
+isI : Digit -> Bool
+isI I = True
+isI O = False
+
+public export
+toNat : Digit -> Nat
+toNat O = 0
+toNat I = 1

libs/contrib/Data/IMaybe.idr

@@ -0,0 +1,23 @@
+||| Version of Maybe indexed by an `isJust' boolean
+module Data.IMaybe
+
+%default total
+
+public export
+data IMaybe : Bool -> Type -> Type where
+  Just : a -> IMaybe True a
+  Nothing : IMaybe False a
+
+public export
+fromJust : IMaybe True a -> a
+fromJust (Just a) = a
+
+public export
+Functor (IMaybe b) where
+  map f (Just a) = Just (f a)
+  map f Nothing = Nothing
+
+public export
+Applicative (IMaybe True) where
+  pure = Just
+  Just f <*> Just x = Just (f x)

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