Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/non-regular.agda @ 285:6e85b8b0d8db
remove ls<n
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Dec 2021 00:28:29 +0900 |
| parents | 681df12f0edc |
| children | c7fbb0b61a8b |
| rev | line source |
|---|---|
| 141 | 1 module non-regular where |
| 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 |
| 141 | 15 |
| 274 | 16 open FiniteSet |
| 17 | |
| 18 inputnn : List In2 → Maybe (List In2) | |
| 19 inputnn [] = just [] | |
| 20 inputnn (i1 ∷ t) = just (i1 ∷ t) | |
| 21 inputnn (i0 ∷ t) with inputnn t | |
| 22 ... | nothing = nothing | |
| 23 ... | just [] = nothing | |
| 277 | 24 ... | just (i0 ∷ t1) = nothing -- can't happen |
| 25 ... | just (i1 ∷ t1) = just t1 -- remove i1 from later part | |
| 274 | 26 |
| 27 inputnn1 : List In2 → Bool | |
| 28 inputnn1 s with inputnn s | |
| 29 ... | nothing = false | |
| 30 ... | just [] = true | |
| 31 ... | just _ = false | |
| 32 | |
| 33 t1 = inputnn1 ( i0 ∷ i1 ∷ [] ) | |
| 34 t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) | |
| 277 | 35 t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) |
| 274 | 36 |
| 37 inputnn0 : ( n : ℕ ) → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ | |
| 38 inputnn0 zero {_} _ _ s = s | |
| 39 inputnn0 (suc n) x y s = x ∷ ( inputnn0 n x y ( y ∷ s ) ) | |
| 40 | |
| 41 t4 : inputnn1 ( inputnn0 5 i0 i1 [] ) ≡ true | |
| 42 t4 = refl | |
| 43 | |
| 44 -- | |
| 45 -- if there is an automaton with n states , which accespt inputnn1, it has a trasition function. | |
| 46 -- The function is determinted by inputs, | |
| 47 -- | |
| 48 | |
| 49 open RegularLanguage | |
| 50 open Automaton | |
| 51 | |
| 52 open _∧_ | |
| 141 | 53 |
| 277 | 54 data Trace { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) : (is : List Σ) → ( List Q) → Set where |
| 55 tend : {q : Q} → aend fa q ≡ true → Trace fa [] (q ∷ []) | |
| 56 tnext : {q : Q} → {i : Σ} { is : List Σ} {qs : List Q} | |
| 57 → Trace fa is (δ fa q i ∷ qs) → Trace fa (i ∷ is) ( q ∷ δ fa q i ∷ qs ) | |
| 58 | |
| 59 tr-accept→ : { Q : Set } { Σ : Set } | |
| 60 → (fa : Automaton Q Σ ) | |
| 61 → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → accept fa q is ≡ true | |
| 62 tr-accept→ {Q} {Σ} fa [] q [] (tend x) = x | |
| 63 tr-accept→ {Q} {Σ} fa (i ∷ is) q (x ∷ qs) (tnext tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) qs tr | |
| 64 | |
| 65 tr-accept← : { Q : Set } { Σ : Set } | |
| 66 → (fa : Automaton Q Σ ) | |
| 67 → (is : List Σ) → (q : Q) → accept fa q is ≡ true → Trace fa is (trace fa q is) | |
| 68 tr-accept← {Q} {Σ} fa [] q ac = tend ac | |
| 69 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext (tend ac ) | |
| 70 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext (tr-accept← fa (x1 ∷ is) (δ fa q x) ac) | |
| 71 | |
| 279 | 72 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 277 | 73 |
| 279 | 74 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) {is : List Σ} { qs : List Q } (tr : Trace fa is qs) : Set where |
| 75 field | |
| 76 x y z : List Σ | |
| 77 qx qy qz : List Q | |
| 78 trace0 : Trace fa (x ++ y ++ z) (qx ++ qy ++ qz) | |
| 79 trace1 : Trace fa (x ++ y ++ y ++ z) (qx ++ qy ++ qy ++ qz) | |
| 80 trace-eq : trace0 ≅ tr | |
| 277 | 81 |
| 82 tr-append : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q ) | |
| 279 | 83 → dup-in-list finq q qs ≡ true |
| 84 → (tr : Trace fa is qs ) → TA fa tr | |
| 85 tr-append {Q} {Σ} fa finq q is qs dup tr = tra-phase1 qs is tr dup where | |
| 86 tra-phase3 : (qs : List Q) → (is : List Σ) → (tr : Trace fa is qs ) → {!!} | |
| 87 → (qy : List Q) → (iy : List Σ) → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true → {!!} | |
| 88 → Trace fa (iy ++ is) (qy ++ qs) | |
| 89 tra-phase3 = {!!} | |
| 90 tra-phase2 : (qs : List Q) → (is : List Σ) → (tr : Trace fa is qs ) → phase2 finq q qs ≡ true | |
| 91 → (qy : List Q) → (iy : List Σ) → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true | |
| 92 → TA fa tr | |
| 93 tra-phase2 (q0 ∷ []) is (tend x₁) p qy iy ty py = {!!} | |
| 94 tra-phase2 (q0 ∷ (q₁ ∷ qs)) (x ∷ is) (tnext tr) p qy iy ty py with equal? finq q q0 | |
| 95 ... | true = {!!} | |
| 96 ... | false = {!!} where | |
| 97 tr1 : TA fa tr | |
| 98 tr1 = tra-phase2 (q₁ ∷ qs) is tr p qy iy ty py | |
| 99 tra-phase1 : (qs : List Q) → (is : List Σ) → (tr : Trace fa is qs ) → phase1 finq q qs ≡ true → TA fa tr | |
| 100 tra-phase1 (q0 ∷ []) is (tend x₁) p = {!!} | |
| 101 tra-phase1 (q0 ∷ (q₁ ∷ qs)) (x ∷ is) (tnext tr) p with equal? finq q q0 | |
| 102 ... | true = {!!} where | |
| 103 tr2 : TA fa tr | |
| 104 tr2 = tra-phase2 (q₁ ∷ qs) is tr p (q₁ ∷ qs) is tr p | |
| 105 ... | false = {!!} where | |
| 106 tr1 : TA fa tr | |
| 107 tr1 = tra-phase1 (q₁ ∷ qs) is tr p | |
| 277 | 108 |
| 280 | 109 open RegularLanguage |
| 110 | |
| 274 | 111 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) |
| 280 | 112 lemmaNN r Rg = {!!} where |
| 113 n : ℕ | |
| 114 n = suc (finite (afin r)) | |
| 115 nn = inputnn0 n i0 i1 [] | |
| 116 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true | |
| 117 nn01 = {!!} | |
| 118 nn03 : accept (automaton r) (astart r) nn ≡ true | |
| 119 nn03 = {!!} | |
| 120 nntrace = trace (automaton r) (astart r) nn | |
| 121 nn04 : Trace (automaton r) nn nntrace | |
| 122 nn04 = tr-accept← (automaton r) nn (astart r) nn03 | |
| 123 nn02 : TA (automaton r) nn04 | |
| 124 nn02 = tr-append (automaton r) (afin r) (Dup-in-list.dup nn05) _ _ (Dup-in-list.is-dup nn05) nn04 where | |
| 125 nn05 : Dup-in-list ( afin r) nntrace | |
| 126 nn05 = dup-in-list>n (afin r) nntrace {!!} | |
| 127 |