Prelude.Lists.Indexed

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)