Source code on Github
------------------------------------------------------------------------
-- Indexed operations on lists.

{-# OPTIONS --safe #-}
module Prelude.Lists.Indexed where

open import Prelude.Init; open SetAsType
open L.Mem using (_∈_; ∈-map⁺; mapWith∈)
open Nat   using (_<_; ≤-pred)
open F     using (toℕ; fromℕ<)
open import Prelude.General
open import Prelude.Bifunctor
open import Prelude.InferenceRules
open import Prelude.Split

private variable
  A : Type ; B : Type ℓ′
  P Q : Pred A ℓ″

Index : List A  Type
Index = Fin  length

Index⁺ : List A  Type
Index⁺ = Fin  suc  length

infix 3 _‼_
_‼_ : (vs : List A)  Index vs  A
_‼_ = L.lookup

infix 3 _⁉_
_⁉_ : List A    Maybe A
[]        _     = nothing
(x  xs)  zero  = just x
(x  xs)  suc n = xs  n

remove : (vs : List A)  Index vs  List A
remove []       ()
remove (_  xs) fzero    = xs
remove (x  vs) (fsuc f) = x  remove vs f

_at_⟨_⟩ : (vs : List A)  Index vs  A  List A
[]       at ()        _ 
(_  xs) at fzero     x  = x  xs
(y  vs) at (fsuc f)  x  = y  (vs at f  x )

_at_⟨_⟩remove_ : (vs : List A)  Index vs  A  Index vs  List A
[] at ()  _ ⟩remove ()
(_  vs) at fzero   _  ⟩remove fzero  = vs
(_  vs) at fzero   xv ⟩remove fsuc y = xv  remove vs y
(_  vs) at fsuc x  xv ⟩remove fzero  = vs at x  xv 
(v  vs) at fsuc x  xv ⟩remove fsuc y = v  vs at x  xv ⟩remove y

indices : List A  List 
indices xs = upTo (length xs)

fin-indices : (xs : List A)  List (Index xs)
fin-indices = allFin  length

enumerate : (xs : List A)  List (Index xs × A)
enumerate xs = zip (fin-indices xs) xs

findElem :  {P : Pred₀ A}  Decidable¹ P  List A  Maybe (A × List A)
findElem P? xs with L.Any.any? P? xs
... | yes px = let i = L.Any.index px in just ((xs  i) , remove xs i)
... | no  _  = nothing



private Ix = Index

module _ {A B : Type} where
  private variable xs : List A; ys : List B

  length≡⇒Ix : length xs  length ys  Ix xs  Ix ys
  length≡⇒Ix {[]}{[]} eq =  ()) ,  ())
  length≡⇒Ix {x  xs}{y  ys} eq =
    let IH : Ix xs  Ix ys
        IH = length≡⇒Ix {xs}{ys} $ Nat.suc-injective eq
    in  where 0F  0F; (fsuc i)  fsuc (IH .proj₁ i))
     ,  where 0F  0F; (fsuc i)  fsuc (IH .proj₂ i))

  module ∣length≡⇒Ix∣ (len≡ : length xs  length ys) where
     = (Ix xs  Ix ys)  length≡⇒Ix {xs}{ys} len≡ .proj₁
     = (Ix ys  Ix xs)  length≡⇒Ix {xs}{ys} len≡ .proj₂

length-allFin :  n  length (allFin n)  n
length-allFin n = L.length-tabulate id

module _ {A B : Type} (xs : List A) (ys : List B) where
  length-zip : length (zip xs ys)  length xs  length ys
  length-zip = L.length-zipWith _,_ xs ys

  length-zip≡ˡ : length xs  length ys  length (zip xs ys)  length xs
  length-zip≡ˡ len≡ =
    begin
      length (zip xs ys)
    ≡⟨ length-zip 
      length xs  length ys
    ≡⟨ Nat.m≤n⇒m⊓n≡m $ Nat.≤-reflexive $ len≡ 
      length xs
     where open ≡-Reasoning

  length-zip≡ʳ : length xs  length ys  length (zip xs ys)  length ys
  length-zip≡ʳ len≡ = trans (length-zip≡ˡ len≡) len≡

module _ {A : Type} where
  private variable xs : List A

  length-enumerate : length (enumerate xs)  length xs
  length-enumerate {xs = xs} =
    begin
      length (enumerate xs)
    ≡⟨ length-zip (fin-indices xs) xs 
      length (fin-indices xs)  length xs
    ≡⟨ Nat.m≥n⇒m⊓n≡n $ Nat.≤-reflexive $ sym $ length-allFin (length xs) 
      length xs
     where open ≡-Reasoning

