# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1701247255 -32400
# Node ID 207e6c4e155c354f03896f4f85ace778a67e5d54
# Parent  db02b6938e0431ec0acb4559368518247ff7518e
...

diff -r db02b6938e04 -r 207e6c4e155c automaton-in-agda/src/nfa.agda
--- a/automaton-in-agda/src/nfa.agda	Wed Nov 22 17:07:01 2023 +0900
+++ b/automaton-in-agda/src/nfa.agda	Wed Nov 29 17:40:55 2023 +0900
@@ -41,25 +41,6 @@
 
 -- given list of all states, extract list of q which qs q is true
 
-to-list : {Q : Set} → List Q → ( Q → Bool ) → List Q
-to-list {Q} x exists = to-list1 x [] where
-   to-list1 : List Q → List Q → List Q 
-   to-list1 [] x = x
-   to-list1  (q ∷ qs) x with exists q
-   ... | true  = to-list1 qs (q ∷ x )
-   ... | false = to-list1 qs x
-
-Nmoves : { Q : Set } { Σ : Set  }
-    → NAutomaton Q  Σ
-    → (exists : ( Q → Bool ) → Bool)
-    →  ( Qs : Q → Bool )  → (s : Σ ) → ( Q → Bool )
-Nmoves {Q} { Σ} M exists  Qs  s  = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
-
---
---  Q is finiteSet
---  so we have 
---     exists : ( P : Q → Bool ) → Bool
---  which checks if there is a q in Q such that P q is true
 
 Naccept : { Q : Set } { Σ : Set  } 
     → NAutomaton Q  Σ
@@ -85,6 +66,25 @@
 --     ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
 --     ... | false = ndepth qs sb (i ∷ is) t t1
 
+to-list : {Q : Set} → List Q → ( Q → Bool ) → List Q
+to-list {Q} x exists = to-list1 x [] where
+   to-list1 : List Q → List Q → List Q 
+   to-list1 [] x = x
+   to-list1  (q ∷ qs) x with exists q
+   ... | true  = to-list1 qs (q ∷ x )
+   ... | false = to-list1 qs x
+
+Nmoves : { Q : Set } { Σ : Set  }
+    → NAutomaton Q  Σ
+    → (exists : ( Q → Bool ) → Bool)
+    →  ( Qs : Q → Bool )  → (s : Σ ) → ( Q → Bool )
+Nmoves {Q} { Σ} M exists  Qs  s  = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
+
+--
+--  Q is finiteSet
+--  so we have 
+--     exists : ( P : Q → Bool ) → Bool
+--  which checks if there is a q in Q such that P q is true
 -- trace in state set
 --
 Ntrace : { Q : Set } { Σ : Set  } 
@@ -179,7 +179,7 @@
 test1 : Bool
 test1 = existsS1 fin1
 
-test2 = Nmoves am2 existsS1 start1 
+-- test2 = Nmoves am2 existsS1 start1 
 
 open import automaton 
 
diff -r db02b6938e04 -r 207e6c4e155c automaton-in-agda/src/regex.agda
--- a/automaton-in-agda/src/regex.agda	Wed Nov 22 17:07:01 2023 +0900
+++ b/automaton-in-agda/src/regex.agda	Wed Nov 29 17:40:55 2023 +0900
@@ -14,13 +14,17 @@
 open import logic
 open import regular-language
 
+--  (abc|d.*)
+--  any = < a > || < b > || < c > || < d >
+--  ( < a > & < b > & < c > ) || ( <d > & ( any * ) )
+
 data Regex ( Σ : Set) : Set  where
   ε     : Regex Σ                -- empty
-  φ     : Regex  Σ               -- fail
-  _*    : Regex  Σ  → Regex  Σ 
-  _&_   : Regex  Σ  → Regex  Σ → Regex Σ
-  _||_  : Regex  Σ  → Regex  Σ → Regex Σ
-  <_>   : Σ → Regex  Σ
+  φ     : Regex Σ               -- fail
+  _*    : Regex Σ → Regex Σ 
+  _&_   : Regex Σ → Regex Σ → Regex Σ
+  _||_  : Regex Σ → Regex Σ → Regex Σ
+  <_>   : Σ → Regex Σ
 
 infixr 40 _&_ _||_
 
@@ -30,9 +34,9 @@
 regex-language φ cmp _ = false
 regex-language ε cmp [] = true
 regex-language ε cmp (_ ∷ _) = false
