CODEWITHSUNDEEP
listagda
Musa Al-hassy
Musa Al-hassy

Reputation: 982

Lookup on an argument of a concatenation is just lookup on the whole concatenation using a raised or injected index

I needed to use lists for something I'm doing and needed look-up,

open import Data.List.Properties
open import Data.List
open import Data.Fin

infix 10 _‼_
_‼_ : ∀ {X : Set} → (xs : List X) → Fin (length xs) → X
[] ‼ ()
(x ∷ xs) ‼ fzero = x
(x ∷ xs) ‼ fsuc i = xs ‼ i

I had to define it myself since I could not find it in the libraries. I wish the libraries where easier to navigate and search. Any suggestions on better navigating or searching the libraries is much appreciated.

I wanted to show that look-ups on one argument of a concatenation is just lookup on the whole concatenation using a raised or injected index, namely

open import Relation.Binary.PropositionalEquality

‼-upper : ∀ {X} (pre main : List X) (i : Fin (length main))
      → let #pre+i = subst Fin (sym (length-++ pre)) (raise (length pre) i)in
      (pre ++ main) ‼ #pre+i ≡ main ‼ i
‼-upper = ?

and dually

open import Data.Nat
open import Relation.Binary using
open DecTotalOrder decTotalOrder renaming (refl to ≤ℕ-refl ; trans to ≤ℕ-trans ; reflexive to ≤ℕ-reflexive)

open import Data.Nat.Properties

‼-lower : ∀ {X} (main pos : List X) (i : Fin (length main))
      → let i∶Fin#m++p = inject≤ i (≤ℕ-trans (m≤m+n _ (length pos) (≤ℕ-reflexive (sym (length-++ main)))) in
      (main ++ pos) ‼ i∶Fin#m++p ≡ main ‼ i  
‼-lower = {!!}

I originally proved these two for a variant of vectors, Fin n → X, and used pasting of such sequences in place of concatenation. Now I just want to do the same thing but for the usual List datatype. Any advice is appreciated.

Upvotes: 3

Views: 48

Answers (1)

effectfully
effectfully

Reputation: 12715

Usually, when you have subst at the type level (which is a rather bad situation) you can eliminate it with rewrite at the value level. So let's try it:

‼-upper : ∀ {X} (pre main : List X) (i : Fin (length main))
      → let #pre+i = subst Fin (sym (length-++ pre)) (raise (length pre) i)in
      (pre ++ main) ‼ #pre+i ≡ main ‼ i
‼-upper  []       main i = refl
‼-upper (x ∷ pre) main i rewrite length-++ pre {main} = ?

Agda refuses:

w != foldr (λ _ → suc) 0 (pre ++ main) of type ℕ
when checking that the type

OK, something clashes with something. To remove this clashing we can instead rewrite by a "bigger" equation:

lem : ∀ {n m} (i : Fin n) (p : m ≡ n)
    -> subst Fin (sym (cong suc p)) (fsuc i) ≡ fsuc (subst Fin (sym p) i)
lem i refl = refl

‼-upper : ∀ {X} (pre main : List X) (i : Fin (length main))
      → let #pre+i = subst Fin (sym (length-++ pre)) (raise (length pre) i)in
      (pre ++ main) ‼ #pre+i ≡ main ‼ i
‼-upper  []       main i = refl
‼-upper (x ∷ pre) main i rewrite lem (raise (length pre) i) (length-++ pre {main})
                               = ‼-upper pre main i

I guess ‼-lower is similar (also, it should be simpler if you replace inject≤ with inject+, see lookup-++-inject+ in Data.Vec.Properties). An alternative way is to define specialized versions of raise and inject:

raise-length : ∀ {α} {A : Set α}
             -> (xs ys : List A) -> Fin (length ys) -> Fin (length (xs ++ ys))
raise-length  []      ys i = i
raise-length (x ∷ xs) ys i = fsuc (raise-length xs ys i)

inject-length : ∀ {α} {A : Set α} {ys}
             -> (xs : List A) -> Fin (length xs) -> Fin (length (xs ++ ys))
inject-length  []       ()
inject-length (x ∷ xs)  fzero   = fzero
inject-length (x ∷ xs) (fsuc i) = fsuc (inject-length xs i)

‼-upper : ∀ {X} (pre main : List X) (i : Fin (length main))
        -> (pre ++ main) ‼ raise-length pre main i ≡ main ‼ i
‼-upper  []       main i = refl
‼-upper (x ∷ pre) main i = ‼-upper pre main i

‼-lower : ∀ {X} (main pos : List X) (i : Fin (length main))
        -> (main ++ pos) ‼ inject-length main i ≡ main ‼ i  
‼-lower  []        pos  ()
‼-lower (x ∷ main) pos  fzero   = refl
‼-lower (x ∷ main) pos (fsuc i) = ‼-lower main pos i

But I would simply use some form of vectors — why complicate your life?

Upvotes: 1

Related Questions