Mercurial > hg > Members > kono > Proof > automaton

changeset 384:a5c874396cc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Jul 2023 09:36:00 +0900
parents 708570e55a91
children 101080136450
files automaton-in-agda/src/derive.agda automaton-in-agda/src/regex.agda automaton-in-agda/src/regex1-ex.agda automaton-in-agda/src/regex1.agda automaton-in-agda/src/regex2.agda automaton-in-agda/src/regular-language.agda
diffstat 6 files changed, 240 insertions(+), 219 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Tue Jul 25 11:26:17 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Wed Jul 26 09:36:00 2023 +0900
@@ -263,8 +263,6 @@
 ... | yes _ | false = false
 ... | no _ | false = false
 
-open import regex1
-
 ISB→Regex : (r : Regex Σ) →  (ISB r → Bool) → Regex Σ
 ISB→Regex ε f with f record { s = ε ; is-sub = sunit  }
 ... | true = ε
@@ -279,10 +277,6 @@
 ... | true = < x >
 ... | false = φ
 
-lem00 : (r : Regex Σ) → (z : Σ) (x : List Σ )→ regex-language r eq? (z ∷ x ) ≡  
-                                               regex-language (ISB→Regex r (λ isb → (sbderive r (toSB r ) z isb)))  eq? x  
-lem00 r z x = {!!}
-
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
 
@@ -295,7 +289,48 @@
 regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool
 regex-match1 r is = accept ( regex→automaton1 r ) (λ sb → toSB r sb) is
 
+derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match r x
+derive-is-regex-language ε [] = refl
+derive-is-regex-language ε (x ∷ x₁) = ?
+derive-is-regex-language φ [] = refl
+derive-is-regex-language φ (x ∷ x₁) = ?
+derive-is-regex-language (r *) x = ?
+derive-is-regex-language (r & r₁) x = ?
+derive-is-regex-language (r || r₁) x = ?
+derive-is-regex-language < x₁ > [] = refl
+derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x
+... | yes _  = refl
+... | no _  = refl
+derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = ? where -- rg01 (eq? x₁ x) where
+    rg01 : Dec ( x₁ ≡ x ) →  regex-language < x₁ > eq? (x ∷ x₂ ∷ x₃ ) ≡ false
+    rg01 (yes eq) = refl
+    rg01 (no neq) = refl
+    rg03 : (x s : Σ) → (derivative < x > s ≡ ε ) ∨ (derivative < x > s ≡ φ )
+    rg03 x s with eq? x s
+    ... | yes _ = case1 refl
+    ... | no _ = case2 refl
+    rg02 : regex-match < x₁ > (x ∷ x₂ ∷ x₃ ) ≡ false
+    rg02 with rg03 x₁ x
+    ... | case1 eq = ?
+    ... | case2 eq = ?
+--    immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b)
+
+derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-match r x ≡ regex-match1 r x
+derive=ISB ε [] = refl
+derive=ISB ε (x ∷ x₁) = ?
+derive=ISB φ [] = refl
+derive=ISB φ (x ∷ x₁) = ?
+derive=ISB (r *) x = ?
+derive=ISB (r & r₁) x = ?
+derive=ISB (r || r₁) x = ?
+derive=ISB < x₁ > [] = refl
+derive=ISB < x₁ > (x ∷ []) with eq? x₁ x
+... | yes _ = ?
+... | no _ = refl
+derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ?
+
+ISB-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match1 r x
+ISB-is-regex-language r x = trans ( derive-is-regex-language r x ) (derive=ISB r x)
 
 
 
-
--- a/automaton-in-agda/src/regex.agda	Tue Jul 25 11:26:17 2023 +0900
+++ b/automaton-in-agda/src/regex.agda	Wed Jul 26 09:36:00 2023 +0900
@@ -1,5 +1,17 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module regex where
 
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Fin hiding ( pred )
+open import Data.Nat hiding ( _≟_ )
+open import Data.List hiding ( any ;  [_] )
+-- import Data.Bool using ( Bool ; true ; false ; _∧_ )
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import logic
+open import regular-language
+
 data Regex ( Σ : Set) : Set  where
   ε     : Regex Σ                -- empty
   φ     : Regex  Σ               -- fail
