0 | module Data.Vect.Properties.Fin
 1 |
 2 | import Data.Vect
 3 | import Data.Vect.Elem
 4 | import Data.Vect.Extra
 5 | import Data.Fin
 6 | import Data.Nat
 7 |
 8 | ||| Witnesses non-empty runtime-irrelevant vectors. Analogous to Data.List.NonEmpty
 9 | public export
10 | data NonEmpty : Vect n a -> Type where
11 |   IsNonEmpty : NonEmpty (x :: xs)
12 |
13 | ||| eta-law (extensionality) of head-tail cons
14 | export
15 | etaCons : (xs : Vect (S n) a) -> head xs :: tail xs = xs
16 | etaCons (x :: xs) = Refl
17 |
18 | ||| Inhabitants of `Fin n` witness `NonZero n`
19 | export
20 | finNonZero : Fin n -> NonZero n
21 | finNonZero  FZ    = ItIsSucc
22 | finNonZero (FS i) = ItIsSucc
23 |
24 | ||| Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty
25 | export
26 | finNonEmpty : (0 xs : Vect n a) -> NonZero n -> NonEmpty xs
27 | finNonEmpty xs ItIsSucc = replace {p = NonEmpty} (etaCons xs) IsNonEmpty
28 |
29 | ||| Cast an index into a runtime-irrelevant `Vect` into the position
30 | ||| of the corresponding element
31 | public export
32 | finToElem : (0 xs : Vect n a) -> (i : Fin n) -> (index i xs) `Elem` xs
33 | finToElem  {n      }       xs  i with (finNonEmpty xs $ finNonZero i)
34 |  finToElem {n = S n} (x :: xs)  FZ    | IsNonEmpty = Here
35 |  finToElem {n = S n} (x :: xs) (FS i) | IsNonEmpty = There (finToElem xs i)
36 |
37 | ||| Analogous to `indexNaturality`, but morphisms can (irrelevantly) know the context
38 | export
39 | indexNaturalityWithElem : (i : Fin n) -> (xs : Vect n a) -> (f : (x : a) -> (0 pos : x `Elem` xs) -> b)
40 |   -> index i (mapWithElem xs f) = f (index i xs) (finToElem xs i)
41 | indexNaturalityWithElem  {n    } i       xs  f with (finNonEmpty xs (finNonZero i))
42 |  indexNaturalityWithElem {n = _}  FZ    (x :: xs) f | IsNonEmpty = Refl
43 |  indexNaturalityWithElem {n = _} (FS i) (x :: xs) f | IsNonEmpty = indexNaturalityWithElem i xs _
44 |