我可以在 Idris 中证明 (s : Stream a) -> (head s :: tail s = s) 吗？答案

【问题标题】：Can I prove (s : Stream a) -> (head s :: tail s = s) in Idris?我可以在 Idris 中证明 (s : Stream a) -> (head s :: tail s = s) 吗？
【发布时间】：2018-01-03 13:40:21
【问题描述】：

以下 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 的懒惰。

我的工作理论是 Idris 不喜欢简化 Delay 内部的任何内容，因为那样可能会陷入无限循环。但是，无论如何，我都想强迫 Idris 试一试，因为 Prelude.Stream.tail 的定义保证了 LHS 将减少到 x :: Delay xs，从而完成了我的证明。

我的怀疑正确吗？我能以某种方式修正证明吗？

【问题讨论】：

标签： lazy-evaluation idris

【解决方案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

【讨论】：

在这种情况下，我无法使用标准的 cong 引理。