Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/non-regular.agda @ 301:30033f273f1d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 31 Dec 2021 23:06:08 +0900 |
| parents | 67d8e42b7782 |
| children | 55f8031e4214 |
| 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 | |
| 291 | 44 t5 : ( n : ℕ ) → Set |
| 45 t5 n = inputnn1 ( inputnn0 n i0 i1 [] ) ≡ true | |
| 46 | |
| 274 | 47 -- |
| 48 -- if there is an automaton with n states , which accespt inputnn1, it has a trasition function. | |
| 49 -- The function is determinted by inputs, | |
| 50 -- | |
| 51 | |
| 52 open RegularLanguage | |
| 53 open Automaton | |
| 54 | |
| 55 open _∧_ | |
| 141 | 56 |
| 295 | 57 data Trace { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) : (is : List Σ) → Q → Set where |
| 58 tend : {q : Q} → aend fa q ≡ true → Trace fa [] q | |
| 59 tnext : (q : Q) → {i : Σ} { is : List Σ} | |
| 60 → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q | |
| 277 | 61 |
| 294 | 62 tr-len : { Q : Set } { Σ : Set } |
| 63 → (fa : Automaton Q Σ ) | |
| 295 | 64 → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is ) |
| 65 tr-len {Q} {Σ} fa .[] q (tend x) = refl | |
| 66 tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t) | |
| 294 | 67 |
| 277 | 68 tr-accept→ : { Q : Set } { Σ : Set } |
| 69 → (fa : Automaton Q Σ ) | |
| 295 | 70 → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true |
| 71 tr-accept→ {Q} {Σ} fa [] q (tend x) = x | |
| 72 tr-accept→ {Q} {Σ} fa (i ∷ is) q (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr | |
| 277 | 73 |
| 74 tr-accept← : { Q : Set } { Σ : Set } | |
| 75 → (fa : Automaton Q Σ ) | |
| 295 | 76 → (is : List Σ) → (q : Q) → accept fa q is ≡ true → Trace fa is q |
| 277 | 77 tr-accept← {Q} {Σ} fa [] q ac = tend ac |
| 295 | 78 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac ) |
| 79 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is) (δ fa q x) ac) | |
| 80 | |
| 81 tr→qs : { Q : Set } { Σ : Set } | |
| 82 → (fa : Automaton Q Σ ) | |
| 83 → (is : List Σ) → (q : Q) → Trace fa is q → List Q | |
| 84 tr→qs fa [] q (tend x) = [] | |
| 85 tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr | |
| 86 | |
| 87 tr→qs=is : { Q : Set } { Σ : Set } | |
| 88 → (fa : Automaton Q Σ ) | |
| 89 → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡ length (tr→qs fa is q tr) | |
| 90 tr→qs=is fa .[] q (tend x) = refl | |
| 91 tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is (δ fa q i) tr) | |
| 277 | 92 |
| 294 | 93 open Data.Maybe |
| 94 | |
| 95 -- head : {a : Set} → List a → Maybe a | |
| 96 -- head [] = nothing | |
| 97 -- head (h ∷ _ ) = just h | |
| 98 | |
| 99 tr-append1 : { Q : Set } { Σ : Set } | |
| 100 → (fa : Automaton Q Σ ) | |
| 295 | 101 → (i : Σ) → ( q : Q) |
| 294 | 102 → (is : List Σ) |
| 295 | 103 → Trace fa is ( δ fa q i ) → Trace fa (i ∷ is) q |
| 104 tr-append1 fa i q is tr = tnext _ tr | |
| 294 | 105 |
| 279 | 106 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 277 | 107 |
| 300 | 108 record TA1 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) ( q qd : Q ) (is : List Σ) : Set where |
| 299 | 109 field |
| 110 y z : List Σ | |
| 111 yz=is : y ++ z ≡ is | |
| 300 | 112 trace-z : Trace fa z qd |
| 299 | 113 trace-yz : Trace fa (y ++ z) q |
| 114 | |
| 115 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) ( q : Q ) (is : List Σ) : Set where | |
| 279 | 116 field |
| 296 | 117 x y z : List Σ |
| 298 | 118 xyz=is : x ++ y ++ z ≡ is |
| 299 | 119 trace-xyz : Trace fa (x ++ y ++ z) q |
| 120 trace-xyyz : Trace fa (x ++ y ++ y ++ z) q | |
| 296 | 121 |
| 122 open import nat | |
| 277 | 123 |
| 295 | 124 make-TA : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) |
| 125 → (tr : Trace fa is q ) | |
| 126 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true | |
| 299 | 127 → TA fa q is |
| 295 | 128 make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where |
| 294 | 129 open TA |
| 300 | 130 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) |
| 131 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa q qd is | |
| 297 | 132 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q |
| 300 | 133 ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl |
| 134 ; trace-z = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr } | |
| 135 ... | false | record { eq = eq } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) | |
| 136 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where | |
| 137 ta : TA1 fa (δ fa q i) qd is | |
| 138 ta = tra-phase2 (δ fa q i) is tr p | |
| 299 | 139 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 | 140 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q |
| 298 | 141 | phase1 finq qd (tr→qs fa is (δ fa q i) tr) | inspect ( phase1 finq qd) (tr→qs fa is (δ fa q i) tr) |
| 299 | 142 ... | true | record { eq = eq } | false | record { eq = np} = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta) |
| 300 | 143 ; trace-xyz = tnext q (TA1.trace-yz ta) |
| 301 | 144 ; trace-xyyz = tnext q ( tra-02 (TA1.y ta) (δ fa q i) (sym (equal→refl finq eq)) {!!} {!!} {!!} ) } where |
| 145 -- Trace fa ([] ++ (i ∷ TA1.y ta) ++ (i ∷ TA1.y ta) ++ TA1.z ta) q | |
| 300 | 146 -- tra-02 (i ∷ TA1.y ta) q (sym (equal→refl finq eq)) (tnext q (TA1.trace-yz ta)) {!!} {!!} } where |
| 147 ta : TA1 fa (δ fa q i ) qd is | |
| 148 ta = tra-phase2 (δ fa q i ) is tr p | |
| 301 | 149 tra-02 : (y1 : List Σ) → (q0 : Q) → q ≡ qd → (tr : Trace fa (y1 ++ TA1.z ta) q0) |
| 300 | 150 → phase2 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ true |
| 151 → phase1 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ false | |
| 301 | 152 → Trace fa (y1 ++ i ∷ TA1.y ta ++ TA1.z ta) q0 |
| 300 | 153 tra-02 [] q0 q=qd tr p np with equal? finq qd q0 | inspect ( equal? finq qd) q0 |
| 154 ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ TA1.y ta ++ TA1.z ta) k ) {!!} (tnext q (TA1.trace-yz ta) ) where | |
| 155 tra-03 : q ≡ q0 | |
| 156 tra-03 = trans q=qd ((equal→refl finq eq) ) | |
| 298 | 157 ... | false | record { eq = ne } = {!!} |
| 300 | 158 tra-02 (y1 ∷ ys) q0 q=qd (tnext q tr) p np with equal? finq qd q | inspect ( equal? finq qd) q |
| 298 | 159 ... | true | record { eq = eq } = {!!} |
| 300 | 160 ... | false | record { eq = ne } = {!!} -- tnext q (tra-02 ys (δ fa q y1) q=qd tr p np ) |
| 299 | 161 ... | true | record { eq = eq } | true | record { eq = np} = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) |
| 162 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where | |
| 163 ta : TA fa (δ fa q i ) is | |
| 164 ta = tra-phase1 (δ fa q i ) is tr np | |
| 165 ... | false | _ | _ | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) | |
| 166 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where | |
| 167 ta : TA fa (δ fa q i ) is | |
| 168 ta = tra-phase1 (δ fa q i ) is tr p | |
| 277 | 169 |
| 280 | 170 open RegularLanguage |
| 294 | 171 open import Data.Nat.Properties |
| 172 open import nat | |
| 280 | 173 |
| 274 | 174 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) |
| 280 | 175 lemmaNN r Rg = {!!} where |
| 176 n : ℕ | |
| 177 n = suc (finite (afin r)) | |
| 178 nn = inputnn0 n i0 i1 [] | |
| 179 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true | |
| 294 | 180 nn01 zero = refl |
| 181 nn01 (suc i) with nn01 i | |
| 182 ... | t = {!!} | |
| 280 | 183 nn03 : accept (automaton r) (astart r) nn ≡ true |
| 294 | 184 nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n) |
| 185 count : In2 → List In2 → ℕ | |
| 186 count _ [] = 0 | |
| 187 count i0 (i0 ∷ s) = suc (count i0 s) | |
| 188 count i1 (i1 ∷ s) = suc (count i1 s) | |
| 189 count x (_ ∷ s) = count x s | |
| 190 nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s | |
| 191 nn10 = {!!} | |
| 192 nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t | |
| 193 nn11 = {!!} | |
| 280 | 194 nntrace = trace (automaton r) (astart r) nn |
| 295 | 195 nn04 : Trace (automaton r) nn (astart r) |
| 280 | 196 nn04 = tr-accept← (automaton r) nn (astart r) nn03 |
| 294 | 197 nn07 : (n : ℕ) → length (inputnn0 n i0 i1 []) ≡ n + n |
| 198 nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where | |
| 199 nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s | |
| 200 nn08 zero s = refl | |
| 201 nn08 (suc n) s = begin | |
| 202 length (inputnn0 (suc n) i0 i1 s) ≡⟨ refl ⟩ | |
| 203 suc (length (inputnn0 n i0 i1 (i1 ∷ s))) ≡⟨ cong suc (nn08 n (i1 ∷ s)) ⟩ | |
| 204 suc (n + n + suc (length s)) ≡⟨ +-assoc (suc n) n _ ⟩ | |
| 205 suc n + (n + suc (length s)) ≡⟨ cong (λ k → suc n + k) (sym (+-assoc n _ _)) ⟩ | |
| 206 suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩ | |
| 207 suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n) _ _) ⟩ | |
| 208 suc n + suc n + length s ∎ where open ≡-Reasoning | |
| 209 nn09 : (n m : ℕ) → n ≤ n + m | |
| 210 nn09 zero m = z≤n | |
| 211 nn09 (suc n) m = s≤s (nn09 n m) | |
| 212 nn05 : length nntrace > finite (afin r) | |
| 213 nn05 = begin | |
| 214 suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩ | |
| 215 n + n ≡⟨ sym (nn07 n) ⟩ | |
| 216 length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s ⟩ | |
| 295 | 217 {!!} ≤⟨ {!!} ⟩ |
| 294 | 218 length nntrace ∎ where open ≤-Reasoning |
| 296 | 219 nn02 : {!!} -- TA (automaton r) {!!} {!!} {!!} |
| 295 | 220 nn02 = {!!} where -- make-TA (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) ? where |
| 294 | 221 nn06 : Dup-in-list ( afin r) nntrace |
| 222 nn06 = dup-in-list>n (afin r) nntrace nn05 | |
| 223 nn12 : (x y z : List In2) | |
| 224 → ¬ y ≡ [] | |
| 225 → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true) | |
| 226 nn12 x y z p q = {!!} where | |
| 227 mono-color : List In2 → Bool | |
| 228 mono-color [] = true | |
| 229 mono-color (i0 ∷ s) = mono-color0 s where | |
| 230 mono-color0 : List In2 → Bool | |
| 231 mono-color0 [] = true | |
| 232 mono-color0 (i1 ∷ s) = false | |
| 233 mono-color0 (i0 ∷ s) = mono-color0 s | |
| 234 mono-color (i1 ∷ s) = mono-color1 s where | |
| 235 mono-color1 : List In2 → Bool | |
| 236 mono-color1 [] = true | |
| 237 mono-color1 (i0 ∷ s) = false | |
| 238 mono-color1 (i1 ∷ s) = mono-color1 s | |
| 239 mono-color (i1 ∷ s) = {!!} | |
| 240 i1-i0? : List In2 → Bool | |
| 241 i1-i0? [] = false | |
| 242 i1-i0? (i1 ∷ []) = false | |
| 243 i1-i0? (i0 ∷ []) = false | |
| 244 i1-i0? (i1 ∷ i0 ∷ s) = true | |
| 245 i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1) | |
| 246 nn13 : mono-color y ≡ true → count i0 (x ++ y ++ z) ≡ count i1 (x ++ y ++ z) → | |
| 247 ¬ ( count i0 (x ++ y ++ y ++ z) ≡ count i1 (x ++ y ++ y ++ z) ) | |
| 248 nn13 = {!!} | |
| 249 nn16 : (s : List In2 ) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s | |
| 250 nn16 = {!!} | |
| 251 nn15 : (s : List In2 ) → i1-i0? s ≡ true → accept (automaton r) (astart r) s ≡ false | |
| 252 nn15 = {!!} | |
| 253 nn14 : mono-color y ≡ false → i1-i0? (x ++ y ++ y ++ z) ≡ true | |
| 254 nn14 = {!!} | |
| 255 nn17 : accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true) | |
| 256 nn17 p q with mono-color y | inspect mono-color y | |
| 257 ... | true | record { eq = eq } = {!!} | |
| 258 ... | false | record { eq = eq } = {!!} -- q ( nn15 (x ++ y ++ z) (nn14 eq)) | |
| 259 |