-regex-language (x *) cmp = repeat ( regex-language x cmp  )
-regex-language (x & y) cmp  = split ( λ z → regex-language x  cmp z ) (λ z →  regex-language y  cmp z )
-regex-language (x || y) cmp  = λ s → ( regex-language x  cmp s )  \/  ( regex-language y  cmp s)
+regex-language (x *) cmp = repeat ( regex-language x cmp  ) [] 
+regex-language (x & y) cmp  = split ( λ z → regex-language x  cmp z ) (regex-language y  cmp  ) 
+regex-language (x || y) cmp = λ s → ( regex-language x  cmp s )  \/  ( regex-language y  cmp s)
 regex-language < h > cmp  [] = false
 regex-language < h > cmp  (h1  ∷ [] ) with cmp h h1
 ... | yes _ = true
diff -r db02b6938e04 -r 207e6c4e155c automaton-in-agda/src/regex1-ex.agda
--- a/automaton-in-agda/src/regex1-ex.agda	Wed Nov 22 17:07:01 2023 +0900
+++ b/automaton-in-agda/src/regex1-ex.agda	Wed Nov 29 17:40:55 2023 +0900
@@ -35,20 +35,24 @@
 
 open import nfa
 
-tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] ) ≡ ?
-tt1 P Q = ?
+tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] ) ≡ 
+   P [] /\ Q (a ∷ b ∷ c ∷ []) \/
+   P (a ∷ []) /\ Q (b ∷ c ∷ []) \/
+   P (a ∷ b ∷ []) /\ Q (c ∷ []) \/ P (a ∷ b ∷ c ∷ []) /\ Q []
+tt1 P Q = refl
 
+test-AB→repeat3 : {Σ : Set} → {A : List In → Bool} → repeat A  [] ( a ∷ [] )  ≡  A (a ∷ [] )
+test-AB→repeat3 {_} {A} = refl
 
-test-AB→repeat1 : {Σ : Set} → {A : List In → Bool} → repeat A  ( a ∷ b ∷ c ∷ [] ) ≡  
-    A (a ∷ []) /\ (
-           (A (b ∷ [])     /\ (A (c ∷ []) /\ true \/ false) )
-        \/ (A (b ∷ c ∷ []) /\ true \/ false))
-    \/ A (a ∷ b ∷ []) /\ (A (c ∷ []) /\ true \/ false) 
-    \/ A (a ∷ b ∷ c ∷ []) /\ true \/ false
+test-AB→repeat2 : {Σ : Set} → {A : List In → Bool} → repeat A  [] ( a ∷ b ∷ [] )  ≡  A (a ∷ []) /\ A (b ∷ []) \/ A (a ∷ b ∷ [])
+test-AB→repeat2 {_} {A} = refl
+
+test-AB→repeat1 : {Σ : Set} → {A : List In → Bool} → repeat A  [] ( a ∷ b ∷ c ∷ [] )  ≡  
+    A (a ∷ []) /\ ((A (b ∷ []) /\ A (c ∷ [])) \/ A (b ∷ c ∷ []))    
+    \/ A (a ∷ b ∷ []) /\ A (c ∷ [])    -- ok
+    \/ A (a ∷ b ∷ c ∷ [])  -- ok
 test-AB→repeat1 {_} {A}  = refl
 
-
-
 cmpi : (x y : In ) → Dec (x ≡ y)
 cmpi a a = yes refl
 cmpi b b =  yes refl
@@ -67,7 +71,7 @@
 cmpi d b = no (λ ()) 
 cmpi d c = no (λ ()) 
 
-test-regex : regex-language r1' cmpi ( a ∷ [] ) ≡ false
+test-regex : regex-language r1' cmpi ( a ∷ b ∷ c ∷ [] ) ≡ true
 test-regex = refl
 
 -- test-regex2 : regex-language r2 cmpi ( b ∷ c ∷ a ∷ b ∷ [] ) ≡ false
diff -r db02b6938e04 -r 207e6c4e155c automaton-in-agda/src/regular-language.agda
--- a/automaton-in-agda/src/regular-language.agda	Wed Nov 22 17:07:01 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Nov 29 17:40:55 2023 +0900
@@ -3,11 +3,11 @@
 module regular-language where
 
 open import Level renaming ( suc to Suc ; zero to Zero )
-open import Data.List 
+open import Data.List
 open import Data.Nat hiding ( _≟_ )
 open import Data.Fin hiding ( _+_ )
-open import Data.Empty 
-open import Data.Unit 
+open import Data.Empty
+open import Data.Unit
 open import Data.Product
 -- open import Data.Maybe
 open import  Relation.Nullary
@@ -40,18 +40,28 @@
 
 -- Terminating version of Star1
 --
-repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
-repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool
-repeat2 x pre [] = true
-repeat2 x pre (h ∷ y) = 
-   (x (pre ++ (h ∷ [])) /\ repeat x y )
-   \/ repeat2 x (pre ++ (h ∷ [])) y 
 
-repeat {Σ} x [] = true
-repeat {Σ} x (h ∷ y) = repeat2 x [] (h ∷ y) 
+-- regular-langue (P *) ( a ∷ b ∷ c ∷ [] ) =
+--   (P []) \/
+--   (P (a ∷ []) /\ repeat P (b ∷ c ∷ []) ) \/
+--   (P (a ∷ b ∷ []) /\ repeat P (c ∷ []) ) \/
+--   (P (a ∷ b ∷ c ∷ [])
+--
+-- repeat : {Σ : Set} → (x : language {Σ} ) → language {Σ}
+-- repeat x [] = true
+-- repeat x (h  ∷ t) = (x [] /\ ? (h  ∷ t)) \/
+--   repeat (λ t1 → x ( h ∷ t1 ))  t
 
-Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
-Star {Σ} x y = repeat x y
+repeat : {Σ : Set} → (P : List Σ → Bool) → (pre y : List Σ ) → Bool
+repeat P [] [] = true
+repeat P (h ∷ t) [] = P (h ∷ t)
+repeat P pre (h ∷ []) =      P (pre ++ (h ∷ []))
+repeat P pre (h ∷ y@(_ ∷ _)) =
+   ((P (pre ++ (h ∷ []))) /\ repeat P [] y )
+   \/ repeat P (pre ++ (h ∷ [])) y
+
+Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool
+Star {Σ} x y = repeat x [] y
 
 -- We have to prove definitions of Concat and Star are equivalent to the set theoretic definitions
 
@@ -62,17 +72,17 @@
 -- lemma-Union : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) → Union A B x ≡ ( A x \/ B x )
 -- lemma-Union = ?
 
--- lemma-Concat : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) 
+-- lemma-Concat : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ )
 --    → Concat A B x ≡ ( ∃ λ y → ∃ λ z → A y /\ B z /\ x ≡ y ++ z )
 -- lemma-Concat = ?
 
 open import automaton-ex
 
 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
-       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
-       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
+       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
+       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
        ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
-       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 
+       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  )
    )
 test-AB→split {_} {A} {B} = refl
 
@@ -97,8 +107,8 @@
 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
 isRegular A x r = A x ≡ contain r x
 
-RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ  → language {Σ} 
-RegularLanguage-is-language {Σ} R = RegularLanguage.contain R 
+RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ  → language {Σ}
+RegularLanguage-is-language {Σ} R = RegularLanguage.contain R
 
 RegularLanguage-is-language' : { Σ : Set } → RegularLanguage Σ  → List Σ  → Bool
 RegularLanguage-is-language' {Σ} R x = accept (automaton R) (astart R) x where
@@ -106,7 +116,7 @@
 
 --  a language is implemented by an automaton
 
--- postulate 
+-- postulate
 --   fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
 
 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
@@ -118,7 +128,7 @@
              δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
            ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
         }
-   }  
+   }
 
 closed-in-union :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
 closed-in-union A B [] = lemma where
@@ -126,14 +136,14 @@
            aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
    lemma = refl
 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
-   lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) → 
+   lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
      accept (automaton A) qa t \/ accept (automaton B) qb  t
        ≡ accept (automaton (M-Union A B)) (qa , qb) t
    lemma1 [] qa qb = refl
    lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
 
 
-       
+
 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
     field
         sp0 sp1 : List Σ
@@ -161,7 +171,7 @@
 c-split-lemma {Σ} A B h t eq p = sym ( begin
       true
   ≡⟨  sym eq  ⟩
-      split A B (h ∷ t ) 
+      split A B (h ∷ t )
   ≡⟨⟩
       A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
   ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩
@@ -169,14 +179,14 @@
   ≡⟨ bool-or-1 refl ⟩
       split (λ t1 → A (h ∷ t1)) B t
   ∎ ) where
-     open ≡-Reasoning 
+     open ≡-Reasoning
      lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false
      lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A )
      lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B )
 
 split→AB :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
-split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true 
-split→AB {Σ} A B [] eq | yes eqa | yes eqb = 
+split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true
+split→AB {Σ} A B [] eq | yes eqa | yes eqb =
     record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
 split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
 split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
@@ -207,15 +217,15 @@
       true ∎  where open ≡-Reasoning
 
 
-split→AB1 :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x →  split A B x ≡ true 
+split→AB1 :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x →  split A B x ≡ true
 split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S)  )
