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