0 | module Data.Fin.Extra
  1 |
  2 | import Data.Fin
  3 | import public Data.Fin.Arith as Data.Fin.Extra
  4 | import public Data.Fin.Properties as Data.Fin.Extra
  5 | import public Data.Fin.Split as Data.Fin.Extra
  6 | import Data.Nat
  7 | import Data.Nat.Division
  8 |
  9 | import Syntax.WithProof
 10 | import Syntax.PreorderReasoning
 11 |
 12 | %default total
 13 |
 14 | -------------------------------------------------
 15 | --- Inversion function and related properties ---
 16 | -------------------------------------------------
 17 |
 18 | -- These deprecated functions are to be removed as soon as 0.8.0 is released.
 19 |
 20 | %deprecate -- Use `Data.Fin.complement` instead
 21 | public export %inline
 22 | invFin : {n : Nat} -> Fin n -> Fin n
 23 | invFin = complement
 24 |
 25 | %deprecate -- Use `Data.Fin.Properties.complementSpec` instead
 26 | export %inline
 27 | invFinSpec : {n : _} -> (i : Fin n) -> 1 + finToNat i + finToNat (complement i) = n
 28 | invFinSpec = complementSpec
 29 |
 30 | %deprecate -- Use `Data.Fin.Properties.complementWeakenIsFS` instead
 31 | export %inline
 32 | invFinWeakenIsFS : {n : Nat} -> (m : Fin n) -> complement (weaken m) = FS (complement m)
 33 | invFinWeakenIsFS = complementWeakenIsFS
 34 |
 35 | %deprecate -- Use `Data.Fin.Properties.complementLastIsFZ` instead
 36 | export %inline
 37 | invFinLastIsFZ : {n : Nat} -> complement (last {n}) = FZ
 38 | invFinLastIsFZ = complementLastIsFZ
 39 |
 40 | %deprecate -- Use `Data.Fin.Properties.complementInvolutive` instead
 41 | export %inline
 42 | invFinInvolutive : {n : Nat} -> (m : Fin n) -> complement (complement m) = m
 43 | invFinInvolutive = complementInvolutive
 44 |
 45 | -----------------------------------
 46 | --- Division-related properties ---
 47 | -----------------------------------
 48 |
 49 | ||| A view of Nat as a quotient of some number and a finite remainder.
 50 | public export
 51 | data FractionView : (n : Nat) -> (d : Nat) -> Type where
 52 |     Fraction : (n : Nat) -> (d : Nat) -> {auto ok: GT d Z} ->
 53 |                 (q : Nat) -> (r : Fin d) ->
 54 |                 q * d + finToNat r = n -> FractionView n d
 55 |
 56 | ||| Converts Nat to the fractional view with a non-zero divisor.
 57 | export
 58 | divMod : (n, d : Nat) -> {auto ok: GT d Z} -> FractionView n d
 59 | divMod Z (S d) = Fraction Z (S d) Z FZ Refl
 60 | divMod {ok=_} (S n) (S d) =
 61 |     let Fraction {ok=ok} n (S d) q r eq = divMod n (S d) in
 62 |     case strengthen' r of
 63 |         Left eq' => Fraction {ok=ok} (S n) (S d) (S q) FZ $
 64 |             rewrite sym eq in
 65 |                 rewrite trans (cong finToNat eq') finToNatLastIsBound in
 66 |                     cong S $ trans
 67 |                         (plusZeroRightNeutral (d + q * S d))
 68 |                         (plusCommutative d (q * S d))
 69 |         Right (r' ** eq') => Fraction {ok=ok} (S n) (S d) q (FS r') $
 70 |             rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in
 71 |                 cong S $ trans (sym $ cong (plus (q * S d)) eq') eq
 72 |
 73 | ||| Compute n % m as a Fin with upper bound m.
 74 | |||
 75 | ||| Useful, for example, when iterating through a large index, computing
 76 | ||| subindices as a function of the larger index (e.g. a flattened 2D-array)
 77 | export
 78 | modFin :  (n : Nat)
 79 |        -> (m : Nat)
 80 |        -> {auto mNZ : NonZero m}
 81 |        -> Fin m
 82 | modFin n 0 impossible
 83 | modFin 0 (S k) = FZ
 84 | modFin (S j) (S k) =
 85 |   let n' : Nat
 86 |       n' = modNatNZ (S j) (S k) mNZ in
 87 |   let ok = boundModNatNZ (S j) (S k) mNZ
 88 |   in natToFinLT n' @{ok}
 89 |
 90 | ||| Tighten the bound on a Fin by taking its current bound modulo the given
 91 | ||| non-zero number.
 92 | export
 93 | strengthenMod :  {n : _}
 94 |              -> Fin n
 95 |              -> (m : Nat)
 96 |              -> {auto mNZ : NonZero m}
 97 |              -> Fin m
 98 | strengthenMod _ Z impossible
 99 | strengthenMod {n = 0} f m@(S k) = weakenN m f
100 | strengthenMod {n = (S j)} f m@(S k) =
101 |  let n' : Nat
102 |      n' = modNatNZ (S j) (S k) %search in
103 |  let ok = boundModNatNZ (S j) (S k) %search
104 |  in natToFinLT n' @{ok}
105 |
106 | -------------------
107 | --- Conversions ---
108 | -------------------
109 |
110 | ||| Total function to convert a nat to a Fin, given a proof
111 | ||| that it is less than the bound.
112 | public export
113 | natToFinLTE : (n : Nat) -> (0 _ : LT n m) -> Fin m
114 | natToFinLTE Z     (LTESucc _) = FZ
115 | natToFinLTE (S k) (LTESucc l) = FS $ natToFinLTE k l
116 |
117 | ||| Converting from a Nat to a Fin and back is the identity.
118 | public export
119 | natToFinToNat :
120 |   (n : Nat)
121 |   -> (lte : LT n m)
122 |   -> finToNat (natToFinLTE n lte) = n
123 | natToFinToNat 0 (LTESucc lte) = Refl
124 | natToFinToNat (S k) (LTESucc lte) = cong S (natToFinToNat k lte)
125 |