|
176
|
1 module bijection where
|
|
141
|
2
|
|
|
3 open import Level renaming ( zero to Zero ; suc to Suc )
|
|
|
4 open import Data.Nat
|
|
142
|
5 open import Data.Maybe
|
|
256
|
6 open import Data.List hiding ([_] ; sum )
|
|
141
|
7 open import Data.Nat.Properties
|
|
|
8 open import Relation.Nullary
|
|
|
9 open import Data.Empty
|
|
256
|
10 open import Data.Unit hiding ( _≤_ )
|
|
142
|
11 open import Relation.Binary.Core hiding (_⇔_)
|
|
141
|
12 open import Relation.Binary.Definitions
|
|
|
13 open import Relation.Binary.PropositionalEquality
|
|
|
14
|
|
|
15 open import logic
|
|
256
|
16 open import nat
|
|
141
|
17
|
|
|
18 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
|
|
|
19 field
|
|
|
20 fun← : S → R
|
|
|
21 fun→ : R → S
|
|
|
22 fiso← : (x : R) → fun← ( fun→ x ) ≡ x
|
|
|
23 fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x
|
|
|
24
|
|
164
|
25 injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
|
|
|
26 injection R S f = (x y : R) → f x ≡ f y → x ≡ y
|
|
|
27
|
|
141
|
28 open Bijection
|
|
|
29
|
|
164
|
30 b→injection0 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection R S (fun→ b)
|
|
|
31 b→injection0 R S b x y eq = begin
|
|
|
32 x
|
|
|
33 ≡⟨ sym ( fiso← b x ) ⟩
|
|
|
34 fun← b ( fun→ b x )
|
|
|
35 ≡⟨ cong (λ k → fun← b k ) eq ⟩
|
|
|
36 fun← b ( fun→ b y )
|
|
|
37 ≡⟨ fiso← b y ⟩
|
|
|
38 y
|
|
|
39 ∎ where open ≡-Reasoning
|
|
|
40
|
|
|
41 b→injection1 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection S R (fun← b)
|
|
|
42 b→injection1 R S b x y eq = trans ( sym ( fiso→ b x ) ) (trans ( cong (λ k → fun→ b k ) eq ) ( fiso→ b y ))
|
|
|
43
|
|
|
44 -- ¬ A = A → ⊥
|
|
|
45
|
|
174
|
46 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool
|
|
164
|
47 diag b n = not (fun← b n n)
|
|
|
48
|
|
174
|
49 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S
|
|
|
50 diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
|
|
|
51 diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n )
|
|
164
|
52 diagn1 n dn = ¬t=f (diag b n ) ( begin
|
|
|
53 not (diag b n)
|
|
141
|
54 ≡⟨⟩
|
|
|
55 not (not fun← b n n)
|
|
|
56 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩
|
|
164
|
57 not (fun← b (fun→ b (diag b)) n)
|
|
141
|
58 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
|
|
|
59 not (fun← b n n)
|
|
|
60 ≡⟨⟩
|
|
164
|
61 diag b n
|
|
141
|
62 ∎ ) where open ≡-Reasoning
|
|
|
63
|
|
256
|
64
|
|
|
65 open _∧_
|
|
|
66
|
|
|
67 record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) (n→nxn : ℕ → ℕ ∧ ℕ) : Set where
|
|
|
68 field
|
|
|
69 j k sum stage : ℕ
|
|
|
70 nn : j + k ≡ sum
|
|
|
71 ni : i ≡ j + stage
|
|
|
72 k1 : nxn→n j k ≡ i
|
|
|
73 k0 : n→nxn i ≡ ⟪ j , k ⟫
|
|
|
74 nn-unique : {j0 k0 : ℕ } → nxn→n j0 k0 ≡ i → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫
|
|
|
75
|
|
|
76 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0
|
|
|
77 i≤0→i≡0 {0} z≤n = refl
|
|
|
78
|
|
|
79
|
|
|
80 nxn : Bijection ℕ (ℕ ∧ ℕ)
|
|
|
81 nxn = record {
|
|
|
82 fun← = λ p → nxn→n (proj1 p) (proj2 p)
|
|
|
83 ; fun→ = n→nxn
|
|
|
84 ; fiso← = n-id
|
|
|
85 ; fiso→ = λ x → nn-id (proj1 x) (proj2 x)
|
|
|
86 } where
|
|
|
87 nxn→n : ℕ → ℕ → ℕ
|
|
|
88 nxn→n zero zero = zero
|
|
|
89 nxn→n zero (suc j) = j + suc (nxn→n zero j)
|
|
|
90 nxn→n (suc i) zero = suc i + suc (nxn→n i zero)
|
|
|
91 nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j))
|
|
|
92 n→nxn : ℕ → ℕ ∧ ℕ
|
|
|
93 n→nxn zero = ⟪ 0 , 0 ⟫
|
|
|
94 n→nxn (suc i) with n→nxn i
|
|
|
95 ... | ⟪ x , zero ⟫ = ⟪ zero , suc x ⟫
|
|
|
96 ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
|
|
|
97
|
|
|
98 nxn→n0 : { j k : ℕ } → nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 )
|
|
|
99 nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫
|
|
|
100 nxn→n0 {zero} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → 0 < k) (+-comm _ k) (s≤s z≤n)))
|
|
|
101 nxn→n0 {(suc j)} {zero} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
|
|
|
102 nxn→n0 {(suc j)} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
|
|
|
103
|
|
|
104 nid20 : (i : ℕ) → i + (nxn→n 0 i) ≡ nxn→n i 0
|
|
|
105 nid20 zero = refl -- suc (i + (i + suc (nxn→n 0 i))) ≡ suc (i + suc (nxn→n i 0))
|
|
|
106 nid20 (suc i) = begin
|
|
|
107 suc (i + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (i + k)) (sym (+-assoc i 1 (nxn→n 0 i))) ⟩
|
|
|
108 suc (i + ((i + 1) + nxn→n 0 i)) ≡⟨ cong (λ k → suc (i + (k + nxn→n 0 i))) (+-comm i 1) ⟩
|
|
|
109 suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i) ⟩
|
|
|
110 suc (i + suc (nxn→n i 0)) ∎ where open ≡-Reasoning
|
|
|
111
|
|
|
112 nid4 : {i j : ℕ} → i + 1 + j ≡ i + suc j
|
|
|
113 nid4 {zero} {j} = refl
|
|
|
114 nid4 {suc i} {j} = cong suc (nid4 {i} {j} )
|
|
|
115 nid5 : {i j k : ℕ} → i + suc (suc j) + suc k ≡ i + suc j + suc (suc k )
|
|
|
116 nid5 {zero} {j} {k} = begin
|
|
|
117 suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩
|
|
|
118 1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩
|
|
|
119 (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩
|
|
|
120 suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩
|
|
|
121 suc j + suc (suc k) ∎ where open ≡-Reasoning
|
|
|
122 nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
|
|
|
123
|
|
|
124 nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
|
|
|
125 nid2 zero zero = refl
|
|
|
126 nid2 zero (suc j) = refl
|
|
|
127 nid2 (suc i) zero = begin
|
|
|
128 suc (nxn→n (suc i) 1) ≡⟨ refl ⟩
|
|
|
129 suc (suc (i + 1 + suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (suc k)) nid4 ⟩
|
|
|
130 suc (suc (i + suc (suc (nxn→n i 1)))) ≡⟨ cong (λ k → suc (suc (i + suc (suc k)))) (nid3 i) ⟩
|
|
|
131 suc (suc (i + suc (suc (i + suc (nxn→n i 0))))) ≡⟨ refl ⟩
|
|
|
132 nxn→n (suc (suc i)) zero ∎ where
|
|
|
133 open ≡-Reasoning
|
|
|
134 nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0)
|
|
|
135 nid3 zero = refl
|
|
|
136 nid3 (suc i) = begin
|
|
|
137 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
|
|
|
138 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k → suc (i + suc (suc k))) (nid3 i) ⟩
|
|
|
139 suc (i + suc (suc (i + suc (nxn→n i 0))))
|
|
|
140 ∎
|
|
|
141 nid2 (suc i) (suc j) = begin
|
|
|
142 suc (nxn→n (suc i) (suc (suc j))) ≡⟨ refl ⟩
|
|
|
143 suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j))))) ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩
|
|
|
144 suc (suc (i + suc (suc j) + suc (i + suc j + suc (nxn→n i (suc j))))) ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩
|
|
|
145 suc (suc (i + suc j + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩
|
|
|
146 nxn→n (suc (suc i)) (suc j) ∎ where
|
|
|
147 open ≡-Reasoning
|
|
|
148
|
|
|
149 nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i)
|
|
|
150 nid00 zero = refl
|
|
|
151 nid00 (suc i) = begin
|
|
|
152 suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩
|
|
|
153 suc (suc (i + (nxn→n 0 (suc i)))) ≡⟨ refl ⟩
|
|
|
154 suc (suc (i + (i + suc (nxn→n 0 i)))) ≡⟨ cong suc (sym ( +-assoc 1 i (i + suc (nxn→n 0 i)))) ⟩
|
|
|
155 suc ((1 + i) + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (k + (i + suc (nxn→n 0 i)))) (+-comm 1 i) ⟩
|
|
|
156 suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩
|
|
|
157 suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning
|
|
|
158
|
|
|
159 nn : ( i : ℕ) → NN i nxn→n n→nxn
|
|
|
160 nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl
|
|
|
161 ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
|
|
|
162 nn (suc i) with NN.k (nn i) | inspect NN.k (nn i)
|
|
|
163 ... | zero | record { eq = eq } = record { k = suc (NN.sum (nn i)) ; j = 0 ; sum = suc (NN.sum (nn i)) ; stage = suc (NN.sum (nn i)) + (NN.stage (nn i))
|
|
|
164 ; nn = refl
|
|
|
165 ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ; nn-unique = nn04 } where
|
|
|
166 sum = NN.sum (nn i)
|
|
|
167 stage = NN.stage (nn i)
|
|
|
168 j = NN.j (nn i)
|
|
|
169 nn01 : suc i ≡ 0 + (suc sum + stage )
|
|
|
170 nn01 = begin
|
|
|
171 suc i ≡⟨ cong suc (NN.ni (nn i)) ⟩
|
|
|
172 suc ((NN.j (nn i) ) + stage ) ≡⟨ cong (λ k → suc (k + stage )) (+-comm 0 _ ) ⟩
|
|
|
173 suc ((NN.j (nn i) + 0 ) + stage ) ≡⟨ cong (λ k → suc ((NN.j (nn i) + k) + stage )) (sym eq) ⟩
|
|
|
174 suc ((NN.j (nn i) + NN.k (nn i)) + stage ) ≡⟨ cong (λ k → suc ( k + stage )) (NN.nn (nn i)) ⟩
|
|
|
175 0 + (suc sum + stage ) ∎ where open ≡-Reasoning
|
|
|
176 nn02 : nxn→n 0 (suc sum) ≡ suc i
|
|
|
177 nn02 = begin
|
|
|
178 sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩
|
|
|
179 (sum + 1) + nxn→n 0 sum ≡⟨ cong (λ k → k + nxn→n 0 sum ) (+-comm sum 1 )⟩
|
|
|
180 suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩
|
|
|
181 suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NN.nn (nn i))) ⟩
|
|
|
182 suc (nxn→n (NN.j (nn i) + (NN.k (nn i)) ) 0) ≡⟨ cong₂ (λ j k → suc (nxn→n (NN.j (nn i) + j) k )) eq (sym eq) ⟩
|
|
|
183 suc (nxn→n (NN.j (nn i) + 0 ) (NN.k (nn i))) ≡⟨ cong (λ k → suc ( nxn→n k (NN.k (nn i)))) (+-comm (NN.j (nn i)) 0) ⟩
|
|
|
184 suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩
|
|
|
185 suc i ∎ where open ≡-Reasoning
|
|
|
186 nn03 : n→nxn (suc i) ≡ ⟪ 0 , suc (NN.sum (nn i)) ⟫ -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫
|
|
|
187 nn03 with n→nxn i | inspect n→nxn i
|
|
|
188 ... | ⟪ x , zero ⟫ | record { eq = eq1 } = begin
|
|
|
189 ⟪ zero , suc x ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (sym (cong proj1 eq1)) ⟩
|
|
|
190 ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (cong proj1 (NN.k0 (nn i))) ⟩
|
|
|
191 ⟪ zero , suc (NN.j (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (+-comm 0 _ ) ⟩
|
|
|
192 ⟪ zero , suc (NN.j (nn i) + 0) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc (NN.j (nn i) + k) ⟫ ) (sym eq) ⟩
|
|
|
193 ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫ ) (NN.nn (nn i)) ⟩
|
|
|
194 ⟪ 0 , suc sum ⟫ ∎ where open ≡-Reasoning
|
|
|
195 ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 (NN.k0 (nn i)))) (begin
|
|
|
196 suc (NN.k (nn i)) ≡⟨ cong suc eq ⟩
|
|
|
197 suc 0 ≤⟨ s≤s z≤n ⟩
|
|
|
198 suc y ≡⟨ sym (cong proj2 eq1) ⟩
|
|
|
199 proj2 (n→nxn i) ∎ )) where open ≤-Reasoning
|
|
|
200 -- nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
|
|
|
201 nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (NN.sum (nn i)) ⟫ ≡ ⟪ j0 , k0 ⟫
|
|
|
202 nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i --
|
|
|
203 nn07 : nxn→n k0 0 ≡ i
|
|
|
204 nn07 = cong pred ( begin
|
|
|
205 suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩
|
|
|
206 nxn→n 0 (suc k0 ) ≡⟨ eq1 ⟩
|
|
|
207 suc i ∎ ) where open ≡-Reasoning
|
|
|
208 nn08 : k0 ≡ sum
|
|
|
209 nn08 = begin
|
|
|
210 k0 ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩
|
|
|
211 NN.j (nn i) ≡⟨ +-comm 0 _ ⟩
|
|
|
212 NN.j (nn i) + 0 ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩
|
|
|
213 NN.j (nn i) + NN.k (nn i) ≡⟨ NN.nn (nn i) ⟩
|
|
|
214 sum ∎ where open ≡-Reasoning
|
|
|
215 nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where
|
|
|
216 nn05 : nxn→n j0 (suc k0) ≡ i
|
|
|
217 nn05 = begin
|
|
|
218 nxn→n j0 (suc k0) ≡⟨ cong pred ( begin
|
|
|
219 suc (nxn→n j0 (suc k0)) ≡⟨ nid2 j0 k0 ⟩
|
|
|
220 nxn→n (suc j0) k0 ≡⟨ eq1 ⟩
|
|
|
221 suc i ∎ ) ⟩
|
|
|
222 i ∎ where open ≡-Reasoning
|
|
|
223 nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
|
|
|
224 nn06 = NN.nn-unique (nn i)
|
|
|
225 ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = nn10
|
|
|
226 ; ni = cong suc (NN.ni (nn i)) ; k1 = nn11 ; k0 = nn12 ; nn-unique = nn13 } where
|
|
|
227 nn10 : suc (NN.j (nn i)) + k ≡ NN.sum (nn i)
|
|
|
228 nn10 = begin
|
|
|
229 suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _) ⟩
|
|
|
230 (NN.j (nn i) + 1) + k ≡⟨ +-assoc (NN.j (nn i)) 1 k ⟩
|
|
|
231 NN.j (nn i) + suc k ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩
|
|
|
232 NN.j (nn i) + NN.k (nn i) ≡⟨ NN.nn (nn i) ⟩
|
|
|
233 NN.sum (nn i) ∎ where open ≡-Reasoning
|
|
|
234 nn11 : nxn→n (suc (NN.j (nn i))) k ≡ suc i -- nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i
|
|
|
235 nn11 = begin
|
|
|
236 nxn→n (suc (NN.j (nn i))) k ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩
|
|
|
237 suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k → suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩
|
|
|
238 suc (nxn→n ( NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i)) ⟩
|
|
|
239 suc i ∎ where open ≡-Reasoning
|
|
|
240 nn18 : zero < NN.k (nn i)
|
|
|
241 nn18 = subst (λ k → 0 < k ) ( begin
|
|
|
242 suc k ≡⟨ sym eq ⟩
|
|
|
243 NN.k (nn i) ∎ ) (s≤s z≤n ) where open ≡-Reasoning
|
|
|
244 nn12 : n→nxn (suc i) ≡ ⟪ suc (NN.j (nn i)) , k ⟫ -- n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫
|
|
|
245 nn12 with n→nxn i | inspect n→nxn i
|
|
|
246 ... | ⟪ x , zero ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 eq1))
|
|
|
247 (subst (λ k → 0 < k ) ( begin
|
|
|
248 suc k ≡⟨ sym eq ⟩
|
|
|
249 NN.k (nn i) ≡⟨ cong proj2 (sym (NN.k0 (nn i)) ) ⟩
|
|
|
250 proj2 (n→nxn i) ∎ ) (s≤s z≤n )) ) where open ≡-Reasoning -- eq1 n→nxn i ≡ ⟪ x , zero ⟫
|
|
|
251 ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = begin -- n→nxn i ≡ ⟪ x , suc y ⟫
|
|
|
252 ⟪ suc x , y ⟫ ≡⟨ refl ⟩
|
|
|
253 ⟪ suc x , pred (suc y) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin
|
|
|
254 ⟪ x , suc y ⟫ ≡⟨ sym eq1 ⟩
|
|
|
255 n→nxn i ≡⟨ NN.k0 (nn i) ⟩
|
|
|
256 ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ∎ ) ⟩
|
|
|
257 ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫) eq ⟩
|
|
|
258 ⟪ suc (NN.j (nn i)) , k ⟫ ∎ where open ≡-Reasoning
|
|
|
259 nn13 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫
|
|
|
260 nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where -- (nxn→n zero (suc k0)) ≡ suc i
|
|
|
261 nn16 : nxn→n k0 zero ≡ i
|
|
|
262 nn16 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid00 k0 )) eq1 )
|
|
|
263 nn17 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ k0 , zero ⟫
|
|
|
264 nn17 = NN.nn-unique (nn i) nn16
|
|
|
265 nn13 {suc j0} {k0} eq1 = begin
|
|
|
266 ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩
|
|
|
267 ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin
|
|
|
268 ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡⟨ nn15 ⟩
|
|
|
269 ⟪ j0 , suc k0 ⟫ ∎ ) ⟩
|
|
|
270 ⟪ suc j0 , k0 ⟫ ∎ where -- nxn→n (suc j0) k0 ≡ suc i
|
|
|
271 open ≡-Reasoning
|
|
|
272 nn14 : nxn→n j0 (suc k0) ≡ i
|
|
|
273 nn14 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid2 j0 k0 )) eq1 )
|
|
|
274 nn15 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
|
|
|
275 nn15 = NN.nn-unique (nn i) nn14
|
|
|
276
|
|
|
277 n-id : (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
|
|
|
278 n-id i = subst (λ k → nxn→n (proj1 k) (proj2 k) ≡ i ) (sym (NN.k0 (nn i))) (NN.k1 (nn i))
|
|
|
279
|
|
|
280 nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫
|
|
|
281 nn-id j k = begin
|
|
|
282 n→nxn (nxn→n j k) ≡⟨ NN.k0 (nn (nxn→n j k)) ⟩
|
|
|
283 ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩
|
|
|
284 ⟪ j , k ⟫ ∎ where open ≡-Reasoning
|
|
|
285
|
|
|
286
|
|
164
|
287 b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ
|
|
|
288 b1 b = fun→ b (diag b)
|
|
|
289
|
|
|
290 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
|
|
|
291 b-iso b = fiso← b _
|
|
|
292
|
|
141
|
293 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
|
|
|
294 to1 {n} {R} b = record {
|
|
|
295 fun← = to11
|
|
|
296 ; fun→ = to12
|
|
|
297 ; fiso← = to13
|
|
|
298 ; fiso→ = to14
|
|
|
299 } where
|
|
|
300 to11 : ⊤ ∨ R → ℕ
|
|
|
301 to11 (case1 tt) = 0
|
|
|
302 to11 (case2 x) = suc ( fun← b x )
|
|
|
303 to12 : ℕ → ⊤ ∨ R
|
|
|
304 to12 zero = case1 tt
|
|
|
305 to12 (suc n) = case2 ( fun→ b n)
|
|
|
306 to13 : (x : ℕ) → to11 (to12 x) ≡ x
|
|
|
307 to13 zero = refl
|
|
|
308 to13 (suc x) = cong suc (fiso← b x)
|
|
|
309 to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
|
|
|
310 to14 (case1 x) = refl
|
|
|
311 to14 (case2 x) = cong case2 (fiso→ b x)
|
|
|
312
|
|
|
313 open _∧_
|
|
|
314
|
|
172
|
315 open import nat
|
|
|
316
|
|
173
|
317 open ≡-Reasoning
|
|
|
318
|
|
172
|
319 -- [] 0
|
|
|
320 -- 0 → 1
|
|
|
321 -- 1 → 2
|
|
|
322 -- 01 → 3
|
|
|
323 -- 11 → 4
|
|
|
324 -- ...
|
|
141
|
325 --
|
|
172
|
326 {-# TERMINATING #-}
|
|
|
327 LBℕ : Bijection ℕ ( List Bool )
|
|
|
328 LBℕ = record {
|
|
|
329 fun← = λ x → lton x
|
|
|
330 ; fun→ = λ n → ntol n
|
|
|
331 ; fiso← = lbiso0
|
|
173
|
332 ; fiso→ = lbisor
|
|
172
|
333 } where
|
|
|
334 lton1 : List Bool → ℕ
|
|
|
335 lton1 [] = 0
|
|
|
336 lton1 (true ∷ t) = suc (lton1 t + lton1 t)
|
|
|
337 lton1 (false ∷ t) = lton1 t + lton1 t
|
|
|
338 lton : List Bool → ℕ
|
|
|
339 lton [] = 0
|
|
|
340 lton x = suc (lton1 x)
|
|
|
341 ntol1 : ℕ → List Bool
|
|
|
342 ntol1 0 = []
|
|
|
343 ntol1 (suc x) with div2 (suc x)
|
|
181
|
344 ... | ⟪ x1 , true ⟫ = true ∷ ntol1 x1 -- non terminating
|
|
172
|
345 ... | ⟪ x1 , false ⟫ = false ∷ ntol1 x1
|
|
|
346 ntol : ℕ → List Bool
|
|
|
347 ntol 0 = []
|
|
|
348 ntol 1 = false ∷ []
|
|
|
349 ntol (suc n) = ntol1 n
|
|
|
350 xx : (x : ℕ ) → List Bool ∧ ℕ
|
|
|
351 xx x = ⟪ (ntol x) , lton ((ntol x)) ⟫
|
|
181
|
352 add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc (x1 + x1))
|
|
|
353 add11 zero = refl
|
|
|
354 add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x)))
|
|
|
355 add12 : (x1 x : ℕ ) → suc x1 + x ≡ x1 + suc x
|
|
|
356 add12 zero x = refl
|
|
|
357 add12 (suc x1) x = cong suc (add12 x1 x)
|
|
175
|
358 ---- div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
|
|
181
|
359 div20 : (x x1 : ℕ ) → div2 (suc x) ≡ ⟪ x1 , false ⟫ → x1 + x1 ≡ suc x
|
|
|
360 div20 x x1 eq = begin
|
|
|
361 x1 + x1 ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
|
|
|
362 div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
|
|
|
363 suc x ∎
|
|
|
364 div21 : (x x1 : ℕ ) → div2 (suc x) ≡ ⟪ x1 , true ⟫ → suc (x1 + x1) ≡ suc x
|
|
|
365 div21 x x1 eq = begin
|
|
|
366 suc (x1 + x1) ≡⟨ cong (λ k → div2-rev k ) (sym eq) ⟩
|
|
|
367 div2-rev (div2 (suc x)) ≡⟨ div2-eq _ ⟩
|
|
|
368 suc x ∎
|
|
172
|
369 lbiso1 : (x : ℕ) → suc (lton1 (ntol1 x)) ≡ suc x
|
|
173
|
370 lbiso1 zero = refl
|
|
175
|
371 lbiso1 (suc x) with div2 (suc x) | inspect div2 (suc x)
|
|
|
372 ... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin
|
|
181
|
373 suc (suc (lton1 (ntol1 x1) + lton1 (ntol1 x1))) ≡⟨ sym (add11 _) ⟩
|
|
173
|
374 suc (lton1 (ntol1 x1)) + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + k ) (lbiso1 x1) ⟩
|
|
181
|
375 suc x1 + suc x1 ≡⟨ add11 x1 ⟩
|
|
|
376 suc (suc (x1 + x1)) ≡⟨ cong suc (div21 x x1 eq1) ⟩
|
|
173
|
377 suc (suc x) ∎
|
|
181
|
378 ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
|
|
|
379 suc (lton1 (ntol1 x1) + lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + lton1 (ntol1 x1) ) (lbiso1 x1) ⟩
|
|
|
380 suc x1 + lton1 (ntol1 x1) ≡⟨ add12 _ _ ⟩
|
|
|
381 x1 + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → x1 + k ) (lbiso1 x1) ⟩
|
|
|
382 x1 + suc x1 ≡⟨ +-comm x1 _ ⟩
|
|
|
383 suc (x1 + x1) ≡⟨ cong suc (div20 x x1 eq1) ⟩
|
|
|
384 suc (suc x) ∎
|
|
172
|
385 lbiso0 : (x : ℕ) → lton (ntol x) ≡ x
|
|
|
386 lbiso0 zero = refl
|
|
|
387 lbiso0 (suc zero) = refl
|
|
173
|
388 lbiso0 (suc (suc x)) = subst (λ k → k ≡ suc (suc x)) (hh x) ( lbiso1 (suc x)) where
|
|
|
389 hh : (x : ℕ ) → suc (lton1 (ntol1 (suc x))) ≡ lton (ntol (suc (suc x)))
|
|
|
390 hh x with div2 (suc x)
|
|
181
|
391 ... | ⟪ _ , true ⟫ = refl
|
|
|
392 ... | ⟪ _ , false ⟫ = refl
|
|
|
393 lbisor0 : (x : List Bool) → ntol1 (lton1 (true ∷ x)) ≡ true ∷ x
|
|
|
394 lbisor0 = {!!}
|
|
|
395 lbisor1 : (x : List Bool) → ntol1 (lton1 (false ∷ x)) ≡ false ∷ x
|
|
|
396 lbisor1 = {!!}
|
|
173
|
397 lbisor : (x : List Bool) → ntol (lton x) ≡ x
|
|
|
398 lbisor [] = refl
|
|
|
399 lbisor (false ∷ []) = refl
|
|
|
400 lbisor (true ∷ []) = refl
|
|
181
|
401 lbisor (false ∷ t) = trans {!!} ( lbisor1 t )
|
|
|
402 lbisor (true ∷ t) = trans {!!} ( lbisor0 t )
|
|
141
|
403
|
|
|
404
|
