module Data.List.At where open import Data.Nat open import Data.List open import Data.List.All hiding (map; lookup) open import Data.List.Any hiding (map) open import Data.List.Any.Membership.Propositional open import Data.Fin hiding (_<_) open import Data.Maybe hiding (map; All) open import Data.Product hiding (map) open import Relation.Binary.PropositionalEquality open import Relation.Binary.List.Pointwise hiding (refl; map) open import Relation.Nullary maybe-lookup : ∀ {a}{A : Set a} → ℕ → List A → Maybe A maybe-lookup n [] = nothing maybe-lookup zero (x ∷ μ) = just x maybe-lookup (suc n) (x ∷ μ) = maybe-lookup n μ maybe-write : ∀ {a}{A : Set a} → ℕ → A → List A → Maybe (List A) maybe-write n _ [] = nothing maybe-write zero v (x ∷ z) = just (v ∷ z) maybe-write (suc n) v (x ∷ z) = maybe-write n v z _[_]=_ : ∀ {a}{A : Set a} → List A → ℕ → A → Set _ l [ i ]= x = maybe-lookup i l ≡ just x []=-map : ∀ {a b}{A : Set a}{B : Set b}{x} i → (l : List A) → l [ i ]= x → ∀ (f : A → B) → (map f l) [ i ]= (f x) []=-map _ [] () []=-map zero (x ∷ l) refl = λ f → refl []=-map (suc i) (x ∷ l) p = []=-map i l p lookup : ∀ {a} {A : Set a} → (l : List A) → Fin (length l) → A lookup [] () lookup (x ∷ l) zero = x lookup (x ∷ l) (suc p) = lookup l p at-lookup : ∀ {a}{A : Set a} → (l : List A) → (i : Fin (length l)) → l [ toℕ i ]= (lookup l i) at-lookup [] () at-lookup (x ∷ l) zero = refl at-lookup (x ∷ l) (suc i) = at-lookup l i lookup-in : ∀ {a}{A : Set a} → (l : List A) → (i : Fin (length l)) → (lookup l i) ∈ l lookup-in [] () lookup-in (x ∷ l) zero = here refl lookup-in (x ∷ l) (suc i) = there (lookup-in l i) dec-lookup : ∀ {a} {A : Set a} → (i : ℕ) → (l : List A) → Dec (∃ λ x → l [ i ]= x) dec-lookup _ [] = no (λ{ (_ , ())}) dec-lookup zero (x ∷ l) = yes (x , refl) dec-lookup (suc i) (_ ∷ l) = dec-lookup i l all-lookup : ∀ {a} {A : Set a} {l : List A} {i x p P} → l [ i ]= x → All {p = p} P l → P x all-lookup {l = []} () q all-lookup {l = x ∷ l} {zero} refl (px ∷ q) = px all-lookup {l = x ∷ l} {suc i} p (px ∷ q) = all-lookup p q []=-length : ∀ {a} {A : Set a} (L : List A) {i x} → L [ i ]= x → i < length L []=-length [] () []=-length (x ∷ L) {zero} refl = s≤s z≤n []=-length (x ∷ L) {suc i} p = s≤s ([]=-length L p) ∷ʳ[length] : ∀ {a} {A : Set a} (l : List A) x → (l ∷ʳ x) [ length l ]= x ∷ʳ[length] [] y = refl ∷ʳ[length] (x ∷ Σ) y = ∷ʳ[length] Σ y pointwise-lookup : ∀ {a b ℓ A B P l m i x} → Rel {a} {b} {ℓ} {A} {B} P l m → l [ i ]= x → ∃ λ y → m [ i ]= y × P x y pointwise-lookup [] () pointwise-lookup {i = zero} (x∼y ∷ q) refl = _ , refl , x∼y pointwise-lookup {i = suc i} (x∼y ∷ q) p = pointwise-lookup q p pointwise-lookup′ : ∀ {a b ℓ A B P l m i x y} → Rel {a} {b} {ℓ} {A} {B} P l m → l [ i ]= x → m [ i ]= y → P x y pointwise-lookup′ [] () q pointwise-lookup′ {i = zero} (x∼y ∷ z) refl refl = x∼y pointwise-lookup′ {i = suc i} (x∼y ∷ z) p q = pointwise-lookup′ z p q