Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

1 files changed, 109 insertions, 0 deletions

diff --git a/src/Problem8.agda b/src/Problem8.agda
new file mode 100644
index 0000000..9329964
--- /dev/null
+++ b/src/Problem8.agda
@@ -0,0 +1,109 @@
+{-# 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                                           ∎)