Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/non-regular.agda @ 405:af8f630b7e60
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 24 Sep 2023 18:02:04 +0900 |
parents | c298981108c1 |
children | b85402051cdb |
rev | line source |
---|---|
405 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
2 | |
141 | 3 module non-regular where |
4 | |
5 open import Data.Nat | |
274 | 6 open import Data.Empty |
141 | 7 open import Data.List |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
277
diff
changeset
|
8 open import Data.Maybe hiding ( map ) |
141 | 9 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
10 open import logic | |
11 open import automaton | |
274 | 12 open import automaton-ex |
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
277
diff
changeset
|
13 open import finiteSetUtil |
141 | 14 open import finiteSet |
392 | 15 open import Relation.Nullary |
274 | 16 open import regular-language |
306 | 17 open import nat |
385 | 18 open import pumping |
306 | 19 |
141 | 20 |
274 | 21 open FiniteSet |
22 | |
385 | 23 list-eq : List In2 → List In2 → Bool |
24 list-eq [] [] = true | |
25 list-eq [] (x ∷ s1) = false | |
26 list-eq (x ∷ s) [] = false | |
27 list-eq (i0 ∷ s) (i0 ∷ s1) = false | |
28 list-eq (i0 ∷ s) (i1 ∷ s1) = false | |
29 list-eq (i1 ∷ s) (i0 ∷ s1) = false | |
392 | 30 list-eq (i1 ∷ s) (i1 ∷ s1) = list-eq s s1 |
385 | 31 |
392 | 32 input-addi0 : ( n : ℕ ) → List In2 → List In2 |
385 | 33 input-addi0 zero x = x |
34 input-addi0 (suc i) x = i0 ∷ input-addi0 i x | |
35 | |
392 | 36 input-addi1 : ( n : ℕ ) → List In2 |
385 | 37 input-addi1 zero = [] |
38 input-addi1 (suc i) = i1 ∷ input-addi1 i | |
274 | 39 |
392 | 40 inputnn0 : ( n : ℕ ) → List In2 |
385 | 41 inputnn0 n = input-addi0 n (input-addi1 n) |
42 | |
43 inputnn1-i1 : (i : ℕ) → List In2 → Bool | |
44 inputnn1-i1 zero [] = true | |
45 inputnn1-i1 (suc _) [] = false | |
46 inputnn1-i1 zero (i1 ∷ x) = false | |
47 inputnn1-i1 (suc i) (i1 ∷ x) = inputnn1-i1 i x | |
48 inputnn1-i1 zero (i0 ∷ x) = false | |
49 inputnn1-i1 (suc _) (i0 ∷ x) = false | |
50 | |
51 inputnn1-i0 : (i : ℕ) → List In2 → ℕ ∧ List In2 | |
52 inputnn1-i0 i [] = ⟪ i , [] ⟫ | |
53 inputnn1-i0 i (i1 ∷ x) = ⟪ i , (i1 ∷ x) ⟫ | |
392 | 54 inputnn1-i0 i (i0 ∷ x) = inputnn1-i0 (suc i) x |
385 | 55 |
56 open _∧_ | |
57 | |
58 inputnn1 : List In2 → Bool | |
59 inputnn1 x = inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) | |
274 | 60 |
61 t1 = inputnn1 ( i0 ∷ i1 ∷ [] ) | |
62 t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) | |
277 | 63 t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) |
274 | 64 |
385 | 65 t4 : inputnn1 ( inputnn0 5 ) ≡ true |
274 | 66 t4 = refl |
67 | |
291 | 68 t5 : ( n : ℕ ) → Set |
385 | 69 t5 n = inputnn1 ( inputnn0 n ) ≡ true |
70 | |
405 | 71 import Level |
72 | |
73 cons-inject : {n : Level.Level } (A : Set n) { a b : A } {x1 x2 : List A} → a ∷ x1 ≡ b ∷ x2 → x1 ≡ x2 | |
74 cons-inject _ refl = refl | |
385 | 75 |
76 append-[] : {A : Set} {x1 : List A } → x1 ++ [] ≡ x1 | |
77 append-[] {A} {[]} = refl | |
78 append-[] {A} {x ∷ x1} = cong (λ k → x ∷ k) (append-[] {A} {x1} ) | |
79 | |
80 open import Data.Nat.Properties | |
81 open import Relation.Binary.Definitions | |
82 open import Relation.Binary.PropositionalEquality | |
291 | 83 |
388 | 84 nn30 : (y : List In2) → (j : ℕ) → proj2 (inputnn1-i0 (suc j) y) ≡ proj2 (inputnn1-i0 j y ) |
85 nn30 [] _ = refl | |
86 nn30 (i0 ∷ y) j = nn30 y (suc j) | |
87 nn30 (i1 ∷ y) _ = refl | |
88 | |
89 nn31 : (y : List In2) → (j : ℕ) → proj1 (inputnn1-i0 (suc j) y) ≡ suc (proj1 (inputnn1-i0 j y )) | |
90 nn31 [] _ = refl | |
91 nn31 (i0 ∷ y) j = nn31 y (suc j) | |
92 nn31 (i1 ∷ y) _ = refl | |
93 | |
385 | 94 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i ) ≡ true |
95 nn01 i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i) where | |
96 nn07 : (j x : ℕ) → x + j ≡ i → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j | |
405 | 97 nn07 zero x eq with input-addi1 i in eq1 |
98 ... | [] = +-comm 0 _ | |
99 ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where | |
385 | 100 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) |
101 nn08 zero () | |
102 nn08 (suc i) () | |
405 | 103 ... | i1 ∷ t = +-comm 0 _ |
392 | 104 nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) ) |
385 | 105 (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) )) |
106 nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i | |
405 | 107 nn09 zero with input-addi1 i in eq1 |
108 ... | [] = refl | |
109 ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where | |
385 | 110 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) |
111 nn08 zero () | |
112 nn08 (suc i) () | |
405 | 113 ... | i1 ∷ t = refl |
392 | 114 nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) |
385 | 115 nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true |
116 nn04 zero = refl | |
117 nn04 (suc i) = nn04 i | |
118 | |
393 | 119 half : (x : List In2) → ℕ |
120 half [] = 0 | |
121 half (x ∷ []) = 0 | |
122 half (x ∷ x₁ ∷ x₂) = suc (half x₂) | |
123 | |
124 top-is-i0 : (x : List In2) → Bool | |
125 top-is-i0 [] = true | |
126 top-is-i0 (i0 ∷ _) = true | |
127 top-is-i0 (i1 ∷ _) = false | |
128 | |
397 | 129 -- if this is easy, we may have an easy proof |
130 -- nn02 : (x : List In2) → inputnn1 x ≡ true → x ≡ inputnn0 (half x) | |
395 | 131 |
274 | 132 -- |
133 -- if there is an automaton with n states , which accespt inputnn1, it has a trasition function. | |
134 -- The function is determinted by inputs, | |
135 -- | |
136 | |
137 open RegularLanguage | |
138 open Automaton | |
139 | |
140 open _∧_ | |
141 | 141 |
277 | 142 |
280 | 143 open RegularLanguage |
294 | 144 open import Data.Nat.Properties |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
145 open import Data.List.Properties |
294 | 146 open import nat |
280 | 147 |
392 | 148 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) |
332 | 149 lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) (TA.xyz=is TAnn) (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyz TAnn) ) |
317 | 150 (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyyz TAnn) ) where |
280 | 151 n : ℕ |
152 n = suc (finite (afin r)) | |
392 | 153 nn = inputnn0 n |
280 | 154 nn03 : accept (automaton r) (astart r) nn ≡ true |
294 | 155 nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n) |
304 | 156 nn09 : (n m : ℕ) → n ≤ n + m |
157 nn09 zero m = z≤n | |
158 nn09 (suc n) m = s≤s (nn09 n m) | |
295 | 159 nn04 : Trace (automaton r) nn (astart r) |
392 | 160 nn04 = tr-accept← (automaton r) nn (astart r) nn03 |
315 | 161 nntrace = tr→qs (automaton r) nn (astart r) nn04 |
392 | 162 nn07 : (n : ℕ) → length (inputnn0 n ) ≡ n + n |
385 | 163 nn07 i = nn19 i where |
164 nn17 : (i : ℕ) → length (input-addi1 i) ≡ i | |
165 nn17 zero = refl | |
166 nn17 (suc i)= cong suc (nn17 i) | |
167 nn18 : (i j : ℕ) → length (input-addi0 j (input-addi1 i)) ≡ j + length (input-addi1 i ) | |
168 nn18 i zero = refl | |
169 nn18 i (suc j)= cong suc (nn18 i j) | |
170 nn19 : (i : ℕ) → length (input-addi0 i ( input-addi1 i )) ≡ i + i | |
171 nn19 i = begin | |
172 length (input-addi0 i ( input-addi1 i )) ≡⟨ nn18 i i ⟩ | |
173 i + length (input-addi1 i) ≡⟨ cong (λ k → i + k) ( nn17 i) ⟩ | |
392 | 174 i + i ∎ where open ≡-Reasoning |
294 | 175 nn05 : length nntrace > finite (afin r) |
176 nn05 = begin | |
177 suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩ | |
178 n + n ≡⟨ sym (nn07 n) ⟩ | |
385 | 179 length (inputnn0 n ) ≡⟨ tr→qs=is (automaton r) (inputnn0 n ) (astart r) nn04 ⟩ |
294 | 180 length nntrace ∎ where open ≤-Reasoning |
315 | 181 nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04) |
304 | 182 nn06 = dup-in-list>n (afin r) nntrace nn05 |
332 | 183 |
304 | 184 TAnn : TA (automaton r) (astart r) nn |
317 | 185 TAnn = pumping-lemma (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06) |
332 | 186 |
385 | 187 open import Tactic.MonoidSolver using (solve; solve-macro) |
188 | |
392 | 189 -- there is a counter example |
190 -- | |
317 | 191 tann : {x y z : List In2} → ¬ y ≡ [] |
192 → x ++ y ++ z ≡ nn | |
193 → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true ) | |
387 | 194 tann {x} {y} {z} ny eq axyz axyyz = ¬-bool (nn10 x y z ny (trans (Rg (x ++ y ++ z)) axyz ) ) (trans (Rg (x ++ y ++ y ++ z)) axyyz ) where |
385 | 195 count0 : (x : List In2) → ℕ |
196 count0 [] = 0 | |
197 count0 (i0 ∷ x) = suc (count0 x) | |
198 count0 (i1 ∷ x) = count0 x | |
199 count1 : (x : List In2) → ℕ | |
200 count1 [] = 0 | |
201 count1 (i1 ∷ x) = suc (count1 x) | |
202 count1 (i0 ∷ x) = count1 x | |
392 | 203 -- |
204 -- prove some obvious fact | |
205 -- | |
387 | 206 c0+1=n : (x : List In2 ) → count0 x + count1 x ≡ length x |
207 c0+1=n [] = refl | |
208 c0+1=n (i0 ∷ t) = cong suc ( c0+1=n t ) | |
209 c0+1=n (i1 ∷ t) = begin | |
392 | 210 count0 t + suc (count1 t) ≡⟨ sym (+-assoc (count0 t) _ _) ⟩ |
211 (count0 t + 1 ) + count1 t ≡⟨ cong (λ k → k + count1 t) (+-comm _ 1 ) ⟩ | |
212 suc (count0 t + count1 t) ≡⟨ cong suc ( c0+1=n t ) ⟩ | |
387 | 213 suc (length t) ∎ where open ≡-Reasoning |
392 | 214 -- |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
215 nn15 : (x : List In2 ) → inputnn1 x ≡ true → count0 x ≡ count1 x |
388 | 216 nn15 x eq = nn18 where |
392 | 217 nn17 : (x : List In2 ) → (count0 x ≡ proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x))) |
388 | 218 ∧ (count1 x ≡ 0 + count1 (proj2 (inputnn1-i0 0 x))) |
219 nn17 [] = ⟪ refl , refl ⟫ | |
220 nn17 (i0 ∷ t ) with nn17 t | |
221 ... | ⟪ eq1 , eq2 ⟫ = ⟪ begin | |
222 suc (count0 t ) ≡⟨ cong suc eq1 ⟩ | |
223 suc (proj1 (inputnn1-i0 0 t) + count0 (proj2 (inputnn1-i0 0 t))) ≡⟨ cong₂ _+_ (sym (nn31 t 0)) (cong count0 (sym (nn30 t 0))) ⟩ | |
392 | 224 proj1 (inputnn1-i0 1 t) + count0 (proj2 (inputnn1-i0 1 t)) ∎ |
388 | 225 , trans eq2 (cong count1 (sym (nn30 t 0))) ⟫ where |
226 open ≡-Reasoning | |
227 nn20 : proj2 (inputnn1-i0 1 t) ≡ proj2 (inputnn1-i0 0 t) | |
228 nn20 = nn30 t 0 | |
229 nn17 (i1 ∷ x₁) = ⟪ refl , refl ⟫ | |
230 nn19 : (n : ℕ) → (y : List In2 ) → inputnn1-i1 n y ≡ true → (count0 y ≡ 0) ∧ (count1 y ≡ n) | |
231 nn19 zero [] eq = ⟪ refl , refl ⟫ | |
232 nn19 zero (i0 ∷ y) () | |
233 nn19 zero (i1 ∷ y) () | |
392 | 234 nn19 (suc i) (i1 ∷ y) eq with nn19 i y eq |
388 | 235 ... | t = ⟪ proj1 t , cong suc (proj2 t ) ⟫ |
236 nn18 : count0 x ≡ count1 x | |
237 nn18 = begin | |
392 | 238 count0 x ≡⟨ proj1 (nn17 x) ⟩ |
239 proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x)) ≡⟨ cong (λ k → proj1 (inputnn1-i0 0 x) + k) | |
240 (proj1 (nn19 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) eq)) ⟩ | |
241 proj1 (inputnn1-i0 0 x) + 0 ≡⟨ +-comm _ 0 ⟩ | |
242 0 + proj1 (inputnn1-i0 0 x) ≡⟨ cong (λ k → 0 + k) (sym (proj2 (nn19 _ _ eq))) ⟩ | |
243 0 + count1 (proj2 (inputnn1-i0 0 x)) ≡⟨ sym (proj2 (nn17 x)) ⟩ | |
388 | 244 count1 x ∎ where open ≡-Reasoning |
392 | 245 distr0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y |
246 distr0 [] y = refl | |
247 distr0 (i0 ∷ x) y = cong suc (distr0 x y) | |
248 distr0 (i1 ∷ x) y = distr0 x y | |
249 distr1 : (x y : List In2 ) → count1 (x ++ y ) ≡ count1 x + count1 y | |
250 distr1 [] y = refl | |
251 distr1 (i1 ∷ x) y = cong suc (distr1 x y) | |
252 distr1 (i0 ∷ x) y = distr1 x y | |
253 -- | |
254 -- i0 .. i0 ∷ i1 .. i1 sequece does not contains i1 → i0 transition | |
255 -- | |
385 | 256 record i1i0 (z : List In2) : Set where |
257 field | |
258 a b : List In2 | |
259 i10 : z ≡ a ++ (i1 ∷ i0 ∷ b ) | |
388 | 260 nn12 : (x : List In2 ) → inputnn1 x ≡ true → ¬ i1i0 x |
391 | 261 nn12 x eq = nn17 x 0 eq where |
392 | 262 nn17 : (x : List In2 ) → (i : ℕ) |
391 | 263 → inputnn1-i1 (proj1 (inputnn1-i0 i x)) (proj2 (inputnn1-i0 i x)) ≡ true → ¬ i1i0 x |
390 | 264 nn17 [] i eq li with i1i0.a li | i1i0.i10 li |
388 | 265 ... | [] | () |
266 ... | x ∷ s | () | |
392 | 267 nn17 (i0 ∷ x₁) i eq li = nn17 x₁ (suc i) eq record { a = nn18 (i1i0.a li) (i1i0.i10 li) ; b = i1i0.b li |
391 | 268 ; i10 = nn19 (i1i0.a li) (i1i0.i10 li) } where |
392 | 269 -- first half |
391 | 270 nn18 : (a : List In2 ) → i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) → List In2 |
271 nn18 (i0 ∷ t) eq = t | |
272 nn19 : (a : List In2 ) → (eq : i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) ) | |
273 → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li | |
405 | 274 nn19 (i0 ∷ a) eq = cons-inject In2 eq |
391 | 275 nn17 (i1 ∷ x₁) i eq li = nn20 (i1 ∷ x₁) i eq li where |
392 | 276 -- second half |
391 | 277 nn20 : (x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → i1i0 x → ⊥ |
392 | 278 nn20 x i eq li = nn21 (i1i0.a li) x i eq (i1i0.i10 li) where |
279 nn21 : (a x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → x ≡ a ++ i1 ∷ i0 ∷ i1i0.b li → ⊥ | |
280 nn21 [] [] zero eq1 () | |
281 nn21 (i0 ∷ a) [] zero eq1 () | |
282 nn21 (i1 ∷ a) [] zero eq1 () | |
283 nn21 a (i0 ∷ x₁) zero () eq0 | |
284 nn21 [] (i0 ∷ x₁) (suc i) () eq0 | |
285 nn21 (x ∷ a) (i0 ∷ x₁) (suc i) () eq0 | |
286 nn21 [] (i1 ∷ i0 ∷ x₁) (suc zero) () eq0 | |
287 nn21 [] (i1 ∷ i0 ∷ x₁) (suc (suc i)) () eq0 | |
405 | 288 nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject In2 eq0) |
387 | 289 nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) |
392 | 290 nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) |
388 | 291 ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where |
392 | 292 -- |
293 -- we need simple calcuraion to obtain count0 y ≡ count1 y | |
294 -- | |
385 | 295 nn21 : count0 x + count0 y + count0 y + count0 z ≡ count1 x + count1 y + count1 y + count1 z |
296 nn21 = begin | |
297 (count0 x + count0 y + count0 y) + count0 z ≡⟨ solve +-0-monoid ⟩ | |
392 | 298 count0 x + (count0 y + (count0 y + count0 z)) ≡⟨ sym (cong (λ k → count0 x + (count0 y + k)) (distr0 y _ )) ⟩ |
299 count0 x + (count0 y + count0 (y ++ z)) ≡⟨ sym (cong (λ k → count0 x + k) (distr0 y _ )) ⟩ | |
300 count0 x + (count0 (y ++ y ++ z)) ≡⟨ sym (distr0 x _ ) ⟩ | |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
301 count0 (x ++ y ++ y ++ z) ≡⟨ nn15 (x ++ y ++ y ++ z) xyyz ⟩ |
392 | 302 count1 (x ++ y ++ y ++ z) ≡⟨ distr1 x _ ⟩ |
303 count1 x + (count1 (y ++ y ++ z)) ≡⟨ cong (λ k → count1 x + k) (distr1 y _ ) ⟩ | |
304 count1 x + (count1 y + count1 (y ++ z)) ≡⟨ (cong (λ k → count1 x + (count1 y + k)) (distr1 y _ )) ⟩ | |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
305 count1 x + (count1 y + (count1 y + count1 z)) ≡⟨ solve +-0-monoid ⟩ |
385 | 306 count1 x + count1 y + count1 y + count1 z ∎ where open ≡-Reasoning |
307 nn20 : count0 x + count0 y + count0 z ≡ count1 x + count1 y + count1 z | |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
308 nn20 = begin |
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
309 count0 x + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ |
392 | 310 count0 x + (count0 y + count0 z) ≡⟨ cong (λ k → count0 x + k) (sym (distr0 y z)) ⟩ |
311 count0 x + (count0 (y ++ z)) ≡⟨ sym (distr0 x _) ⟩ | |
312 count0 (x ++ (y ++ z)) ≡⟨ nn15 (x ++ y ++ z) xyz ⟩ | |
313 count1 (x ++ (y ++ z)) ≡⟨ distr1 x _ ⟩ | |
314 count1 x + count1 (y ++ z) ≡⟨ cong (λ k → count1 x + k) (distr1 y z) ⟩ | |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
315 count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩ |
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
316 count1 x + count1 y + count1 z ∎ where open ≡-Reasoning |
387 | 317 -- this takes very long time to check and needs 10GB |
385 | 318 bb22 : count0 y ≡ count1 y |
403 | 319 bb22 = begin |
405 | 320 count0 y ≡⟨ ? ⟩ |
321 -- count0 y ≡⟨ sym ( +-cancelʳ-≡ (count1 z + count0 x + count0 y + count0 z) (count1 y) (count0 y) (+-cancelˡ-≡ _ (count1 x + count1 y) ( | |
322 -- begin | |
323 -- count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ | |
324 -- (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ | |
325 -- (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ | |
326 -- (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ | |
327 -- count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z | |
328 -- ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ | |
329 -- count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ | |
330 -- count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z | |
331 -- ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ | |
332 -- count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ | |
333 -- count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ | |
403 | 334 count1 y ∎ where open ≡-Reasoning |
392 | 335 -- |
336 -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y | |
337 -- | |
385 | 338 bb23 : count0 y ≡ count1 y → i1i0 (y ++ y) |
387 | 339 bb23 eq = bb25 y y bb26 (subst (λ k → 0 < k ) (sym eq) bb26) where |
340 bb26 : 0 < count1 y | |
341 bb26 with <-cmp 0 (count1 y) | |
342 ... | tri< a ¬b ¬c = a | |
343 ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (sym bb27 ) (0<ly y ny) ) where | |
392 | 344 0<ly : (y : List In2) → ¬ y ≡ [] → 0 < length y |
387 | 345 0<ly [] ne = ⊥-elim ( ne refl ) |
346 0<ly (x ∷ y) ne = s≤s z≤n | |
347 bb27 : length y ≡ 0 | |
348 bb27 = begin | |
349 length y ≡⟨ sym (c0+1=n y) ⟩ | |
350 count0 y + count1 y ≡⟨ cong (λ k → k + count1 y ) eq ⟩ | |
351 count1 y + count1 y ≡⟨ cong₂ _+_ (sym b) (sym b) ⟩ | |
352 0 ∎ where open ≡-Reasoning | |
353 bb25 : (x y : List In2 ) → 0 < count1 x → 0 < count0 y → i1i0 (x ++ y) | |
354 bb25 (i0 ∷ x₁) y 0<x 0<y with bb25 x₁ y 0<x 0<y | |
355 ... | t = record { a = i0 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i0 ∷_) (i1i0.i10 t) } | |
356 bb25 (i1 ∷ []) y 0<x 0<y = bb27 y 0<y where | |
357 bb27 : (y : List In2 ) → 0 < count0 y → i1i0 (i1 ∷ y ) | |
392 | 358 bb27 (i0 ∷ y) 0<y = record { a = [] ; b = y ; i10 = refl } |
387 | 359 bb27 (i1 ∷ y) 0<y with bb27 y 0<y |
360 ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) } | |
361 bb25 (i1 ∷ i0 ∷ x₁) y 0<x 0<y = record { a = [] ; b = x₁ ++ y ; i10 = refl } | |
362 bb25 (i1 ∷ i1 ∷ x₁) y (s≤s z≤n) 0<y with bb25 (i1 ∷ x₁) y (s≤s z≤n) 0<y | |
363 ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) } | |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
364 bb24 : x ++ y ++ y ++ z ≡ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z |
385 | 365 bb24 = begin |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
366 x ++ y ++ y ++ z ≡⟨ solve (++-monoid In2) ⟩ |
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
367 x ++ (y ++ y) ++ z ≡⟨ cong (λ k → x ++ k ++ z) (i1i0.i10 (bb23 bb22)) ⟩ |
387 | 368 x ++ (i1i0.a (bb23 bb22) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) ++ z ≡⟨ cong (λ k → x ++ k) -- solver does not work here |
369 (++-assoc (i1i0.a (bb23 bb22)) (i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) z ) ⟩ | |
370 x ++ (i1i0.a (bb23 bb22) ++ (i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z)) ≡⟨ sym (++-assoc x _ _ ) ⟩ | |
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
371 (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning |
385 | 372 |
387 | 373 nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false |
405 | 374 nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) in eq1 |
375 ... | true = ⊥-elim ( nn11 x y z my eq eq1 ) | |
376 ... | false = refl | |
385 | 377 |
304 | 378 |
385 | 379 |
380 | |
381 | |
382 |