Beweis der Funktorgesetze des Stromes

Question

Ich habe etwas ähnlich einem Strom geschrieben. Ich bin in der Lage jedes Funktors Gesetz zu beweisen, aber ich kann nicht einen Weg finden, um zu beweisen, dass es 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 

Gibt:

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

Gibt es einen Trick, um die Funktors Gesetze über CODATA zu beweisen, die übergibt auch die Totalitätsprüfung?

Answer 1

Ich konnte eine kleine Hilfe über IRC von Daniel Peebles (copumpkin) bekommen, die erklärte, dass es in der Regel nicht erlaubt ist, propositionale Gleichheit über Codata zu verwenden. Er wies darauf hin, dass es möglich ist, eine individuelle Äquivalenzrelation zu definieren, wie, wie Agda diejenigen für Data.Stream definiert:

data _≈_ {A} : Stream A → Stream A → Set where 
    _∷_ : ∀ {x y xs ys} 
     (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys 

konnte ich ein straight forward Übersetzung dieser Definition zu Idris tun:

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 

Und das hat den Totality Checker einfach bestanden, da wir jetzt einfach eine Coinduktion machen.

Diese Tatsache ist ein wenig enttäuschend, da es scheint, dass es bedeutet, dass wir keinen VerifiedFunctor für unseren Stream-Typ definieren können.

Daniel wies auch darauf hin, dass Observational Type Theory tut erlauben propositional Gleichheit über Codata, die etwas zu untersuchen ist.