# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1690391367 -32400
# Node ID 2d3364cc88adf83e0d9963fa108923310477cfa8
# Parent  6ef927ac832c7ac1c47a08770048426f93960a78
...

diff -r 6ef927ac832c -r 2d3364cc88ad automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Thu Jul 27 00:50:16 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Jul 27 02:09:27 2023 +0900
@@ -166,7 +166,7 @@
     tann : {x y z : List In2} → ¬ y ≡ []
        → x ++ y ++ z ≡ nn
        → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z)  ≡ true )
-    tann {x} {y} {z} ny eq axyz axyyz = ¬-bool (nn10 x y z (trans (Rg (x ++ y ++ z)) axyz ) ) (trans (Rg (x ++ y ++ y ++ z)) axyyz ) where
+    tann {x} {y} {z} ny eq axyz axyyz = ¬-bool (nn10 x y z ny (trans (Rg (x ++ y ++ z)) axyz ) ) (trans (Rg (x ++ y ++ y ++ z)) axyyz ) where
           count0 : (x : List In2) → ℕ
           count0 [] = 0
           count0 (i0 ∷ x) = suc (count0 x)
@@ -175,8 +175,22 @@
           count1 [] = 0
           count1 (i1 ∷ x) = suc (count1 x)
           count1 (i0 ∷ x) = count1 x
+          c0+1=n : (x : List In2 ) → count0 x + count1 x ≡ length x
+          c0+1=n [] = refl
+          c0+1=n (i0 ∷ t) = cong suc ( c0+1=n t )
+          c0+1=n (i1 ∷ t) = begin
+             count0 t + suc (count1 t) ≡⟨ sym (+-assoc (count0 t) _ _) ⟩ 
+             (count0 t + 1 ) + count1 t ≡⟨ cong (λ k → k + count1 t) (+-comm _ 1 ) ⟩ 
+             suc (count0 t + count1 t) ≡⟨ cong suc ( c0+1=n t )  ⟩ 
+             suc (length t) ∎ where open  ≡-Reasoning
           nn15 : (x : List In2 ) → inputnn1 x ≡ true → count0 x ≡ count1 x
-          nn15 = ?
+          nn15 x eq = ? where
+               nn18 : inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true
+               nn18 = eq
+               nn16 : (x : List In2 ) → proj1 (inputnn1-i0 (count0 x) x ) ≡ count0 x
+               nn16 = ?
+               nn17 : (x : List In2 ) → count1 (proj2 (inputnn1-i0 (count0 x) x ) ) ≡ count1 x
+               nn17 = ?
           cong0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y
           cong0 [] y = refl
           cong0 (i0 ∷ x)  y = cong suc (cong0 x y)
@@ -191,8 +205,8 @@
                 i10 : z ≡ a ++ (i1 ∷ i0 ∷ b )
           nn12 : (z : List In2 ) → inputnn1 z ≡ true → ¬ i1i0 z
           nn12 = ?
-          nn11 : (x y z : List In2 ) → inputnn1  (x ++ y ++ z) ≡ true → ¬ ( inputnn1  (x ++ y ++ y ++ z) ≡ true )
-          nn11 x y z xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } )  where
+          nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1  (x ++ y ++ z) ≡ true → ¬ ( inputnn1  (x ++ y ++ y ++ z) ≡ true )
+          nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } )  where
                nn21 : count0 x + count0 y + count0 y + count0 z ≡ count1 x + count1 y + count1 y + count1 z
                nn21 = begin
                     (count0 x + count0 y + count0 y) + count0 z ≡⟨ solve +-0-monoid ⟩
@@ -215,34 +229,61 @@
                     count1 x + count1 (y ++ z)  ≡⟨ cong (λ k → count1 x + k) (cong1 y z) ⟩
                     count1 x + (count1 y + count1 z)  ≡⟨ solve +-0-monoid ⟩
                     count1 x + count1 y + count1 z ∎ where open ≡-Reasoning
+               -- this takes very long time to check and needs 10GB
                bb22 : count0 y ≡ count1 y
