Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/nfa136.agda @ 283:e5a0499e7b40

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Dec 2021 19:48:00 +0900
parents 3fa72793620b
children 6f3636fbc481
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
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
5 open import automaton
104
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
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
62 exists136 : (StatesQ → Bool) → Bool
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
63 exists136 f = f q1 \/ f q2 \/ f q3
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
64
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
65 to-list-136 : (StatesQ → Bool) → List StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
66 to-list-136 f = tl1 where
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
67 tl3 : List StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
68 tl3 with f q3
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
69 ... | true = q3 ∷ []
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
70 ... | false = []
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
71 tl2 : List StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
72 tl2 with f q2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
73 ... | true = q2 ∷ tl3
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
74 ... | false = tl3
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
75 tl1 : List StatesQ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
76 tl1 with f q1
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
77 ... | true = q1 ∷ tl2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
78 ... | false = tl2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
79
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 nfa136 : NAutomaton StatesQ A2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 nfa136 = record { Nδ = transition136; Nend = end136 }
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
83 example136-1 = Naccept nfa136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
84
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
85 t146-1 = Ntrace nfa136 exists136 to-list-136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
87 example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] )
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
89 example136-2 = Naccept nfa136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
90 t146-2 = Ntrace nfa136 exists136 to-list-136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] )
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 open FiniteSet
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 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
95 nx now [] = now
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
96 nx now ( i ∷ ni ) = (Nmoves nfa136 exists136 (nx now ni) i )
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
98 example136-3 = to-list-136 start136
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
99 example136-4 = to-list-136 (nx start136 ( a0 ∷ b0 ∷ a0 ∷ [] ))
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 open import sbconst2
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 fm136 : Automaton ( StatesQ → Bool ) A2
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
104 fm136 = subset-construction exists136 nfa136
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 open NAutomaton
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
108 lemma136 : ( x : List A2 ) → Naccept nfa136 exists136 start136 x ≡ accept fm136 start136 x
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 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
110 lemma136-1 : ( x : List A2 ) → ( states : StatesQ → Bool )
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
111 → Naccept nfa136 exists136 states x ≡ accept fm136 states x
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 lemma136-1 [] _ = refl
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
113 lemma136-1 (h ∷ t) states = lemma136-1 t (δconv exists136 (Nδ nfa136) states h)