Идрис переписать не изменил тип - PullRequest
Новая
       11

Идрис переписать не изменил тип

0 голосов
/ 15 мая 2018

Я пытаюсь доказать, что после разбиения Vect на три части длина каждой части меньше, чем у исходного вектора.И вот моя реализация: 

||| Split into three parts: two lists and a single element
data Sp : Type -> Type where
 MkSp : List a -> a -> List a -> Sp a

||| cons an element into the left list
spConsL : a -> Sp a -> Sp a
spConsL x (MkSp xs y ys) = MkSp (x :: xs) y ys

||| split a vector according to a predicate
sp : (a -> Bool) -> Bool -> Vect (S l) a -> Sp a
sp f b (x :: []) = MkSp [] x []
sp f False (x :: (y :: xs)) =
  let s' = sp f (f x) (y :: xs)
  in  spConsL x s'
sp f True (x :: xs) = MkSp [] x (toList xs)

||| get the left list from a split
lSp : Sp a -> List a
lSp (MkSp xs x ys) = xs


spConsLEq : {x : a} -> {s : Sp a} ->
            x :: (lSp s) = lSp (spConsL x s)
spConsLEq {x} {s = (MkSp xs y ys)} = Refl


lSpLTE : (vect : Vect (S len) a) ->
         (p : a -> Bool) ->
         (b : Bool) ->
         length (lSp (sp p b vect)) `LTE` S len
lSpLTE (x :: []) p b = LTEZero
lSpLTE (x :: (y :: xs)) p True = LTEZero
lSpLTE (x :: (y :: xs)) p False =
  let ih = lSpLTE (y :: xs) p (p x)
  in  rewrite sym spConsLEq in
      ?lSpLTE_rhs_1

Но, к сожалению, idris выдаст ошибку: 

rewriting
  lSp (spConsL x s) to x :: lSp s
did not change type
  (length
    (lSp (spConsL x (sp p (p x) (y :: xs)))))
  `LTE`
  (S (S len))

И даже после того, как я ввел s следующим образом, ошибка все еще произошла 

rewrite sym $ spConsLEq {s = sp p (p x) (y :: xs)}

Так почему же здесь нельзя переписать работу?

1 Ответ

0 голосов
/ 15 мая 2018

У меня нет удовлетворительного ответа на вопрос "почему?"вопрос, но вы очень близки к полному доказательству.Со следующей модификацией перезапись завершается успешно: 

let ih = lSpLTE (y :: xs) p (p x)
    rule = spConsLEq {x} {s = sp p (p x) (y :: xs)}
in rewrite sym rule in ?hole

И замена LTESucc ih для отверстия завершает доказательство: 

rewrite sym eq in LTESucc ih

Так что, кажется, и {s}, и {x}необходимо указать spConsLEq, а LTESucc выполняет роль следующей леммы: 

lemma : {xs : List a} -> LTE (length xs) k -> LTE (length (_ :: xs)) (S k)
lemma = LTESucc
...