[ base ] Move most useful and stable parts of Data.Fin.Extra to base

CHANGELOG_NEXT.md

@@ -159,6 +159,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Removed need for the runtime value of the implicit length argument in
   `Data.Vect.Elem.dropElem`.
 
+* Some pieces of `Data.Fin.Extra` from `contrib` were moved to `base` to modules
+  `Data.Fin.Properties`, `Data.Fin.Arith` and `Data.Fin.Split`.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.
@@ -170,6 +173,12 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   and removed `Data.HVect` from contrib. See the additional notes in the
   CHANGELOG under the `Library changes`/`Base` section above.
 
+* Some pieces of `Data.Fin.Extra` from `contrib` were moved to `base` to modules
+  `Data.Fin.Properties`, `Data.Fin.Arith` and `Data.Fin.Split`.
+
+* Function `invFin` from `Data.Fin.Extra` was deprecated in favour of
+  `Data.Fin.complement` from `base`.
+
 #### Network
 
 * Add a missing function parameter (the flag) in the C implementation of `idrnet_recv_bytes`

libs/base/Data/Fin/Arith.idr

@@ -0,0 +1,155 @@
+||| Result-type changing `Fin` arithmetics
+module Data.Fin.Arith
+
+import public Data.Fin
+
+import Syntax.PreorderReasoning
+
+%default total
+
+||| Addition of `Fin`s as bounded naturals.
+||| The resulting type has the smallest possible bound
+||| as illustated by the relations with the `last` function.
+public export
+(+) : {m, n : Nat} -> Fin m -> Fin (S n) -> Fin (m + n)
+(+) FZ y = coerce (cong S $ plusCommutative n (pred m)) (weakenN (pred m) y)
+(+) (FS x) y = FS (x + y)
+
+||| Multiplication of `Fin`s as bounded naturals.
+||| The resulting type has the smallest possible bound
+||| as illustated by the relations with the `last` function.
+public export
+(*) : {m, n : Nat} -> Fin (S m) -> Fin (S n) -> Fin (S (m * n))
+(*) FZ _ = FZ
+(*) {m = S _} (FS x) y = y + x * y
+
+--- Properties ---
+
+-- Relation between `+` and `*` and their counterparts on `Nat`
+
+export
+finToNatPlusHomo : {m, n : Nat} -> (x : Fin m) -> (y : Fin (S n)) ->
+                   finToNat (x + y) = finToNat x + finToNat y
+finToNatPlusHomo FZ _
+  = finToNatQuotient $ transitive
+     (coerceEq _)
+     (weakenNNeutral _ _)
+finToNatPlusHomo (FS x) y = cong S (finToNatPlusHomo x y)
+
+export
+finToNatMultHomo : {m, n : Nat} -> (x : Fin (S m)) -> (y : Fin (S n)) ->
+                   finToNat (x * y) = finToNat x * finToNat y
+finToNatMultHomo FZ _ = Refl
+finToNatMultHomo {m = S _} (FS x) y = Calc $
+  |~ finToNat (FS x * y)
+  ~~ finToNat (y + x * y)                 ...( Refl )
+  ~~ finToNat y + finToNat (x * y)        ...( finToNatPlusHomo y (x * y) )
+  ~~ finToNat y + finToNat x * finToNat y ...( cong (finToNat y +) (finToNatMultHomo x y) )
+  ~~ finToNat (FS x) * finToNat y         ...( Refl )
+
+-- Relations to `Fin`'s `last`
+
+export
+plusPreservesLast : (m, n : Nat) -> Fin.last {n=m} + Fin.last {n} = Fin.last
+plusPreservesLast Z     n
+  = homoPointwiseIsEqual $ transitive
+      (coerceEq _)
+      (weakenNNeutral _ _)
+plusPreservesLast (S m) n = cong FS (plusPreservesLast m n)
+
+export
+multPreservesLast : (m, n : Nat) -> Fin.last {n=m} * Fin.last {n} = Fin.last
+multPreservesLast Z n = Refl
+multPreservesLast (S m) n = Calc $
+  |~ last + (last * last)
+  ~~ last + last          ...( cong (last +) (multPreservesLast m n) )
+  ~~ last                 ...( plusPreservesLast n (m * n) )
+
+-- General addition properties
+
+export
+plusSuccRightSucc : {m, n : Nat} -> (left : Fin m) -> (right : Fin (S n)) ->
+                    FS (left + right) ~~~ left + FS right
+plusSuccRightSucc FZ        right = FS $ congCoerce reflexive
+plusSuccRightSucc (FS left) right = FS $ plusSuccRightSucc left right
+
+-- Relations to `Fin`-specific `shift` and `weaken`
+
+export
+shiftAsPlus : {m, n : Nat} -> (k : Fin (S m)) ->
+              shift n k ~~~ last {n} + k
+shiftAsPlus {n=Z}   k =
+  symmetric $ transitive (coerceEq _) (weakenNNeutral _ _)
+shiftAsPlus {n=S n} k = FS (shiftAsPlus k)
+
+export
+weakenNAsPlusFZ : {m, n : Nat} -> (k : Fin n) ->
+                  weakenN m k = k + the (Fin (S m)) FZ
+weakenNAsPlusFZ FZ = Refl
+weakenNAsPlusFZ (FS k) = cong FS (weakenNAsPlusFZ k)
+
+export
+weakenNPlusHomo : {0 m, n : Nat} -> (k : Fin p) ->
+                  weakenN n (weakenN m k) ~~~ weakenN (m + n) k
+weakenNPlusHomo FZ = FZ
+weakenNPlusHomo (FS k) = FS (weakenNPlusHomo k)
+
+export
+weakenNOfPlus :
+  {m, n : Nat} -> (k : Fin m) -> (l : Fin (S n)) ->
+  weakenN w (k + l) ~~~ weakenN w k + l
+weakenNOfPlus FZ l
+  = transitive (congWeakenN (coerceEq _))
+  $ transitive (weakenNPlusHomo l)
+  $ symmetric (coerceEq _)
+weakenNOfPlus (FS k) l = FS (weakenNOfPlus k l)
+-- General addition properties (continued)
+
+export
+plusZeroLeftNeutral : (k : Fin (S n)) -> FZ + k ~~~ k
+plusZeroLeftNeutral k = transitive (coerceEq _) (weakenNNeutral _ k)
+
+export
+congPlusLeft : {m, n, p : Nat} -> {k : Fin m} -> {l : Fin n} ->
+               (c : Fin (S p)) -> k ~~~ l -> k + c ~~~ l + c
+congPlusLeft c FZ
+  = transitive (plusZeroLeftNeutral c)
+               (symmetric $ plusZeroLeftNeutral c)
+congPlusLeft c (FS prf) = FS (congPlusLeft c prf)
+
+export
+plusZeroRightNeutral : (k : Fin m) -> k + FZ ~~~ k
+plusZeroRightNeutral FZ = FZ
+plusZeroRightNeutral (FS k) = FS (plusZeroRightNeutral k)
+
+export
+congPlusRight : {m, n, p : Nat} -> {k : Fin (S n)} -> {l : Fin (S p)} ->
+                (c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
+congPlusRight c FZ
+  = transitive (plusZeroRightNeutral c)
+               (symmetric $ plusZeroRightNeutral c)
+congPlusRight {n = S _} {p = S _} c (FS prf)
+  = transitive (symmetric $ plusSuccRightSucc c _)
+  $ transitive (FS $ congPlusRight c prf)
+               (plusSuccRightSucc c _)
+congPlusRight {p = Z} c (FS prf) impossible
+
+export
+plusCommutative : {m, n : Nat} -> (left : Fin (S m)) -> (right : Fin (S n)) ->
+                  left + right ~~~ right + left
+plusCommutative FZ        right
+  = transitive (plusZeroLeftNeutral right)
+               (symmetric $ plusZeroRightNeutral right)
+plusCommutative {m = S _} (FS left) right
+  = transitive (FS (plusCommutative left right))
+               (plusSuccRightSucc right left)
+
+export
+plusAssociative :
+  {m, n, p : Nat} ->
+  (left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) ->
+  left + (centre + right) ~~~ (left + centre) + right
+plusAssociative FZ centre right
+  = transitive (plusZeroLeftNeutral (centre + right))
+               (congPlusLeft right (symmetric $ plusZeroLeftNeutral centre))
+plusAssociative (FS left) centre right = FS (plusAssociative left centre right)

libs/base/Data/Fin/Properties.idr

@@ -0,0 +1,124 @@
+||| Some properties of functions defined in `Data.Fin`
+module Data.Fin.Properties
+
+import public Data.Fin
+
+import Syntax.PreorderReasoning
+
+%default total
+
+-------------------------------
+--- `finToNat`'s properties ---
+-------------------------------
+
+||| A Fin's underlying natural number is smaller than the bound
+export
+elemSmallerThanBound : (n : Fin m) -> finToNat n `LT` m
+elemSmallerThanBound FZ = LTESucc LTEZero
+elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)
+
+||| Last's underlying natural number is the bound's predecessor
+export
+finToNatLastIsBound : {n : Nat} -> finToNat (Fin.last {n}) = n
+finToNatLastIsBound {n=Z} = Refl
+finToNatLastIsBound {n=S k} = cong S finToNatLastIsBound
+
+||| Weaken does not modify the underlying natural number
+export
+finToNatWeakenNeutral : {n : Fin m} -> finToNat (weaken n) = finToNat n
+finToNatWeakenNeutral = finToNatQuotient (weakenNeutral n)
+
+||| WeakenN does not modify the underlying natural number
+export
+finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) ->
+                         finToNat (weakenN m k) = finToNat k
+finToNatWeakenNNeutral m k = finToNatQuotient (weakenNNeutral m k)
+
+||| `Shift k` shifts the underlying natural number by `k`.
+export
+finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a
+finToNatShift Z     a = Refl
+finToNatShift (S k) a = cong S (finToNatShift k a)
+
+----------------------------------------------------
+--- Complement (inversion) function's properties ---
+----------------------------------------------------
+
+export
+complementSpec : {n : _} -> (i : Fin n) -> 1 + finToNat i + finToNat (complement i) = n
+complementSpec {n = S k} FZ = cong S finToNatLastIsBound
+complementSpec (FS k) = let H = complementSpec k in
+  let h = finToNatWeakenNeutral {n = complement k} in
+  cong S (rewrite h in H)
+
+||| The inverse of a weakened element is the successor of its inverse
+export
+complementWeakenIsFS : {n : Nat} -> (m : Fin n) -> complement (weaken m) = FS (complement m)
+complementWeakenIsFS FZ = Refl
+complementWeakenIsFS (FS k) = cong weaken (complementWeakenIsFS k)
+
+export
+complementLastIsFZ : {n : Nat} -> complement (last {n}) = FZ
+complementLastIsFZ {n = Z} = Refl
+complementLastIsFZ {n = S n} = cong weaken (complementLastIsFZ {n})
+
+||| `complement` is involutive (i.e. applied twice it is the identity)
+export
+complementInvolutive : {n : Nat} -> (m : Fin n) -> complement (complement m) = m
+complementInvolutive FZ = complementLastIsFZ
+complementInvolutive (FS k) = Calc $
+   |~ complement (complement (FS k))
+   ~~ complement (weaken (complement k)) ...( Refl )
+   ~~ FS (complement (complement k))     ...( complementWeakenIsFS (complement k) )
+   ~~ FS k                       ...( cong FS (complementInvolutive k) )
+
+--------------------------------
+--- Strengthening properties ---
+--------------------------------
+
+||| It's possible to strengthen a weakened element of Fin **m**.
+export
+strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Just n
+strengthenWeakenIsRight FZ = Refl
+strengthenWeakenIsRight (FS k) = rewrite strengthenWeakenIsRight k in Refl
+
+||| It's not possible to strengthen the last element of Fin **n**.
+export
+strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Nothing
+strengthenLastIsLeft {n=Z} = Refl
+strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl
+
+||| It's possible to strengthen the inverse of a succesor
+export
+strengthenNotLastIsRight : {n : Nat} -> (m : Fin n) -> strengthen (complement (FS m)) = Just (complement m)
+strengthenNotLastIsRight m = strengthenWeakenIsRight (complement m)
+
+||| Either tightens the bound on a Fin or proves that it's the last.
+export
+strengthen' : {n : Nat} -> (m : Fin (S n)) ->
+              Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
+strengthen' {n = Z} FZ = Left Refl
+strengthen' {n = S k} FZ = Right (FZ ** Refl)
+strengthen' {n = S k} (FS m) = case strengthen' m of
+    Left eq => Left $ cong FS eq
+    Right (m' ** eq) => Right (FS m' ** cong S eq)
+
+----------------------------
+--- Weakening properties ---
+----------------------------
+
+export
+weakenNZeroIdentity : (k : Fin n) ->  weakenN 0 k ~~~ k
+weakenNZeroIdentity FZ = FZ
+weakenNZeroIdentity (FS k) = FS (weakenNZeroIdentity k)
+
+export
+shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)
+shiftFSLinear Z     f = reflexive
+shiftFSLinear (S m) f = FS (shiftFSLinear m f)
+
+export
+shiftLastIsLast : (m : Nat) -> {n : Nat} ->
+                  shift m (Fin.last {n}) ~~~ Fin.last {n=m+n}
+shiftLastIsLast Z = reflexive
+shiftLastIsLast (S m) = FS (shiftLastIsLast m)