{-
Die Aufgaben 3 und 4 der Probeklausur[0] für THProg im SS24, in Agda[1]

[0] https://www8.cs.fau.de/ext/teaching/sose2024/thprog/ProbeklausurSS24.pdf
[1] https://agda.readthedocs.io/en/latest
-}

{-# OPTIONS --guardedness #-} -- für Koinduktion

open import Relation.Binary.PropositionalEquality using (_≡_ ; cong ; refl)
open import Function using (_∘_)

-- 3 ========================================

data HList (a b : Set) : Set where
  HNil : HList a b
  ConsA : a → HList a b → HList a b
  ConsB : b → HList a b → HList a b

module _ {a b c : Set} where

  mapA : (a → c) → HList a b → HList c b
  mapA f HNil = HNil
  mapA f (ConsA x zs) = ConsA (f x) (mapA f zs)
  mapA f (ConsB y zs) = ConsB y (mapA f zs)

  mapB : (b → c) → HList a b → HList a c
  mapB f HNil = HNil
  mapB f (ConsA x zs) = ConsA x (mapB f zs)
  mapB f (ConsB y zs) = ConsB (f y) (mapB f zs)


module _ {a b : Set} where

  swap : HList a b → HList b a
  swap HNil = HNil
  swap (ConsA x zs) = ConsB x (swap zs)
  swap (ConsB y zs) = ConsA y (swap zs)

lemma : ∀ {a b : Set} (zs : HList a b) → swap (swap zs) ≡ zs
lemma HNil = refl
lemma (ConsA x zs') = cong (ConsA x) (lemma zs')
lemma (ConsB y zs') = cong (ConsB y) (lemma zs')


lemma' : ∀ {a b c d : Set} {f : a → c} {g : b → d} (zs : HList a b) →
         mapA f (mapB g zs) ≡ mapB g (mapA f zs)
lemma' HNil = refl
lemma' {f = f} (ConsA x zs') = cong (ConsA (f x)) (lemma' zs')
lemma' {g = g} (ConsB y zs') = cong (ConsB (g y)) (lemma' zs')


module _ {a b c : Set} where

  foldH : c → (a → c → c) → (b → c → c) → HList a b → c
  foldH hn ha hb HNil = hn
  foldH hn ha hb (ConsA x zs) = ha x (foldH hn ha hb zs)
  foldH hn ha hb (ConsB y zs) = hb y (foldH hn ha hb zs)


module _ {a b c : Set} where

  mapA' : (a → c) → HList a b → HList c b
  mapA' f zs = foldH HNil (ConsA ∘ f) ConsB zs

  mapB' : (b → c) → HList a b → HList a c
  mapB' g zs = foldH HNil ConsA (ConsB ∘ g) zs


-- 4 ========================================

record Stream (a : Set) : Set where
  coinductive
  field
    hd : a
    tl : Stream a
open Stream

record _≈_ {a : Set} (s t : Stream a) : Set where
  coinductive
  field
    hd-≡ : hd s ≡ hd t
    tl-≈ : tl s ≈ tl t
open _≈_

-- `sound` folgt normalerweise durch die Eigenschaft der terminalen Koalgebra
postulate sound : ∀ {a : Set} {s t : Stream a} → s ≈ t → s ≡ t

module _ {a b : Set} where

  map : (a → b) → Stream a → Stream b
  hd (map f s) = f (hd s)
  tl (map f s) = map f (tl s)


module _ {a : Set} where

  transpose : Stream (Stream a) → Stream (Stream a)
  hd (transpose s) = map hd s
  tl (transpose s) = transpose (map tl s)


lemma1 : ∀ {a : Set} (s : Stream (Stream a)) → map hd (transpose s) ≈ hd s
hd-≡ (lemma1 s) = refl
tl-≈ (lemma1 s) = helper s
  where
    helper : ∀ s → map hd (transpose (map tl s)) ≈ tl (hd s)
    hd-≡ (helper s) = refl
    tl-≈ (helper s) = lemma1 (map tl (map tl s))

lemma2 : ∀ {a : Set} (s : Stream (Stream a)) → map tl (transpose s) ≈ transpose (tl s)
hd-≡ (lemma2 s) = refl
tl-≈ (lemma2 s) = lemma2 (map tl s)

lemma3 : ∀ {a : Set} (s : Stream (Stream a)) → transpose (transpose s) ≈ s
hd-≡ (lemma3 s) = sound (lemma1 s)
tl-≈ (lemma3 s) rewrite (sound (lemma2 s))= lemma3 (tl s)