Как я могу организовать сопоставление с образцом в зависимом представлении?

Я написал несколько простых типов для просмотра значений 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])

и поскольку ++ не является инъективным, мне нужно поработать магией, чтобы убедить контролер типов в том, что все имеет смысл. Но я недостаточно хорошо это понимаю, чтобы сказать наверняка.


dependent-type idris
person dfeuer    schedule 22.04.2015    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Наконец-то я понял! Я полагаю, что должен быть лучший способ, но это работает.

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

Редактировать

Дэвид Кристиансен предлагает исключить vectLengthConv и вместо этого использовать cong {f=\len=>Vect len a} (plusLeftCancel n k 1 prf) в предложении with. Это немного помогает.

person dfeuer    schedule 22.04.2015