Idris rewrite无法修改类型问题：向量拆分长度证明报错

我正在尝试证明将Vect拆分为三部分后，左侧列表的长度小于等于原向量的长度，但在使用rewrite步骤时遇到了困惑——Idris提示改写没有改变目标类型，即使我显式指定了参数。下面是我的实现代码：

||| 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)}

问题原因 #

其实这里的rewrite完全是多余的——因为spConsLEq的证明是基于定义上的相等（Refl），也就是说lSp (spConsL x s)和x :: lSp s在Idris的类型系统中本来就是可转换的。Idris已经知道这两个表达式的长度是相等的，所以当你尝试用rewrite改写时，它会提示“没有改变类型”——因为这两个表达式的类型在Idris看来已经是完全一样的。

你的目标是证明length (lSp (spConsL x s)) LTE S (S len)，而递归假设ih是length (lSp s) LTE S len。由于length (lSp (spConsL x s))定义上等于length (x :: lSp s)，也就是S (length (lSp s))，你只需要利用succLTEsucc规则，把递归假设的两边都加上S，就能得到目标结论。

解决方法 #

直接去掉rewrite步骤，用succLTEsucc ih填充洞即可：

lSpLTE (x :: (y :: xs)) p False = 
  let ih = lSpLTE (y :: xs) p (p x) 
  in succLTEsucc ih

这样Idris就能顺利通过类型检查，因为：

1. length (lSp (spConsL x s))自动转换为S (length (lSp s))
2. succLTEsucc ih将length (lSp s) LTE S len转换为S (length (lSp s)) LTE S (S len)，正好匹配目标类型

内容的提问来源于stack exchange，提问作者w0mTea