在Idris中证明流函数的属性

Question

我试图证明关于流函数和Monadic Stream函数[1]（最终是FRP程序）的属性。

Idris对我的流函数形式化很满意：

module SF

import Data.Vect
import Syntax.PreorderReasoning

%default total

data SF : Type -> Type -> Type where
  SFG : (a -> (b, Inf (SF a b))) -> SF a b

steps : {n : Nat} -> SF a b -> Vect n a -> Vect n b
steps {n = Z}   (SFG s) []        = []
steps {n = S m} (SFG s) (a :: as) =
    let (b, s') = s a
        bs = steps s' as
    in (b::bs)

我可以简单地定义提升/逐点应用功能：

liftM : (a -> b) -> SF a b
liftM f = SFG $ \a => (f a, liftM f)

以及SF的身份的两个变体：

identityM : SF a a
identityM = SFG $ \a => (a, identityM)

identity2 : SF a a
identity2 = liftM id

这通过了Idris的整体检查。但是，如果我现在试图证明identityM和identity2是平等的，我会遇到问题。我可以说明该财产如下：

proof1 :  (Eq b)
       => (n : Nat)
       -> (v : Vect n a)
       -> (steps identityM v) = (steps identity2 v)
proof1 Z [] = ?proof1_rhs_1
proof1 (S k) v = ?proof1_rhs_2

如果我要求?proof1_rhs_1的类型，idris正确地说steps identityM [] = steps identity2 []。但是，如果我尝试使用等式推理来表达：

proof1 Z [] = (steps {n=Z} identityM []) ={ ?someR }=
              (steps {n=Z} identity2 []) QED

然后伊德里斯不高兴：

When checking argument x to function Syntax.PreorderReasoning.Equal.qed:
        Type mismatch between
                steps identity2 [] (Inferred value)
        and
                steps identity2 [] (Given value)

        Specifically:
                Type mismatch between
                        steps identity2
                and
                        []Unification failure

有没有办法让这项工作？

[1] https://dl.acm.org/citation.cfm?id=2976010

Answer 1

这是通常的“伊德里斯”隐含的泛化导致混淆范围规则“：

proof1 :  (Eq b)
       => (n : Nat)
       -> (v : Vect n a)
       -> (steps identityM v) = (steps identity2 v)

手段

proof1 : {identityM : _} -> {identity2 : _} -> (...)
       -> (steps identityM v) = (steps identity2 v)

要引用先前的定义，您需要使用限定名称SF.identityM和SF.identity2。你可能还有其他问题（Eq b与b在其他类型中提到的其他地方似乎可疑）。