{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Exercise 8: Coinductive types Deadline: 26/3/10 Use the coursework submission (id: ???) 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 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 (a ∷ as) = a ∷ ♯ odds (♭ as) odds : ∀ {A} → Stream A → Stream A odds (a ∷ as) = evens (♭ as) {- Define an operation merge which merges two streams like a zipper -} merge : ∀ {A} → Stream A → Stream A → Stream A merge (a ∷ as) bs = a ∷ ♯ merge bs (♭ as) {- And prove it correct -} mergeLem : ∀ {A} → (as : Stream A) → merge (evens as) (odds as) ≈ as mergeLem (a ∷ as) = a ∷ ♯ mergeLem (♭ as) {- 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' : (m n : ℕ) → (m ≡ n + n) → evens (from m) ≈ mapStream (λ n → n + n) (from n) evensLem' .(n + n) n refl = n + n ∷ ♯ evensLem' (suc (suc (n + n))) (suc n) (cong suc (ℕ.+-comm (suc n) n)) evensLem : (n : ℕ) → evens (from (n + n)) ≈ mapStream (λ n → n + n) (from n) evensLem n = evensLem' (n + n) n refl {- 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 (l 〈 _ 〉 r) = (♯ (refl≈T (♭ l))) 〈〉 (♯ (refl≈T (♭ r)) ) sym≈T : {A : Set}{t u : Tree∞ A} → t ≈T u → u ≈T t sym≈T (l 〈〉 r) = (♯ sym≈T (♭ l)) 〈〉 (♯ sym≈T (♭ r)) trans≈T : {A : Set}{t u v : Tree∞ A} → t ≈T u → u ≈T v → t ≈T v trans≈T (l 〈〉 r) (l' 〈〉 r') = (♯ trans≈T (♭ l) (♭ l')) 〈〉 (♯ trans≈T (♭ r) (♭ r') ) {- 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 φ (l 〈 a 〉 r) [] = a φ (l 〈 a 〉 r) (true ∷ xs) = φ (♭ l) xs φ (l 〈 a 〉 r) (false ∷ xs) = φ (♭ r) xs ψ : {A : Set} → (X → A) → Tree∞ A ψ f = (♯ (ψ (λ bs → f (true ∷ bs)))) 〈 f [] 〉 ((♯ (ψ (λ bs → f (false ∷ bs))))) {- Show that the two functions defined previously are inverse to each other. -} ψφ : {A : Set}(t : Tree∞ A) → ψ (φ t) ≈T t ψφ (l 〈 a 〉 r) = (♯ (ψφ (♭ l))) 〈〉 ((♯ (ψφ (♭ r)))) φψ : {A : Set}(f : X → A)(bs : X) → φ (ψ f) bs ≡ f bs φψ f [] = refl φψ f (true ∷ xs) = φψ ((λ bs → f (true ∷ bs))) xs φψ f (false ∷ xs) = φψ ((λ bs → f (false ∷ bs))) xs