{-# OPTIONS --safe #-}

module Problem8 where

open import Data.Nat hiding (_≟_)
open import Data.Product hiding (map)
open import Data.Bool
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Empty
open import Data.Vec
open import Data.Bool.Properties using (¬-not; not-¬)

open ≡-Reasoning

data CompressedString : ℕ → Set where
    empty : CompressedString 0
    one   : Bool → (n : ℕ) → CompressedString (suc n)
    cons  : ∀{m} → (n : ℕ) → CompressedString (suc m) → CompressedString (suc (suc (n + m)))

head-c : ∀{n} → CompressedString (suc n) → Bool
head-c (one x n) = x
head-c (cons n str) = not (head-c str)

tail-c : ∀{n} → CompressedString (suc n) → CompressedString n
tail-c (one x zero) = empty
tail-c (one x (suc n)) = one x n
tail-c (cons zero str) = str
tail-c (cons (suc n) str) = cons n str

cons-c : ∀{n} → Bool → CompressedString  n → CompressedString (suc n)
cons-c b empty = one b 0
cons-c b (one x n) with b ≟ x
... | yes _ = one x (suc n)
... | no  _ = cons 0 (one x n)
cons-c b (cons n str) with b ≟ head-c (cons n str)
... | yes _ = cons (suc n) str
... | no  _ = cons 0 (cons n str)


compress : ∀{n} → Vec Bool n → CompressedString n
compress [] = empty
compress (l ∷ ls) = cons-c l (compress ls)


decompress : ∀{n} → CompressedString n → Vec Bool n
decompress {zero} empty = []
decompress {suc n} str = head-c str ∷ decompress (tail-c str)

-- Consing the opposite element introduces a cons constructor.

cons-c-¬head : ∀ {n} (xs : CompressedString (suc n)) → cons-c (not (head-c xs)) xs ≡ cons zero xs
cons-c-¬head (one x _) with not x ≟ x
... | yes ¬x≡x = ⊥-elim (not-¬ refl (sym ¬x≡x))
... | no _ = refl
cons-c-¬head (cons n xs) with not (not (head-c xs)) ≟ not (head-c xs)
... | yes ¬¬x≡¬x = ⊥-elim (not-¬ refl (sym ¬¬x≡¬x))
... | no _ = refl

-- Eta equality

cons-c∘<head-c,tail-c> : ∀ {n} (xs : CompressedString (suc n)) → cons-c (head-c xs) (tail-c xs) ≡ xs
cons-c∘<head-c,tail-c> (one x zero) = refl
cons-c∘<head-c,tail-c> (one x (suc n)) with x ≟ x
... | yes _ = refl
... | no x≢x = ⊥-elim (x≢x refl)
cons-c∘<head-c,tail-c> (cons zero xs) = cons-c-¬head xs
cons-c∘<head-c,tail-c> (cons (suc n) xs) with not (head-c xs) ≟ not (head-c xs)
... | yes _ = refl
... | no x≢x = ⊥-elim (x≢x refl)

-- Beta equalities

head-c∘cons-c : ∀ {n} x (xs : CompressedString n) → head-c (cons-c x xs) ≡ x
head-c∘cons-c x empty = refl
head-c∘cons-c x (one y n) with x ≟ y
... | yes x≡y = sym x≡y
... | no x≢y = sym (¬-not x≢y)
head-c∘cons-c x (cons n xs) with x ≟ not (head-c xs)
... | yes x≡¬y = sym x≡¬y
... | no x≢¬y = sym (¬-not x≢¬y)

tail-c∘cons-c : ∀ {n} x (xs : CompressedString n) → tail-c (cons-c x xs) ≡ xs
tail-c∘cons-c x empty = refl
tail-c∘cons-c x (one y n) with x ≟ y
... | yes _ = refl
... | no _ = refl
tail-c∘cons-c x (cons n xs) with x ≟ not (head-c xs)
... | yes _ = refl
... | no _ = refl

-- Goals

prf₁ : ∀{n} (xs : CompressedString n) → compress (decompress xs) ≡ xs
prf₁ {zero} empty = refl
prf₁ {suc n} xs = begin
  cons-c (head-c xs) (compress (decompress (tail-c xs))) ≡⟨ cong (cons-c (head-c xs)) (prf₁ (tail-c xs)) ⟩
  cons-c (head-c xs) (tail-c xs)                         ≡⟨ cons-c∘<head-c,tail-c> xs ⟩
  xs                                                     ∎

prf₂ : ∀{n} (xs : Vec Bool n) → decompress (compress xs) ≡ xs
prf₂ [] = refl
prf₂ (x ∷ xs) =
  cong₂ _∷_
    (head-c∘cons-c x (compress xs))
    (begin
      decompress (tail-c (cons-c x (compress xs))) ≡⟨ cong decompress (tail-c∘cons-c x (compress xs)) ⟩
      decompress (compress xs)                     ≡⟨ prf₂ xs ⟩
      xs                                           ∎)