如何安排在依赖视图上进行模式匹配？

Question

我写了一些用于查看 Vect 值的简单类型：

data SnocVect : Vect n a -> Type where
  SnocNil : SnocVect []
  Snoc : (xs : Vect n a) -> (x : a) -> SnocVect (xs ++ [x])

data Split : (m : Nat) -> Vect n a -> Type where
  MkSplit : (xs : Vect j a) -> (ys : Vect k a) ->
              Split j (xs ++ ys)

现在在我看来完全合理的是，如果我有一个 Split 分隔向量的最后一个元素，我应该能够将其转换为 SnocVect:

splitToSnocVect : .{xs : Vect (S n) a} -> Split n xs ->
    SnocVect xs

不幸的是，我似乎找不到任何方法来实现这个东西。特别是，我还没有找到任何方法让它让我在 Split n xs 参数上进行模式匹配，没有它我显然无法到达任何地方。我认为基本问题是我有一些类型

Split j (ps ++ [p])

并且由于 ++ 不是单射的，我需要使用某种魔法来说服类型检查器事情是有意义的。但我不太了解这一点，无法肯定地说。

Answer 1

我终于明白了！我想必须是更好的方法，但这行得通。

vectLengthConv : {auto a : Type} -> m = n ->
                    Vect m a = Vect n a
vectLengthConv prf = rewrite prf in Refl

splitToSnocVect' : .(n : Nat) -> .(xs : Vect m a) ->
              .(m = n+1) -> Split n xs -> SnocVect xs
splitToSnocVect' n (ys ++ zs) prf (MkSplit {k} ys zs) 
     with (vectLengthConv (plusLeftCancel n k 1 prf))

  splitToSnocVect' n (ys ++ []) prf
      (MkSplit {k = Z} ys []) | Refl impossible

  splitToSnocVect' n (ys ++ (z :: [])) prf 
     (MkSplit {k = (S Z)} ys (z :: [])) | lenconv =
        Snoc ys z

  splitToSnocVect' n (ys ++ zs) prf 
    (MkSplit {k = (S (S k))} ys zs) | Refl impossible

splitToSnocVect : .{n : Nat} -> .{xs : Vect (S n) a} ->
                       Split n xs -> SnocVect xs
splitToSnocVect {n} {xs} splt =
    splitToSnocVect' n xs (plusCommutative 1 n) splt

编辑

David Christiansen 建议放弃 vectLengthConv 并在 with 子句中使用 cong {f=\len=>Vect len a} (plusLeftCancel n k 1 prf)。这有点帮助。

如何安排在依赖视图上进行模式匹配？

How can I arrange to pattern match on a dependent view?

dependent-type

idris

编辑