Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/non-regular.agda @ 405:af8f630b7e60

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 Sun, 24 Sep 2023 18:02:04 +0900
parents c298981108c1
children b85402051cdb
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 module non-regular where 3 module non-regular where
2 4
3 open import Data.Nat 5 open import Data.Nat
4 open import Data.Empty 6 open import Data.Empty
5 open import Data.List 7 open import Data.List
64 t4 = refl 66 t4 = refl
65 67
66 t5 : ( n : ℕ ) → Set 68 t5 : ( n : ℕ ) → Set
67 t5 n = inputnn1 ( inputnn0 n ) ≡ true 69 t5 n = inputnn1 ( inputnn0 n ) ≡ true
68 70
69 cons-inject : {A : Set} {x1 x2 : List A } { a : A } → a ∷ x1 ≡ a ∷ x2 → x1 ≡ x2 71 import Level
70 cons-inject refl = refl 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
71 75
72 append-[] : {A : Set} {x1 : List A } → x1 ++ [] ≡ x1 76 append-[] : {A : Set} {x1 : List A } → x1 ++ [] ≡ x1
73 append-[] {A} {[]} = refl 77 append-[] {A} {[]} = refl
74 append-[] {A} {x ∷ x1} = cong (λ k → x ∷ k) (append-[] {A} {x1} ) 78 append-[] {A} {x ∷ x1} = cong (λ k → x ∷ k) (append-[] {A} {x1} )
75 79
88 nn31 (i1 ∷ y) _ = refl 92 nn31 (i1 ∷ y) _ = refl
89 93
90 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i ) ≡ true 94 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i ) ≡ true
91 nn01 i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i) where 95 nn01 i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i) where
92 nn07 : (j x : ℕ) → x + j ≡ i → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j 96 nn07 : (j x : ℕ) → x + j ≡ i → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j
93 nn07 zero x eq with input-addi1 i | inspect input-addi1 i 97 nn07 zero x eq with input-addi1 i in eq1
94 ... | [] | _ = +-comm 0 _ 98 ... | [] = +-comm 0 _
95 ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where 99 ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where
96 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) 100 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t )
97 nn08 zero () 101 nn08 zero ()
98 nn08 (suc i) () 102 nn08 (suc i) ()
99 ... | i1 ∷ t | _ = +-comm 0 _ 103 ... | i1 ∷ t = +-comm 0 _
100 nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) ) 104 nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) )
101 (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) )) 105 (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) ))
102 nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i 106 nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i
103 nn09 zero with input-addi1 i | inspect input-addi1 i 107 nn09 zero with input-addi1 i in eq1
104 ... | [] | _ = refl 108 ... | [] = refl
105 ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where 109 ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where
106 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) 110 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t )
107 nn08 zero () 111 nn08 zero ()
108 nn08 (suc i) () 112 nn08 (suc i) ()
109 ... | i1 ∷ t | _ = refl 113 ... | i1 ∷ t = refl
110 nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) 114 nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j )
111 nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true 115 nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true
112 nn04 zero = refl 116 nn04 zero = refl
113 nn04 (suc i) = nn04 i 117 nn04 (suc i) = nn04 i
114 118
265 -- first half 269 -- first half
266 nn18 : (a : List In2 ) → i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) → List In2 270 nn18 : (a : List In2 ) → i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) → List In2
267 nn18 (i0 ∷ t) eq = t 271 nn18 (i0 ∷ t) eq = t
268 nn19 : (a : List In2 ) → (eq : i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) ) 272 nn19 : (a : List In2 ) → (eq : i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) )
269 → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li 273 → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li
270 nn19 (i0 ∷ a) eq = cons-inject eq 274 nn19 (i0 ∷ a) eq = cons-inject In2 eq
271 nn17 (i1 ∷ x₁) i eq li = nn20 (i1 ∷ x₁) i eq li where 275 nn17 (i1 ∷ x₁) i eq li = nn20 (i1 ∷ x₁) i eq li where
272 -- second half 276 -- second half
273 nn20 : (x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → i1i0 x → ⊥ 277 nn20 : (x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → i1i0 x → ⊥
274 nn20 x i eq li = nn21 (i1i0.a li) x i eq (i1i0.i10 li) where 278 nn20 x i eq li = nn21 (i1i0.a li) x i eq (i1i0.i10 li) where
275 nn21 : (a x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → x ≡ a ++ i1 ∷ i0 ∷ i1i0.b li → ⊥ 279 nn21 : (a x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → x ≡ a ++ i1 ∷ i0 ∷ i1i0.b li → ⊥
279 nn21 a (i0 ∷ x₁) zero () eq0 283 nn21 a (i0 ∷ x₁) zero () eq0
280 nn21 [] (i0 ∷ x₁) (suc i) () eq0 284 nn21 [] (i0 ∷ x₁) (suc i) () eq0
281 nn21 (x ∷ a) (i0 ∷ x₁) (suc i) () eq0 285 nn21 (x ∷ a) (i0 ∷ x₁) (suc i) () eq0
282 nn21 [] (i1 ∷ i0 ∷ x₁) (suc zero) () eq0 286 nn21 [] (i1 ∷ i0 ∷ x₁) (suc zero) () eq0
283 nn21 [] (i1 ∷ i0 ∷ x₁) (suc (suc i)) () eq0 287 nn21 [] (i1 ∷ i0 ∷ x₁) (suc (suc i)) () eq0
284 nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject eq0) 288 nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject In2 eq0)
285 nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) 289 nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true )
286 nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) 290 nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 )
287 ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where 291 ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where
288 -- 292 --
289 -- we need simple calcuraion to obtain count0 y ≡ count1 y 293 -- we need simple calcuraion to obtain count0 y ≡ count1 y
311 count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩ 315 count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩
312 count1 x + count1 y + count1 z ∎ where open ≡-Reasoning 316 count1 x + count1 y + count1 z ∎ where open ≡-Reasoning
313 -- this takes very long time to check and needs 10GB 317 -- this takes very long time to check and needs 10GB
314 bb22 : count0 y ≡ count1 y 318 bb22 : count0 y ≡ count1 y
315 bb22 = begin 319 bb22 = begin
316 count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( 320 count0 y ≡⟨ ? ⟩
317 begin 321 -- count0 y ≡⟨ sym ( +-cancelʳ-≡ (count1 z + count0 x + count0 y + count0 z) (count1 y) (count0 y) (+-cancelˡ-≡ _ (count1 x + count1 y) (
318 count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ 322 -- begin
319 (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ 323 -- count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩
320 (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ 324 -- (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩
321 (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ 325 -- (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩
322 count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z 326 -- (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩
323 ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ 327 -- count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z
324 count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ 328 -- ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩
325 count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z 329 -- count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩
326 ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ 330 -- count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z
327 count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ 331 -- ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩
328 count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 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)) ∎ ))) ⟩
329 count1 y ∎ where open ≡-Reasoning 334 count1 y ∎ where open ≡-Reasoning
330 -- 335 --
331 -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y 336 -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y
332 -- 337 --
333 bb23 : count0 y ≡ count1 y → i1i0 (y ++ y) 338 bb23 : count0 y ≡ count1 y → i1i0 (y ++ y)
364 (++-assoc (i1i0.a (bb23 bb22)) (i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) z ) ⟩ 369 (++-assoc (i1i0.a (bb23 bb22)) (i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) z ) ⟩
365 x ++ (i1i0.a (bb23 bb22) ++ (i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z)) ≡⟨ sym (++-assoc x _ _ ) ⟩ 370 x ++ (i1i0.a (bb23 bb22) ++ (i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z)) ≡⟨ sym (++-assoc x _ _ ) ⟩
366 (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning 371 (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning
367 372
368 nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false 373 nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false
369 nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) | inspect inputnn1 (x ++ y ++ y ++ z) 374 nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) in eq1
370 ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z my eq eq1 ) 375 ... | true = ⊥-elim ( nn11 x y z my eq eq1 )
371 ... | false | _ = refl 376 ... | false = refl
372 377
373 378
374 379
375 380
376 381
377 382