{- 
  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
φψ = ?