@@ -10,5 +22,18 @@
 
 infixr 40 _&_ _||_
 
+-- Meaning of regular expression
 
+regex-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y))  →  List Σ → Bool
+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 < h > cmp  [] = false
+regex-language < h > cmp  (h1  ∷ [] ) with cmp h h1
+... | yes _ = true
+... | no _  = false
+regex-language < h >  _ (_ ∷ _ ∷ _)  = false
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/regex1-ex.agda	Wed Jul 26 09:36:00 2023 +0900
@@ -0,0 +1,167 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module regex1-ex where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Fin hiding ( pred )
+open import Data.Nat hiding ( _≟_ )
+open import Data.List hiding ( any ;  [_] )
+-- import Data.Bool using ( Bool ; true ; false ; _∧_ )
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import regex
+open import logic
+open import regular-language
+
+-- postulate a b c d : Set
+
+data In : Set where
+   a : In
+   b : In
+   c : In
+   d : In
+
+-- infixr 40 _&_ _||_
+
+r1' =    (< a > & < b >) & < c >                                         --- abc
+r1 =    < a > &  < b > & < c >                                            --- abc
+r0 : ¬ (r1' ≡ r1)
+r0 ()
+any = < a > || < b >  || < c > || < d >                                   --- a|b|c|d
+r2 =    ( any * ) & ( < a > & < b > & < c > )                            -- .*abc
+r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
+r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
+r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
+
+open import nfa
+
+tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] ) ≡ ?
+tt1 P Q = ?
+
+
+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→repeat1 {_} {A}  = refl
+
+
+
+cmpi : (x y : In ) → Dec (x ≡ y)
+cmpi a a = yes refl
+cmpi b b =  yes refl
+cmpi c c =  yes refl
+cmpi d d =  yes refl
+cmpi a b =  no (λ ())
+cmpi a c =  no (λ ())
+cmpi a d =  no (λ ())
+cmpi b a = no (λ ())
+cmpi b c = no (λ ()) 
+cmpi b d = no (λ ()) 
+cmpi c a = no (λ ()) 
+cmpi c b = no (λ ()) 
+cmpi c d = no (λ ()) 
+cmpi d a = no (λ ()) 
+cmpi d b = no (λ ()) 
+cmpi d c = no (λ ()) 
+
+test-regex : regex-language r1' cmpi ( a ∷ [] ) ≡ false
+test-regex = refl
+
+-- test-regex2 : regex-language r2 cmpi ( b ∷ c ∷ a ∷ b ∷ [] ) ≡ false
+-- test-regex2 = refl
+
+test-regex1 : regex-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true
+test-regex1 = refl
+
+                                                                                                                    
+--test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ (
+--        ( A [] /\ B ( a ∷ b ∷ a ∷ [] ) ) \/
+--        ( A ( a ∷ [] ) /\ B ( b ∷ a ∷ [] ) ) \/
+--        ( A ( a ∷ b ∷ [] ) /\ B ( a ∷ [] ) ) \/
+--        ( A ( a ∷ b ∷ a ∷ [] ) /\ B  []  )
+--    )
+-- test-AB→split {_} {A} {B} = refl
+
+list-eq : {Σ : Set} → (cmpi : (s t : Σ)  → Dec (s ≡ t ))  → (s t : List Σ ) → Bool
+list-eq cmpi [] [] = true
+list-eq cmpi [] (x ∷ t) = false
+list-eq cmpi (x ∷ s) [] = false
+list-eq cmpi (x ∷ s) (y ∷ t) with cmpi x y
+... | yes _ = list-eq cmpi s t
+... | no _ = false
+
+-- split-spec-01 :  {s t u : List In } → s ++ t ≡ u → split (list-eq cmpi s) (list-eq cmpi t)  u ≡ true
+-- split-spec-01 = {!!}
+
+-- from example 1.53 1
+
+ex53-1 : Set 
+ex53-1 = (s : List In ) → regex-language ( (< a > *) & < b > & (< a > *) ) cmpi s ≡ true → {!!} -- contains exact one b
+
+ex53-2 : Set 
+ex53-2 = (s : List In ) → regex-language ( (any * ) & < b > & (any *) ) cmpi s ≡ true → {!!} -- contains at lease one b
+
+evenp : {Σ : Set} →  List Σ → Bool
+oddp : {Σ : Set} →  List Σ → Bool
+oddp [] = false
+oddp (_ ∷ t) = evenp t
+
+evenp [] = true
+evenp (_ ∷ t) = oddp t
+
+-- from example 1.53 5
+egex-even : Set
+egex-even = (s : List In ) → regex-language ( ( any & any ) * ) cmpi s ≡ true → evenp s ≡ true
+
+test11 =  regex-language ( ( any & any ) * ) cmpi (a ∷ [])
+test12 =  regex-language ( ( any & any ) * ) cmpi (a ∷ b ∷ [])
+
+-- proof-egex-even : egex-even 
+-- proof-egex-even [] _ = refl
+-- proof-egex-even (a ∷ []) ()
+-- proof-egex-even (b ∷ []) ()
+-- proof-egex-even (c ∷ []) ()
+-- proof-egex-even (x ∷ x₁ ∷ s) y = proof-egex-even s {!!}
+
+open import finiteSet
+
+iFin : FiniteSet In
+iFin = record {
+     finite = finite0
+   ; Q←F = Q←F0
+   ; F←Q = F←Q0
+   ; finiso→ = finiso→0
+   ; finiso← = finiso←0
+ } where
+     finite0 : ℕ
+     finite0 = 4
+     Q←F0 : Fin finite0 → In
+     Q←F0 zero = a
+     Q←F0 (suc zero) = b
+     Q←F0 (suc (suc zero)) = c
+     Q←F0 (suc (suc (suc zero))) = d
+     F←Q0 : In → Fin finite0
+     F←Q0 a = # 0
+     F←Q0 b = # 1
+     F←Q0 c = # 2
+     F←Q0 d = # 3
+     finiso→0 : (q : In) → Q←F0 ( F←Q0 q ) ≡ q
+     finiso→0 a = refl
+     finiso→0 b = refl
+     finiso→0 c =  refl
+     finiso→0 d =  refl
+     finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
+     finiso←0 zero = refl
+     finiso←0 (suc zero) = refl
+     finiso←0 (suc (suc zero)) = refl
+     finiso←0 (suc (suc (suc zero))) = refl
+
+
+-- open import derive In iFin
+-- open import automaton
+
+-- ra-ex = trace (regex→automaton cmpi r2) (record { state = r2 ; is-derived = unit refl }) ( a ∷ b ∷ c ∷ [])
+
--- a/automaton-in-agda/src/regex1.agda	Tue Jul 25 11:26:17 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,207 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-module regex1 where
-
-open import Level renaming ( suc to succ ; zero to Zero )
-open import Data.Fin hiding ( pred )
-open import Data.Nat hiding ( _≟_ )
-open import Data.List hiding ( any ;  [_] )
--- import Data.Bool using ( Bool ; true ; false ; _∧_ )
--- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
-open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import regex
-open import logic
-open import regular-language
-
--- postulate a b c d : Set
-
-data In : Set where
-   a : In
-   b : In
-   c : In
-   d : In
-
--- infixr 40 _&_ _||_
-
-r1' =    (< a > & < b >) & < c >                                         --- abc
-r1 =    < a > &  < b > & < c >                                            --- abc
-r0 : ¬ (r1' ≡ r1)
-r0 ()
-any = < a > || < b >  || < c > || < d >                                   --- a|b|c|d
-r2 =    ( any * ) & ( < a > & < b > & < c > )                            -- .*abc
-r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
-r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
-r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
-
-open import nfa
-
---    former ++ later  ≡ x
--- split : {Σ : Set} → (x : List Σ → Bool) → (y :  List Σ → Bool) → (z : List Σ ) → Bool
--- split x y  [] = x [] /\ y []
--- split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
---   split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
-
----   ( a ∷ b ∷ c ∷ [] )
---
----     former ( a ∷ b ∷ c ∷ [] ) ∧ later []
---- ∨ ( former ( a ∷ b ∷ [] ) ∧ later (c ∷ [] ) )
---- ∨ ( former ( a ∷ [] ) ∧ later (b ∷ c ∷ [] ) )
---- ∨ ( former ( [] ) ∧ later (a ∷ b ∷ c ∷ [] ) )
-
-tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] ) ≡ ?
-tt1 P Q = ?
-
-{-# TERMINATING #-}
-repeat-t : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
-repeat-t x [] = true
-repeat-t {Σ} x ( h  ∷ t ) = split x (repeat-t {Σ} x) ( h  ∷ t )
-
-repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
-repeat {Σ} x [] = true
-repeat {Σ} x (h ∷ y) = repeat2 [] (h ∷ y) where
-    repeat2 : (pre y : List Σ ) → Bool
-    repeat2 pre [] = false
-    repeat2 pre (h ∷ y) = 
-       (x (pre ++ (h ∷ [])) /\ repeat x y )
-       \/ repeat2 (pre ++ (h ∷ [])) y 
-
-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→repeat1 {_} {A}  = refl
-
-
--- Meaning of regular expression
-
-regex-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y))  →  List Σ → Bool
-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 < h > cmp  [] = false
-regex-language < h > cmp  (h1  ∷ [] ) with cmp h h1
-... | yes _ = true
-... | no _  = false
-regex-language < h >  _ (_ ∷ _ ∷ _)  = false
-
-cmpi : (x y : In ) → Dec (x ≡ y)
-cmpi a a = yes refl
-cmpi b b =  yes refl
-cmpi c c =  yes refl
-cmpi d d =  yes refl
-cmpi a b =  no (λ ())
-cmpi a c =  no (λ ())
-cmpi a d =  no (λ ())
-cmpi b a = no (λ ())
-cmpi b c = no (λ ()) 
-cmpi b d = no (λ ()) 
-cmpi c a = no (λ ()) 
-cmpi c b = no (λ ()) 
-cmpi c d = no (λ ()) 
-cmpi d a = no (λ ()) 
-cmpi d b = no (λ ()) 
-cmpi d c = no (λ ()) 
-
-test-regex : regex-language r1' cmpi ( a ∷ [] ) ≡ false
-test-regex = refl
-
--- test-regex2 : regex-language r2 cmpi ( b ∷ c ∷ a ∷ b ∷ [] ) ≡ false
--- test-regex2 = refl
-
-test-regex1 : regex-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true
-test-regex1 = refl
-
-                                                                                                                    
---test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ (
---        ( A [] /\ B ( a ∷ b ∷ a ∷ [] ) ) \/
---        ( A ( a ∷ [] ) /\ B ( b ∷ a ∷ [] ) ) \/
---        ( A ( a ∷ b ∷ [] ) /\ B ( a ∷ [] ) ) \/
---        ( A ( a ∷ b ∷ a ∷ [] ) /\ B  []  )
---    )
--- test-AB→split {_} {A} {B} = refl
-
-list-eq : {Σ : Set} → (cmpi : (s t : Σ)  → Dec (s ≡ t ))  → (s t : List Σ ) → Bool
-list-eq cmpi [] [] = true
-list-eq cmpi [] (x ∷ t) = false
-list-eq cmpi (x ∷ s) [] = false
-list-eq cmpi (x ∷ s) (y ∷ t) with cmpi x y
-... | yes _ = list-eq cmpi s t
-... | no _ = false
-
--- split-spec-01 :  {s t u : List In } → s ++ t ≡ u → split (list-eq cmpi s) (list-eq cmpi t)  u ≡ true
--- split-spec-01 = {!!}
-
--- from example 1.53 1
-
-ex53-1 : Set 
-ex53-1 = (s : List In ) → regex-language ( (< a > *) & < b > & (< a > *) ) cmpi s ≡ true → {!!} -- contains exact one b
-
-ex53-2 : Set 
-ex53-2 = (s : List In ) → regex-language ( (any * ) & < b > & (any *) ) cmpi s ≡ true → {!!} -- contains at lease one b
-
-evenp : {Σ : Set} →  List Σ → Bool
-oddp : {Σ : Set} →  List Σ → Bool
-oddp [] = false
-oddp (_ ∷ t) = evenp t
-
-evenp [] = true
-evenp (_ ∷ t) = oddp t
-
--- from example 1.53 5
-egex-even : Set
-egex-even = (s : List In ) → regex-language ( ( any & any ) * ) cmpi s ≡ true → evenp s ≡ true
-
-test11 =  regex-language ( ( any & any ) * ) cmpi (a ∷ [])
-test12 =  regex-language ( ( any & any ) * ) cmpi (a ∷ b ∷ [])
-
--- proof-egex-even : egex-even 
--- proof-egex-even [] _ = refl
--- proof-egex-even (a ∷ []) ()
--- proof-egex-even (b ∷ []) ()
--- proof-egex-even (c ∷ []) ()
--- proof-egex-even (x ∷ x₁ ∷ s) y = proof-egex-even s {!!}
-
-open import finiteSet
-
-iFin : FiniteSet In
-iFin = record {
-     finite = finite0
-   ; Q←F = Q←F0
-   ; F←Q = F←Q0
-   ; finiso→ = finiso→0
-   ; finiso← = finiso←0
- } where
-     finite0 : ℕ
-     finite0 = 4
-     Q←F0 : Fin finite0 → In
-     Q←F0 zero = a
-     Q←F0 (suc zero) = b
-     Q←F0 (suc (suc zero)) = c
-     Q←F0 (suc (suc (suc zero))) = d
-     F←Q0 : In → Fin finite0
-     F←Q0 a = # 0
-     F←Q0 b = # 1
-     F←Q0 c = # 2
-     F←Q0 d = # 3
-     finiso→0 : (q : In) → Q←F0 ( F←Q0 q ) ≡ q
-     finiso→0 a = refl
-     finiso→0 b = refl
-     finiso→0 c =  refl
-     finiso→0 d =  refl
-     finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
-     finiso←0 zero = refl
-     finiso←0 (suc zero) = refl
-     finiso←0 (suc (suc zero)) = refl
-     finiso←0 (suc (suc (suc zero))) = refl
-
-
--- open import derive In iFin
--- open import automaton
-
--- ra-ex = trace (regex→automaton cmpi r2) (record { state = r2 ; is-derived = unit refl }) ( a ∷ b ∷ c ∷ [])
-
--- a/automaton-in-agda/src/regex2.agda	Tue Jul 25 11:26:17 2023 +0900
+++ b/automaton-in-agda/src/regex2.agda	Wed Jul 26 09:36:00 2023 +0900
@@ -21,7 +21,6 @@
 open import regex
 open import regular-language
 open import automaton
-open import regex1
 open import logic
 
 open import regular-star 
--- a/automaton-in-agda/src/regular-language.agda	Tue Jul 25 11:26:17 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Jul 26 09:36:00 2023 +0900
@@ -36,15 +36,17 @@
 Star1 {Σ} A [] = true
 Star1 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t)
 
-Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
-Star {Σ} x [] = true
-Star {Σ} x (h ∷ y) = repeat2 [] (h ∷ y) where
+repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
+repeat {Σ} x [] = true
+repeat {Σ} x (h ∷ y) = repeat2 [] (h ∷ y) where
     repeat2 : (pre y : List Σ ) → Bool
     repeat2 pre [] = false
     repeat2 pre (h ∷ y) = 
-       (x (pre ++ (h ∷ [])) /\ Star x y )
+       (x (pre ++ (h ∷ [])) /\ repeat x y )
        \/ repeat2 (pre ++ (h ∷ [])) y 
 
+Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
+Star {Σ} x y = repeat x y
 
 open import automaton-ex