agda - Agda 中的 splitAt 平等

Question

有人如何证明这种平等

≡splitAt : {α : Level} {A : Set α} {l₁ l₂ : Nat}
         -> (xs₁ : Vec A l₁)
         -> (xs₂ : Vec A l₂)
         -> (xs₁ , xs₂ , refl) ≡ splitAt l₁ (xs₁ ++ xs₂)

? 基本情况很明显

≡splitAt  []       xs₂ = refl

但是之后

≡splitAt (x ∷ xs₁) xs₂

给

Goal: (x ∷ xs₁ , xs₂ , refl) ≡
      (splitAt (suc .n) (x ∷ xs₁ ++ xs₂)
       | splitAt .n (xs₁ ++ xs₂))

这

≡splitAt (x ∷ xs₁) xs₂ with ≡splitAt xs₁ xs₂
... | refl = {!!}

抛出错误：“拒绝解决异构约束 refl ...”。

还有这个

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ with splitAt l₁ (xs₁ ++ xs₂)
...                                  | (xs₁' , xs₂' , refl)

引发错误：“xs₁ != xs₁' 类型为 Vec A l₁...”。我写了这个定义：

++≡++ : {α : Level} {A : Set α} {l₁ l₂ : Nat}
      -> (xs₁ : Vec A l₁)
      -> (xs₂ : Vec A l₂)
      -> (xs₁' : Vec A l₁)
      -> (xs₂' : Vec A l₂)
      -> xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'
++≡++ _ _ _ _ = {!!}

但是不知道怎么用。

也许有一些来源，我可以从中了解更多关于 with-expressions 的信息？

谢谢。

Answer 1