# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572525714 -32400
# Node ID 13822f5f9c859a8dfd6c7cda194fc4f6c8c00269
# Parent  b9679ebd115611f7618afd9a88470b721ff83161
use Vec

diff -r b9679ebd1156 -r 13822f5f9c85 agda/automaton-text.agda
--- a/agda/automaton-text.agda	Thu Oct 31 13:53:26 2019 +0900
+++ b/agda/automaton-text.agda	Thu Oct 31 21:41:54 2019 +0900
@@ -2,7 +2,7 @@
 
 -- open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Nat
-open import Data.List
+open import Data.Vec
 open import Data.Maybe
 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ )
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
@@ -11,6 +11,7 @@
 -- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )
 
 open import automaton
+open import Data.Vec
 
 open Automaton
 
@@ -25,6 +26,9 @@
 lemma5 {zero} = s≤s z≤n
 lemma5 {suc n} =  s≤s lemma5
 
+length : {S : Set} {n : ℕ} → Vec S n → ℕ
+length {_} {n} _ = n
+
 record accept-n { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (astart : Q ) (n : ℕ ) (s : {i : ℕ } → (i < n)  → Σ ) : Set where
    field
       r : (i : ℕ ) → i < suc n  → Q
@@ -32,26 +36,34 @@
       accept-2 : (i : ℕ ) → (i<n : i < n ) → δ M (r i (lemma4 i<n)) (s i<n) ≡ r (suc i) (s≤s i<n)
       accept-3 : aend M (r n lemma5 ) ≡ true
 
-get : { Σ : Set  } →  (x : List Σ ) → { i : ℕ } → i < length x  → Σ
+get : { Σ : Set  } {n : ℕ} →  (x : Vec Σ n ) → { i : ℕ } → i < n  → Σ
 get [] ()
 get (h ∷ t) {0} (s≤s lt) = h
 get (h ∷ t) {suc i} (s≤s lt) = get t lt
 
-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
-lemma7 M q h t eq with accept M (δ M q h) t
+accept-v : { Q : Set } { Σ : Set  } {n : ℕ }
+    → Automaton Q  Σ
+    → (astart : Q)
+    → Vec Σ n → Bool
+accept-v {Q} { Σ} M q [] = aend M q
+accept-v {Q} { Σ} M q ( H  ∷ T ) = accept-v M ( (δ M) q H ) T
+
+lemma7 : { Q : Set } { Σ : Set  } {n : ℕ} (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ) → (t : Vec Σ n )
+   → accept-v M q (h ∷ t) ≡ true →  accept-v M (δ M q h) t ≡ true
+lemma7 M q h t eq with accept-v M (δ M q h) t
 lemma7 M q h t refl | true = refl
 lemma7 M q h t () | false 
 
 open accept-n
 
-lemma→ :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept M q x ≡ true → accept-n M q (length x) (get x )
+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 )
 lemma→ {Q} {Σ} M q [] eq = record { r = λ i lt → get [ q ] {i} lt ; accept-1 = refl ; accept-2 = λ _ () ; accept-3 = eq  } 
-lemma→ {Q} {Σ} M q (h ∷ t) eq with lemma→ M (δ M q h) t (lemma7 M q h t eq) 
+lemma→ {Q} {Σ} {n} M q (h ∷ t) eq with lemma→ M (δ M q h) t (lemma7 M q h t eq) 
 ... | an = record { r = seq ; accept-1 = refl ; accept-2 = acc2 ; accept-3 = accept-3 an } where
-    seq : (i : ℕ) → i < suc (suc (foldr (λ _ → suc) 0 t)) → Q
+    seq : (i : ℕ) → i < suc n → Q
     seq 0 lt = q
     seq (suc i) (s≤s lt) = r an i lt
-    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)
+    acc2 : (i : ℕ) (i<n : i < n) → δ M (seq i (lemma4 i<n)) (get (h ∷ t) i<n) ≡ seq (suc i) (s≤s i<n)
     acc2 zero (s≤s z≤n) = begin
          δ M (seq zero (lemma4 (s≤s z≤n))) (get (h ∷ t) (s≤s z≤n))
        ≡⟨⟩
@@ -61,7 +73,7 @@
        ∎ where open ≡-Reasoning
     acc2 (suc i)  (s≤s lt) = accept-2 an i lt
 
-an-1 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ ) → (t : List Σ )
+an-1 : { Q : Set } { Σ : Set  } {n : ℕ} (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ ) → (t : Vec Σ n )
     → accept-n M q (length (h ∷ t)) (get (h ∷ t) ) 
     → accept-n M (δ M q h) (length t) (get t )
 an-1 {Q} {Σ} M q h t an = record {
@@ -85,7 +97,7 @@
        acc2 : (i : ℕ) (i<n : i < length t) → δ M (seq i (lemma4 i<n)) (get t i<n) ≡ seq (suc i) (s≤s i<n)
        acc2 i lt = accept-2 an (suc i) (s≤s lt)
 
-lemma← :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept-n M q (length x) (get x ) → accept M q x ≡ true 
+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 
 lemma← {Q} {Σ} M q [] an with accept-1 an | accept-3 an
 ... | eq1 | eq3 = begin
          aend M q