<commit_before>module Prelude.Fin

import Prelude.Nat
import Prelude.Either
import Prelude.Uninhabited

%default total

||| Numbers strictly less than some bound.  The name comes from "finite sets".
|||
||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
||| exceedingly inefficient at run time.
||| @ n the upper bound
data Fin : (n : Nat) -> Type where
    fZ : Fin (S k)
    fS : Fin k -> Fin (S k)

instance Uninhabited (Fin Z) where
  uninhabited fZ impossible
  uninhabited (fS f) impossible

fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n
fSInjective left _ refl = refl

instance Eq (Fin n) where
    (==) fZ fZ = True
    (==) (fS k) (fS k') = k == k'
    (==) _ _ = False

||| There are no elements of `Fin Z`
FinZAbsurd : Fin Z -> _|_
FinZAbsurd fZ impossible

FinZElim : Fin Z -> a
FinZElim x = FalseElim (FinZAbsurd x)

||| Convert a Fin to a Nat
finToNat : Fin n -> Nat
finToNat fZ = Z
finToNat (fS k) = S (finToNat k)

||| `finToNat` is injective
finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
finToNatInjective fZ     fZ     refl = refl
finToNatInjective (fS m) fZ     refl impossible
finToNatInjective fZ     (fS n) refl impossible
finToNatInjective (fS m) (fS n) prf  =
  cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf)) 

instance Cast (Fin n) Nat where
    cast x = finToNat x

||| Convert a Fin to an Integer
finToInteger : Fin n -> Integer
finToInteger fZ     = 0
finToInteger (fS k) = 1 + finToInteger k

instance Cast (Fin n) Integer where
    cast x = finToInteger x

||| Weaken the bound on a Fin by 1
weaken : Fin n -> Fin (S n)
weaken fZ     = fZ
weaken (fS k) = fS (weaken k)

||| Weaken the bound on a Fin by some amount
weakenN : (n : Nat) -> Fin m -> Fin (m + n)
weakenN n fZ = fZ
weakenN n (fS f) = fS (weakenN n f)

||| Attempt to tighten the bound on a Fin.
||| Return `Left` if the bound could not be tightened, or `Right` if it could.
strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
strengthen {n = S k} fZ = Right fZ
strengthen {n = S k} (fS i) with (strengthen i)
  strengthen (fS k) | Left x   = Left (fS x)
  strengthen (fS k) | Right x  = Right (fS x)
strengthen f = Left f

||| Add some natural number to a Fin, extending the bound accordingly
||| @ n the previous bound
||| @ m the number to increase the Fin by
shift : (m : Nat) -> Fin n -> Fin (m + n)
shift Z f = f
shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

||| The largest element of some Fin type
last : Fin (S n)
last {n=Z} = fZ
last {n=S _} = fS last

total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
fSinjective refl = refl

<commit_msg>Give Fin an Ord instance.<commit_after>module Prelude.Fin

import Prelude.Nat
import Prelude.Either
import Prelude.Uninhabited

%default total

||| Numbers strictly less than some bound.  The name comes from "finite sets".
|||
||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
||| exceedingly inefficient at run time.
||| @ n the upper bound
data Fin : (n : Nat) -> Type where
    fZ : Fin (S k)
    fS : Fin k -> Fin (S k)

instance Uninhabited (Fin Z) where
  uninhabited fZ impossible
  uninhabited (fS f) impossible

fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n
fSInjective left _ refl = refl

instance Eq (Fin n) where
    (==) fZ fZ = True
    (==) (fS k) (fS k') = k == k'
    (==) _ _ = False

||| There are no elements of `Fin Z`
FinZAbsurd : Fin Z -> _|_
FinZAbsurd fZ impossible

FinZElim : Fin Z -> a
FinZElim x = FalseElim (FinZAbsurd x)

||| Convert a Fin to a Nat
finToNat : Fin n -> Nat
finToNat fZ = Z
finToNat (fS k) = S (finToNat k)

||| `finToNat` is injective
finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
finToNatInjective fZ     fZ     refl = refl
finToNatInjective (fS m) fZ     refl impossible
finToNatInjective fZ     (fS n) refl impossible
finToNatInjective (fS m) (fS n) prf  =
  cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf)) 

instance Cast (Fin n) Nat where
    cast x = finToNat x

||| Convert a Fin to an Integer
finToInteger : Fin n -> Integer
finToInteger fZ     = 0
finToInteger (fS k) = 1 + finToInteger k

instance Cast (Fin n) Integer where
    cast x = finToInteger x

||| Weaken the bound on a Fin by 1
weaken : Fin n -> Fin (S n)
weaken fZ     = fZ
weaken (fS k) = fS (weaken k)

||| Weaken the bound on a Fin by some amount
weakenN : (n : Nat) -> Fin m -> Fin (m + n)
weakenN n fZ = fZ
weakenN n (fS f) = fS (weakenN n f)

||| Attempt to tighten the bound on a Fin.
||| Return `Left` if the bound could not be tightened, or `Right` if it could.
strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
strengthen {n = S k} fZ = Right fZ
strengthen {n = S k} (fS i) with (strengthen i)
  strengthen (fS k) | Left x   = Left (fS x)
  strengthen (fS k) | Right x  = Right (fS x)
strengthen f = Left f

||| Add some natural number to a Fin, extending the bound accordingly
||| @ n the previous bound
||| @ m the number to increase the Fin by
shift : (m : Nat) -> Fin n -> Fin (m + n)
shift Z f = f
shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)

||| The largest element of some Fin type
last : Fin (S n)
last {n=Z} = fZ
last {n=S _} = fS last

total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
fSinjective refl = refl

instance Ord (Fin n) where
  compare  fZ     fZ    = EQ
  compare  fZ    (fS _) = LT
  compare (fS _)  fZ    = GT
  compare (fS x) (fS y) = compare x y
  
{'fraction_non_alphanumeric': 0.12248201438848921, 'fraction_numerical': 0.001079136690647482, 'mean_word_length': 2.9636493228795437, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 45, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4598350', 'n_tokens_mistral': 2218, 'n_tokens_neox': 2146, 'n_words': 903}