verification - Proof of stream's functor laws

Question

I've been writing something similar to a Stream. I am able to prove each functor law but I can not figure out a way to prove that it's total:

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

Gives:

*Stream> :total streamFunctorComposition
Stream.streamFunctorComposition is possibly not total due to recursive path:
    Stream.streamFunctorComposition, Stream.streamFunctorComposition

Is there a trick to proving the functor laws over codata which also passes the totality checker?

Answer 1

我从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为我们的流类型定义 a。

Daniel 还指出，观察类型理论确实允许在 codata 上进行命题相等，这是值得研究的。