我可以在Idris中证明（s：Stream a） - >（head s :: tail s = s）吗？

Question

以下Idris证明没有进行类型检查。

hts : (s : Stream a) -> (head s :: tail s = s)
hts (x::xs) = Refl

我得到的错误是：

    Type mismatch between
            x :: Delay xs = x :: Delay xs
    and
            x :: Delay (tail (x :: Delay xs)) = x :: Delay xs

非空Vects类型检查的类似证据就好了：

import Data.Vect
htv : (s : Vect (S k) a) -> (head s :: tail s = s)
htv (x::xs) = Refl

所以我猜这个问题是在Stream的懒惰中。

---

我的工作理论是，伊德里斯不喜欢简化Delay内部的任何内容，因为它可能会以这种方式进入无限循环。然而，我想强迫伊德里斯无论如何都要趾高气扬，因为Prelude.Stream.tail的定义保证LHS会减少到x :: Delay xs，完成我的证明。

我的怀疑是否正确？我能以某种方式修复证据吗？

Answer 1

是的，可以做到。我使用了辅助同余引理：

%default total

consCong : {xs, ys : Stream a} -> (x : a) -> xs = ys -> x :: xs = x :: ys
consCong _ Refl = Refl

证明主要引理：

hts : (s : Stream a) -> (head s :: tail s = s)
hts (x :: xs) = consCong _ $ Refl