verification - 流仿函数定律的证明

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 的一些帮助谁解释说，能够在 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 进行命题相等，这是需要研究的。