-               bb22 = begin
-                    count0 y ≡⟨ sym ( +-cancelʳ-≡  {count1 z  + count0 x + count0 y + count0 z} (count1 y) (count0 y)  (+-cancelˡ-≡ (count1 x + count1 y) (
-                       begin 
-                       count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z))  ≡⟨ solve +-0-monoid  ⟩
-                       (count1 x + count1 y + count1 y + count1 z)  + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩
-                       (count0 x + count0 y + count0 y + count0 z)  + (count1 x + count1 y + count1 z) ≡⟨  +-comm _ (count1 x + count1 y + count1 z) ⟩
-                       (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z)    ≡⟨  solve +-0-monoid ⟩
-                        count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z    
-                            ≡⟨  cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩
-                        count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z    ≡⟨ solve +-0-monoid ⟩
-                        count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z    
-                            ≡⟨  cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z    ) (+-comm (count1 z) _) ⟩
-                        count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z    ≡⟨  solve +-0-monoid ⟩
-                        count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z))    ∎ ))) ⟩
-                    count1 y ∎ where open ≡-Reasoning
+               bb22 = ? -- begin
+--                    count0 y ≡⟨ sym ( +-cancelʳ-≡  {count1 z  + count0 x + count0 y + count0 z} (count1 y) (count0 y)  (+-cancelˡ-≡ (count1 x + count1 y) (
+--                       begin 
+--                       count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z))  ≡⟨ solve +-0-monoid  ⟩
+--                       (count1 x + count1 y + count1 y + count1 z)  + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩
+--                       (count0 x + count0 y + count0 y + count0 z)  + (count1 x + count1 y + count1 z) ≡⟨  +-comm _ (count1 x + count1 y + count1 z) ⟩
+--                       (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z)    ≡⟨  solve +-0-monoid ⟩
+--                        count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z    
+--                            ≡⟨  cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩
+--                        count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z    ≡⟨ solve +-0-monoid ⟩
+--                        count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z    
+--                            ≡⟨  cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z    ) (+-comm (count1 z) _) ⟩
+--                        count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z    ≡⟨  solve +-0-monoid ⟩
+--                        count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z))    ∎ ))) ⟩
+--                    count1 y ∎ where open ≡-Reasoning
                bb23 : count0 y ≡ count1 y → i1i0 (y ++ y)
-               bb23 = ? 
+               bb23 eq = bb25 y y bb26 (subst (λ k → 0 < k ) (sym eq) bb26)  where
+                    bb26 : 0 < count1 y
+                    bb26 with <-cmp 0 (count1 y)
+                    ... | tri< a ¬b ¬c = a
+                    ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (sym bb27 ) (0<ly y ny) ) where
+                         0<ly : (y : List In2) → ¬ y ≡ []  → 0 < length y 
+                         0<ly [] ne = ⊥-elim ( ne refl )
+                         0<ly (x ∷ y) ne = s≤s z≤n
+                         bb27 : length y ≡ 0
+                         bb27 = begin
+                            length y ≡⟨ sym (c0+1=n y) ⟩
+                            count0 y + count1 y ≡⟨ cong (λ k → k + count1 y ) eq  ⟩
+                            count1 y + count1 y ≡⟨ cong₂ _+_ (sym b) (sym b) ⟩
+                            0 ∎ where open ≡-Reasoning
+                    bb25 : (x y : List In2 ) →  0 < count1 x → 0 < count0 y → i1i0 (x ++ y)
+                    bb25 (i0 ∷ x₁) y 0<x 0<y with bb25 x₁ y 0<x 0<y
+                    ... | t = record { a = i0 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i0 ∷_) (i1i0.i10 t) }
+                    bb25 (i1 ∷ []) y 0<x 0<y = bb27 y 0<y where
+                        bb27 : (y : List In2 ) → 0 < count0 y → i1i0 (i1 ∷ y )
+                        bb27 (i0 ∷ y) 0<y = record { a = [] ; b = y ; i10 = refl } 
+                        bb27 (i1 ∷ y) 0<y with bb27 y 0<y
+                        ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) }
+                    bb25 (i1 ∷ i0 ∷ x₁) y 0<x 0<y = record { a = [] ; b = x₁ ++ y ; i10 = refl }
+                    bb25 (i1 ∷ i1 ∷ x₁) y (s≤s z≤n) 0<y with bb25 (i1 ∷ x₁) y (s≤s z≤n) 0<y
+                    ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) }
                bb24 : x ++ y ++ y ++ z ≡ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z
                bb24 = begin
                     x ++ y ++ y ++ z ≡⟨ solve (++-monoid In2) ⟩
                     x ++ (y ++ y) ++ z ≡⟨ cong (λ k → x ++ k ++ z) (i1i0.i10 (bb23 bb22)) ⟩
-                    x ++ (i1i0.a (bb23 bb22) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) ++ z ≡⟨ solve (++-monoid In2) ⟩
+                    x ++ (i1i0.a (bb23 bb22) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) ++ z ≡⟨ cong (λ k → x ++ k)  -- solver does not work here
+                            (++-assoc (i1i0.a (bb23 bb22)) (i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) z ) ⟩
+                    x ++ (i1i0.a (bb23 bb22) ++ (i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z)) ≡⟨ sym (++-assoc x _ _ ) ⟩
                     (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning
 
-          nn10 : (x y z : List In2 ) → inputnn1  (x ++ y ++ z) ≡ true → inputnn1  (x ++ y ++ y ++ z) ≡ false
-          nn10 x y z eq with inputnn1  (x ++ y ++ y ++ z)  | inspect inputnn1  (x ++ y ++ y ++ z)  
-          ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z eq eq1 )
+          nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1  (x ++ y ++ z) ≡ true → inputnn1  (x ++ y ++ y ++ z) ≡ false
+          nn10 x y z my eq with inputnn1  (x ++ y ++ y ++ z)  | inspect inputnn1  (x ++ y ++ y ++ z)  
+          ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z my eq eq1 )
           ... | false | _ = refl