查找串联的参数只是使用提升或注入的索引查找整个串联

Question

我需要使用列表来处理我正在做的事情并且需要查找，

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

我不得不自己定义它，因为我在库中找不到它。我希望图书馆更容易导航和搜索。 非常感谢任何有关更好地浏览或搜索库的建议。

我想证明对串联的一个参数的查找只是使用提升或注入索引对整个串联的查找，即

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 = ?

和双重

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 = {!!}

我最初证明了这两个向量的变体，Fin n → X，并使用此类序列的粘贴来代替连接。现在我只想做同样的事情，但对于通常的 List 数据类型。任何建议表示赞赏。

Answer 1

通常，当你在类型级别上有 subst 时（这是一个相当糟糕的情况），你可以在值级别上用 rewrite 消除它。那么让我们来试试吧：

‼-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 拒绝：

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

好吧，有些事情与某些事情发生冲突。为了消除这种冲突，我们可以改写为 "bigger" 等式：

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

我猜‼-lower也差不多（另外，如果把inject≤换成inject+应该更简单，见Data.Vec.Properties中的lookup-++-inject+）。另一种方法是定义 raise 和 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

但我会简单地使用某种形式的向量——为什么要让你的生活复杂化？

查找串联的参数只是使用提升或注入的索引查找整个串联

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

list

agda