1

我写了一些简单的类型来查看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])

并且由于++不是单射的，我需要使用某种魔法来让类型检查器相信事情是有意义的。但我对这一点理解得不够清楚，不能肯定地说。

4

1 回答 1

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 建议在子句中使用nixingvectLengthConv并改为使用。这有点帮助。cong {f=\len=>Vect len a} (plusLeftCancel n k 1 prf)with

于 2015-04-22T02:22:51.257 回答