时间戳

首页 > 解决方案 > Idris rewrite 没有改变类型

idris - Idris rewrite 没有改变类型

问题描述

我试图证明将 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)}

那么为什么不能在这里重写工作呢？

标签： idris

解决方案

对于“为什么”，我没有满意的答案。问题，但是您非常接近完整的证明。通过以下修改，重写成功：

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

推荐阅读