--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/automaton-text.agda	Thu Oct 31 13:53:26 2019 +0900
@@ -0,0 +1,97 @@
+module automaton-text where
+
+-- open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.List
+open import Data.Maybe
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ )
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import logic
+-- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )
+
+open import automaton
+
+open Automaton
+
+
+lemma4 : {i n : ℕ } → i < n → i < suc n
+lemma4 {0} {0} ()
+lemma4 {0} {suc n} lt = s≤s z≤n
+lemma4 {suc i} {0} ()
+lemma4 {suc i} {suc n} (s≤s lt) =  s≤s (lemma4 lt)
+
+lemma5 : {n : ℕ } → n < suc n
+lemma5 {zero} = s≤s z≤n
+lemma5 {suc n} =  s≤s lemma5
+
+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
+      accept-1 : r 0 (s≤s z≤n)  ≡ astart
+      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 [] ()
+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
+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} {Σ} 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) 
+... | 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 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 zero (s≤s z≤n) = begin
+         δ M (seq zero (lemma4 (s≤s z≤n))) (get (h ∷ t) (s≤s z≤n))
+       ≡⟨⟩
+         δ M q h
+       ≡⟨ sym ( accept-1 an)  ⟩
+         seq 1 (s≤s (s≤s z≤n))
+       ∎ 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 Σ )
+    → 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 {
+      r = seq
+    ; accept-1 = acc1
+    ; accept-2 = acc2
+    ; accept-3 = accept-3 an
+   } where
+       seq : (i : ℕ) → i < suc (length t) → Q
+       seq i lt = r an (suc i) ( s≤s lt)
+       acc1 : seq 0 (s≤s z≤n) ≡ δ M q h
+       acc1 = begin
+              seq 0 (s≤s z≤n)
+           ≡⟨⟩
+              r an 1 (s≤s (s≤s z≤n))
+           ≡⟨ sym (accept-2 an 0 (s≤s z≤n)) ⟩
+              δ M (r an 0 (s≤s z≤n)) h
+           ≡⟨ cong (λ k → δ M k h) (accept-1 an)  ⟩
+              δ M q h
+           ∎ where open ≡-Reasoning
+       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} {Σ} M q [] an with accept-1 an | accept-3 an
+... | eq1 | eq3 = begin
+         aend M q
+       ≡⟨ cong ( λ k → aend M k ) (sym (accept-1 an))  ⟩
+         aend M (r an 0 lemma5)
+       ≡⟨ accept-3 an  ⟩
+         true
+       ∎ where open ≡-Reasoning
+lemma← {Q} {Σ} M q (h ∷ t) an = lemma← M (δ M q h) t ( an-1 M q h t an )