我一直在写类似于 Stream 的东西。我能够证明每个仿函数定律,但我无法想出一种方法来证明它是完整的:
module Stream
import Classes.Verified
%default total
codata MyStream a = MkStream a (MyStream a)
mapStream : (a -> b) -> MyStream a -> MyStream b
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s)
streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (f x)) s = mapStream g (mapStream f s)
streamFunctorComposition (MkStream x y) f g =
let inductiveHypothesis = streamFunctorComposition y f g
in ?streamFunctorCompositionStepCase
---------- Proofs ----------
streamFunctorCompositionStepCase = proof
intros
rewrite inductiveHypothesis
trivial
给出:
*Stream> :total streamFunctorComposition
Stream.streamFunctorComposition is possibly not total due to recursive path:
Stream.streamFunctorComposition, Stream.streamFunctorComposition
是否有一个技巧来证明 codata 上的仿函数定律也通过了总体检查器?
最佳答案
我能够从 Daniel Peebles (copumpkin) 获得有关 IRC 的一些帮助谁解释说,能够在 codata 上使用命题相等通常是不允许的。他指出,可以定义自定义等价关系,就像 Agda 为 Data.Stream 定义的一样。 :
data _≈_ {A} : Stream A → Stream A → Set where
_∷_ : ∀ {x y xs ys}
(x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys
我能够将此定义直接翻译为 Idris:
module MyStream
%default total
codata MyStream a = MkStream a (MyStream a)
infixl 9 =#=
data (=#=) : MyStream a -> MyStream a -> Type where
(::) : a = b -> Inf (as =#= bs) -> MkStream a as =#= MkStream b bs
mapStream : (a -> b) -> MyStream a -> MyStream b
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s)
streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (f x)) s =#= mapStream g (mapStream f s)
streamFunctorComposition (MkStream x y) f g =
Refl :: streamFunctorComposition y f g
这很容易通过了整体检查器,因为我们现在只是在做简单的联合归纳。
这个事实有点令人失望,因为这似乎意味着我们无法定义
VerifiedFunctor
对于我们的流类型。Daniel 还指出观察类型理论确实允许对 codata 进行命题相等,这是需要研究的。
关于verification - 流仿函数定律的证明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30448651/