------------------------------------------------------------------------ -- Instantiation of Contractive for streams ------------------------------------------------------------------------ -- Taken from the paper. -- The definition of Eq has been changed slightly, as compared to the -- paper. The paper uses -- Eq = λ n xs ys → take n xs ≡ take n ys. -- The reason for the change is that with the definition above -- coherence does not say anything about the first element in limU s. -- With the definition in the paper head (s 0), which is the first -- element in limU s, does not have to be related to head (s n) for -- any other n, and this makes it impossible to prove isLimitU. -- (Unless I have missed something.) module Contractive.Stream {A : Set} where open import Coinduction open import Contractive open import Data.Nat open import Data.Nat.Properties open import Data.Stream import Data.Vec as Vec open Vec using (_∷_; []) open import Function open import Relation.Unary open import Relation.Binary.PropositionalEquality open import Induction.Nat <′-isWellFoundedOrder : IsWellFoundedOrder _<′_ <′-isWellFoundedOrder = record { trans = λ {i} {j} {k} i+1≤j j+1≤k → ≤⇒≤′ (begin suc i ≤⟨ ≤′⇒≤ (≤′-step i+1≤j) ⟩ suc j ≤⟨ ≤′⇒≤ j+1≤k ⟩ k ∎) ; isWellFounded = <-well-founded } where open ≤-Reasoning ofe : OFE ofe = record { Carrier = ℕ ; Domain = Stream A ; _<_ = _<′_ ; isWellFoundedOrder = <′-isWellFoundedOrder ; Eq = λ n xs ys → take (suc n) xs ≡ take (suc n) ys ; isEquivalence = λ _ → record { refl = refl ; sym = sym ; trans = trans } } open OFE ofe private limU : (ℕ → Stream A) → Stream A limU s = head (s 0) ∷ ♯ limU (tail ∘ s ∘ suc) η : ∀ {n} {xs : Stream A} → Eq n xs (head xs ∷ ♯ tail xs) η {xs = x ∷ xs} = refl step : ∀ s → IsCoherent {U} (lift s) → IsCoherent {U} (lift (tail ∘ s ∘ suc)) step s coh {m} {n} _ _ m