Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/non-regular.agda @ 296:2f113cac060b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 31 Dec 2021 14:36:44 +0900 |
| parents | 99c2cbe6a862 |
| children | afc7db9b917d |
| 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 |
| 296 | 108 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (phase : ℕ) ( q qd : Q ) : Set where |
| 279 | 109 field |
| 296 | 110 x y z : List Σ |
| 111 trace-z : phase > 1 → Trace fa z qd | |
| 112 trace-yz : phase > 0 → Trace fa (y ++ z) qd | |
| 113 trace-xyz : phase ≡ 0 → Trace fa (x ++ y ++ z) q | |
| 114 trace-xyyz : phase ≡ 0 → Trace fa (x ++ y ++ y ++ z) q | |
| 115 | |
| 116 open import nat | |
| 277 | 117 |
| 295 | 118 make-TA : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) |
| 119 → (tr : Trace fa is q ) | |
| 120 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true | |
| 296 | 121 → TA fa 0 q qd |
| 295 | 122 make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where |
| 294 | 123 open TA |
| 296 | 124 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA fa 1 q qd |
| 295 | 125 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q |
| 296 | 126 ... | true = {!!} |
| 127 ... | false = {!!} | |
| 128 tra-phase1 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true → TA fa 0 q qd | |
| 129 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | |
| 130 ... | true = record { x = [] ; y = y TA0 ; z = z TA0 ; trace-z = λ () ; trace-yz = λ _ → trace-yz TA0 a<sa | |
| 131 ; trace-xyz = λ _ → subst (λ k → Trace fa (y TA0 ++ z TA0) k ) {!!} (trace-yz TA0 a<sa) | |
| 132 ; trace-xyyz = λ _ → {!!}} where | |
| 133 TA0 : {!!} | |
| 295 | 134 TA0 = tra-phase2 (δ fa q i ) is tr p |
| 296 | 135 ... | false = record { x = i ∷ x TA0 ; y = y TA0 ; z = z TA0 ; trace-z = λ () ; trace-yz = λ () |
| 136 ; trace-xyz = λ _ → tnext q (trace-xyz TA0 refl ) ; trace-xyyz = λ _ → tnext q (trace-xyyz TA0 refl )} where | |
| 137 TA0 : TA fa 0 (δ fa q i ) qd | |
| 295 | 138 TA0 = tra-phase1 (δ fa q i ) is tr p |
| 277 | 139 |
| 280 | 140 open RegularLanguage |
| 294 | 141 open import Data.Nat.Properties |
| 142 open import nat | |
| 280 | 143 |
| 274 | 144 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) |
| 280 | 145 lemmaNN r Rg = {!!} where |
| 146 n : ℕ | |
| 147 n = suc (finite (afin r)) | |
| 148 nn = inputnn0 n i0 i1 [] | |
| 149 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true | |
| 294 | 150 nn01 zero = refl |
| 151 nn01 (suc i) with nn01 i | |
| 152 ... | t = {!!} | |
| 280 | 153 nn03 : accept (automaton r) (astart r) nn ≡ true |
| 294 | 154 nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n) |
| 155 count : In2 → List In2 → ℕ | |
| 156 count _ [] = 0 | |
| 157 count i0 (i0 ∷ s) = suc (count i0 s) | |
| 158 count i1 (i1 ∷ s) = suc (count i1 s) | |
| 159 count x (_ ∷ s) = count x s | |
| 160 nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s | |
| 161 nn10 = {!!} | |
| 162 nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t | |
| 163 nn11 = {!!} | |
| 280 | 164 nntrace = trace (automaton r) (astart r) nn |
| 295 | 165 nn04 : Trace (automaton r) nn (astart r) |
| 280 | 166 nn04 = tr-accept← (automaton r) nn (astart r) nn03 |
| 294 | 167 nn07 : (n : ℕ) → length (inputnn0 n i0 i1 []) ≡ n + n |
| 168 nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where | |
| 169 nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s | |
| 170 nn08 zero s = refl | |
| 171 nn08 (suc n) s = begin | |
| 172 length (inputnn0 (suc n) i0 i1 s) ≡⟨ refl ⟩ | |
| 173 suc (length (inputnn0 n i0 i1 (i1 ∷ s))) ≡⟨ cong suc (nn08 n (i1 ∷ s)) ⟩ | |
| 174 suc (n + n + suc (length s)) ≡⟨ +-assoc (suc n) n _ ⟩ | |
| 175 suc n + (n + suc (length s)) ≡⟨ cong (λ k → suc n + k) (sym (+-assoc n _ _)) ⟩ | |
| 176 suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩ | |
| 177 suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n) _ _) ⟩ | |
| 178 suc n + suc n + length s ∎ where open ≡-Reasoning | |
| 179 nn09 : (n m : ℕ) → n ≤ n + m | |
| 180 nn09 zero m = z≤n | |
| 181 nn09 (suc n) m = s≤s (nn09 n m) | |
| 182 nn05 : length nntrace > finite (afin r) | |
| 183 nn05 = begin | |
| 184 suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩ | |
| 185 n + n ≡⟨ sym (nn07 n) ⟩ | |
| 186 length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s ⟩ | |
| 295 | 187 {!!} ≤⟨ {!!} ⟩ |
| 294 | 188 length nntrace ∎ where open ≤-Reasoning |
| 296 | 189 nn02 : {!!} -- TA (automaton r) {!!} {!!} {!!} |
| 295 | 190 nn02 = {!!} where -- make-TA (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) ? where |
| 294 | 191 nn06 : Dup-in-list ( afin r) nntrace |
| 192 nn06 = dup-in-list>n (afin r) nntrace nn05 | |
| 193 nn12 : (x y z : List In2) | |
| 194 → ¬ y ≡ [] | |
| 195 → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true) | |
| 196 nn12 x y z p q = {!!} where | |
| 197 mono-color : List In2 → Bool | |
| 198 mono-color [] = true | |
| 199 mono-color (i0 ∷ s) = mono-color0 s where | |
| 200 mono-color0 : List In2 → Bool | |
| 201 mono-color0 [] = true | |
| 202 mono-color0 (i1 ∷ s) = false | |
| 203 mono-color0 (i0 ∷ s) = mono-color0 s | |
| 204 mono-color (i1 ∷ s) = mono-color1 s where | |
| 205 mono-color1 : List In2 → Bool | |
| 206 mono-color1 [] = true | |
| 207 mono-color1 (i0 ∷ s) = false | |
| 208 mono-color1 (i1 ∷ s) = mono-color1 s | |
| 209 mono-color (i1 ∷ s) = {!!} | |
| 210 i1-i0? : List In2 → Bool | |
| 211 i1-i0? [] = false | |
| 212 i1-i0? (i1 ∷ []) = false | |
| 213 i1-i0? (i0 ∷ []) = false | |
| 214 i1-i0? (i1 ∷ i0 ∷ s) = true | |
| 215 i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1) | |
| 216 nn13 : mono-color y ≡ true → count i0 (x ++ y ++ z) ≡ count i1 (x ++ y ++ z) → | |
| 217 ¬ ( count i0 (x ++ y ++ y ++ z) ≡ count i1 (x ++ y ++ y ++ z) ) | |
| 218 nn13 = {!!} | |
| 219 nn16 : (s : List In2 ) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s | |
| 220 nn16 = {!!} | |
| 221 nn15 : (s : List In2 ) → i1-i0? s ≡ true → accept (automaton r) (astart r) s ≡ false | |
| 222 nn15 = {!!} | |
| 223 nn14 : mono-color y ≡ false → i1-i0? (x ++ y ++ y ++ z) ≡ true | |
| 224 nn14 = {!!} | |
| 225 nn17 : accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true) | |
| 226 nn17 p q with mono-color y | inspect mono-color y | |
| 227 ... | true | record { eq = eq } = {!!} | |
| 228 ... | false | record { eq = eq } = {!!} -- q ( nn15 (x ++ y ++ z) (nn14 eq)) | |
| 229 |