Idris rewrite 没有改变类型答案

【问题标题】：Idris rewrite did not change the typeIdris rewrite 没有改变类型
【发布时间】：2018-10-25 08:36:03
【问题描述】：

我试图证明这一点在将 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

【解决方案1】：

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

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

【讨论】：