我可以在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.tailLHS 的保证定义会减少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