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 は、ニクシングvectLengthConvを提案し、代わりに節で使用cong {f=\len=>Vect len a} (plusLeftCancel n k 1 prf)します。withこれは少し役立ちます。

于 2015-04-22T02:22:51.257 に答える