0 | ||| Indexing into Lists.
  1 | |||
  2 | ||| `Elem` proofs give existential quantification that a given element
  3 | ||| *is* in the list, but not where in the list it is!  Here we give a
  4 | ||| predicate that presents proof that a given index in a list, given
  5 | ||| by a natural number, will return a certain element.
  6 |
  7 | module Data.List.AtIndex
  8 |
  9 | import Data.DPair
 10 | import Data.List.HasLength
 11 | import Data.Nat
 12 | import Decidable.Equality
 13 |
 14 | %default total
 15 |
 16 | ||| @AtIndex witnesses the fact that a natural number encodes a membership proof.
 17 | ||| It is meant to be used as a runtime-irrelevant gadget to guarantee that the
 18 | ||| natural number is indeed a valid index.
 19 | public export
 20 | data AtIndex : a -> List a -> Nat -> Type where
 21 |   Z : AtIndex a (a :: as) Z
 22 |   S : AtIndex a as n -> AtIndex a (b :: as) (S n)
 23 |
 24 | ||| Inversion principle for Z constructor
 25 | export
 26 | inverseZ : AtIndex x (y :: xs) Z -> x === y
 27 | inverseZ Z = Refl
 28 |
 29 | ||| inversion principle for S constructor
 30 | export
 31 | inverseS : AtIndex x (y :: xs) (S n) -> AtIndex x xs n
 32 | inverseS (S p) = p
 33 |
 34 | ||| An empty list cannot possibly have members
 35 | export
 36 | Uninhabited (AtIndex a [] n) where
 37 |   uninhabited Z impossible
 38 |   uninhabited (S _) impossible
 39 |
 40 | ||| For a given list and a given index, there is only one possible value
 41 | ||| stored at that index in that list
 42 | export
 43 | atIndexUnique : AtIndex a as n -> AtIndex b as n -> a === b
 44 | atIndexUnique Z Z = Refl
 45 | atIndexUnique (S p) (S q) = atIndexUnique p q
 46 |
 47 | ||| Provided that equality is decidable, we can look for the first occurrence
 48 | ||| of a value inside of a list
 49 | public export
 50 | find : DecEq a => (x : a) -> (xs : List a) -> Dec (Subset Nat (AtIndex x xs))
 51 | find x [] = No (\ p => void (absurd (snd p)))
 52 | find x (y :: xs) with (decEq x y)
 53 |   find x (x :: xs) | Yes Refl = Yes (Element Z Z)
 54 |   find x (y :: xs) | No neqxy = case find x xs of
 55 |       Yes (Element n prf) => Yes (Element (S n) (S prf))
 56 |       No notInxs => No $ \case
 57 |         (Element Z p) => void (neqxy (inverseZ p))
 58 |         (Element (S n) prf) => absurd (notInxs (Element n (inverseS prf)))
 59 |
 60 | ||| Given an index, we can decide whether there is a value corresponding to it
 61 | public export
 62 | lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\ x => AtIndex x xs n))
 63 | lookup n [] = No (\ p => void (absurd (snd p)))
 64 | lookup Z (x :: xs) = Yes (Element x Z)
 65 | lookup (S n) (x :: xs) = case lookup n xs of
 66 |   Yes (Element x p) => Yes (Element x (S p))
 67 |   No notInxs => No (\ (Element x p) => void (notInxs (Element x (inverseS p))))
 68 |
 69 | ||| An AtIndex proof implies that n is less than the length of the list indexed into
 70 | public export
 71 | inRange : (n : Nat) -> (xs : List a) -> (0 _ : AtIndex x xs n) -> LTE n (length xs)
 72 | inRange n [] p = void (absurd p)
 73 | inRange Z (x :: xs) p = LTEZero
 74 | inRange (S n) (x :: xs) p = LTESucc (inRange n xs (inverseS p))
 75 |
 76 | ||| An index remains unchanged if we extend the list to the right
 77 | export
 78 | weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n
 79 | weakenR Z = Z
 80 | weakenR (S p) = S (weakenR p)
 81 |
 82 | ||| An index into `xs` is shifted by `m` if we prepend a list of size `m`
 83 | ||| in front of it
 84 | export
 85 | weakenL : (p : Subset Nat (flip HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n)
 86 | weakenL m p with (view m)
 87 |   weakenL (Element 0 Z) p | Z = p
 88 |   weakenL (Element (S (fst m)) (S (snd m))) p | (S m) = S (weakenL m p)
 89 |
 90 | ||| Conversely to `weakenR`, if an index is smaller than the length of
 91 | ||| a prefix then it points into that prefix.
 92 | export
 93 | strengthenL : (p : Subset Nat (flip HasLength xs)) ->
 94 |               lt n (fst p) === True ->
 95 |               AtIndex x (xs ++ ys) n -> AtIndex x xs n
 96 | strengthenL m lt idx with (view m)
 97 |   strengthenL (Element (S (fst m)) (S (snd m))) lt Z | (S m) = Z
 98 |   strengthenL (Element (S (fst m)) (S (snd m))) lt (S k) | (S m) = S (strengthenL m lt k)
 99 |
100 | ||| Conversely to `weakenL`, if an index is larger than the length of
101 | ||| a prefix then it points into the suffix.
102 | export
103 | strengthenR : (p : Subset Nat (flip HasLength ws)) ->
104 |               lte (fst p) n === True ->
105 |               AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p))
106 | strengthenR m lt idx with (view m)
107 |   strengthenR (Element 0 Z) lt idx | Z = rewrite minusZeroRight n in idx
108 |   strengthenR (Element (S (fst m)) (S (snd m))) lt (S k) | (S m) = strengthenR m lt k
109 |