流的仿函数定律的证明

Question

我一直在写类似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的仿函数法则也通过整体检查器？

Answer 1

我能够从Daniel Peebles(copumpkin)那里得到一些关于IRC的帮助,他解释说,能够使用命题平等而不是通常允许的东西.他指出可以定义自定义等价关系,就像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

我能够直接将这个定义翻译成伊德里斯:

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为我们的流类型定义一个.

丹尼尔还指出,观察类型理论确实允许命题平等超过密码,这是值得研究的东西.