Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/bijection.agda @ 256:5aff0067b194

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Jul 2021 11:10:15 +0900
parents 3fa72793620b
children 246da8456ad1
comparison
equal deleted inserted replaced
255:4e4e148eb7e5 256:5aff0067b194
1 module bijection where 1 module bijection where
2 2
3 open import Level renaming ( zero to Zero ; suc to Suc ) 3 open import Level renaming ( zero to Zero ; suc to Suc )
4 open import Data.Nat 4 open import Data.Nat
5 open import Data.Maybe 5 open import Data.Maybe
6 open import Data.List hiding ([_]) 6 open import Data.List hiding ([_] ; sum )
7 open import Data.Nat.Properties 7 open import Data.Nat.Properties
8 open import Relation.Nullary 8 open import Relation.Nullary
9 open import Data.Empty 9 open import Data.Empty
10 open import Data.Unit 10 open import Data.Unit hiding ( _≤_ )
11 open import Relation.Binary.Core hiding (_⇔_) 11 open import Relation.Binary.Core hiding (_⇔_)
12 open import Relation.Binary.Definitions 12 open import Relation.Binary.Definitions
13 open import Relation.Binary.PropositionalEquality 13 open import Relation.Binary.PropositionalEquality
14 14
15 open import logic 15 open import logic
16 open import nat
16 17
17 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where 18 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
18 field 19 field
19 fun← : S → R 20 fun← : S → R
20 fun→ : R → S 21 fun→ : R → S
57 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ 58 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
58 not (fun← b n n) 59 not (fun← b n n)
59 ≡⟨⟩ 60 ≡⟨⟩
60 diag b n 61 diag b n
61 ∎ ) where open ≡-Reasoning 62 ∎ ) where open ≡-Reasoning
63
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
62 286
63 b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ 287 b1 : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ
64 b1 b = fun→ b (diag b) 288 b1 b = fun→ b (diag b)
65 289
66 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b) 290 b-iso : (b : Bijection ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)