Data.Fin


   0 | module Data.Fin
   1 | 
   2 | import Control.Function
   3 | import public Control.Ord
   4 | import Data.List1
   5 | import public Data.Maybe
   6 | import public Data.Nat
   7 | import public Data.So
   8 | import Decidable.Equality.Core
   9 | 
  10 | %default total
  11 | 
  12 | ||| Numbers strictly less than some bound.  The name comes from "finite sets".
  13 | |||
  14 | ||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
  15 | ||| exceedingly inefficient at run time.
  16 | ||| @ n the upper bound
  17 | public export
  18 | data Fin : (n : Nat) -> Type where
  19 |     FZ : Fin (S k)
  20 |     FS : Fin k -> Fin (S k)
  21 | 
  22 | ||| Coerce between Fins with equal indices
  23 | public export
  24 | coerce : {n : Nat} -> (0 eq : m = n) -> Fin m -> Fin n -- TODO: make linear
  25 | coerce {n = S _} eq FZ = FZ
  26 | coerce {n = Z} eq FZ impossible
  27 | coerce {n = S _} eq (FS k) = FS (coerce (injective eq) k)
  28 | coerce {n = Z} eq (FS k) impossible
  29 | 
  30 | %transform "coerce-identity" coerce eq k = replace {p = Fin} eq k
  31 | 
  32 | export
  33 | Uninhabited (Fin Z) where
  34 |   uninhabited FZ impossible
  35 |   uninhabited (FS f) impossible
  36 | 
  37 | export
  38 | Uninhabited (FZ = FS k) where
  39 |   uninhabited Refl impossible
  40 | 
  41 | export
  42 | Uninhabited (FS k = FZ) where
  43 |   uninhabited Refl impossible
  44 | 
  45 | export
  46 | Uninhabited (n = m) => Uninhabited (FS n = FS m) where
  47 |   uninhabited Refl @{nm} = uninhabited Refl @{nm}
  48 | 
  49 | export
  50 | Injective FS where
  51 |   injective Refl = Refl
  52 | 
  53 | ||| Convert a Fin to a Nat
  54 | public export
  55 | finToNat : Fin n -> Nat
  56 | finToNat FZ = Z
  57 | finToNat (FS k) = S $ finToNat k
  58 | 
  59 | export
  60 | Eq (Fin n) where
  61 |   x == y = finToNat x == finToNat y
  62 | 
  63 | finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
  64 | finToNatInjective FZ     FZ     _    = Refl
  65 | finToNatInjective (FS _) FZ     Refl impossible
  66 | finToNatInjective FZ     (FS _) Refl impossible
  67 | finToNatInjective (FS m) (FS n) prf  =
  68 |   cong FS $ finToNatInjective m n $ injective prf
  69 | 
  70 | ||| `finToNat` is injective
  71 | export
  72 | Injective Fin.finToNat where
  73 |  injective = (finToNatInjective _ _)
  74 | 
  75 | export
  76 | Cast (Fin n) Nat where
  77 |     cast = finToNat
  78 | 
  79 | ||| Convert a Fin to an Integer
  80 | public export
  81 | finToInteger : Fin n -> Integer
  82 | finToInteger FZ     = 0
  83 | finToInteger (FS k) = 1 + finToInteger k
  84 | 
  85 | -- %builtin NaturalToInteger Data.Fin.finToInteger
  86 | 
  87 | export
  88 | Show (Fin n) where
  89 |   show = show . finToInteger
  90 | 
  91 | export
  92 | Cast (Fin n) Integer where
  93 |     cast = finToInteger
  94 | 
  95 | ||| Weaken the bound on a Fin by 1
  96 | public export
  97 | weaken : Fin n -> Fin (S n)
  98 | weaken FZ     = FZ
  99 | weaken (FS k) = FS $ weaken k
 100 | 
 101 | ||| Weaken the bound on a Fin by some amount
 102 | public export
 103 | weakenN : (0 n : Nat) -> Fin m -> Fin (m + n)
 104 | weakenN n FZ = FZ
 105 | weakenN n (FS f) = FS $ weakenN n f
 106 | 
 107 | ||| Weaken the bound on a Fin using a constructive comparison
 108 | public export
 109 | weakenLTE : Fin n -> LTE n m -> Fin m
 110 | weakenLTE  FZ     LTEZero impossible
 111 | weakenLTE (FS _)  LTEZero impossible
 112 | weakenLTE  FZ    (LTESucc _) = FZ
 113 | weakenLTE (FS x) (LTESucc y) = FS $ weakenLTE x y
 114 | 
 115 | ||| Attempt to tighten the bound on a Fin.
 116 | ||| Return the tightened bound if there is one, else nothing.
 117 | export
 118 | strengthen : {n : _} -> Fin (S n) -> Maybe (Fin n)
 119 | strengthen {n = S _} FZ = Just FZ
 120 | strengthen {n = S _} (FS p) with (strengthen p)
 121 |   strengthen (FS _) | Nothing = Nothing
 122 |   strengthen (FS _) | Just q  = Just $ FS q
 123 | strengthen _ = Nothing
 124 | 
 125 | ||| Add some natural number to a Fin, extending the bound accordingly
 126 | ||| @ n the previous bound
 127 | ||| @ m the number to increase the Fin by
 128 | public export
 129 | shift : (m : Nat) -> Fin n -> Fin (m + n)
 130 | shift Z f = f
 131 | shift (S m) f = FS $ shift m f
 132 | 
 133 | ||| Increment a Fin, wrapping on overflow
 134 | public export
 135 | finS : {n : Nat} -> Fin n -> Fin n
 136 | finS {n = S _} x = case strengthen x of
 137 |     Nothing => FZ
 138 |     Just y => FS y
 139 | 
 140 | ||| The largest element of some Fin type
 141 | public export
 142 | last : {n : _} -> Fin (S n)
 143 | last {n=Z} = FZ
 144 | last {n=S _} = FS last
 145 | 
 146 | ||| The finite complement of some Fin.
 147 | ||| The number as far along as the input, but starting from the other end.
 148 | public export
 149 | complement : {n : Nat} -> Fin n -> Fin n
 150 | complement {n = S _} FZ = last
 151 | complement {n = S _} (FS x) = weaken $ complement x
 152 | 
 153 | namespace List
 154 | 
 155 |   ||| All of the Fin elements
 156 |   public export
 157 |   allFins : (n : Nat) -> List (Fin n)
 158 |   allFins Z = []
 159 |   allFins (S n) = FZ :: map FS (allFins n)
 160 | 
 161 | namespace List1
 162 | 
 163 |   ||| All of the Fin elements
 164 |   public export
 165 |   allFins : (n : Nat) -> List1 (Fin (S n))
 166 |   allFins Z = FZ ::: []
 167 |   allFins (S n) = FZ ::: map FS (forget (allFins n))
 168 | 
 169 | 
 170 | export
 171 | Ord (Fin n) where
 172 |   compare x y = compare (finToNat x) (finToNat y)
 173 | 
 174 | namespace Monoid
 175 | 
 176 |   public export
 177 |   [Minimum] {n : Nat} -> Monoid (Fin $ S n) using Semigroup.Minimum where
 178 |     neutral = last
 179 | 
 180 |   public export
 181 |   [Maximum] Monoid (Fin $ S n) using Semigroup.Maximum where
 182 |     neutral = FZ
 183 | 
 184 | public export
 185 | natToFinLT : (x : Nat) -> {0 n : Nat} ->
 186 |              {auto 0 prf : x `LT` n} ->
 187 |              Fin n
 188 | natToFinLT Z {prf = LTESucc _} = FZ
 189 | natToFinLT (S k) {prf = LTESucc _} = FS $ natToFinLT k
 190 | 
 191 | public export
 192 | natToFinLt : (x : Nat) -> {0 n : Nat} ->
 193 |              {auto 0 prf : So (x < n)} ->
 194 |              Fin n
 195 | natToFinLt x = let 0 p := ltOpReflectsLT x n prf in natToFinLT x
 196 | 
 197 | public export
 198 | natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
 199 | natToFin x n = case isLT x n of
 200 |     Yes prf => Just $ natToFinLT x
 201 |     No contra => Nothing
 202 | 
 203 | ||| Convert an `Integer` to a `Fin`, provided the integer is within bounds.
 204 | ||| @n The upper bound of the Fin
 205 | public export
 206 | integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
 207 | integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!
 208 | integerToFin x n = if x >= 0 then natToFin (fromInteger x) n else Nothing
 209 | 
 210 | public export
 211 | maybeLTE : (x : Nat) -> (y : Nat) -> Maybe (x `LTE` y)
 212 | maybeLTE Z _ = Just LTEZero
 213 | maybeLTE (S x) (S y) = LTESucc <$> maybeLTE x y
 214 | maybeLTE _ _ = Nothing
 215 | 
 216 | public export
 217 | maybeLT : (x : Nat) -> (y : Nat) -> Maybe (x `LT` y)
 218 | maybeLT x y = maybeLTE (S x) y
 219 | 
 220 | public export
 221 | finFromInteger : (x : Integer) ->
 222 |                  {auto 0 prf : So (fromInteger x < n)} ->
 223 |                  Fin n
 224 | finFromInteger x = natToFinLt (fromInteger x)
 225 | 
 226 | -- Direct comparison between `Integer` and `Nat`.
 227 | -- We cannot convert the `Nat` to `Integer`, because that will not work with open terms;
 228 | -- but we cannot convert the `Integer` to `Nat` either, because that slows down typechecking
 229 | -- even when the function is unused (issue #2032)
 230 | public export
 231 | integerLessThanNat : Integer -> Nat -> Bool
 232 | integerLessThanNat 0 (S m) = True
 233 | integerLessThanNat x n with (x < the Integer 0)
 234 |   integerLessThanNat _ _     | True  = False                           -- don't support negative literals
 235 |   integerLessThanNat x (S m) | False = integerLessThanNat (x-1) m      -- recursive case
 236 |   integerLessThanNat x Z     | False = False                           -- `x >= 0` contradicts `x < Z`
 237 | 
 238 | ||| Allow overloading of Integer literals for Fin.
 239 | ||| @ x the Integer that the user typed
 240 | ||| @ prf an automatically-constructed proof that `x` is in bounds
 241 | public export
 242 | fromInteger : (x : Integer) ->
 243 |               {auto 0 prf : So (integerLessThanNat x n)} ->
 244 |               Fin n
 245 | fromInteger x = finFromInteger x {prf = lemma prf} where
 246 |   -- to be minimally invasive, we just call the previous implementation.
 247 |   -- however, having a different proof obligation resolves #2032
 248 |   0 lemma : {x : Integer} -> So (integerLessThanNat x n) -> So (fromInteger {ty=Nat} x < n)
 249 |   lemma oh = believe_me oh
 250 | 
 251 | -- %builtin IntegerToNatural Data.Fin.fromInteger
 252 | 
 253 | ||| Convert an Integer to a Fin in the required bounds/
 254 | ||| This is essentially a composition of `mod` and `fromInteger`
 255 | public export
 256 | restrict : (n : Nat) -> Integer -> Fin (S n)
 257 | restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
 258 |                      -- reasoning about primitives, so we need the
 259 |                      -- 'believe_me'. It's fine because val' must be
 260 |                      -- in the right range
 261 |                      fromInteger {n = S n} val'
 262 |                          {prf = believe_me {a=IsJust (Just val')} ItIsJust}
 263 | 
 264 | --------------------------------------------------------------------------------
 265 | -- Num
 266 | --------------------------------------------------------------------------------
 267 | 
 268 | public export
 269 | {n : Nat} -> Num (Fin (S n)) where
 270 |   FZ + y = y
 271 |   (+) {n = S _} (FS x) y = finS $ assert_smaller x (weaken x) + y
 272 | 
 273 |   FZ * y = FZ
 274 |   (FS x) * y = y + (assert_smaller x $ weaken x) * y
 275 | 
 276 |   fromInteger = restrict n
 277 | 
 278 | public export
 279 | {n : Nat} -> Neg (Fin (S n)) where
 280 |   negate = finS . complement
 281 | 
 282 |   x - y = x + (negate y)
 283 | 
 284 | --------------------------------------------------------------------------------
 285 | -- DecEq
 286 | --------------------------------------------------------------------------------
 287 | 
 288 | public export
 289 | DecEq (Fin n) where
 290 |   decEq FZ FZ = Yes Refl
 291 |   decEq (FS f) (FS f') = decEqCong $ decEq f f'
 292 |   decEq FZ (FS f) = No absurd
 293 |   decEq (FS f) FZ = No absurd
 294 | 
 295 | namespace Equality
 296 | 
 297 |   ||| Pointwise equality of Fins
 298 |   ||| It is sometimes complicated to prove equalities on type-changing
 299 |   ||| operations on Fins.
 300 |   ||| This inductive definition can be used to simplify proof. We can
 301 |   ||| recover proofs of equalities by using `homoPointwiseIsEqual`.
 302 |   public export
 303 |   data Pointwise : Fin m -> Fin n -> Type where
 304 |     FZ : Pointwise FZ FZ
 305 |     FS : Pointwise k l -> Pointwise (FS k) (FS l)
 306 | 
 307 |   export infix 6 ~~~
 308 |   ||| Convenient infix notation for the notion of pointwise equality of Fins
 309 |   public export
 310 |   (~~~) : Fin m -> Fin n -> Type
 311 |   (~~~) = Pointwise
 312 | 
 313 |   export
 314 |   Uninhabited (FS k ~~~ FZ) where
 315 |     uninhabited FZ impossible
 316 |     uninhabited (FS _) impossible
 317 | 
 318 |   export
 319 |   Uninhabited (FZ ~~~ FS k) where
 320 |     uninhabited FZ impossible
 321 |     uninhabited (FS _) impossible
 322 | 
 323 |   ||| Pointwise equality is reflexive
 324 |   export
 325 |   reflexive : {k : Fin m} -> k ~~~ k
 326 |   reflexive {k = FZ} = FZ
 327 |   reflexive {k = FS k} = FS reflexive
 328 | 
 329 |   ||| Pointwise equality is symmetric
 330 |   export
 331 |   symmetric : k ~~~ l -> l ~~~ k
 332 |   symmetric FZ = FZ
 333 |   symmetric (FS prf) = FS (symmetric prf)
 334 | 
 335 |   ||| Pointwise equality is transitive
 336 |   export
 337 |   transitive : j ~~~ k -> k ~~~ l -> j ~~~ l
 338 |   transitive FZ FZ = FZ
 339 |   transitive (FS prf) (FS prg) = FS (transitive prf prg)
 340 | 
 341 |   ||| Pointwise equality is compatible with coerce
 342 |   export
 343 |   coerceEq : {k : Fin m} -> (0 eq : m = n) -> coerce eq k ~~~ k
 344 |   coerceEq {k = FZ} Refl = FZ
 345 |   coerceEq {k = FS k} Refl = FS (coerceEq _)
 346 | 
 347 |   ||| The actual proof used by coerce is irrelevant
 348 |   export
 349 |   congCoerce : {0 n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
 350 |                {0 eq1 : m = n} -> {0 eq2 : p = q} ->
 351 |                k ~~~ l ->
 352 |                coerce eq1 k ~~~ coerce eq2 l
 353 |   congCoerce eq
 354 |     = transitive (coerceEq _)
 355 |     $ transitive eq $ symmetric $ coerceEq _
 356 | 
 357 |   ||| Last is congruent wrt index equality
 358 |   export
 359 |   congLast : {m : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
 360 |   congLast Refl = reflexive
 361 | 
 362 |   export
 363 |   congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l
 364 |   congShift Z prf = prf
 365 |   congShift (S m) prf = FS (congShift m prf)
 366 | 
 367 |   ||| WeakenN is congruent wrt pointwise equality
 368 |   export
 369 |   congWeakenN : k ~~~ l -> weakenN n k ~~~ weakenN n l
 370 |   congWeakenN FZ = FZ
 371 |   congWeakenN (FS prf) = FS (congWeakenN prf)
 372 | 
 373 |   ||| Pointwise equality is propositional equality on Fins that have the same type
 374 |   export
 375 |   homoPointwiseIsEqual : {0 k, l : Fin m} -> k ~~~ l -> k === l
 376 |   homoPointwiseIsEqual FZ = Refl
 377 |   homoPointwiseIsEqual (FS prf) = cong FS (homoPointwiseIsEqual prf)
 378 | 
 379 |   ||| Pointwise equality is propositional equality modulo transport on Fins that
 380 |   ||| have provably equal types
 381 |   export
 382 |   hetPointwiseIsTransport :
 383 |      {0 k : Fin m} -> {0 l : Fin n} ->
 384 |      (0 eq : m === n) -> k ~~~ l -> k === rewrite eq in l
 385 |   hetPointwiseIsTransport Refl = homoPointwiseIsEqual
 386 | 
 387 |   export
 388 |   finToNatQuotient : k ~~~ l -> finToNat k === finToNat l
 389 |   finToNatQuotient FZ = Refl
 390 |   finToNatQuotient (FS prf) = cong S (finToNatQuotient prf)
 391 | 
 392 |   ||| Propositional equality on `finToNat`s implies pointwise equality on the `Fin`s themselves
 393 |   export
 394 |   finToNatEqualityAsPointwise : (k : Fin m) ->
 395 |                                 (l : Fin n) ->
 396 |                                 finToNat k = finToNat l ->
 397 |                                 k ~~~ l
 398 |   finToNatEqualityAsPointwise FZ FZ _ = FZ
 399 |   finToNatEqualityAsPointwise FZ (FS _) prf = absurd prf
 400 |   finToNatEqualityAsPointwise (FS _) FZ prf = absurd prf
 401 |   finToNatEqualityAsPointwise (FS k) (FS l) prf = FS $ finToNatEqualityAsPointwise k l (injective prf)
 402 | 
 403 |   export
 404 |   weakenNeutral : (k : Fin n) -> weaken k ~~~ k
 405 |   weakenNeutral FZ = FZ
 406 |   weakenNeutral (FS k) = FS (weakenNeutral k)
 407 | 
 408 |   export
 409 |   weakenNNeutral : (0 m : Nat) -> (k : Fin n) -> weakenN m k ~~~ k
 410 |   weakenNNeutral m FZ = FZ
 411 |   weakenNNeutral m (FS k) = FS (weakenNNeutral m k)
 412 |