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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
{-# OPTIONS --safe #-}
module Problem24 where
open import Data.Bool using (true; false)
open import Data.Empty using (⊥-elim)
open import Data.List
open import Data.List.Properties
open import Data.List.Relation.Unary.All hiding (toList)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Data.Product.Properties
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open ≡-Reasoning
data Tree : Set where
Leaf : Tree
Branch : Tree → Tree → Tree
toList : ℕ → Tree → List ℕ
toList d Leaf = [ d ]
toList d (Branch t₁ t₂) = toList (suc d) t₁ ++ toList (suc d) t₂
-- We write a parser for lists into forests with a labelled root depth, from
-- right to left.
--
-- The empty list is an empty forest.
--
-- For a given natural `n` and forest `ts`, we try and merge the labelled tree
-- `(n , Leaf)` into the forest.
--
-- Merging a tree `(n , t)` into a forest `ts` is again done by induction.
LabelledTree : Set
LabelledTree = ℕ × Tree
Forest : Set
Forest = List LabelledTree
addTree : LabelledTree → Forest → Forest
addTree (n , t) [] = [ (n , t) ]
addTree (n , t) ((k , t′) ∷ ts) with n ≟ k
... | yes p = addTree (pred n , Branch t t′) ts
... | no p = (n , t) ∷ (k , t′) ∷ ts
parseList : List ℕ → Forest
parseList [] = []
parseList (x ∷ xs) = addTree (x , Leaf) (parseList xs)
-- Properties ------------------------------------------------------------------
private
variable
k d : ℕ
xs ys : List ℕ
t t′ : Tree
ts : Forest
-- A forest blocks at `d` if trying to add any `1+n+d` tree fails.
data Blocking (d : ℕ) : (ts : Forest) → Set where
empty : Blocking d []
cons : {ts : Forest} → k ≤ d → Blocking d ((k , t) ∷ ts)
-- Adding a tree at a lower depth is blocking, even if it is merged into existing trees.
blocking-addTree :
(d≥k : d ≥ k) (t : Tree) (ts : Forest) → Blocking d (addTree (k , t) ts)
blocking-addTree d≥k t [] = cons d≥k
blocking-addTree {k = k} d≥k t ((n , t′) ∷ ts) with k ≟ n
... | yes refl = blocking-addTree (≤-trans pred[n]≤n d≥k) (Branch t t′) ts
... | no p = cons d≥k
-- Blocking is closed for higher depths
blocking-suc : Blocking d ts → Blocking (suc d) ts
blocking-suc empty = empty
blocking-suc (cons k≤d) = cons (≤-step k≤d)
-- The fundamental theorem of blocking:
-- if a forest blocks at `d`, adding a tree with depth `1+d` conses the tree
-- onto the forest.
addTree-blocking[1+n] :
(d : ℕ) (t : Tree) {ts : Forest} → Blocking d ts →
addTree (suc d , t) ts ≡ (suc d , t) ∷ ts
addTree-blocking[1+n] d t empty = refl
addTree-blocking[1+n] d t (cons {k} k≤d) with suc d ≟ k
... | yes 1+d≡k = ⊥-elim (≤⇒≯ k≤d (≤-reflexive 1+d≡k))
... | no _ = refl
-- Adding two trees of depth `1+n` onto a forest blocking at `n` is equivalent
-- to adding their composite.
addTree-branch′ :
(n : ℕ) (t₁ t₂ : Tree) (ts : Forest) →
addTree (suc n , t₁) ((suc n , t₂) ∷ ts) ≡ addTree (n , Branch t₁ t₂) ts
addTree-branch′ n t₁ t₂ ts with suc n ≟ suc n
... | yes _ = refl
... | no p = ⊥-elim (p refl)
addTree-branch :
(n : ℕ) (t₁ t₂ : Tree) {ts : Forest} → Blocking n ts →
addTree (suc n , t₁) (addTree (suc n , t₂) ts) ≡ addTree (n , Branch t₁ t₂) ts
addTree-branch n t₁ t₂ {ts} block = begin
addTree (suc n , t₁) (addTree (suc n , t₂) ts) ≡⟨ cong (addTree (suc n , t₁)) (addTree-blocking[1+n] n t₂ block) ⟩
addTree (suc n , t₁) ((suc n , t₂) ∷ ts) ≡⟨ addTree-branch′ n t₁ t₂ ts ⟩
addTree (n , Branch t₁ t₂) ts ∎
-- Main result of parse: parsing inverts conversion to lists, as long as the
-- tail blocks.
--
-- We prove a blocking lemma at the same time. Using the correctness proof
-- significantly reduces the amount of work.
blocking-parseList :
(d : ℕ) (t : Tree) {xs : List ℕ} → Blocking d (parseList xs) →
Blocking d (parseList (toList d t ++ xs))
parseList-++ :
(d : ℕ) (t : Tree) {xs : List ℕ} → Blocking d (parseList xs) →
parseList (toList d t ++ xs) ≡ addTree (d , t) (parseList xs)
blocking-parseList d t {xs} block =
subst (Blocking d)
(sym (parseList-++ d t block))
(blocking-addTree ≤-refl t (parseList xs))
parseList-++ d Leaf block = refl
parseList-++ d (Branch t₁ t₂) {xs} block = begin
parseList ((toList (suc d) t₁ ++ toList (suc d) t₂) ++ xs) ≡⟨ cong parseList (++-assoc (toList (suc d) t₁) (toList (suc d) t₂) xs) ⟩
parseList (toList (suc d) t₁ ++ toList (suc d) t₂ ++ xs) ≡⟨ parseList-++ (suc d) t₁ (blocking-parseList (suc d) t₂ (blocking-suc block)) ⟩
addTree (suc d , t₁) (parseList (toList (suc d) t₂ ++ xs)) ≡⟨ cong (addTree (suc d , t₁)) (parseList-++ (suc d) t₂ (blocking-suc block)) ⟩
addTree (suc d , t₁) (addTree (suc d , t₂) (parseList xs)) ≡⟨ addTree-branch d t₁ t₂ block ⟩
addTree (d , Branch t₁ t₂) (parseList xs) ∎
-- Proof that parse is an inverse of `toList` (modulo some wrapping)
parse-correct : (d : ℕ) (t : Tree) → parseList (toList d t) ≡ [ d , t ]
parse-correct d t = begin
parseList (toList d t) ≡˘⟨ cong parseList (++-identityʳ (toList d t)) ⟩
parseList (toList d t ++ []) ≡⟨ parseList-++ d t empty ⟩
addTree (d , t) [] ≡⟨⟩
[ d , t ] ∎
-- Goal
toList-injective : ∀{n} t t′ → toList n t ≡ toList n t′ → t ≡ t′
toList-injective {n} t t′ eq = ,-injectiveʳ (∷-injectiveˡ (begin
[ n , t ] ≡˘⟨ parse-correct n t ⟩
parseList (toList n t) ≡⟨ cong parseList eq ⟩
parseList (toList n t′) ≡⟨ parse-correct n t′ ⟩
[ n , t′ ] ∎))
|
