Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/non-regular.agda @ 309:acb0214ea4d8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Jan 2022 15:27:17 +0900 |
| parents | 2effd9a23299 |
| children | 271ded718895 |
| 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 |
| 306 | 15 open import nat |
| 16 | |
| 141 | 17 |
| 274 | 18 open FiniteSet |
| 19 | |
| 20 inputnn : List In2 → Maybe (List In2) | |
| 21 inputnn [] = just [] | |
| 22 inputnn (i1 ∷ t) = just (i1 ∷ t) | |
| 23 inputnn (i0 ∷ t) with inputnn t | |
| 24 ... | nothing = nothing | |
| 25 ... | just [] = nothing | |
| 277 | 26 ... | just (i0 ∷ t1) = nothing -- can't happen |
| 27 ... | just (i1 ∷ t1) = just t1 -- remove i1 from later part | |
| 274 | 28 |
| 29 inputnn1 : List In2 → Bool | |
| 30 inputnn1 s with inputnn s | |
| 31 ... | nothing = false | |
| 32 ... | just [] = true | |
| 33 ... | just _ = false | |
| 34 | |
| 35 t1 = inputnn1 ( i0 ∷ i1 ∷ [] ) | |
| 36 t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) | |
| 277 | 37 t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) |
| 274 | 38 |
| 39 inputnn0 : ( n : ℕ ) → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ | |
| 40 inputnn0 zero {_} _ _ s = s | |
| 41 inputnn0 (suc n) x y s = x ∷ ( inputnn0 n x y ( y ∷ s ) ) | |
| 42 | |
| 43 t4 : inputnn1 ( inputnn0 5 i0 i1 [] ) ≡ true | |
| 44 t4 = refl | |
| 45 | |
| 291 | 46 t5 : ( n : ℕ ) → Set |
| 47 t5 n = inputnn1 ( inputnn0 n i0 i1 [] ) ≡ true | |
| 48 | |
| 274 | 49 -- |
| 50 -- if there is an automaton with n states , which accespt inputnn1, it has a trasition function. | |
| 51 -- The function is determinted by inputs, | |
| 52 -- | |
| 53 | |
| 54 open RegularLanguage | |
| 55 open Automaton | |
| 56 | |
| 57 open _∧_ | |
| 141 | 58 |
| 295 | 59 data Trace { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) : (is : List Σ) → Q → Set where |
| 60 tend : {q : Q} → aend fa q ≡ true → Trace fa [] q | |
| 61 tnext : (q : Q) → {i : Σ} { is : List Σ} | |
| 62 → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q | |
| 277 | 63 |
| 294 | 64 tr-len : { Q : Set } { Σ : Set } |
| 65 → (fa : Automaton Q Σ ) | |
| 295 | 66 → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is ) |
| 67 tr-len {Q} {Σ} fa .[] q (tend x) = refl | |
| 68 tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t) | |
| 294 | 69 |
| 277 | 70 tr-accept→ : { Q : Set } { Σ : Set } |
| 71 → (fa : Automaton Q Σ ) | |
| 295 | 72 → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true |
| 73 tr-accept→ {Q} {Σ} fa [] q (tend x) = x | |
| 74 tr-accept→ {Q} {Σ} fa (i ∷ is) q (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr | |
| 277 | 75 |
| 76 tr-accept← : { Q : Set } { Σ : Set } | |
| 77 → (fa : Automaton Q Σ ) | |
| 295 | 78 → (is : List Σ) → (q : Q) → accept fa q is ≡ true → Trace fa is q |
| 277 | 79 tr-accept← {Q} {Σ} fa [] q ac = tend ac |
| 295 | 80 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac ) |
| 81 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is) (δ fa q x) ac) | |
| 82 | |
| 83 tr→qs : { Q : Set } { Σ : Set } | |
| 84 → (fa : Automaton Q Σ ) | |
| 85 → (is : List Σ) → (q : Q) → Trace fa is q → List Q | |
| 86 tr→qs fa [] q (tend x) = [] | |
| 87 tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr | |
| 88 | |
| 89 tr→qs=is : { Q : Set } { Σ : Set } | |
| 90 → (fa : Automaton Q Σ ) | |
| 91 → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡ length (tr→qs fa is q tr) | |
| 92 tr→qs=is fa .[] q (tend x) = refl | |
| 93 tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is (δ fa q i) tr) | |
| 277 | 94 |
| 294 | 95 open Data.Maybe |
| 96 | |
| 306 | 97 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 98 open import Relation.Binary.Definitions | |
| 99 open import Data.Unit using (⊤ ; tt) | |
| 100 open import Data.Nat.Properties | |
| 294 | 101 |
| 306 | 102 sometime : { a : Set } (x : List a ) → (n : ℕ) → n ≤ length x → (P : a → Set) → Set |
| 103 sometime {a} [] .zero z≤n P = ⊤ | |
| 104 sometime {a} (x ∷ x₁) zero z≤n P = P x | |
| 105 sometime {a} (x ∷ x₁) (suc n) (s≤s lt) P = sometime {a} x₁ n lt P | |
| 294 | 106 |
| 306 | 107 get : { a : Set } (x : List a ) → (n : ℕ) → Maybe a |
| 108 get [] zero = nothing | |
| 109 get [] (suc n) = nothing | |
| 110 get (x ∷ x₁) zero = just x | |
| 111 get (x ∷ x₁) (suc n) = get x₁ n | |
| 277 | 112 |
| 307 | 113 is0-bool : ( i : ℕ ) → Bool |
| 114 is0-bool zero = true | |
| 115 is0-bool (suc i) = false | |
| 116 | |
| 309 | 117 data QDSEQ { Q : Set } { Σ : Set } { fa : Automaton Q Σ} ( finq : FiniteSet Q) (qd : Q) (z1 : List Σ) : |
| 118 {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where | |
| 119 qd-next : (i : Σ) (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ is0-bool (length y2) | |
| 120 → QDSEQ finq qd z1 tr | |
| 121 → QDSEQ finq qd z1 (tnext q tr) | |
| 122 | |
| 302 | 123 record TA1 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) ( q qd : Q ) (is : List Σ) : Set where |
| 299 | 124 field |
| 125 y z : List Σ | |
| 126 yz=is : y ++ z ≡ is | |
| 300 | 127 trace-z : Trace fa z qd |
| 299 | 128 trace-yz : Trace fa (y ++ z) q |
| 307 | 129 q=qd : equal? finq qd q ≡ is0-bool (length y) |
| 299 | 130 |
| 131 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) ( q : Q ) (is : List Σ) : Set where | |
| 279 | 132 field |
| 296 | 133 x y z : List Σ |
| 298 | 134 xyz=is : x ++ y ++ z ≡ is |
| 299 | 135 trace-xyz : Trace fa (x ++ y ++ z) q |
| 136 trace-xyyz : Trace fa (x ++ y ++ y ++ z) q | |
| 304 | 137 non-nil-y : ¬ (y ≡ []) |
| 296 | 138 |
| 305 | 139 make-TA : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (fins : FiniteSet Σ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) |
| 295 | 140 → (tr : Trace fa is q ) |
| 141 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true | |
| 299 | 142 → TA fa q is |
| 305 | 143 make-TA {Q} {Σ} fa fins finq q qd is tr dup = tra-phase1 q is tr dup where |
| 294 | 144 open TA |
| 300 | 145 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) |
| 302 | 146 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is |
| 297 | 147 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q |
| 307 | 148 ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = eq |
| 300 | 149 ; trace-z = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr } |
| 307 | 150 ... | false | record { eq = eq } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) ; q=qd = eq |
| 300 | 151 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where |
| 302 | 152 ta : TA1 fa finq (δ fa q i) qd is |
| 300 | 153 ta = tra-phase2 (δ fa q i) is tr p |
| 299 | 154 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 | 155 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q |
| 298 | 156 | phase1 finq qd (tr→qs fa is (δ fa q i) tr) | inspect ( phase1 finq qd) (tr→qs fa is (δ fa q i) tr) |
| 299 | 157 ... | 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) |
| 304 | 158 ; non-nil-y = λ () |
| 300 | 159 ; trace-xyz = tnext q (TA1.trace-yz ta) |
| 308 | 160 ; trace-xyyz = tra-04 (i ∷ TA1.y ta) q (tnext q (subst (λ k → Trace fa (y1 ++ z1) (δ fa k i) ) (equal→refl finq eq) tryz0)) } where |
| 302 | 161 ta : TA1 fa finq (δ fa q i ) qd is |
| 300 | 162 ta = tra-phase2 (δ fa q i ) is tr p |
| 308 | 163 y1 = TA1.y ta |
| 164 z1 = TA1.z ta | |
| 165 tryz0 : Trace fa (y1 ++ z1) (δ fa qd i) | |
| 166 tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr | |
| 167 tryz : Trace fa (i ∷ y1 ++ z1) qd | |
| 168 tryz = tnext qd tryz0 | |
| 169 tra-06 : equal? finq qd (δ fa q i) ≡ is0-bool (length y1) | |
| 170 tra-06 = TA1.q=qd ta | |
| 171 tra-05 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → equal? finq qd q ≡ is0-bool (length y2) | |
| 172 tra-05 y2 q tr = {!!} | |
| 173 tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) | |
| 306 | 174 → Trace fa (y2 ++ (i ∷ y1) ++ z1) q |
| 308 | 175 tra-04 [] q tr with equal? finq qd q | inspect (equal? finq qd) q |
| 176 ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz | |
| 177 ... | false | record { eq = ne } = ⊥-elim ( ¬-bool ne (tra-05 [] q tr) ) | |
| 178 tra-04 (y0 ∷ y2) q (tnext q tr) with equal? finq qd q | inspect (equal? finq qd) q | |
| 179 ... | true | record { eq = eq } = ⊥-elim ( ¬-bool (tra-05 (y0 ∷ y2) q (tnext q tr)) eq ) where -- y2 + z1 contains two qd | |
| 180 ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr ) | |
| 299 | 181 ... | 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) |
| 304 | 182 ; non-nil-y = non-nil-y ta |
| 299 | 183 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where |
| 184 ta : TA fa (δ fa q i ) is | |
| 185 ta = tra-phase1 (δ fa q i ) is tr np | |
| 186 ... | false | _ | _ | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) | |
| 304 | 187 ; non-nil-y = non-nil-y ta |
| 299 | 188 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where |
| 189 ta : TA fa (δ fa q i ) is | |
| 190 ta = tra-phase1 (δ fa q i ) is tr p | |
| 277 | 191 |
| 280 | 192 open RegularLanguage |
| 294 | 193 open import Data.Nat.Properties |
| 194 open import nat | |
| 280 | 195 |
| 274 | 196 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) |
| 280 | 197 lemmaNN r Rg = {!!} where |
| 198 n : ℕ | |
| 199 n = suc (finite (afin r)) | |
| 200 nn = inputnn0 n i0 i1 [] | |
| 201 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true | |
| 294 | 202 nn01 zero = refl |
| 203 nn01 (suc i) with nn01 i | |
| 204 ... | t = {!!} | |
| 280 | 205 nn03 : accept (automaton r) (astart r) nn ≡ true |
| 294 | 206 nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n) |
| 304 | 207 nn09 : (n m : ℕ) → n ≤ n + m |
| 208 nn09 zero m = z≤n | |
| 209 nn09 (suc n) m = s≤s (nn09 n m) | |
| 295 | 210 nn04 : Trace (automaton r) nn (astart r) |
| 280 | 211 nn04 = tr-accept← (automaton r) nn (astart r) nn03 |
| 304 | 212 nntrace = trace (automaton r) (astart r) nn |
| 294 | 213 nn07 : (n : ℕ) → length (inputnn0 n i0 i1 []) ≡ n + n |
| 214 nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where | |
| 215 nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s | |
| 216 nn08 zero s = refl | |
| 217 nn08 (suc n) s = begin | |
| 218 length (inputnn0 (suc n) i0 i1 s) ≡⟨ refl ⟩ | |
| 219 suc (length (inputnn0 n i0 i1 (i1 ∷ s))) ≡⟨ cong suc (nn08 n (i1 ∷ s)) ⟩ | |
| 220 suc (n + n + suc (length s)) ≡⟨ +-assoc (suc n) n _ ⟩ | |
| 221 suc n + (n + suc (length s)) ≡⟨ cong (λ k → suc n + k) (sym (+-assoc n _ _)) ⟩ | |
| 222 suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩ | |
| 223 suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n) _ _) ⟩ | |
| 224 suc n + suc n + length s ∎ where open ≡-Reasoning | |
| 225 nn05 : length nntrace > finite (afin r) | |
| 226 nn05 = begin | |
| 227 suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩ | |
| 228 n + n ≡⟨ sym (nn07 n) ⟩ | |
| 229 length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s ⟩ | |
| 295 | 230 {!!} ≤⟨ {!!} ⟩ |
| 294 | 231 length nntrace ∎ where open ≤-Reasoning |
| 304 | 232 nn06 : Dup-in-list ( afin r) nntrace |
| 233 nn06 = dup-in-list>n (afin r) nntrace nn05 | |
| 234 TAnn : TA (automaton r) (astart r) nn | |
| 305 | 235 TAnn = make-TA (automaton r) {!!} (afin r) (astart r) {!!} nn {!!} {!!} |
| 304 | 236 count : In2 → List In2 → ℕ |
| 237 count _ [] = 0 | |
| 238 count i0 (i0 ∷ s) = suc (count i0 s) | |
| 239 count i1 (i1 ∷ s) = suc (count i1 s) | |
| 240 count x (_ ∷ s) = count x s | |
| 241 nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t | |
| 242 nn11 = {!!} | |
| 243 nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s | |
| 244 nn10 = {!!} | |
| 245 i1-i0? : List In2 → Bool | |
| 246 i1-i0? [] = false | |
| 247 i1-i0? (i1 ∷ []) = false | |
| 248 i1-i0? (i0 ∷ []) = false | |
| 249 i1-i0? (i1 ∷ i0 ∷ s) = true | |
| 250 i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1) | |
| 251 nn20 : {s s0 s1 : List In2} → accept (automaton r) (astart r) s ≡ true → ¬ ( s ≡ s0 ++ i1 ∷ i0 ∷ s1 ) | |
| 252 nn20 = {!!} | |
| 253 mono-color : List In2 → Bool | |
| 254 mono-color [] = true | |
| 255 mono-color (i0 ∷ s) = mono-color0 s where | |
| 256 mono-color0 : List In2 → Bool | |
| 257 mono-color0 [] = true | |
| 258 mono-color0 (i1 ∷ s) = false | |
| 259 mono-color0 (i0 ∷ s) = mono-color0 s | |
| 260 mono-color (i1 ∷ s) = mono-color1 s where | |
| 261 mono-color1 : List In2 → Bool | |
| 262 mono-color1 [] = true | |
| 263 mono-color1 (i0 ∷ s) = false | |
| 264 mono-color1 (i1 ∷ s) = mono-color1 s | |
| 265 record Is10 (s : List In2) : Set where | |
| 266 field | |
| 267 s0 s1 : List In2 | |
| 268 is-10 : s ≡ s0 ++ i1 ∷ i0 ∷ s1 | |
| 269 not-mono : { s : List In2 } → ¬ (mono-color s ≡ true) → Is10 (s ++ s) | |
| 270 not-mono = {!!} | |
| 271 mono-count : { s : List In2 } → mono-color s ≡ true → (length s ≡ count i0 s) ∨ ( length s ≡ count i1 s) | |
| 272 mono-count = {!!} | |
| 273 tann : {x y z : List In2} → ¬ y ≡ [] → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true ) | |
| 274 tann {x} {y} {z} ny axyz axyyz with mono-color y | |
| 275 ... | true = {!!} | |
| 276 ... | false = {!!} | |
| 277 |