Mercurial > hg > Members > kono > Proof > automaton

comparison agda/automaton-text.agda @ 67:b9679ebd1156

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 Thu, 31 Oct 2019 13:53:26 +0900
parents agda/regular-language.agda@293a2075514b
children 13822f5f9c85
comparison
equal deleted inserted replaced
66:8f0efa93b354 67:b9679ebd1156
1 module automaton-text where
2
3 -- open import Level renaming ( suc to succ ; zero to Zero )
4 open import Data.Nat
5 open import Data.List
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)
10 open import logic
11 -- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )
12
13 open import automaton
14
15 open Automaton
16
17
18 lemma4 : {i n : ℕ } → i < n → i < suc n
19 lemma4 {0} {0} ()
20 lemma4 {0} {suc n} lt = s≤s z≤n
21 lemma4 {suc i} {0} ()
22 lemma4 {suc i} {suc n} (s≤s lt) = s≤s (lemma4 lt)
23
24 lemma5 : {n : ℕ } → n < suc n
25 lemma5 {zero} = s≤s z≤n
26 lemma5 {suc n} = s≤s lemma5
27
28 record accept-n { Q : Set } { Σ : Set } (M : Automaton Q Σ ) (astart : Q ) (n : ℕ ) (s : {i : ℕ } → (i < n) → Σ ) : Set where
29 field
30 r : (i : ℕ ) → i < suc n → Q
31 accept-1 : r 0 (s≤s z≤n) ≡ astart
32 accept-2 : (i : ℕ ) → (i<n : i < n ) → δ M (r i (lemma4 i<n)) (s i<n) ≡ r (suc i) (s≤s i<n)
33 accept-3 : aend M (r n lemma5 ) ≡ true
34
35 get : { Σ : Set } → (x : List Σ ) → { i : ℕ } → i < length x → Σ
36 get [] ()
37 get (h ∷ t) {0} (s≤s lt) = h
38 get (h ∷ t) {suc i} (s≤s lt) = get t lt
39
40 lemma7 : { Q : Set } { Σ : Set } (M : Automaton Q Σ ) (q : Q ) → (h : Σ) → (t : List Σ ) → accept M q (h ∷ t) ≡ true → accept M (δ M q h) t ≡ true
41 lemma7 M q h t eq with accept M (δ M q h) t
42 lemma7 M q h t refl | true = refl
43 lemma7 M q h t () | false
44
45 open accept-n
46
47 lemma→ : { Q : Set } { Σ : Set } (M : Automaton Q Σ ) (q : Q ) → (x : List Σ ) → accept M q x ≡ true → accept-n M q (length x) (get x )
48 lemma→ {Q} {Σ} M q [] eq = record { r = λ i lt → get [ q ] {i} lt ; accept-1 = refl ; accept-2 = λ _ () ; accept-3 = eq }
49 lemma→ {Q} {Σ} M q (h ∷ t) eq with lemma→ M (δ M q h) t (lemma7 M q h t eq)
50 ... | an = record { r = seq ; accept-1 = refl ; accept-2 = acc2 ; accept-3 = accept-3 an } where
51 seq : (i : ℕ) → i < suc (suc (foldr (λ _ → suc) 0 t)) → Q
52 seq 0 lt = q
53 seq (suc i) (s≤s lt) = r an i lt
54 acc2 : (i : ℕ) (i<n : i < suc (foldr (λ _ → suc) 0 t)) → δ M (seq i (lemma4 i<n)) (get (h ∷ t) i<n) ≡ seq (suc i) (s≤s i<n)
55 acc2 zero (s≤s z≤n) = begin
56 δ M (seq zero (lemma4 (s≤s z≤n))) (get (h ∷ t) (s≤s z≤n))
57 ≡⟨⟩
58 δ M q h
59 ≡⟨ sym ( accept-1 an) ⟩
60 seq 1 (s≤s (s≤s z≤n))
61 ∎ where open ≡-Reasoning
62 acc2 (suc i) (s≤s lt) = accept-2 an i lt
63
64 an-1 : { Q : Set } { Σ : Set } (M : Automaton Q Σ ) (q : Q ) → (h : Σ ) → (t : List Σ )
65 → accept-n M q (length (h ∷ t)) (get (h ∷ t) )
66 → accept-n M (δ M q h) (length t) (get t )
67 an-1 {Q} {Σ} M q h t an = record {
68 r = seq
69 ; accept-1 = acc1
70 ; accept-2 = acc2
71 ; accept-3 = accept-3 an
72 } where
73 seq : (i : ℕ) → i < suc (length t) → Q
74 seq i lt = r an (suc i) ( s≤s lt)
75 acc1 : seq 0 (s≤s z≤n) ≡ δ M q h
76 acc1 = begin
77 seq 0 (s≤s z≤n)
78 ≡⟨⟩
79 r an 1 (s≤s (s≤s z≤n))
80 ≡⟨ sym (accept-2 an 0 (s≤s z≤n)) ⟩
81 δ M (r an 0 (s≤s z≤n)) h
82 ≡⟨ cong (λ k → δ M k h) (accept-1 an) ⟩
83 δ M q h
84 ∎ where open ≡-Reasoning
85 acc2 : (i : ℕ) (i<n : i < length t) → δ M (seq i (lemma4 i<n)) (get t i<n) ≡ seq (suc i) (s≤s i<n)
86 acc2 i lt = accept-2 an (suc i) (s≤s lt)
87
88 lemma← : { Q : Set } { Σ : Set } (M : Automaton Q Σ ) (q : Q ) → (x : List Σ ) → accept-n M q (length x) (get x ) → accept M q x ≡ true
89 lemma← {Q} {Σ} M q [] an with accept-1 an | accept-3 an
90 ... | eq1 | eq3 = begin
91 aend M q
92 ≡⟨ cong ( λ k → aend M k ) (sym (accept-1 an)) ⟩
93 aend M (r an 0 lemma5)
94 ≡⟨ accept-3 an ⟩
95 true
96 ∎ where open ≡-Reasoning
97 lemma← {Q} {Σ} M q (h ∷ t) an = lemma← M (δ M q h) t ( an-1 M q h t an )