module _ {A B : Type} where
  private variable xs : List A; ys : List B

  open Nat using (_≤_)

  ‼-zip⁺ˡ : Ix xs  {_ : length xs  length ys}  Ix (zip xs ys)
  ‼-zip⁺ˡ {[]}     {_} ()
  ‼-zip⁺ˡ {_  xs} {_  _} = λ where
    0F  0F
    (fsuc i) {s≤s p}  fsuc (‼-zip⁺ˡ {xs} i {p})
  ‼-zip⁺ˡ {_  _} {[]} _ {()}

  ‼-zip⁺ʳ : Ix ys  {_ : length ys  length xs}  Ix (zip xs ys)
  ‼-zip⁺ʳ {[]}     {_} ()
  ‼-zip⁺ʳ {_  ys} {_  xs} = λ where
    0F  0F
    (fsuc i) {s≤s p}  fsuc (‼-zip⁺ʳ {ys}{xs} i {p})
  ‼-zip⁺ʳ {_  _} {[]} _ {()}

  ‼-zip⁻ˡ : Ix (zip xs ys)  Ix xs
  ‼-zip⁻ˡ {[]} {_} ()
  ‼-zip⁻ˡ {_  _} {[]} ()
  ‼-zip⁻ˡ {_  xs} {_  _} = λ where
    0F  0F
    (fsuc i)  fsuc (‼-zip⁻ˡ {xs} i)

  ‼-zip⁻ʳ : Ix (zip xs ys)  Ix ys
  ‼-zip⁻ʳ {[]} {_} ()
  ‼-zip⁻ʳ {_  _} {[]} ()
  ‼-zip⁻ʳ {_  xs} {_  _} = λ where
    0F  0F
    (fsuc i)  fsuc (‼-zip⁻ʳ {xs} i)

  mapWithIx : (xs : List A)  (A  Ix xs  B)  List B
  mapWithIx xs f = map (uncurry (flip f)) $ enumerate xs

  length-mapWithIx : (f : A  Ix xs  B) 
    length (mapWithIx xs f)  length xs
  length-mapWithIx {xs = xs} f
    = trans (L.length-map (uncurry (flip f)) (enumerate xs))
            (length-enumerate {xs = xs})

  length-mapWith∈ : (f :  {x}  x L.Mem.∈ xs  B) 
    length (L.Mem.mapWith∈ xs f)  length xs
  length-mapWith∈ {xs = []} _ = refl
  length-mapWith∈ {xs = _  xs} f = cong suc $ length-mapWith∈ {xs = xs} (f  there)

  module _ (f : A  B) {xs : List A} where
    open ∣length≡⇒Ix∣ {xs = map f xs}{xs} (L.length-map f xs)
      renaming ( to ‼-map⁻;  to ‼-map⁺) public

  module _  {xs : List A} (f :  {x : A}  x  xs  B) where
    open ∣length≡⇒Ix∣ {xs = mapWith∈ xs f}{xs} (length-mapWith∈ {xs = xs} f)
      renaming ( to ‼-mapWith∈⁻;  to ‼-mapWith∈⁺) public

  module _  {xs : List A} (f : A  Ix xs  B) where
    open ∣length≡⇒Ix∣ {xs = mapWithIx xs f}{xs} (length-mapWithIx {xs = xs} f)
      renaming ( to ‼-mapWithIx⁻;  to ‼-mapWithIx⁺) public

module _ {A : Type} {xs : List A} where
  open ∣length≡⇒Ix∣ {xs = enumerate xs}{xs} (length-enumerate {xs = xs})
    renaming ( to ‼-enumerate⁻;  to ‼-enumerate⁺) public

private variable
  m n : 
  x : A; xs ys : List A

-- ** indexℕ

indexℕ : Any P xs  
indexℕ = toℕ  L.Any.index

indexℕ-Any-map :  {f : P ⊆¹ Q}
   (x∈ : Any P xs)
   indexℕ (L.Any.map f x∈)
   indexℕ x∈
indexℕ-Any-map = λ where
  (here _)   refl
  (there p)  cong suc $ indexℕ-Any-map p

indexℕ-Any-map⁺ :  {f : A  B} {P : Pred B }
   (x∈ : Any (P  f) xs)
   indexℕ (L.Any.map⁺ {f = f} {P = P} x∈)
   indexℕ x∈
indexℕ-Any-map⁺ = λ where
  (here _)   refl
  (there p)  cong suc $ indexℕ-Any-map⁺ p

zip-∈ :  {xs : List A} {ys : List B} {x : A} {y : B}
   (x , y)  zip xs ys  (x  xs) × (y  ys)
