Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/pumping.agda @ 405:af8f630b7e60
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 18:02:04 +0900 |
| parents | c298981108c1 |
| children |
| rev | line source |
|---|---|
| 405 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 2 | |
| 385 | 3 module pumping where |
| 141 | 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 |
| 15 open import Relation.Nullary | |
| 274 | 16 open import regular-language |
| 306 | 17 open import nat |
| 18 | |
| 141 | 19 |
| 274 | 20 open FiniteSet |
| 21 | |
| 22 -- | |
| 23 -- if there is an automaton with n states , which accespt inputnn1, it has a trasition function. | |
| 24 -- The function is determinted by inputs, | |
| 25 -- | |
| 26 | |
| 27 open RegularLanguage | |
| 28 open Automaton | |
| 29 | |
| 30 open _∧_ | |
| 141 | 31 |
| 295 | 32 data Trace { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) : (is : List Σ) → Q → Set where |
| 33 tend : {q : Q} → aend fa q ≡ true → Trace fa [] q | |
| 34 tnext : (q : Q) → {i : Σ} { is : List Σ} | |
| 35 → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q | |
| 277 | 36 |
| 294 | 37 tr-len : { Q : Set } { Σ : Set } |
| 38 → (fa : Automaton Q Σ ) | |
| 295 | 39 → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is ) |
| 40 tr-len {Q} {Σ} fa .[] q (tend x) = refl | |
| 41 tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t) | |
| 294 | 42 |
| 277 | 43 tr-accept→ : { Q : Set } { Σ : Set } |
| 44 → (fa : Automaton Q Σ ) | |
| 295 | 45 → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true |
| 46 tr-accept→ {Q} {Σ} fa [] q (tend x) = x | |
| 47 tr-accept→ {Q} {Σ} fa (i ∷ is) q (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr | |
| 277 | 48 |
| 49 tr-accept← : { Q : Set } { Σ : Set } | |
| 50 → (fa : Automaton Q Σ ) | |
| 295 | 51 → (is : List Σ) → (q : Q) → accept fa q is ≡ true → Trace fa is q |
| 277 | 52 tr-accept← {Q} {Σ} fa [] q ac = tend ac |
| 295 | 53 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac ) |
| 54 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is) (δ fa q x) ac) | |
| 55 | |
| 56 tr→qs : { Q : Set } { Σ : Set } | |
| 57 → (fa : Automaton Q Σ ) | |
| 58 → (is : List Σ) → (q : Q) → Trace fa is q → List Q | |
| 59 tr→qs fa [] q (tend x) = [] | |
| 60 tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr | |
| 61 | |
| 62 tr→qs=is : { Q : Set } { Σ : Set } | |
| 63 → (fa : Automaton Q Σ ) | |
| 64 → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡ length (tr→qs fa is q tr) | |
| 65 tr→qs=is fa .[] q (tend x) = refl | |
| 66 tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is (δ fa q i) tr) | |
| 277 | 67 |
| 294 | 68 open Data.Maybe |
| 69 | |
| 403 | 70 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 306 | 71 open import Relation.Binary.Definitions |
| 72 open import Data.Unit using (⊤ ; tt) | |
| 73 open import Data.Nat.Properties | |
| 294 | 74 |
| 309 | 75 data QDSEQ { Q : Set } { Σ : Set } { fa : Automaton Q Σ} ( finq : FiniteSet Q) (qd : Q) (z1 : List Σ) : |
| 76 {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where | |
| 311 | 77 qd-nil : (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr |
| 78 qd-next : {i : Σ} (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ false | |
| 309 | 79 → QDSEQ finq qd z1 tr |
| 80 → QDSEQ finq qd z1 (tnext q tr) | |
| 81 | |
| 302 | 82 record TA1 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) ( q qd : Q ) (is : List Σ) : Set where |
| 299 | 83 field |
| 84 y z : List Σ | |
| 85 yz=is : y ++ z ≡ is | |
| 300 | 86 trace-z : Trace fa z qd |
| 299 | 87 trace-yz : Trace fa (y ++ z) q |
| 310 | 88 q=qd : QDSEQ finq qd z trace-yz |
| 316 | 89 |
| 90 -- | |
| 317 | 91 -- using accept ≡ true may simplify the pumping-lemma |
| 316 | 92 -- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧ ... |
| 93 -- | |
| 94 -- like this ... | |
| 95 -- record TA2 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) ( q qd : Q ) (is : List Σ) : Set where | |
| 96 -- field | |
| 97 -- y z : List Σ | |
| 98 -- yz=is : y ++ z ≡ is | |
| 99 -- trace-z : accpet fa z qd ≡ true | |
| 100 -- trace-yz : accept fa (y ++ z) q ≡ true | |
| 101 -- q=qd : last (tr→qs fa q trace-yz) ≡ just qd | |
| 102 -- ¬q=qd : non-last (tr→qs fa q trace-yz) ≡ just qd | |
| 299 | 103 |
| 104 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) ( q : Q ) (is : List Σ) : Set where | |
| 279 | 105 field |
| 296 | 106 x y z : List Σ |
| 298 | 107 xyz=is : x ++ y ++ z ≡ is |
| 299 | 108 trace-xyz : Trace fa (x ++ y ++ z) q |
| 109 trace-xyyz : Trace fa (x ++ y ++ y ++ z) q | |
| 304 | 110 non-nil-y : ¬ (y ≡ []) |
| 296 | 111 |
| 317 | 112 pumping-lemma : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) |
| 295 | 113 → (tr : Trace fa is q ) |
| 114 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true | |
| 299 | 115 → TA fa q is |
| 317 | 116 pumping-lemma {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where |
| 294 | 117 open TA |
| 300 | 118 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) |
| 302 | 119 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is |
| 405 | 120 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq |
| 121 ... | true = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq | |
| 300 | 122 ; trace-z = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr } |
| 405 | 123 ... | false = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) |
| 310 | 124 ; q=qd = tra-08 |
| 300 | 125 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where |
| 302 | 126 ta : TA1 fa finq (δ fa q i) qd is |
| 300 | 127 ta = tra-phase2 (δ fa q i) is tr p |
| 310 | 128 tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i) |
| 129 tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr | |
| 130 tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta)) | |
| 405 | 131 tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) eq (TA1.q=qd ta) |
| 299 | 132 tra-phase1 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true → TA fa q is |
| 405 | 133 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq |
| 134 ... | true = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta) | |
| 304 | 135 ; non-nil-y = λ () |
| 300 | 136 ; trace-xyz = tnext q (TA1.trace-yz ta) |
| 314 | 137 ; trace-xyyz = tnext q tra-05 } where |
| 302 | 138 ta : TA1 fa finq (δ fa q i ) qd is |
| 300 | 139 ta = tra-phase2 (δ fa q i ) is tr p |
| 308 | 140 y1 = TA1.y ta |
| 141 z1 = TA1.z ta | |
| 142 tryz0 : Trace fa (y1 ++ z1) (δ fa qd i) | |
| 143 tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr | |
| 144 tryz : Trace fa (i ∷ y1 ++ z1) qd | |
| 145 tryz = tnext qd tryz0 | |
| 316 | 146 -- create Trace (y ++ y ++ z) |
| 308 | 147 tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) |
| 315 | 148 → QDSEQ finq qd z1 {q} {y2} tr |
| 306 | 149 → Trace fa (y2 ++ (i ∷ y1) ++ z1) q |
| 405 | 150 tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q in eq |
| 151 ... | true = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz | |
| 152 ... | false = ⊥-elim ( ¬-bool refl x₁ ) | |
| 153 tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q in eq | |
| 154 ... | true = ⊥-elim ( ¬-bool x₁ refl ) | |
| 155 ... | false = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) | |
| 314 | 156 tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i) |
| 157 tra-05 with equal→refl finq eq | |
| 158 ... | refl = tra-04 y1 (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta) | |
| 405 | 159 ... | false = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) |
| 304 | 160 ; non-nil-y = non-nil-y ta |
| 299 | 161 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where |
| 162 ta : TA fa (δ fa q i ) is | |
| 163 ta = tra-phase1 (δ fa q i ) is tr p | |
| 277 | 164 |