Mercurial > hg > Members > kono > Proof > automaton
annotate agda/regular-language.agda @ 110:795850729aaa
clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 17 Nov 2019 18:07:47 +0900 |
| parents | 330fa494f0e8 |
| children | ed0a2dad62f4 |
| rev | line source |
|---|---|
| 65 | 1 module regular-language where |
| 2 | |
| 3 open import Level renaming ( suc to Suc ; zero to Zero ) | |
| 4 open import Data.List | |
| 5 open import Data.Nat hiding ( _≟_ ) | |
| 70 | 6 open import Data.Fin hiding ( _+_ ) |
| 72 | 7 open import Data.Empty |
| 101 | 8 open import Data.Unit |
| 65 | 9 open import Data.Product |
| 10 -- open import Data.Maybe | |
| 11 open import Relation.Nullary | |
| 12 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 13 open import logic | |
| 70 | 14 open import nat |
| 65 | 15 open import automaton |
| 16 open import finiteSet | |
| 17 | |
| 18 language : { Σ : Set } → Set | |
| 19 language {Σ} = List Σ → Bool | |
| 20 | |
| 21 language-L : { Σ : Set } → Set | |
| 22 language-L {Σ} = List (List Σ) | |
| 23 | |
| 24 open Automaton | |
| 25 | |
| 26 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where | |
| 27 field | |
| 28 states : Set | |
| 29 astart : states | |
| 70 | 30 aℕ : ℕ |
| 31 afin : FiniteSet states {aℕ} | |
| 65 | 32 automaton : Automaton states Σ |
| 33 contain : List Σ → Bool | |
| 34 contain x = accept automaton astart x | |
| 35 | |
| 36 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} | |
| 37 Union {Σ} A B x = (A x ) \/ (B x) | |
| 38 | |
| 39 split : {Σ : Set} → (List Σ → Bool) | |
| 40 → ( List Σ → Bool) → List Σ → Bool | |
| 41 split x y [] = x [] /\ y [] | |
| 42 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/ | |
| 43 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t | |
| 44 | |
| 45 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} | |
| 46 Concat {Σ} A B = split A B | |
| 47 | |
| 48 {-# TERMINATING #-} | |
| 49 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ} | |
| 50 Star {Σ} A = split A ( Star {Σ} A ) | |
| 51 | |
| 87 | 52 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ ( |
| 69 | 53 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ |
| 54 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ | |
| 55 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/ | |
| 56 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] ) | |
| 57 ) | |
| 87 | 58 test-AB→split {_} {A} {B} = refl |
| 69 | 59 |
| 65 | 60 open RegularLanguage |
| 61 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set | |
| 62 isRegular A x r = A x ≡ contain r x | |
| 63 | |
| 73 | 64 postulate |
| 65 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b} | |
| 66 | |
| 65 | 67 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ |
| 68 M-Union {Σ} A B = record { | |
| 69 states = states A × states B | |
| 70 ; astart = ( astart A , astart B ) | |
| 73 | 71 ; aℕ = aℕ A * aℕ B |
| 72 ; afin = fin-× (afin A) (afin B) | |
| 65 | 73 ; automaton = record { |
| 74 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x ) | |
| 75 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) ) | |
| 76 } | |
| 77 } | |
| 78 | |
| 79 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B ) | |
| 80 closed-in-union A B [] = lemma where | |
| 81 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡ | |
| 82 aend (automaton A) (astart A) \/ aend (automaton B) (astart B) | |
| 83 lemma = refl | |
| 84 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where | |
| 85 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) → | |
| 86 accept (automaton A) qa t \/ accept (automaton B) qb t | |
| 87 ≡ accept (automaton (M-Union A B)) (qa , qb) t | |
| 88 lemma1 [] qa qb = refl | |
| 89 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h)) | |
| 90 | |
| 91 -- M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ | |
| 92 -- M-Concat {Σ} A B = record { | |
| 93 -- states = states A ∨ states B | |
| 94 -- ; astart = case1 (astart A ) | |
| 95 -- ; automaton = record { | |
| 96 -- δ = {!!} | |
| 97 -- ; aend = {!!} | |
| 98 -- } | |
| 99 -- } | |
| 100 -- | |
| 101 -- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B ) | |
| 102 -- closed-in-concat = {!!} | |
| 70 | 103 |
| 104 open import nfa | |
| 105 open import sbconst2 | |
| 106 open FiniteSet | |
| 86 | 107 open import Data.Nat.Properties hiding ( _≟_ ) |
| 70 | 108 open import Relation.Binary as B hiding (Decidable) |
| 109 | |
| 73 | 110 postulate |
| 111 fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b} | |
| 112 fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a} | |
| 70 | 113 |
| 114 Concat-NFA : {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ | |
| 86 | 115 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } |
| 116 module Concat-NFA where | |
| 70 | 117 δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool |
| 118 δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁ | |
| 88 | 119 δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ |
| 120 (equal? (afin B) qb (δ (automaton B) (astart B) i) ) | |
| 70 | 121 δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁ |
| 122 δnfa _ i _ = false | |
| 123 nend : states A ∨ states B → Bool | |
| 124 nend (case2 q) = aend (automaton B) q | |
| 88 | 125 nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case |
| 70 | 126 |
| 127 Concat-NFA-start : {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool | |
| 75 | 128 Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q |
| 70 | 129 |
| 130 M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ | |
| 131 M-Concat {Σ} A B = record { | |
| 132 states = states A ∨ states B → Bool | |
| 133 ; astart = Concat-NFA-start A B | |
| 134 ; aℕ = finℕ finf | |
| 135 ; afin = finf | |
| 136 ; automaton = subset-construction fin (Concat-NFA A B) (case1 (astart A)) | |
| 137 } where | |
| 138 fin : FiniteSet (states A ∨ states B ) {aℕ A + aℕ B} | |
| 139 fin = fin-∨ (afin A) (afin B) | |
| 140 finf : FiniteSet (states A ∨ states B → Bool ) | |
| 141 finf = fin→ fin | |
| 142 | |
| 72 | 143 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where |
| 144 field | |
| 145 sp0 : List Σ | |
| 146 sp1 : List Σ | |
| 147 sp-concat : sp0 ++ sp1 ≡ x | |
| 148 prop0 : A sp0 ≡ true | |
| 149 prop1 : B sp1 ≡ true | |
| 150 | |
| 151 open Split | |
| 152 | |
| 153 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] ) | |
| 154 list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl } | |
| 155 list-empty++ [] (x ∷ y) () | |
| 156 list-empty++ (x ∷ x₁) y () | |
| 157 | |
| 158 open _∧_ | |
| 159 | |
| 74 | 160 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 71 | 161 |
| 74 | 162 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true |
| 163 → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) | |
| 164 → split (λ t1 → A (h ∷ t1)) B t ≡ true | |
| 165 c-split-lemma {Σ} A B h t eq (case1 ¬p ) = sym ( begin | |
| 166 true | |
| 167 ≡⟨ sym eq ⟩ | |
| 168 split A B (h ∷ t ) | |
| 169 ≡⟨⟩ | |
| 170 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t | |
| 171 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-1 (¬-bool-t ¬p)) ⟩ | |
| 172 false \/ split (λ t1 → A (h ∷ t1)) B t | |
| 173 ≡⟨ bool-or-1 refl ⟩ | |
| 174 split (λ t1 → A (h ∷ t1)) B t | |
| 175 ∎ ) where open ≡-Reasoning | |
| 176 c-split-lemma {Σ} A B h t eq (case2 ¬p ) = sym ( begin | |
| 177 true | |
| 178 ≡⟨ sym eq ⟩ | |
| 179 split A B (h ∷ t ) | |
| 180 ≡⟨⟩ | |
| 181 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t | |
| 182 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-2 (¬-bool-t ¬p)) ⟩ | |
| 183 false \/ split (λ t1 → A (h ∷ t1)) B t | |
| 184 ≡⟨ bool-or-1 refl ⟩ | |
| 185 split (λ t1 → A (h ∷ t1)) B t | |
| 186 ∎ ) where open ≡-Reasoning | |
| 187 | |
| 87 | 188 split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x |
| 189 split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true | |
| 190 split→AB {Σ} A B [] eq | yes eqa | yes eqb = | |
| 73 | 191 record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb } |
| 87 | 192 split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p )) |
| 193 split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p )) | |
| 194 split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true | |
| 74 | 195 ... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py } |
| 87 | 196 ... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) ) |
| 74 | 197 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } |
| 87 | 198 split→AB {Σ} A B (h ∷ t ) eq | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) ) |
| 74 | 199 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } |
| 200 | |
| 87 | 201 AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true |
| 202 AB→split {Σ} A B [] [] eqa eqb = begin | |
| 74 | 203 split A B [] |
| 204 ≡⟨⟩ | |
| 205 A [] /\ B [] | |
| 206 ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩ | |
| 207 true | |
| 208 ∎ where open ≡-Reasoning | |
| 87 | 209 AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin |
| 74 | 210 split A B (h ∷ y ) |
| 211 ≡⟨⟩ | |
| 212 A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y | |
| 213 ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩ | |
| 214 true /\ true \/ split (λ t1 → A (h ∷ t1)) B y | |
| 215 ≡⟨⟩ | |
| 216 true \/ split (λ t1 → A (h ∷ t1)) B y | |
| 217 ≡⟨⟩ | |
| 218 true | |
| 219 ∎ where open ≡-Reasoning | |
| 87 | 220 AB→split {Σ} A B (h ∷ t) y eqa eqb = begin |
| 74 | 221 split A B ((h ∷ t) ++ y) |
| 222 ≡⟨⟩ | |
| 223 A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y) | |
| 224 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) ( begin | |
| 225 split (λ t1 → A (h ∷ t1)) B (t ++ y) | |
| 87 | 226 ≡⟨ AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩ |
| 74 | 227 true |
| 228 ∎ ) ⟩ | |
| 229 A [] /\ B (h ∷ t ++ y) \/ true | |
| 230 ≡⟨ bool-or-3 ⟩ | |
| 231 true | |
| 232 ∎ where open ≡-Reasoning | |
| 233 | |
| 75 | 234 open NAutomaton |
| 89 | 235 open import Data.List.Properties |
| 70 | 236 |
| 71 | 237 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B ) |
| 87 | 238 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where |
| 239 finab = (fin-∨ (afin A) (afin B)) | |
| 76 | 240 NFA = (Concat-NFA A B) |
| 241 abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B | |
| 242 abmove (case1 q) h = case1 (δ (automaton A) q h) | |
| 243 abmove (case2 q) h = case2 (δ (automaton B) q h) | |
| 88 | 244 lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true |
| 245 lemma-nmove-ab (case1 q) _ = equal?-refl (afin A) | |
| 246 lemma-nmove-ab (case2 q) _ = equal?-refl (afin B) | |
| 76 | 247 nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) → |
| 87 | 248 exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true |
| 88 | 249 nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q) h) ) |
| 100 | 250 nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) |
| 88 | 251 acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) |
| 87 | 252 → Naccept NFA finab nq z ≡ true |
| 88 | 253 acceptB [] q nq nqt fb = lemma8 where |
| 87 | 254 lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true |
| 88 | 255 lemma8 = found finab (case2 q) ( bool-and-tt nqt fb ) |
| 256 acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA finab nq h) (nmove (case2 q) nq nq=q h) fb | |
| 257 acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true) | |
| 75 | 258 → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) |
| 87 | 259 → Naccept NFA finab nq (y ++ z) ≡ true |
| 88 | 260 acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb )) |
| 261 acceptA [] (h ∷ z) q nq nq=q fa fb = acceptB z nextb (Nmoves NFA finab nq h) lemma70 fb where | |
| 87 | 262 nextb : states B |
| 263 nextb = δ (automaton B) (astart B) h | |
| 264 lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true | |
| 88 | 265 lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) )) |
| 266 acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA finab nq h) (nmove (case1 q) nq nq=q h) fa fb where | |
| 267 acceptAB : Split (contain A) (contain B) x | |
| 87 | 268 → Naccept NFA finab (equal? finab (case1 (astart A))) x ≡ true |
| 88 | 269 acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k ≡ true ) ( sp-concat S ) |
| 270 (acceptA (sp0 S) (sp1 S) (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) ) | |
| 87 | 271 |
| 272 closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true | |
| 273 closed-in-concat→ concat with split→AB (contain A) (contain B) x concat | |
| 75 | 274 ... | S = begin |
| 87 | 275 accept (subset-construction finab NFA (case1 (astart A))) (Concat-NFA-start A B ) x |
| 276 ≡⟨ ≡-Bool-func (subset-construction-lemma← finab NFA (case1 (astart A)) x ) | |
| 277 (subset-construction-lemma→ finab NFA (case1 (astart A)) x ) ⟩ | |
| 278 Naccept NFA finab (equal? finab (case1 (astart A))) x | |
| 88 | 279 ≡⟨ acceptAB S ⟩ |
| 75 | 280 true |
| 281 ∎ where open ≡-Reasoning | |
| 87 | 282 |
| 92 | 283 open Found |
| 99 | 284 |
| 106 | 285 ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set |
| 286 ab-case (case1 qa') qa x = qa' ≡ qa | |
|
109
330fa494f0e8
closed-in-concat← done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
108
diff
changeset
|
287 ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x ≡ true ) |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
288 |
| 100 | 289 contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true ) |
| 106 | 290 → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x ) |
| 94 | 291 → split (accept (automaton A) qa ) (contain B) x ≡ true |
| 106 | 292 contain-A [] nq fn qa cond with found← finab fn |
| 293 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) | |
| 294 ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S) | |
|
109
330fa494f0e8
closed-in-concat← done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
108
diff
changeset
|
295 ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S))) |
| 100 | 296 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true |
| 95 | 297 ... | yes eq = bool-or-41 eq |
| 106 | 298 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where |
| 299 lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t | |
| 108 | 300 lemma11 (case1 qa') ex with found← finab ex |
| 301 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) | |
| 302 ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A) ( bool-∧→tt-1 (found-p S) )) | |
| 303 ... | case2 qb | record { eq = refl } | nb with bool-∧→tt-1 (found-p S) | |
| 304 ... | () -- δnfa (case2 q) i (case1 q₁) is false | |
| 305 lemma11 (case2 qb) ex with found← finab ex | |
| 306 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) | |
|
109
330fa494f0e8
closed-in-concat← done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
108
diff
changeset
|
307 lemma11 (case2 qb) ex | S | case2 qb' | record { eq = refl } | nb = |
| 110 | 308 contra-position lemma13 nb where |
| 309 lemma13 : accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true | |
| 310 lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb | |
|
109
330fa494f0e8
closed-in-concat← done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
108
diff
changeset
|
311 lemma11 (case2 qb) ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S) |
|
330fa494f0e8
closed-in-concat← done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
108
diff
changeset
|
312 ... | eee = contra-position lemma12 ne where |
|
330fa494f0e8
closed-in-concat← done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
108
diff
changeset
|
313 lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true |
|
330fa494f0e8
closed-in-concat← done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
108
diff
changeset
|
314 lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb ) |
| 87 | 315 |
| 316 lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true | |
| 106 | 317 lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where |
| 318 lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x | |
| 319 lemma15 q nq=t with equal→refl finab nq=t | |
| 320 ... | refl = refl | |
| 87 | 321 |
| 322 closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true | |
| 323 closed-in-concat← C with subset-construction-lemma← finab NFA (case1 (astart A)) x C | |
| 324 ... | CC = lemma10 CC | |
| 325 | |
| 71 | 326 |
| 327 | |
| 87 | 328 |