zip-∈ {xs = _  xs} {_  ys} (here refl) = here refl , here refl
zip-∈ {xs = _  xs} {_  ys} (there xy∈) with zip-∈ xy∈
... | (x∈ , y∈) = there x∈ , there y∈

ix∈→x∈ :  {xs : List A} {i : Index xs} {x : A}
   (i , x)  enumerate xs  x  xs
ix∈→x∈ = proj₂  zip-∈

index⁺ : Any P xs  Index⁺ xs
index⁺ = fsuc  L.Any.index

splitAt :  (xs : List A)  Index⁺ xs  List A × List A
splitAt xs       fzero    = [] , xs
splitAt (x  xs) (fsuc i) = map₁ (x ∷_) (splitAt xs i)

splitAtˡ splitAtʳ :  (xs : List A)  Index⁺ xs  List A
splitAtˡ = proj₁ ∘₂ splitAt
splitAtʳ = proj₂ ∘₂ splitAt

splitAt′ :  (xs : List A)    Maybe (List A × List A)
splitAt′ xs n with n Nat.<? suc (length xs)
... | yes n≤ = just $ splitAt xs (F.fromℕ< {m = n} {n = suc (length xs)} n≤)
... | no  _  = nothing

splitAt≡ : (i : Index⁺ xs)
  splitAt′ xs (toℕ i)  just (splitAt xs i)
splitAt≡ {xs = xs} i
  with toℕ i Nat.<? suc (length xs)
... | yes i≤ = cong just (cong (splitAt xs) (F.fromℕ<-toℕ i i≤))
... | no  i≰ = ⊥-elim $ i≰ (F.toℕ<n i)

splitAt⁺ʳ :  (xs : List A)  Index xs
   Σ[ xsˡ  List⁺ A ] Σ[ xsʳ  List A ]
      L.NE.length xsˡ + length xsʳ  length xs
splitAt⁺ʳ (x  xs) fzero    = x  [] , xs , refl
splitAt⁺ʳ (x  xs) (fsuc i) = let xsˡ , xsʳ , p = splitAt⁺ʳ xs i
                              in  x ∷⁺ xsˡ , xsʳ , cong suc p

instance
  Split-∈ :  {A : Type } {xs : List A} {P : Pred A ℓ′} 
    Any P xs -splitsInto- List A
  Split-∈ {xs = xs} .split = splitAt xs  index⁺

