Idris中Stream类型(head s::tail s=s)证明失败：原因及修复？

你的猜想完全正确！Stream的惰性求值特性正是问题的根源，下面我会详细解释原因，并给出两种修复证明的方法。

为什么Vect可以但Stream不行？ #

先回顾两者的定义差异：

• Vect是严格数据类型，构造器(::)直接接受另一个Vect作为参数：

  data Vect : Nat -> Type -> Type where
    Nil : Vect Z a
    (::) : a -> Vect n a -> Vect (S n) a
  

  当你模式匹配(x::xs)时，tail (x::xs)直接归约为xs，所以head s :: tail s就是x::xs，和s完全一致，Refl自然能通过类型检查。

• Stream是惰性数据类型，构造器(::)的第二个参数是Delay (Stream a)（延迟求值的流）：

  data Stream : Type -> Type where
    (::) : (x : a) -> (xs : Delay (Stream a)) -> Stream a
  

  tail的定义是提取延迟内部的值：

  tail : Stream a -> Stream a
  tail (_ :: xs) = force xs
  

  当你模式匹配s为(x::xs)时，xs是Delay (Stream a)类型，而非直接的Stream a。此时head s :: tail s展开后是x :: Delay (force xs)，而s本身是x :: xs。虽然Delay (force xs)和xs在语义上相等，但Idris默认不会自动展开Delay内部的表达式——这是为了避免触发无限求值循环，所以类型检查器无法识别两者的等价性，导致你的原始代码报错。

修复证明的方法 #

方法1：用rewrite显式引入延迟求值的等价性 #

Idris提供了内置定理Delay.forceDelay，它的类型是Delay (force d) = d（对任意d : Delay a成立）。我们可以用rewrite告诉类型检查器这个等价关系，让它能将左边的表达式归约到和右边一致：

hts : (s : Stream a) -> head s :: tail s = s
hts (x :: xs) = rewrite sym (Delay.forceDelay xs) in Refl

如果Delay.forceDelay不可用（比如不同版本的Idris），你也可以自己定义一个辅助定理：

delayForce : (d : Delay a) -> Delay (force d) = d
delayForce d = Refl

然后用这个定理完成证明：

hts : (s : Stream a) -> head s :: tail s = s
hts (x :: xs) = rewrite sym (delayForce xs) in Refl

方法2：用等式推理逐步展开 #

如果你想更清晰地展示每一步的归约过程，可以用等式推理显式写出转换步骤：

hts : (s : Stream a) -> head s :: tail s = s
hts (x :: xs) =
  let -- 第一步：展开head和tail的定义
      step1 : head (x::xs) :: tail (x::xs) = x :: force xs
      step1 = Refl
      -- 第二步：把force xs包装回Delay，匹配Stream构造器的要求
      step2 : x :: force xs = x :: Delay (force xs)
      step2 = Refl
      -- 第三步：利用Delay和force的等价性，将Delay(force xs)替换为xs
      step3 : x :: Delay (force xs) = x :: xs
      step3 = cong (x ::_) (delayForce xs)
  in trans step1 (trans step2 step3)

这里cong是同余定理，它表示如果a = b，那么f a = f b——我们用它将Delay(force xs) = xs的等价关系传递给x ::_这个构造函数。

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