Mercurial > hg > Members > kono > Proof > automaton

comparison agda/sbconst2.agda @ 141:b3f05cd08d24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 27 Dec 2020 13:26:44 +0900
parents 702ce92c45ab
children
comparison
equal deleted inserted replaced
140:4c3fbfde1bc2 141:b3f05cd08d24
8 open import automaton 8 open import automaton
9 open import nfa 9 open import nfa
10 open import logic 10 open import logic
11 open NAutomaton 11 open NAutomaton
12 open Automaton 12 open Automaton
13 open import finiteSet
14 open FiniteSet
15 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 13 open import Relation.Binary.PropositionalEquality hiding ( [_] )
16
17 14
18 open Bool 15 open Bool
19 16
20 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool) 17 δconv : { Q : Set } { Σ : Set } → ( ( Q → Bool ) → Bool ) → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
21 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r /\ nδ r i q ) 18 δconv {Q} { Σ} exists nδ f i q = exists ( λ r → f r /\ nδ r i q )
22 19
23 open FiniteSet 20 subset-construction : { Q : Set } { Σ : Set } →
24 21 ( ( Q → Bool ) → Bool ) →
25 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → 22 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )
26 (NAutomaton Q Σ ) → (astart : Q ) → (Automaton (Q → Bool) Σ ) 23 subset-construction {Q} { Σ} exists NFA = record {
27 subset-construction {Q} { Σ} {n} fin NFA astart = record { 24 δ = λ q x → δconv exists ( Nδ NFA ) q x
28 δ = λ q x → δconv fin ( Nδ NFA ) q x 25 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q )
29 ; aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
30 } 26 }
31 27
32 am2start = λ q1 → equal? finState1 ss q1 28 test4 = subset-construction existsS1 am2
33 29
34 test4 = subset-construction finState1 am2 ss 30 test51 = accept test4 start1 ( i0 ∷ i1 ∷ i0 ∷ [] )
31 test61 = accept test4 start1 ( i1 ∷ i1 ∷ i1 ∷ [] )
35 32
36 test5 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i0 ∷ i1 ∷ i0 ∷ [] ) 33 subset-construction-lemma→ : { Q : Set } { Σ : Set } { n : ℕ } → (exists : ( Q → Bool ) → Bool ) →
37 test6 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i1 ∷ i1 ∷ i1 ∷ [] ) 34 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool )
35 → (x : List Σ)
36 → Naccept NFA exists astart x ≡ true
37 → accept ( subset-construction exists NFA ) astart x ≡ true
38 subset-construction-lemma→ {Q} {Σ} {n} exists NFA astart x naccept = lemma1 x astart naccept where
39 lemma1 : (x : List Σ) → ( states : Q → Bool )
40 → Naccept NFA exists states x ≡ true
41 → accept ( subset-construction exists NFA ) states x ≡ true
42 lemma1 [] states naccept = naccept
43 lemma1 (h ∷ t ) states naccept = lemma1 t (δconv exists (Nδ NFA) states h) naccept
38 44
39 subset-construction-lemma→ : { Q : Set } { Σ : Set } { n : ℕ } → (fin : FiniteSet Q {n} ) → 45 subset-construction-lemma← : { Q : Set } { Σ : Set } { n : ℕ } → (exists : ( Q → Bool ) → Bool ) →
40 (NFA : NAutomaton Q Σ ) → (astart : Q ) 46 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool )
41 → (x : List Σ) 47 → (x : List Σ)
42 → Naccept NFA fin ( λ q1 → equal? fin astart q1) x ≡ true 48 → accept ( subset-construction exists NFA ) astart x ≡ true
43 → accept ( subset-construction fin NFA astart ) ( λ q1 → equal? fin astart q1) x ≡ true 49 → Naccept NFA exists astart x ≡ true
44 subset-construction-lemma→ {Q} {Σ} {n} fin NFA astart x naccept = lemma1 x ( λ q1 → equal? fin astart q1) naccept where 50 subset-construction-lemma← {Q} {Σ} {n} exists NFA astart x saccept = lemma2 x astart saccept where
45 lemma1 : (x : List Σ) → ( states : Q → Bool )
46 → Naccept NFA fin states x ≡ true
47 → accept ( subset-construction fin NFA astart ) states x ≡ true
48 lemma1 [] states naccept = naccept
49 lemma1 (h ∷ t ) states naccept = lemma1 t (δconv fin (Nδ NFA) states h) naccept
50
51 subset-construction-lemma← : { Q : Set } { Σ : Set } { n : ℕ } → (fin : FiniteSet Q {n} ) →
52 (NFA : NAutomaton Q Σ ) → (astart : Q )
53 → (x : List Σ)
54 → accept ( subset-construction fin NFA astart ) ( λ q1 → equal? fin astart q1) x ≡ true
55 → Naccept NFA fin ( λ q1 → equal? fin astart q1) x ≡ true
56 subset-construction-lemma← {Q} {Σ} {n} fin NFA astart x saccept = lemma2 x ( λ q1 → equal? fin astart q1) saccept where
57 lemma2 : (x : List Σ) → ( states : Q → Bool ) 51 lemma2 : (x : List Σ) → ( states : Q → Bool )
58 → accept ( subset-construction fin NFA astart ) states x ≡ true 52 → accept ( subset-construction exists NFA ) states x ≡ true
59 → Naccept NFA fin states x ≡ true 53 → Naccept NFA exists states x ≡ true
60 lemma2 [] states saccept = saccept 54 lemma2 [] states saccept = saccept
61 lemma2 (h ∷ t ) states saccept = lemma2 t (δconv fin (Nδ NFA) states h) saccept 55 lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept