# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1641177718 -32400
# Node ID fd07e3205cea4ae17e51e7dbc0c662736d60d454
# Parent  25ae772402385b2a5cfcf6740b3c0ec7afdc09be
...

diff -r 25ae77240238 -r fd07e3205cea automaton-in-agda/src/finiteSetUtil.agda
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jan 03 00:55:06 2022 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jan 03 11:41:58 2022 +0900
@@ -494,6 +494,10 @@
 ... | true = true
 ... | false = memberQ finq q qs
 
+--
+-- there is a duplicate element in finite list
+--
+
 phase2 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
 phase2 finq q [] = false
 phase2 finq q (x ∷ qs) with equal? finq q x
@@ -508,6 +512,11 @@
 dup-in-list : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
 dup-in-list {Q} finq q qs = phase1 finq q qs 
 
+--
+-- if length of the list is longer than kinds of a finite set, there is a duplicate
+-- prove this based on the theorem on Data.Fin
+--
+
 dup-in-list+fin : { Q : Set }  (finq : FiniteSet Q) 
    → (q : Q) (qs : List Q )
    → fin-dup-in-list (F←Q  finq q) (map (F←Q finq) qs) ≡ true
diff -r 25ae77240238 -r fd07e3205cea automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Mon Jan 03 00:55:06 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Mon Jan 03 11:41:58 2022 +0900
@@ -99,21 +99,6 @@
 open import Data.Unit using (⊤ ; tt)
 open import Data.Nat.Properties
 
-sometime : { a : Set } (x : List a ) → (n : ℕ) → n ≤ length x  → (P : a → Set)  → Set
-sometime {a} [] .zero z≤n P = ⊤
-sometime {a} (x ∷ x₁) zero z≤n P = P x 
-sometime {a} (x ∷ x₁) (suc n) (s≤s lt) P = sometime {a} x₁  n lt P 
-
-get : { a : Set } (x : List a ) → (n : ℕ) → Maybe a
-get [] zero = nothing
-get [] (suc n) = nothing
-get (x ∷ x₁) zero = just x
-get (x ∷ x₁) (suc n) = get x₁ n
-
-is0-bool : ( i :　ℕ ) → Bool
-is0-bool zero = true
-is0-bool (suc i) = false
-
 data QDSEQ { Q : Set } { Σ : Set  } { fa : Automaton  Q  Σ} ( finq : FiniteSet Q) (qd : Q) (z1 :  List Σ) :
        {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where
    qd-nil :  (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr
@@ -128,7 +113,20 @@
        trace-z    : Trace fa z  qd
        trace-yz   : Trace fa (y ++ z)  q
        q=qd : QDSEQ finq qd z trace-yz
-       -- q=qd : equal? finq qd q ≡ is0-bool (length y)
+
+--
+-- using accept ≡ true may simplify the make-TA
+-- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧  ...
+--
+-- like this ...
+-- record TA2 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
+--     field
+--        y z : List Σ
+--        yz=is : y ++ z ≡ is 
+--        trace-z    : accpet fa z qd ≡ true
+--        trace-yz   : accept fa (y ++ z)  q ≡ true
+--        q=qd  : last (tr→qs fa q trace-yz) ≡ just qd 
+--        ¬q=qd : non-last (tr→qs fa q trace-yz) ≡ just qd 
 
 record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
     field
@@ -172,6 +170,7 @@
         tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
         tryz : Trace fa (i ∷ y1 ++ z1) qd
         tryz = tnext qd tryz0
+        -- create Trace (y ++ y ++ z)
         tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
                →  QDSEQ finq qd z1 {q} {y2} tr 
                → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
@@ -201,8 +200,14 @@
     nn =  inputnn0 n i0 i1 []
     nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
     nn01 zero = refl
-    nn01 (suc i) with nn01 i
-    ... | t = {!!}
+    nn01 (suc i) = {!!} where 
+      nn02 : (i : ℕ) → ( x : List In2) → inputnn ( inputnn0 i i0 i1 x ) ≡ inputnn x
+      nn02 zero _ = refl
+      nn02 (suc i) x with inputnn (inputnn0 (suc i) i0 i1 x)
+      ... | nothing = {!!}
+      ... | just []  = {!!}
+      ... | just (i0 ∷ t1)   = {!!}
+      ... | just (i1 ∷ t1)   = {!!}
     nn03 : accept (automaton r) (astart r) nn ≡ true
     nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
     nn09 : (n m : ℕ) → n ≤ n + m
@@ -227,8 +232,7 @@
     nn05 = begin
          suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
          n + n   ≡⟨ sym (nn07 n) ⟩
-         length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
-         {!!} ≤⟨ {!!} ⟩
+         length (inputnn0 n i0 i1 []) ≡⟨ tr→qs=is (automaton r) (inputnn0 n i0 i1 []) (astart r) nn04 ⟩
          length nntrace ∎  where open ≤-Reasoning
     nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04)
     nn06 = dup-in-list>n (afin r) nntrace nn05
@@ -240,7 +244,11 @@
     count i1 (i1 ∷ s) = suc (count i1 s)
     count x (_ ∷ s) = count x s
     nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
-    nn11 = {!!}
+    nn11 {x} [] t = refl
+    nn11 {i0} (i0 ∷ s) t = cong suc ( nn11 s t )
+    nn11 {i0} (i1 ∷ s) t = nn11 s t 
+    nn11 {i1} (i0 ∷ s) t = nn11 s t 
+    nn11 {i1} (i1 ∷ s) t = cong suc ( nn11 s t )
     nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
     nn10 = {!!}
     i1-i0? : List In2 → Bool
@@ -250,7 +258,7 @@
     i1-i0? (i1 ∷ i0 ∷ s) = true
     i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1)  
     nn20 : {s s0 s1 : List In2} → accept (automaton r) (astart r) s ≡ true → ¬ ( s ≡ s0 ++ i1 ∷ i0 ∷ s1 )
-    nn20 = {!!}
+    nn20 {s} {s0} {s1} p np = {!!}
     mono-color : List In2 → Bool
     mono-color [] = true
     mono-color (i0 ∷ s) = mono-color0 s where