|
0
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 module automaton where
|
|
|
3 open import Level hiding ( suc ; zero )
|
|
|
4 open import Data.Empty
|
|
|
5 open import Relation.Nullary
|
|
|
6 open import Relation.Binary.PropositionalEquality -- hiding (_⇔_)
|
|
|
7 open import logic
|
|
|
8 open import Data.List
|
|
|
9
|
|
|
10 record Automaton {n : Level} (Q : Set n) (Σ : Set ) : Set ((Level.suc n) ) where
|
|
|
11 field
|
|
|
12 δ : Q → Σ → Q
|
|
|
13 F : Q → Set
|
|
|
14
|
|
|
15 open Automaton
|
|
|
16
|
|
|
17 accept : {n : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set
|
|
2
|
18 accept {n} {Q} {Σ} atm q [] = F atm q
|
|
|
19 accept {n} {Q} {Σ} atm q (x ∷ input) =
|
|
0
|
20 accept atm (δ atm q x ) input
|
|
|
21
|
|
|
22 trace : {n : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
|
|
|
23 trace {n} {Q} {Σ} A q [] a = q ∷ []
|
|
|
24 trace {n} {Q} {Σ} A q (x ∷ t) a = q ∷ ( trace A (δ A q x) t a )
|
|
|
25
|
|
|
26 data Q3 : Set where
|
|
|
27 q₁ : Q3
|
|
|
28 q₂ : Q3
|
|
|
29 q₃ : Q3
|
|
|
30
|
|
|
31 data Σ2 : Set where
|
|
|
32 s0 : Σ2
|
|
|
33 s1 : Σ2
|
|
|
34
|
|
|
35 δ16 : Q3 → Σ2 → Q3
|
|
|
36 δ16 q₁ s0 = q₁
|
|
|
37 δ16 q₁ s1 = q₂
|
|
|
38 δ16 q₂ s0 = q₃
|
|
|
39 δ16 q₂ s1 = q₂
|
|
|
40 δ16 q₃ s0 = q₂
|
|
|
41 δ16 q₃ s1 = q₂
|
|
|
42
|
|
|
43 δ16' : Q3 → Σ2 → Q3
|
|
|
44 δ16' q₁ s0 = q₁
|
|
|
45 δ16' q₁ s1 = q₂
|
|
|
46 δ16' q₂ s0 = q₃
|
|
|
47 δ16' q₂ s1 = q₂
|
|
|
48 δ16' q₃ s0 = q₂
|
|
|
49 δ16' q₃ s1 = q₃
|
|
|
50
|
|
|
51 data a16end : Q3 → Set where
|
|
|
52 a16q2 : a16end q₂
|
|
|
53
|
|
|
54 a16 : Automaton Q3 Σ2
|
|
1
|
55 a16 = record { δ = δ16 ; F = λ q → a16end q }
|
|
0
|
56
|
|
|
57 a16' : Automaton Q3 Σ2
|
|
1
|
58 a16' = record { δ = δ16' ; F = λ q → q ≡ q₂ }
|
|
0
|
59
|
|
|
60 --
|
|
|
61 -- ∷ → ∷ → ∷ → []
|
|
|
62 -- ↓ ↓ ↓
|
|
|
63 -- s0 s0 s1
|
|
|
64 --
|
|
|
65 input1 : List Σ2
|
|
|
66 input1 = s0 ∷ s0 ∷ s1 ∷ []
|
|
|
67
|
|
|
68 input2 : List Σ2
|
|
|
69 input2 = s0 ∷ s0 ∷ s0 ∷ []
|
|
|
70
|
|
|
71 test1 : accept a16 q₁ input1
|
|
|
72 test1 = a16q2
|
|
|
73
|
|
|
74 lemma0 : accept a16 q₁ input1 ≡ a16end q₂
|
|
|
75 lemma0 = begin
|
|
|
76 accept a16 q₁ ( s0 ∷ s0 ∷ s1 ∷ [] )
|
|
|
77 ≡⟨ refl ⟩ -- x ≡ x
|
|
|
78 accept a16 q₁ ( s0 ∷ s1 ∷ [] )
|
|
|
79 ≡⟨⟩
|
|
|
80 accept a16 q₁ ( s1 ∷ [] )
|
|
|
81 ≡⟨⟩
|
|
|
82 accept a16 q₂ []
|
|
|
83 ≡⟨⟩
|
|
|
84 a16end q₂
|
|
|
85 ∎ where open ≡-Reasoning
|
|
|
86
|
|
|
87 lemma1 : List Q3
|
|
|
88 lemma1 = trace a16 q₁ input1 a16q2
|
|
|
89
|
|
|
90 test1' : accept a16' q₁ input1
|
|
|
91 test1' = refl
|
|
|
92
|
|
|
93 lemma2 : List Q3
|
|
|
94 lemma2 = trace a16' q₁ input1 refl
|
|
|
95
|
|
|
96 test2 : ¬ ( accept a16 q₁ input2 )
|
|
|
97 test2 ()
|
|
|
98
|
|
|
99 open import Data.Bool
|
|
|
100 open import Data.Unit
|
|
|
101
|
|
|
102 -- contains at least 1 s1
|
|
|
103 c1 : List Σ2 → Set
|
|
|
104 c1 [] = ⊥
|
|
|
105 c1 (s1 ∷ t) = ⊤
|
|
|
106 c1 (_ ∷ t) = c1 t
|
|
|
107
|
|
|
108 -- even number of s0
|
|
|
109 even0 : List Σ2 → Set
|
|
|
110 odd0 : List Σ2 → Set
|
|
|
111 odd0 [] = ⊥
|
|
|
112 odd0 (s0 ∷ t) = even0 t
|
|
|
113 odd0 (s1 ∷ t) = odd0 t
|
|
|
114 even0 [] = ⊤
|
|
|
115 even0 (s0 ∷ t) = odd0 t
|
|
|
116 even0 (s1 ∷ t) = even0 t
|
|
|
117
|
|
|
118 -- after
|
|
|
119
|
|
|
120 a0 : List Σ2 → Set
|
|
|
121 a0 [] = ⊥
|
|
|
122 a0 (s1 ∷ t ) = even0 t
|
|
|
123 a0 (s0 ∷ t ) = a0 t
|
|
|
124
|
|
|
125 -- data ⊥ : Set
|
|
|
126 --
|
|
|
127 -- data ⊤ : Set where
|
|
|
128 -- tt : ⊤
|
|
|
129 -- tt : ⊤
|
|
|
130
|
|
|
131 lemma-a : (x : List Σ2 ) → accept a16' q₁ x → a0 x
|
|
|
132 lemma-a x a = a1 x a where
|
|
|
133 a3 : (x : List Σ2 ) → accept a16' q₃ x → odd0 x
|
|
|
134 a2 : (x : List Σ2 ) → accept a16' q₂ x → even0 x
|
|
|
135 a3 [] ()
|
|
|
136 a3 (s0 ∷ t) a = a2 t a
|
|
|
137 a3 (s1 ∷ t) a = a3 t a
|
|
|
138 a2 [] a = tt
|
|
|
139 a2 (s0 ∷ t) a = a3 t a
|
|
|
140 a2 (s1 ∷ t) a = a2 t a
|
|
|
141 a1 : (x : List Σ2 ) → accept a16' q₁ x → a0 x
|
|
|
142 a1 [] () -- a16' does not accept []
|
|
|
143 a1 (s0 ∷ t) a = a1 t a
|
|
|
144 a1 (s1 ∷ t) a = a2 t a
|
|
|
145
|
|
|
146 -- ¬_ : Set → Set
|
|
|
147 -- ¬_ _ = ⊥
|
|
|
148
|
|
|
149 lemma-not-a : ¬ ( (x : List Σ2 ) → accept a16 q₁ x → a0 x )
|
|
|
150 lemma-not-a not1 with not1 (s1 ∷ s0 ∷ s1 ∷ [] ) a16q2
|
|
|
151 ... | ()
|
|
|
152
|
|
|
153 -- can we prove negation similar to the lemma-a?
|
|
|
154 -- lemma-not-a' : ¬ ((x : List Σ2 ) → accept a16 q₁ x → a0 x)
|
|
|
155 -- lemma-not-a' not = {!!} where
|
|
|
156 -- a3 : (x : List Σ2 ) → accept a16 q₃ x → odd0 x
|
|
|
157 -- a2 : (x : List Σ2 ) → accept a16 q₂ x → even0 x
|
|
|
158 -- a3 (s0 ∷ t) a = a2 t a
|
|
|
159 -- a3 (s1 ∷ t) a = {!!}
|
|
|
160 -- a2 [] a = tt
|
|
|
161 -- a2 (s0 ∷ t) a = a3 t a
|
|
|
162 -- a2 (s1 ∷ t) a = a2 t a
|
|
|
163 -- a1 : (x : List Σ2 ) → accept a16 q₁ x → a0 x
|
|
|
164 -- a1 [] ()
|
|
|
165 -- a1 (s0 ∷ t) a = a1 t a
|
|
|
166 -- a1 (s1 ∷ t) a = a2 t a
|
|
|
167
|
|
|
168 open import Data.Nat
|
|
|
169
|
|
|
170 evenℕ : ℕ → Set
|
|
|
171 oddℕ : ℕ → Set
|
|
|
172 oddℕ zero = ⊥
|
|
|
173 oddℕ (suc n) = evenℕ n
|
|
|
174 evenℕ zero = ⊤
|
|
|
175 evenℕ (suc n) = oddℕ n
|
|
|
176
|
|
|
177 count-s0 : (x : List Σ2 ) → ℕ
|
|
|
178 count-s0 [] = zero
|
|
|
179 count-s0 (s0 ∷ t) = suc ( count-s0 t )
|
|
|
180 count-s0 (s1 ∷ t) = count-s0 t
|
|
|
181
|
|
|
182 e1 : (x : List Σ2 ) → even0 x → evenℕ ( count-s0 x )
|
|
|
183 o1 : (x : List Σ2 ) → odd0 x → oddℕ ( count-s0 x )
|
|
|
184 e1 [] e = tt
|
|
|
185 e1 (s0 ∷ t) o = o1 t o
|
|
|
186 e1 (s1 ∷ t) e = e1 t e
|
|
|
187 o1 [] ()
|
|
|
188 o1 (s0 ∷ t) e = e1 t e
|
|
|
189 o1 (s1 ∷ t) o = o1 t o
|
|
|
190
|
|
|
191 δ19 : Q3 → Σ2 → Q3
|
|
|
192 δ19 q₁ s0 = q₁
|
|
|
193 δ19 q₁ s1 = q₂
|
|
|
194 δ19 q₂ s0 = q₁
|
|
|
195 δ19 q₂ s1 = q₂
|
|
|
196 δ19 q₃ _ = q₁
|
|
|
197
|
|
|
198 a19 : Automaton Q3 Σ2
|
|
1
|
199 a19 = record { δ = δ19 ; F = λ q → q ≡ q₁ }
|
|
0
|
200
|
|
|
201 -- input is empty or ends in s0
|
|
|
202
|
|
|
203 end0 : List Σ2 → Set
|
|
|
204 end0 [] = ⊤
|
|
|
205 end0 (s0 ∷ [] ) = ⊤
|
|
|
206 end0 (s1 ∷ [] ) = ⊥
|
|
|
207 end0 (x ∷ t ) = end0 t
|
|
|
208
|
|
|
209 lemma-b : (x : List Σ2 ) → accept a19 q₁ x → end0 x
|
|
|
210 lemma-b = {!!}
|
|
|
211
|
