# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572497606 -32400
# Node ID b9679ebd115611f7618afd9a88470b721ff83161
# Parent  8f0efa93b354d33cc2c44d8d5e3699a246b84f28
...

diff -r 8f0efa93b354 -r b9679ebd1156 agda/automaton-text.agda
--- /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 )
diff -r 8f0efa93b354 -r b9679ebd1156 agda/automaton.agda
--- a/agda/automaton.agda	Thu Oct 31 13:03:14 2019 +0900
+++ b/agda/automaton.agda	Thu Oct 31 13:53:26 2019 +0900
@@ -111,98 +111,3 @@
 -- lemmaNN :  { Q : Set } { Σ : Set  } → (M : Automaton Q  Σ) →  ¬ accept M ( inputnn {n} x y [] )
 -- lemmaNN = ?
 
-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
-
-open import Data.Empty
-
-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 
-
-trace : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → accept M q x ≡ true → List Q
-trace M q [] _ = [ q ]
-trace M q (h ∷ t)  eq = ( q ∷ trace M (δ M q h) t (lemma7 M q h t eq ) )
-
-trace-lemma : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ ) → (eq : accept M q x ≡ true ) → suc (length x) ≡ length (trace M q x eq)
-trace-lemma M q [] eq = refl
-trace-lemma M q (h ∷ t) eq = cong ( λ k → suc k ) ( trace-lemma M (δ M q h) t (lemma7 M q h t eq ))
-
-open accept-n
-
-lemma10 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ )
-   → (eq : accept M q x ≡ true )
-   → (i : ℕ ) → i < suc (length x) → i < length (trace M q x eq)
-lemma10 M q x eq i lt = subst ( λ k → i < k ) (trace-lemma M q x eq) lt
-
-an-1 : { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (h : Σ ) → (t : List Σ ) → (an : 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 = trans (sym (accept-2 an 0 (s≤s z≤n)))( cong (λ k → δ M k h) (accept-1 an))
-    ; 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)
-       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-t :  { Q : Set } { Σ : Set  } (M : Automaton Q  Σ  ) (q : Q ) → (x : List Σ )
-   → (eq : accept M q x ≡ true ) → (an : accept-n M q (length x) (get x ) ) → {i : ℕ }
-   → (lt : i < suc (length x) ) → get (trace M q x eq) (lemma10 M q x eq i lt ) ≡ r an i lt
-lemma-t M q [] eq an {zero} (s≤s z≤n) = sym ( accept-1 an )
-lemma-t M q [] eq an {suc _} (s≤s ())
-lemma-t M q (h ∷ t) eq an {0} = {!!}
-lemma-t M q (h ∷ t) eq an {suc i} (s≤s lt) with lemma-t M (δ M q h) t (lemma7 M q h t eq) (an-1 M q h t an) {i} lt
-... | eq1 = {!!}
-
-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 = λ i lt → get (trace M q (h ∷ t) eq ) {i} (r1 lt) ; accept-1 = {!!} ; accept-2 = {!!} ; accept-3 = lemma8 (accept-3 an) } where
-    r1 : {i : ℕ} → i < 2 + length t → i < length (trace M q (h ∷ t) eq)
-    r1 lt rewrite trace-lemma M q (h ∷ t) eq = lt
-    lemma9 : ( lt : suc (length t) < length (q ∷ trace M q (h ∷ t) eq) ) → r an (length t) lemma5 ≡ get (q ∷ trace M q (h ∷ t) eq ) {suc (length t)} lt 
-    lemma9 = {!!}
-    lemma11 : get (q ∷ trace M (δ M q h) t (lemma7 M q h t eq)) lemma5 ≡ r an (length t) lemma5
-    lemma11 = {!!} -- lemma-t M (δ M q h) (h ∷ t)  ? an ?
-    lemma8 : aend M (r an (length t) lemma5 ) ≡ true → aend M (get (trace M q (h ∷ t) eq) (r1 lemma5)) ≡ true
-    lemma8 eq1 = begin
-        aend M (get (trace M q (h ∷ t) eq) (r1 lemma5))
-       ≡⟨ {!!} ⟩
-        aend M (get (q ∷ (trace M (δ M q h) t (lemma7 M q h t eq ))) lemma5 )
-       ≡⟨ {!!} ⟩
-        aend M (get (trace M (δ M q h) t eq ) {!!} ) 
-       ≡⟨ cong (λ k → aend M k ) ( lemma-t M (δ M q h) t (lemma7 M q h t eq) an lemma5 )  ⟩
-        aend M (r an (length t) lemma5 )
-       ≡⟨ eq1 ⟩
-        true
-       ∎ where open ≡-Reasoning
-    -- with trace-lemma M q ( h ∷ t ) eq | lemma-t M (δ M q h) t (lemma7 M q h t eq) an lemma5
-    -- ... | eq2 | eq3 = subst ( λ k → aend M k ≡ true ) (sym {!!}) eq1 where
-    --     lemma12 : get (q ∷ trace M (δ M q h) t (lemma7 M q h t eq )) (r1 lemma5 ) ≡ r an (foldr (λ _ → suc) 0 t) lemma5
-    --     lemma12 = {!!}
-
-
-