private
  _ : splitAt⁺ʳ (0  1  []) (# 0)  (L.NE.[ 0 ] , [ 1 ] , refl)
  _ = refl

  _ : splitAt⁺ʳ (0  1  []) (# 1)  (0  1  [] , [] , refl)
  _ = refl

length-∈∙left : {xs : List A} (x∈ : Any P xs)  length (x∈ ∙left)  suc (indexℕ x∈)
length-∈∙left {xs = x  xs} (here _) = refl
length-∈∙left {xs = x  xs} (there x∈) rewrite length-∈∙left {xs = xs} x∈ = refl

map-map₁-zip :  {A B C : Type} {xs : List A} {ys : List B} (f : A  C)
   map (map₁ f) (zip xs ys)
   zip (map f xs) ys
map-map₁-zip {xs = []}     {ys = _}      f = refl
map-map₁-zip {xs = _  xs} {ys = []}     f = refl
map-map₁-zip {xs = _  xs} {ys = _  ys} f rewrite map-map₁-zip {xs = xs} {ys = ys} f = refl

enum∈-∷ :  {A : Type} {x y : A} {xs : List A} {i : Index xs}
   (i , y)  enumerate xs
   (fsuc i , y)  enumerate (x  xs)
enum∈-∷ {x = x} {y = y} {xs = xs} {i = i} ix∈
  with ∈-map⁺ (map₁ fsuc) ix∈
... | ix∈′
  rewrite map-map₁-zip {xs = L.tabulate {n = length xs} id} {ys = xs} fsuc
        | L.map-tabulate {n = length xs}  x  x) fsuc
        = there ix∈′

x∈→ix∈ :  {A : Type} {xs : List A} {x : A}
   (x∈ : x  xs)  ((L.Any.index x∈ , x)  enumerate xs)
x∈→ix∈ (here refl) = here refl
x∈→ix∈ {xs = _  xs} (there x∈) = enum∈-∷ (x∈→ix∈ x∈)

mapEnumWith∈ : (xs : List A)  (∀ (i : Index xs) (x : A)  x  xs  B)  List B
mapEnumWith∈ xs f = mapWith∈ (enumerate xs) λ{ {(i , x)} ix∈  f i x (ix∈→x∈ ix∈) }

map∘zip∘tabulate⟨fsuc⟩≈map⟨fsuc⟩∘zip∘tabulate :  {A B : Type} {m : } (xs : List A) {P : Fin (suc m) × A  B} {f : Index xs  Fin m}
  map P (zip (L.tabulate {n = length xs} (fsuc  f)) xs)
  map (P  map₁ fsuc) (zip (L.tabulate {n = length xs} f) xs)
map∘zip∘tabulate⟨fsuc⟩≈map⟨fsuc⟩∘zip∘tabulate [] = refl
map∘zip∘tabulate⟨fsuc⟩≈map⟨fsuc⟩∘zip∘tabulate {A}{B}{m} (x  xs) {P = P} {f = f} = cong (_ ∷_) $ map∘zip∘tabulate⟨fsuc⟩≈map⟨fsuc⟩∘zip∘tabulate {A}{B}{m} xs {P = P} {f = f  fsuc}

‼-suc :  {x : A} {xs : List A} {i : Index xs}
   (x  xs  fsuc i)
   (xs  i)
‼-suc = refl

‼-map :  {xs : List A} {f : A  B}
   Index xs
   Index (map f xs)
‼-map {xs = x  xs} fzero    = fzero
‼-map {xs = x  xs} (fsuc i) = fsuc (‼-map {xs = xs} i)

‼-mapWith∈ :  {xs : List A} {f :  {x}  x  xs  B}
   Index xs
   Index (mapWith∈ xs f)
‼-mapWith∈ {xs = x  xs} fzero    = fzero
‼-mapWith∈ {xs = x  xs} (fsuc i) = fsuc (‼-mapWith∈ {xs = xs} i)

map-‼ :  {xs : List A} {x : A} {f : A  B} (x∈ : x  xs)
   (map f xs  ‼-map {xs = xs} {f = f} (L.Any.index x∈))  f x
map-‼ (here refl) = refl
map-‼ {xs = _  xs} {f = f} (there x∈) rewrite map-‼ {xs = xs} {f = f} x∈ = refl

‼→⁉ :  {xs : List A} {ix : Index xs}
     just (xs  ix)  (xs  toℕ ix)
‼→⁉ {xs = []}     {()}
‼→⁉ {xs = x  xs} {fzero}   = refl
‼→⁉ {xs = x  xs} {fsuc ix} = ‼→⁉ {xs = xs} {ix}

‼-index : (x∈xs : x  xs)
         (xs  L.Any.index x∈xs)  x
‼-index (here refl) = refl
‼-index (there x∈)  rewrite ‼-index x∈ = refl

toℕ< :  (fin : Fin n)  toℕ fin < n
toℕ< fzero    = s≤s z≤n
toℕ< (fsuc f) = s≤s (toℕ< f)

fromℕ<∘toℕ< :  (i : Fin n)  fromℕ< (toℕ< i)  i
fromℕ<∘toℕ< fzero    = refl
fromℕ<∘toℕ< (fsuc i) rewrite fromℕ<∘toℕ< i = refl

‼-fromℕ<∘toℕ< : (i : Index xs)
               (xs  fromℕ< (toℕ< i))  (xs  i)
‼-fromℕ<∘toℕ< i rewrite fromℕ<∘toℕ< i = refl

fromℕ<-≡ : (p₁ : m < length xs)
          (p₂ : m < length xs)
          fromℕ< p₁  fromℕ< p₂
fromℕ<-≡ {m = zero}  {xs = x  xs} p₁ p₂ = refl
fromℕ<-≡ {m = suc m} {xs = x  xs} p₁ p₂ rewrite fromℕ<-≡ {m = m} {xs = xs} (≤-pred p₁) (≤-pred p₂) = refl

‼-fromℕ<-≡ : (p₁ : m < length xs)
            (p₂ : m < length ys)
            xs  ys
            (xs  fromℕ< p₁)
            (ys  fromℕ< p₂)
‼-fromℕ<-≡ {m = m} {xs = xs} p₁ p₂ refl rewrite fromℕ<-≡ {m = m} {xs = xs} p₁ p₂ = refl

proj₁∘find : (x∈xs : x  xs)
            proj₁ (find x∈xs)  x
proj₁∘find (here refl) = refl
proj₁∘find (there x∈)  = proj₁∘find x∈

just-⁉⇒∈ :  {i : }
   (xs  i)  just x
   x  xs
just-⁉⇒∈ {xs = _  _}  {i = zero}  ⁉≡just = here (M.just-injective (sym ⁉≡just))
just-⁉⇒∈ {xs = _  xs} {i = suc i} ⁉≡just = there (just-⁉⇒∈ {xs = xs} {i = i} ⁉≡just)