blob: 932996439df5fabc70b750f31e02d385b6b4b1de (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
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 ∎)
|
