Mercurial > hg > Members > kono > Proof > automaton

annotate agda/nfa136.agda @ 104:fba1cd54581d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use exists in cond, nfa example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 14 Nov 2019 05:13:49 +0900
parents
children b3f05cd08d24
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module nfa136 where
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import logic
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import nfa
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import automaton hiding ( StatesQ )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.List
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import finiteSet
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Data.Fin
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 data StatesQ : Set where
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 q1 : StatesQ
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 q2 : StatesQ
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 q3 : StatesQ
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 data A2 : Set where
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 a0 : A2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 b0 : A2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 finStateQ : FiniteSet StatesQ
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 finStateQ = record {
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 Q←F = Q←F
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 ; F←Q = F←Q
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 ; finiso→ = finiso→
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 ; finiso← = finiso←
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 } where
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 Q←F : Fin 3 → StatesQ
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 Q←F zero = q1
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 Q←F (suc zero) = q2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 Q←F (suc (suc zero)) = q3
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 F←Q : StatesQ → Fin 3
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 F←Q q1 = zero
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 F←Q q2 = suc zero
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 F←Q q3 = suc (suc zero)
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 finiso→ : (q : StatesQ) → Q←F (F←Q q) ≡ q
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 finiso→ q1 = refl
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 finiso→ q2 = refl
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 finiso→ q3 = refl
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 finiso← zero = refl
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 finiso← (suc zero) = refl
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 finiso← (suc (suc zero)) = refl
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 finiso← (suc (suc (suc ())))
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 transition136 : StatesQ → A2 → StatesQ → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 transition136 q1 b0 q2 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 transition136 q1 a0 q1 = true -- q1 → ep → q3
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 transition136 q2 a0 q2 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 transition136 q2 a0 q3 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 transition136 q2 b0 q3 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 transition136 q3 a0 q1 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 transition136 _ _ _ = false
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 end136 : StatesQ → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 end136 q1 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 end136 _ = false
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 start136 : StatesQ → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 start136 q1 = true
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 start136 _ = false
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 nfa136 : NAutomaton StatesQ A2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 nfa136 = record { Nδ = transition136; Nend = end136 }
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 example136-1 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 example136-0 = Naccept nfa136 finStateQ start136( a0 ∷ [] )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 example136-2 = Naccept nfa136 finStateQ start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 open FiniteSet
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 nx : (StatesQ → Bool) → (List A2 ) → StatesQ → Bool
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 nx now [] = now
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 nx now ( i ∷ ni ) = (Nmoves nfa136 finStateQ (nx now ni) i )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 example136-3 = to-list finStateQ start136
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 example136-4 = to-list finStateQ (nx start136 ( a0 ∷ b0 ∷ a0 ∷ [] ))
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 open import sbconst2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 fm136 : Automaton ( StatesQ → Bool ) A2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 -- fm136 = record { δ = λ qs q → transition136 {!!} {!!} ; aend = λ qs → exists finStateQ end136 }
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 fm136 = subset-construction finStateQ nfa136 q1
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 open NAutomaton
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 lemma136 : ( x : List A2 ) → Naccept nfa136 finStateQ start136 x ≡ accept fm136 start136 x
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 lemma136 x = lemma136-1 x start136 where
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 lemma136-1 : ( x : List A2 ) → ( states : StatesQ → Bool )
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 → Naccept nfa136 finStateQ states x ≡ accept fm136 states x
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 lemma136-1 [] _ = refl
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 lemma136-1 (h ∷ t) states = lemma136-1 t (δconv finStateQ (Nδ nfa136) states h)