|
67
|
1 module automaton-text where
|
|
65
|
2
|
|
67
|
3 -- open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
4 open import Data.Nat
|
|
68
|
5 open import Data.Vec
|
|
67
|
6 open import Data.Maybe
|
|
|
7 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ )
|
|
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
9 open import Relation.Nullary using (¬_; Dec; yes; no)
|
|
65
|
10 open import logic
|
|
67
|
11 -- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )
|
|
65
|
12
|
|
67
|
13 open import automaton
|
|
68
|
14 open import Data.Vec
|
|
65
|
15
|
|
|
16 open Automaton
|
|
|
17
|
|
|
18
|
|
67
|
19 lemma4 : {i n : ℕ } → i < n → i < suc n
|
|
|
20 lemma4 {0} {0} ()
|
|
|
21 lemma4 {0} {suc n} lt = s≤s z≤n
|
|
|
22 lemma4 {suc i} {0} ()
|
|
|
23 lemma4 {suc i} {suc n} (s≤s lt) = s≤s (lemma4 lt)
|
|
|
24
|
|
|
25 lemma5 : {n : ℕ } → n < suc n
|
|
|
26 lemma5 {zero} = s≤s z≤n
|
|
|
27 lemma5 {suc n} = s≤s lemma5
|
|
65
|
28
|
|
68
|
29 length : {S : Set} {n : ℕ} → Vec S n → ℕ
|
|
|
30 length {_} {n} _ = n
|
|
|
31
|
|
67
|
32 record accept-n { Q : Set } { Σ : Set } (M : Automaton Q Σ ) (astart : Q ) (n : ℕ ) (s : {i : ℕ } → (i < n) → Σ ) : Set where
|
|
|
33 field
|
|
|
34 r : (i : ℕ ) → i < suc n → Q
|
|
|
35 accept-1 : r 0 (s≤s z≤n) ≡ astart
|
|
|
36 accept-2 : (i : ℕ ) → (i<n : i < n ) → δ M (r i (lemma4 i<n)) (s i<n) ≡ r (suc i) (s≤s i<n)
|
|
|
37 accept-3 : aend M (r n lemma5 ) ≡ true
|
|
65
|
38
|
|
68
|
39 get : { Σ : Set } {n : ℕ} → (x : Vec Σ n ) → { i : ℕ } → i < n → Σ
|
|
67
|
40 get [] ()
|
|
|
41 get (h ∷ t) {0} (s≤s lt) = h
|
|
|
42 get (h ∷ t) {suc i} (s≤s lt) = get t lt
|
|
65
|
43
|
|
68
|
44 accept-v : { Q : Set } { Σ : Set } {n : ℕ }
|
|
|
45 → Automaton Q Σ
|
|
|
46 → (astart : Q)
|
|
|
47 → Vec Σ n → Bool
|
|
|
48 accept-v {Q} { Σ} M q [] = aend M q
|
|
|
49 accept-v {Q} { Σ} M q ( H ∷ T ) = accept-v M ( (δ M) q H ) T
|
|
|
50
|
|
|
51 lemma7 : { Q : Set } { Σ : Set } {n : ℕ} (M : Automaton Q Σ ) (q : Q ) → (h : Σ) → (t : Vec Σ n )
|
|
|
52 → accept-v M q (h ∷ t) ≡ true → accept-v M (δ M q h) t ≡ true
|
|
|
53 lemma7 M q h t eq with accept-v M (δ M q h) t
|
|
67
|
54 lemma7 M q h t refl | true = refl
|
|
|
55 lemma7 M q h t () | false
|
|
65
|
56
|
|
67
|
57 open accept-n
|
|
65
|
58
|
|
68
|
59 lemma→ : { Q : Set } { Σ : Set } {n : ℕ} (M : Automaton Q Σ ) (q : Q ) → (x : Vec Σ n ) → accept-v M q x ≡ true → accept-n M q (length x) (get x )
|
|
67
|
60 lemma→ {Q} {Σ} M q [] eq = record { r = λ i lt → get [ q ] {i} lt ; accept-1 = refl ; accept-2 = λ _ () ; accept-3 = eq }
|
|
68
|
61 lemma→ {Q} {Σ} {n} M q (h ∷ t) eq with lemma→ M (δ M q h) t (lemma7 M q h t eq)
|
|
67
|
62 ... | an = record { r = seq ; accept-1 = refl ; accept-2 = acc2 ; accept-3 = accept-3 an } where
|
|
68
|
63 seq : (i : ℕ) → i < suc n → Q
|
|
67
|
64 seq 0 lt = q
|
|
|
65 seq (suc i) (s≤s lt) = r an i lt
|
|
68
|
66 acc2 : (i : ℕ) (i<n : i < n) → δ M (seq i (lemma4 i<n)) (get (h ∷ t) i<n) ≡ seq (suc i) (s≤s i<n)
|
|
67
|
67 acc2 zero (s≤s z≤n) = begin
|
|
|
68 δ M (seq zero (lemma4 (s≤s z≤n))) (get (h ∷ t) (s≤s z≤n))
|
|
|
69 ≡⟨⟩
|
|
|
70 δ M q h
|
|
|
71 ≡⟨ sym ( accept-1 an) ⟩
|
|
|
72 seq 1 (s≤s (s≤s z≤n))
|
|
|
73 ∎ where open ≡-Reasoning
|
|
|
74 acc2 (suc i) (s≤s lt) = accept-2 an i lt
|
|
65
|
75
|
|
68
|
76 an-1 : { Q : Set } { Σ : Set } {n : ℕ} (M : Automaton Q Σ ) (q : Q ) → (h : Σ ) → (t : Vec Σ n )
|
|
67
|
77 → accept-n M q (length (h ∷ t)) (get (h ∷ t) )
|
|
|
78 → accept-n M (δ M q h) (length t) (get t )
|
|
|
79 an-1 {Q} {Σ} M q h t an = record {
|
|
|
80 r = seq
|
|
|
81 ; accept-1 = acc1
|
|
|
82 ; accept-2 = acc2
|
|
|
83 ; accept-3 = accept-3 an
|
|
|
84 } where
|
|
|
85 seq : (i : ℕ) → i < suc (length t) → Q
|
|
|
86 seq i lt = r an (suc i) ( s≤s lt)
|
|
|
87 acc1 : seq 0 (s≤s z≤n) ≡ δ M q h
|
|
|
88 acc1 = begin
|
|
|
89 seq 0 (s≤s z≤n)
|
|
|
90 ≡⟨⟩
|
|
|
91 r an 1 (s≤s (s≤s z≤n))
|
|
|
92 ≡⟨ sym (accept-2 an 0 (s≤s z≤n)) ⟩
|
|
|
93 δ M (r an 0 (s≤s z≤n)) h
|
|
|
94 ≡⟨ cong (λ k → δ M k h) (accept-1 an) ⟩
|
|
|
95 δ M q h
|
|
|
96 ∎ where open ≡-Reasoning
|
|
|
97 acc2 : (i : ℕ) (i<n : i < length t) → δ M (seq i (lemma4 i<n)) (get t i<n) ≡ seq (suc i) (s≤s i<n)
|
|
|
98 acc2 i lt = accept-2 an (suc i) (s≤s lt)
|
|
65
|
99
|
|
68
|
100 lemma← : { Q : Set } { Σ : Set } {n : ℕ} (M : Automaton Q Σ ) (q : Q ) → (x : Vec Σ n ) → accept-n M q (length x) (get x ) → accept-v M q x ≡ true
|
|
67
|
101 lemma← {Q} {Σ} M q [] an with accept-1 an | accept-3 an
|
|
|
102 ... | eq1 | eq3 = begin
|
|
|
103 aend M q
|
|
|
104 ≡⟨ cong ( λ k → aend M k ) (sym (accept-1 an)) ⟩
|
|
|
105 aend M (r an 0 lemma5)
|
|
|
106 ≡⟨ accept-3 an ⟩
|
|
|
107 true
|
|
|
108 ∎ where open ≡-Reasoning
|
|
|
109 lemma← {Q} {Σ} M q (h ∷ t) an = lemma← M (δ M q h) t ( an-1 M q h t an )
|
