{-# OPTIONS --guardedness #-}
{-
OPLSS 22 : Introduction to Type Theory
Thursday Exercises
-}

open import mylib

{- Finite Sets -}

variable l m n : ℕ

data Fin : ℕ → Set where
  zero : Fin (suc n)
  suc : Fin n → Fin (suc n)

{- define the following functions on Fin -}

max : {n : ℕ} → Fin (suc n)
max = {!!} -- computes the maximal element of a finite type

emb : {n : ℕ} → Fin n → Fin (suc n)
emb = {!!} -- embeds Fn n into Fin (suc n) without changing the value

rev : {n : ℕ} → Fin n → Fin n
rev = {!!} -- reverse the ordering

{- Isos -}

Π : (A : Set)(B : A → Set) → Set
Π A B = (x : A) → B x

{- A → B = Π A (λ _ → B) -}

record Σ(A : Set)(B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁
    
_⊎'_ : Set → Set → Set 
A ⊎' B = Σ Bool AorB
  where AorB : Bool → Set
        AorB true = A
        AorB false = B

_×'_ : Set → Set → Set 
A ×' B = Π Bool AorB
  where AorB : Bool → Set
        AorB true = A
        AorB false = B

{- Construct the functions witnessing isomorphisms
A ⊎' B ≅ A ⊎ B
A ×' B ≅ A × B
You can also prove the isomorphisms but you may need
to assume fun-ext
-}

{- Predicate logic -}


All : (A : Set)(P : A → prop) → prop
All A P = Π A P

Ex : (A : Set)(P : A → prop) → prop
Ex A P = Σ A P

syntax All A (λ x → P)  = ∀[ x ∈ A ] P  
infix 0 All
syntax Ex A (λ x → P) = ∃[ x ∈ A ] P
infix 0 Ex

variable PP QQ : A → prop

taut₁ : (∀[ x ∈ A ] (PP x ∧ QQ x)) ⇔ (∀[ x ∈ A ] PP x) ∧ (∀[ x ∈ A ] QQ x)
taut₁ = {!!}

taut₂ : (∃[ x ∈ A ] (PP x ∧ QQ x)) ⇒ (∃[ x ∈ A ] PP x) ∧ (∃[ x ∈ A ] QQ x)
taut₂ = {!!}

taut₃ : ((∃[ x ∈ A ] PP x) ⇒ R) ⇔ (∀[ x ∈ A ] PP x ⇒ R)
taut₃ = {!!}

{- definition of equality and properties -}

infix 0 _≡_

data _≡_ : A → A → Set where
  refl : {a : A} → a ≡ a

-- what are the basic properties of equality?
-- It is an equivalence relation
-- (actually a congruence)

sym : {a b : A} → a ≡ b → b ≡ a
sym refl = refl

trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl q = q

cong : (f : A → B) → {a b : A} → a ≡ b → f a ≡ f b
cong f refl = refl

{- prove commutativity of addition using pattern matching
   and structural recursion.
   Hint : it is useful to prove some lemmas first
-}

comm : (m n : ℕ) → m + n ≡ n + m
comm = {!!}

{- coinduction -}

from : ℕ → Stream ℕ
head (from n) = n
tail (from n) = from (suc n)

mapS : (A → B) → Stream A → Stream B
head (mapS f as) = f (head as)
tail (mapS f as) = mapS f (tail as)

postulate
  CoInd : (R : Stream A → Stream A → Set)
          → ({as bs : Stream A} → R as bs
             → ((head as ≡ head bs)
              × (R (tail as) (tail bs))))
          → {as bs : Stream A} → R as bs → as ≡ bs

{- Using CoInd prove the following equation -}

thm : (n : ℕ) → mapS suc (from n) ≡ from (suc n)
thm = {!!}