annotate agda/regular-language.agda @ 84:29d81bcff049

found done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Nov 2019 07:47:32 +0900
parents 7b357b295272
children 4c950a6ad6ce
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module regular-language where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level renaming ( suc to Suc ; zero to Zero )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.List
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Nat hiding ( _≟_ )
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
6 open import Data.Fin hiding ( _+_ )
72
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
7 open import Data.Empty
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Data.Product
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 -- open import Data.Maybe
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Nullary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Binary.PropositionalEquality hiding ( [_] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import logic
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
13 open import nat
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import automaton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import finiteSet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 language : { Σ : Set } → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 language {Σ} = List Σ → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 language-L : { Σ : Set } → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 language-L {Σ} = List (List Σ)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 open Automaton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 states : Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 astart : states
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
29 aℕ : ℕ
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
30 afin : FiniteSet states {aℕ}
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 automaton : Automaton states Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 contain : List Σ → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 contain x = accept automaton astart x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 Union {Σ} A B x = (A x ) \/ (B x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 split : {Σ : Set} → (List Σ → Bool)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 → ( List Σ → Bool) → List Σ → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 split x y [] = x [] /\ y []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 Concat {Σ} A B = split A B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 {-# TERMINATING #-}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 Star {Σ} A = split A ( Star {Σ} A )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
51 test-split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
52 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
53 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
54 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
55 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
56 )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
57 test-split {_} {A} {B} = refl
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 65
diff changeset
58
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 open RegularLanguage
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 isRegular A x r = A x ≡ contain r x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
63 postulate
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
64 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
65
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 M-Union {Σ} A B = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 states = states A × states B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 ; astart = ( astart A , astart B )
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
70 ; aℕ = aℕ A * aℕ B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
71 ; afin = fin-× (afin A) (afin B)
65
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 ; automaton = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 closed-in-union A B [] = lemma where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 lemma = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 accept (automaton A) qa t \/ accept (automaton B) qb t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 ≡ accept (automaton (M-Union A B)) (qa , qb) t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 lemma1 [] qa qb = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 -- M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 -- M-Concat {Σ} A B = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 -- states = states A ∨ states B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 -- ; astart = case1 (astart A )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 -- ; automaton = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 -- δ = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 -- ; aend = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 -- }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 -- }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 -- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 -- closed-in-concat = {!!}
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
102
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
103 open import nfa
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
104 open import sbconst2
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
105 open FiniteSet
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
106 open import Data.Nat.Properties
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
107 open import Relation.Binary as B hiding (Decidable)
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
108
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
109 postulate
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
110 fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
111 fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
112
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
113 Concat-NFA : {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
114 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } where
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
115 δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
116 δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
117 δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ (equal? (afin B) qb (astart B) )
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
118 δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
119 δnfa _ i _ = false
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
120 nend : states A ∨ states B → Bool
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
121 nend (case2 q) = aend (automaton B) q
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
122 nend _ = false
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
123
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
124 -- Concat-NFA-start : {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
125 -- Concat-NFA-start A B (case1 q) = equal? (afin A) q (astart A)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
126 -- Concat-NFA-start _ _ _ = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
127
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
128 Concat-NFA-start : {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
129 Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
130
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
131 M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
132 M-Concat {Σ} A B = record {
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
133 states = states A ∨ states B → Bool
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
134 ; astart = Concat-NFA-start A B
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
135 ; aℕ = finℕ finf
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
136 ; afin = finf
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
137 ; automaton = subset-construction fin (Concat-NFA A B) (case1 (astart A))
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
138 } where
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
139 fin : FiniteSet (states A ∨ states B ) {aℕ A + aℕ B}
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
140 fin = fin-∨ (afin A) (afin B)
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
141 finf : FiniteSet (states A ∨ states B → Bool )
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
142 finf = fin→ fin
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
143
72
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
144 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
145 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
146 sp0 : List Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
147 sp1 : List Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
148 sp-concat : sp0 ++ sp1 ≡ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
149 prop0 : A sp0 ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
150 prop1 : B sp1 ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
151
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
152 open Split
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
153
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
154 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
155 list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
156 list-empty++ [] (x ∷ y) ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
157 list-empty++ (x ∷ x₁) y ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
158
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
159 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 71
diff changeset
160
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
161 open import Relation.Binary.PropositionalEquality hiding ( [_] )
71
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
162
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
163 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
164 → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
165 → split (λ t1 → A (h ∷ t1)) B t ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
166 c-split-lemma {Σ} A B h t eq (case1 ¬p ) = sym ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
167 true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
168 ≡⟨ sym eq ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
169 split A B (h ∷ t )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
170 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
171 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
172 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-1 (¬-bool-t ¬p)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
173 false \/ split (λ t1 → A (h ∷ t1)) B t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
174 ≡⟨ bool-or-1 refl ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
175 split (λ t1 → A (h ∷ t1)) B t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
176 ∎ ) where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
177 c-split-lemma {Σ} A B h t eq (case2 ¬p ) = sym ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
178 true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
179 ≡⟨ sym eq ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
180 split A B (h ∷ t )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
181 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
182 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
183 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-2 (¬-bool-t ¬p)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
184 false \/ split (λ t1 → A (h ∷ t1)) B t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
185 ≡⟨ bool-or-1 refl ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
186 split (λ t1 → A (h ∷ t1)) B t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
187 ∎ ) where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
188
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
189 c-split : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
190 c-split {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
191 c-split {Σ} A B [] eq | yes eqa | yes eqb =
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
192 record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
193 c-split {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
194 c-split {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
195 c-split {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
196 ... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
197 ... | no px | _ with c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
198 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
199 c-split {Σ} A B (h ∷ t ) eq | _ | no px with c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
200 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
201
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
202 split++ : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
203 split++ {Σ} A B [] [] eqa eqb = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
204 split A B []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
205 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
206 A [] /\ B []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
207 ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
208 true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
209 ∎ where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
210 split++ {Σ} A B [] (h ∷ y ) eqa eqb = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
211 split A B (h ∷ y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
212 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
213 A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
214 ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
215 true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
216 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
217 true \/ split (λ t1 → A (h ∷ t1)) B y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
218 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
219 true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
220 ∎ where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
221 split++ {Σ} A B (h ∷ t) y eqa eqb = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
222 split A B ((h ∷ t) ++ y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
223 ≡⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
224 A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
225 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) ( begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
226 split (λ t1 → A (h ∷ t1)) B (t ++ y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
227 ≡⟨ split++ {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
228 true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
229 ∎ ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
230 A [] /\ B (h ∷ t ++ y) \/ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
231 ≡⟨ bool-or-3 ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
232 true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
233 ∎ where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
234
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
235 postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
237 open NAutomaton
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
238
71
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
239 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
240 closed-in-concat {Σ} A B x = ≡-Bool-func lemma3 lemma4 where
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
241 finav = (fin-∨ (afin A) (afin B))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
242 NFA = (Concat-NFA A B)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
243 abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
244 abmove (case1 q) h = case1 (δ (automaton A) q h)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
245 abmove (case2 q) h = case2 (δ (automaton B) q h)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
246 nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
247 exists finav (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
248 nmove = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
249 lemma6 : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
250 → Naccept NFA finav nq z ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
251 lemma6 [] q nq _ fb = lemma8 where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
252 lemma8 : exists finav ( λ q → nq q /\ Nend NFA q ) ≡ true
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
253 lemma8 = {!!}
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
254 lemma6 (h ∷ t ) q nq nq=q fb = lemma6 t (δ (automaton B) q h) (Nmoves NFA finav nq h) (nmove (case2 q) nq nq=q h) fb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
255 lemma7 : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
256 → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true )
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
257 → Naccept NFA finav nq (y ++ z) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
258 lemma7 [] z q nq nq=q fa fb = lemma6 z (astart B) nq {!!} fb
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
259 lemma7 (h ∷ t) z q nq nq=q fa fb = lemma7 t z (δ (automaton A) q h) (Nmoves NFA finav nq h) (nmove (case1 q) nq nq=q h) fa fb where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
260 lemma9 : equal? finav (case1 (astart A)) (case1 (astart A)) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
261 lemma9 with Data.Fin._≟_ (F←Q finav (case1 (astart A))) ( F←Q finav (case1 (astart A)) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
262 lemma9 | yes refl = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
263 lemma9 | no ¬p = ⊥-elim ( ¬p refl )
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
264 lemma5 : Split (contain A) (contain B) x
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
265 → Naccept NFA finav (equal? finav (case1 (astart A))) x ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
266 lemma5 S = subst ( λ k → Naccept NFA finav (equal? finav (case1 (astart A))) k ≡ true ) ( sp-concat S )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
267 (lemma7 (sp0 S) (sp1 S) (astart A) (equal? finav (case1 (astart A))) lemma9 (prop0 S) (prop1 S) )
71
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
268 lemma3 : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
269 lemma3 concat with c-split (contain A) (contain B) x concat
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
270 ... | S = begin
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
271 accept (subset-construction finav NFA (case1 (astart A))) (Concat-NFA-start A B ) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
272 ≡⟨ ≡-Bool-func (subset-construction-lemma← finav NFA (case1 (astart A)) x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
273 (subset-construction-lemma→ finav NFA (case1 (astart A)) x ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
274 Naccept NFA finav (equal? finav (case1 (astart A))) x
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
275 ≡⟨ lemma5 S ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
276 true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
277 ∎ where open ≡-Reasoning
71
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
278 lemma4 : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
279 lemma4 C = {!!} -- split++ (contain A) (contain B) x y (accept ?) (accept ?)
71
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
280
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
281