Mercurial > hg > Members > kono > Proof > automaton1

comparison regular-language.agda @ 8:894feefc3084

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
subset construction lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Nov 2020 11:30:49 +0900
parents 7399aae907fc
children 554fa6e5a09d
comparison
equal deleted inserted replaced
7:8f1828ec8d1b 8:894feefc3084
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --allow-unsolved-metas #-}
2 module regular-language where 2 module regular-language where
3 3
4 open import Level renaming ( suc to Suc ; zero to Zero ) 4 open import Level renaming ( suc to Suc ; zero to Zero )
5 open import Data.List 5 open import Data.List hiding ([_])
6 -- open import Data.Nat hiding ( _≟_ ) 6 -- open import Data.Nat hiding ( _≟_ )
7 -- open import Data.Bool 7 -- open import Data.Bool
8 -- open import Data.Fin hiding ( _+_ ) 8 -- open import Data.Fin hiding ( _+_ )
9 open import Data.Empty 9 open import Data.Empty
10 open import Data.Unit 10 open import Data.Unit
58 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) ∧ B [] ) 58 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) ∧ B [] )
59 ) 59 )
60 test-AB→split {_} {A} {B} = refl 60 test-AB→split {_} {A} {B} = refl
61 61
62 open RegularLanguage 62 open RegularLanguage
63 isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set (Suc Zero) 63 isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set
64 isRegular A x r = A x ≡ contain r x 64 isRegular A x r = A x ⇔ contain r x
65 65
66 M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ 66 M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ
67 M-Union {n} {Σ} A B = record { 67 M-Union {n} {Σ} A B = record {
68 states = states A × states B 68 states = states A × states B
69 ; astart = ( astart A , astart B ) 69 ; astart = ( astart A , astart B )
71 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x ) 71 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
72 ; F = λ q → ( F (automaton A) (proj₁ q) ∨ F (automaton B) (proj₂ q) ) 72 ; F = λ q → ( F (automaton A) (proj₁ q) ∨ F (automaton B) (proj₂ q) )
73 } 73 }
74 } 74 }
75 75
76 open _∧_
77
76 closed-in-union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B ) 78 closed-in-union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
77 closed-in-union A B [] = lemma where 79 closed-in-union A B [] = lemma where
78 lemma : F (automaton A) (astart A) ∨ F (automaton B) (astart B) ≡ 80 lemma : (F (automaton A) (astart A) ∨ F (automaton B) (astart B)) ⇔
79 F (automaton A) (astart A) ∨ F (automaton B) (astart B) 81 (F (automaton A) (astart A) ∨ F (automaton B) (astart B))
80 lemma = refl 82 lemma = [ id , id ]
81 closed-in-union {n} {Σ} A B ( h ∷ t ) = lemma4 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where 83 closed-in-union {n} {Σ} A B ( h ∷ t ) = lemma4 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
82 lemma4 : (t : List Σ) → (qa : states A ) → (qb : states B ) → 84 lemma4 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
83 accept (automaton A) qa t ∨ accept (automaton B) qb t 85 (accept (automaton A) qa t ∨ accept (automaton B) qb t)
84 ≡ accept (automaton (M-Union A B)) (qa , qb) t 86 ⇔ accept (automaton (M-Union A B)) (qa , qb) t
85 lemma4 [] qa qb = refl 87 lemma4 [] qa qb = [ id , id ]
86 lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h)) 88 lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
87 89
88 -- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!} 90 -- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!}
89 -- closed-in-concat = {!!} 91 -- closed-in-concat = {!!}
90 92