{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Exercise 8: Coinductive types Deadline: 26/3/10 Use the coursework submission (id: 284) system to submit the coursework after demonstrating it in the lab to me or Darin. Prove the following propositions by completing the sheds { .. }. Note that not all propositions may be provable. If you think that a proposition is unprovable clearly mark this one by adding a line: -- impossible. -} module ex08 where open import Coinduction --open import Data.Stream open import Data.Bool open import Data.List open import Data.Nat open import Data.Nat.Properties --open import Data.Product open import l15 -- import the lecture from Tuesday open import Relation.Binary.PropositionalEquality open import Algebra module ℕ = CommutativeSemiring Data.Nat.Properties.commutativeSemiring mutual {- Define operations evens and odds which return a stream of all the even and odd elements of the given stream. -} evens : ∀ {A} → Stream A → Stream A evens = ? odds : ∀ {A} → Stream A → Stream A odds = ? {- Define an operation merge which merges two streams like a zipper -} merge : ∀ {A} → Stream A → Stream A → Stream A merge = ? {- And prove it correct -} mergeLem : ∀ {A} → (as : Stream A) → merge (evens as) (odds as) ≈ as mergeLem = ? {- Prove the following equality. You will need to use algebraic properties of the natural numbers. Also I recommend to prove the following lemma first: evensLem' : (m n : ℕ) → (m ≡ n + n) → evens (from m) ≈ mapStream (λ n → n + n) (from n) -} evensLem : (n : ℕ) → evens (from (n + n)) ≈ mapStream (λ n → n + n) (from n) evensLem = ? {- We define infinite binary trees: -} data Tree∞ (A : Set): Set where _〈_〉_ : (l : ∞ (Tree∞ A)) → (a : A) → (r : ∞ (Tree∞ A)) → Tree∞ A infix 4 _≈T_ {- and the notion of extensional equivalence: -} data _≈T_ {A : Set} : Tree∞ A → Tree∞ A → Set where _〈〉_ : ∀ {l l' a r r'} → ∞ (♭ l ≈T ♭ l') → ∞ (♭ r ≈T ♭ r') → (l 〈 a 〉 r) ≈T (l' 〈 a 〉 r') {- Show that ≈T is an equivalence relation. -} refl≈T : {A : Set} → (t : Tree∞ A) → t ≈T t refl≈T = ? sym≈T : {A : Set}{t u : Tree∞ A} → t ≈T u → u ≈T t sym≈T = ? trans≈T : {A : Set}{t u v : Tree∞ A} → t ≈T u → u ≈T v → t ≈T v trans≈T = ? {- Find a set X so that infinite binary trees are (extensionally) isomorphic to functions over X -} X : Set X = List Bool φ : {A : Set} → Tree∞ A → X → A φ = ? ψ : {A : Set} → (X → A) → Tree∞ A ψ = ? {- Show that the two functions defined previously are inverse to each other. -} ψφ : {A : Set}(t : Tree∞ A) → ψ (φ t) ≈T t ψφ = ? φψ : {A : Set}(f : X → A)(bs : X) → φ (ψ f) bs ≡ f bs φψ = ?