Remove StreamIntro

parent daabc7fc
\begin{code}
module PiWare.ProofSamples.StreamIntro where
open import Function using (_∘_)
open import Coinduction using (♯_; ♭)
open import Data.Bool using (Bool; false; true; not)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Stream using (Stream; repeat; evens; odds; _∷_; _≈_; iterate; map; tail; head; drop)
open import Data.Stream.Properties using (module Setoidₛ)
open Setoidₛ using () renaming (refl to reflₛ)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
falses : Stream Bool
falses = repeat false
evens-falses-≈-odds-falses : evens falses ≈ odds falses
evens-falses-≈-odds-falses = refl ∷ ♯ evens-falses-≈-odds-falses
truefalses : Stream Bool
truefalses = iterate not true
odds-truefalses-≈-falses : odds truefalses ≈ falses
odds-truefalses-≈-falses = refl ∷ ♯ odds-truefalses-≈-falses
from : ℕ → Stream ℕ
from n = n ∷ ♯ from (suc n)
from-suc-map : ∀ n → from (suc n) ≈ map suc (from n)
from-suc-map n = refl ∷ ♯ from-suc-map (suc n)
myTail : ∀ {α} → Stream α → Stream α
myTail (_ ∷ xs) = ♭ xs
tailsEqual : ∀ {α} {s : Stream α} → tail s ≈ myTail s
tailsEqual {s = _ ∷ xs} with ♭ xs
tailsEqual {s = _ ∷ xs} | y ∷ zs = refl ∷ ♯ tailsEqual {s = y ∷ zs}
assemble≈ : ∀ {α} {s} {x : α} {xs} → head s ≡ x → tail s ≈ xs → s ≈ x ∷ ♯ xs
assemble≈ {s = _ ∷ _} head≡ tail≈ = head≡ ∷ ♯ tail≈
assemble≈∞ : ∀ {α} {s} {x : α} {xs} → head s ≡ x → tail s ≈ ♭ xs → s ≈ x ∷ xs
assemble≈∞ {s = _ ∷ _} head≡ tail≈ = head≡ ∷ ♯ tail≈
myRepeat : ∀ {α} (x : α) → Stream α
myRepeat x = x ∷ ♯ myRepeat x
repeatsEqual : ∀ {α} {x : α} → repeat x ≈ myRepeat x
repeatsEqual = refl ∷ ♯ repeatsEqual
myRepeat₂ : ∀ {α} (x : α) → Stream α
myRepeat₂ x = x ∷ ♯ (x ∷ ♯ myRepeat₂ x)
repeatsEqual₂ : ∀ {α} {x : α} → repeat x ≈ myRepeat₂ x
repeatsEqual₂ {α} {x} = refl ∷ ♯ (refl ∷ ♯ repeatsEqual₂)
tail-drop-comm : ∀ {n α} {s : Stream α} → (tail ∘ drop n) s ≈ (drop n ∘ tail) s
tail-drop-comm {zero} {s = _ ∷ _} = reflₛ
tail-drop-comm {suc n} {s = _ ∷ xs} with ♭ xs
tail-drop-comm {suc n} {s = _ ∷ _} | y ∷ zs = tail-drop-comm {n}
\end{code}
......@@ -73,7 +73,6 @@ import PiWare.ProofSamples.RegN -- M
import PiWare.ProofSamples.RegN' -- M
import PiWare.ProofSamples.RegN'Properties -- M
import PiWare.ProofSamples.RegProperties -- M
import PiWare.ProofSamples.StreamIntro -- M
import PiWare.Samples.BoolTrioComb
import PiWare.Samples.BoolTrioSeq
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment