lazy-evaluation - 我可以在 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

非空的类似证明 Vect s 类型检查就好了:

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

所以我猜问题在于 Stream 的懒惰.

我的工作理论是 Idris 不喜欢简化 Delay 中的任何内容。 ，因为它可能会以这种方式进入无限循环。但是，无论如何，我想强制Idris 涉足，正如 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