-  
+
 
 -- low of exclude middle of Split A B x
 lemma-concat : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Split A B x ∨ ( ¬ Split A B x )
 lemma-concat {Σ} A B x with split A B x in eq
 ... | true = case1 (split→AB A B x eq )
-... | false = case2 (λ p →  ¬-bool eq (split→AB1 A B x p )) 
+... | false = case2 (λ p →  ¬-bool eq (split→AB1 A B x p ))
 
 -- Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
 -- Concat {Σ} A B = split A B
@@ -231,17 +241,39 @@
 
 open StarProp
 
-Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x
-Star→StarProp = ?
+open import Data.List.Properties
 
-StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true
-StarProp→Star {Σ} A x sp = subst (λ k →  Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where
-     spsx : (y : List ( List Σ ) ) → spn sp ≡ y → foldr (λ k → k ++_ ) [] y ≡ x
-     spsx y refl = spn-concat sp 
-     sps1 : (y : List ( List Σ ) ) → spn sp ≡ y → Star A (foldr (λ k → k ++_ ) [] y) ≡ true
-     sps1 = ?
+Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x
+Star→StarProp {Σ} A x ax = ss00 [] x ax  where
+    ss00 :  (pre x : List Σ) → repeat A pre x ≡ true → StarProp A (pre ++ x )
+    ss00 [] [] eq = record { spn = [] ; spn-concat = refl ; propn = eq }
+    ss00 (h ∷ t) [] eq = record { spn = (h ∷ t) ∷ []  ; spn-concat = refl ; propn = bool-and-tt eq refl }
+    ss00 pre (h ∷ []) eq = record { spn = (pre ++ (h ∷ [])) ∷ []  ; spn-concat = ++-assoc pre _ _ 
+       ; propn = bool-and-tt (trans (sym (ss01 pre (h ∷ []) refl )) eq) refl } where
+        ss01 : (pre x : List Σ) → x ≡ h ∷ [] → repeat A pre x ≡ A (pre ++ (h ∷ [])) 
+        ss01 [] (h ∷ []) refl = refl
+        ss01 (x ∷ pre) (h ∷ []) refl = refl
+    ss00 pre (h ∷ y@(i ∷ t)) eq = ? where
+        ss01 : (pre x : List Σ) → x ≡ y → ( ((A (pre ++ (h ∷ []))) /\ repeat A [] y ) \/ repeat A (pre ++ (h ∷ [])) y ) ≡ repeat A pre (h ∷ y )
+        ss01 = ?
+        ss02 :  StarProp A (pre ++ h ∷ y )
+        ss02 with (A (pre ++ (h ∷ []))) /\ repeat A [] y in eq1
+        ... | true = ?
+        ... | false = ? where
+           ss03 : repeat A (pre ++ (h ∷ [])) y ≡ true
+           ss03 = ?
 
-
-lemma-starprop : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x ∨ ( ¬ StarProp A x )
-lemma-starprop = ?
-
+--
+-- StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true
+-- StarProp→Star {Σ} A x sp = subst (λ k →  Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where
+--      spsx : (y : List ( List Σ ) ) → spn sp ≡ y → foldr (λ k → k ++_ ) [] y ≡ x
+--      spsx y refl = spn-concat sp
+--      sps1 : (y : List ( List Σ ) ) → spn sp ≡ y → Star A (foldr (λ k → k ++_ ) [] y) ≡ true
+--      sps1 [] sp=y = refl
+--      sps1 ([] ∷ t) sp=y = ?
+--      sps1 ((x ∷ h) ∷ t) sp=y = ?
+--
+--
+-- lemma-starprop : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x ∨ ( ¬ StarProp A x )
+-- lemma-starprop = ?
+--
diff -r db02b6938e04 -r 207e6c4e155c automaton-in-agda/src/sbconst2.agda
--- a/automaton-in-agda/src/sbconst2.agda	Wed Nov 22 17:07:01 2023 +0900
+++ b/automaton-in-agda/src/sbconst2.agda	Wed Nov 29 17:40:55 2023 +0900
@@ -20,7 +20,8 @@
 --- ( Q → Σ → Q → Bool )              transition of NFA
 --- (Q → Bool) → Σ → (Q → Bool)       generate transition of Automaton  
 
-δconv : { Q : Set } { Σ : Set  } → ( ( Q → Bool ) → Bool ) →  ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
+δconv : { Q : Set } { Σ : Set  } → (exists :( Q → Bool ) → Bool ) →  (nδ : Q → Σ → Q → Bool ) 
+    → (Q → Bool) → Σ → (Q → Bool)
 δconv {Q} { Σ} exists nδ f i q =  exists ( λ r → f r /\ nδ r i q )
 
 subset-construction : { Q : Set } { Σ : Set  } →