Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/regular-concat.agda @ 392:23db567b4098
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Jul 2023 09:03:13 +0900 |
| parents | 1c8ed1220489 |
| children | a60132983557 |
| rev | line source |
|---|---|
| 141 | 1 module regular-concat where |
| 2 | |
| 3 open import Level renaming ( suc to Suc ; zero to Zero ) | |
| 4 open import Data.List | |
| 5 open import Data.Nat hiding ( _≟_ ) | |
| 6 open import Data.Fin hiding ( _+_ ) | |
| 7 open import Data.Empty | |
| 8 open import Data.Unit | |
| 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 | |
| 14 open import nat | |
| 15 open import automaton | |
| 268 | 16 open import regular-language |
| 141 | 17 |
| 18 open import nfa | |
| 19 open import sbconst2 | |
| 268 | 20 open import finiteSet |
| 21 open import finiteSetUtil | |
| 141 | 22 |
| 268 | 23 open Automaton |
| 24 open FiniteSet | |
| 25 | |
| 269 | 26 open RegularLanguage |
| 268 | 27 |
| 28 Concat-NFA : {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ | |
| 29 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } | |
| 141 | 30 module Concat-NFA where |
| 31 δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool | |
| 268 | 32 δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁ |
| 33 δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ | |
| 34 (equal? (afin B) qb (δ (automaton B) (astart B) i) ) | |
| 35 δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁ | |
| 141 | 36 δnfa _ i _ = false |
| 37 nend : states A ∨ states B → Bool | |
| 38 nend (case2 q) = aend (automaton B) q | |
| 39 nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case | |
| 40 | |
| 268 | 41 Concat-NFA-start : {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool |
| 42 Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q | |
| 43 | |
| 44 CNFA-exist : {Σ : Set} → (A B : RegularLanguage Σ ) → (states A ∨ states B → Bool) → Bool | |
| 45 CNFA-exist A B qs = exists (fin-∨ (afin A) (afin B)) qs | |
| 141 | 46 |
| 268 | 47 M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ |
| 48 M-Concat {Σ} A B = record { | |
| 141 | 49 states = states A ∨ states B → Bool |
| 268 | 50 ; astart = Concat-NFA-start A B |
| 51 ; afin = finf | |
| 52 ; automaton = subset-construction (CNFA-exist A B) (Concat-NFA A B) | |
| 141 | 53 } where |
| 268 | 54 fin : FiniteSet (states A ∨ states B ) |
| 55 fin = fin-∨ (afin A) (afin B) | |
| 56 finf : FiniteSet (states A ∨ states B → Bool ) | |
| 57 finf = fin→ fin | |
| 141 | 58 |
| 274 | 59 -- closed-in-concat' : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B ) |
| 60 -- closed-in-concat' {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where | |
| 61 -- closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true | |
| 62 -- closed-in-concat→ = {!!} | |
| 63 -- closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true | |
| 64 -- closed-in-concat← = {!!} | |
| 65 | |
| 141 | 66 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where |
| 67 field | |
| 68 sp0 : List Σ | |
| 69 sp1 : List Σ | |
| 70 sp-concat : sp0 ++ sp1 ≡ x | |
| 71 prop0 : A sp0 ≡ true | |
| 72 prop1 : B sp1 ≡ true | |
| 73 | |
| 74 open Split | |
| 75 | |
| 76 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] ) | |
| 77 list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl } | |
| 78 list-empty++ [] (x ∷ y) () | |
| 79 list-empty++ (x ∷ x₁) y () | |
| 80 | |
| 81 open _∧_ | |
| 82 | |
| 83 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 84 | |
| 85 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true | |
| 86 → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) | |
| 87 → split (λ t1 → A (h ∷ t1)) B t ≡ true | |
| 88 c-split-lemma {Σ} A B h t eq p = sym ( begin | |
| 89 true | |
| 90 ≡⟨ sym eq ⟩ | |
| 91 split A B (h ∷ t ) | |
| 92 ≡⟨⟩ | |
| 93 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t | |
| 94 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩ | |
| 95 false \/ split (λ t1 → A (h ∷ t1)) B t | |
| 96 ≡⟨ bool-or-1 refl ⟩ | |
| 97 split (λ t1 → A (h ∷ t1)) B t | |
| 98 ∎ ) where | |
| 99 open ≡-Reasoning | |
| 100 lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false | |
| 101 lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A ) | |
| 102 lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B ) | |
| 103 | |
| 104 split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x | |
| 105 split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true | |
| 106 split→AB {Σ} A B [] eq | yes eqa | yes eqb = | |
| 107 record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb } | |
| 108 split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p )) | |
| 109 split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p )) | |
| 110 split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true | |
| 111 ... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py } | |
| 112 ... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) ) | |
| 113 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } | |
| 114 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) ) | |
| 115 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } | |
| 116 | |
| 117 AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true | |
| 118 AB→split {Σ} A B [] [] eqa eqb = begin | |
| 119 split A B [] | |
| 120 ≡⟨⟩ | |
| 121 A [] /\ B [] | |
| 122 ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩ | |
| 123 true | |
| 124 ∎ where open ≡-Reasoning | |
| 125 AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin | |
| 126 split A B (h ∷ y ) | |
| 127 ≡⟨⟩ | |
| 128 A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y | |
| 129 ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩ | |
| 130 true /\ true \/ split (λ t1 → A (h ∷ t1)) B y | |
| 131 ≡⟨⟩ | |
| 132 true \/ split (λ t1 → A (h ∷ t1)) B y | |
| 133 ≡⟨⟩ | |
| 134 true | |
| 135 ∎ where open ≡-Reasoning | |
| 136 AB→split {Σ} A B (h ∷ t) y eqa eqb = begin | |
| 137 split A B ((h ∷ t) ++ y) | |
| 138 ≡⟨⟩ | |
| 139 A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y) | |
| 140 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩ | |
| 141 A [] /\ B (h ∷ t ++ y) \/ true | |
| 142 ≡⟨ bool-or-3 ⟩ | |
| 143 true | |
| 144 ∎ where open ≡-Reasoning | |
| 145 | |
| 146 open NAutomaton | |
| 147 open import Data.List.Properties | |
| 148 | |
| 163 | 149 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B ) |
| 141 | 150 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where |
| 163 | 151 finab = (fin-∨ (afin A) (afin B)) |
| 152 NFA = (Concat-NFA A B) | |
| 141 | 153 abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B |
| 154 abmove (case1 q) h = case1 (δ (automaton A) q h) | |
| 155 abmove (case2 q) h = case2 (δ (automaton B) q h) | |
| 156 lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true | |
| 268 | 157 lemma-nmove-ab (case1 q) h = equal?-refl (afin A) |
| 158 lemma-nmove-ab (case2 q) h = equal?-refl (afin B) | |
| 141 | 159 nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) → |
| 163 | 160 exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true |
| 161 nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q) h) ) | |
| 162 nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) | |
| 141 | 163 acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) |
| 268 | 164 → Naccept NFA (CNFA-exist A B) nq z ≡ true |
| 141 | 165 acceptB [] q nq nqt fb = lemma8 where |
| 163 | 166 lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true |
| 167 lemma8 = found finab (case2 q) ( bool-and-tt nqt fb ) | |
| 268 | 168 acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case2 q) nq nq=q h) fb |
| 141 | 169 |
| 170 acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true) | |
| 171 → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) | |
| 268 | 172 → Naccept NFA (CNFA-exist A B) nq (y ++ z) ≡ true |
| 163 | 173 acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb )) |
| 268 | 174 acceptA [] (h ∷ z) q nq nq=q fa fb = acceptB z nextb (Nmoves NFA (CNFA-exist A B) nq h) lemma70 fb where |
| 141 | 175 nextb : states B |
| 176 nextb = δ (automaton B) (astart B) h | |
| 163 | 177 lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true |
| 178 lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) )) | |
| 268 | 179 acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case1 q) nq nq=q h) fa fb |
| 141 | 180 |
| 181 acceptAB : Split (contain A) (contain B) x | |
| 268 | 182 → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x ≡ true |
| 183 acceptAB S = subst ( λ k → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) k ≡ true ) ( sp-concat S ) | |
| 184 (acceptA (sp0 S) (sp1 S) (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) ) | |
| 141 | 185 |
| 163 | 186 closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true |
| 187 closed-in-concat→ concat with split→AB (contain A) (contain B) x concat | |
| 188 ... | S = begin | |
| 268 | 189 accept (subset-construction (CNFA-exist A B) (Concat-NFA A B) ) (Concat-NFA-start A B ) x |
| 190 ≡⟨ ≡-Bool-func (subset-construction-lemma← (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x ) | |
| 191 (subset-construction-lemma→ (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x ) ⟩ | |
| 192 Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x | |
| 163 | 193 ≡⟨ acceptAB S ⟩ |
| 194 true | |
| 195 ∎ where open ≡-Reasoning | |
| 196 | |
| 197 open Found | |
| 141 | 198 |
| 199 ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set | |
| 200 ab-case (case1 qa') qa x = qa' ≡ qa | |
| 201 ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x ≡ true ) | |
| 202 | |
| 268 | 203 contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA (CNFA-exist A B) nq x ≡ true ) |
| 141 | 204 → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x ) |
| 205 → split (accept (automaton A) qa ) (contain B) x ≡ true | |
| 268 | 206 contain-A [] nq fn qa cond with found← finab fn -- at this stage, A and B must be satisfied with [] (ab-case cond forces it) |
| 163 | 207 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) |
| 208 ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S) | |
| 209 ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S))) | |
| 210 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true | |
| 268 | 211 ... | yes eq = bool-or-41 eq -- found A ++ B all end |
| 212 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
213 --- prove ab-case condition (we haven't checked but case2 b may happen) |
| 163 | 214 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 |
| 215 lemma11 (case1 qa') ex with found← finab ex | |
| 216 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) | |
| 217 ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A) ( bool-∧→tt-1 (found-p S) )) -- continued A case | |
| 218 ... | case2 qb | record { eq = refl } | nb with bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false | |
| 219 ... | () | |
| 220 lemma11 (case2 qb) ex with found← finab ex | |
| 221 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) | |
| 222 lemma11 (case2 qb) ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail | |
| 223 lemma13 : accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true | |
| 224 lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb | |
| 225 lemma11 (case2 qb) ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S) | |
| 226 ... | eee = contra-position lemma12 ne where -- starting B case should fail | |
| 227 lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true | |
| 228 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 ) | |
| 141 | 229 |
| 268 | 230 lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true |
| 163 | 231 lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where |
| 232 lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x | |
| 233 lemma15 q nq=t with equal→refl finab nq=t | |
| 234 ... | refl = refl | |
| 141 | 235 |
| 163 | 236 closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true |
| 268 | 237 closed-in-concat← C with subset-construction-lemma← (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x C |
| 163 | 238 ... | CC = lemma10 CC |
| 141 | 239 |
| 240 | |
| 241 | |
| 242 |