# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572484135 -32400
# Node ID 293a2075514b18628cebfbf71f9884fd26f30b29
# Parent  475923938f503bed4a4df272a3c72035c3b38c63
...

diff -r 475923938f50 -r 293a2075514b a03/lecture.ind
--- a/a03/lecture.ind	Wed Oct 30 14:03:37 2019 +0900
+++ b/a03/lecture.ind	Thu Oct 31 10:08:55 2019 +0900
@@ -17,6 +17,11 @@
             aend : Q → Bool
 
 <a href="../agda/automaton.agda"> automaton.agda </a>
+<br>
+<a href="../agda/logic.agda"> logic.agda </a>
+<br>
+<a href="../agda/finiteSet.agda"> finiteSet.agda </a>
+<br>
 
 record は名前のついた数学的構造で、二つの集合 Q と Σの関係定義する関数からなる。
 
@@ -145,6 +150,7 @@
 
 Star
 
+<a href="../agda/regular-language.agda"> Agda での Regular Language </a>
 
 
 
diff -r 475923938f50 -r 293a2075514b agda/automaton.agda
--- a/agda/automaton.agda	Wed Oct 30 14:03:37 2019 +0900
+++ b/agda/automaton.agda	Thu Oct 31 10:08:55 2019 +0900
@@ -18,15 +18,49 @@
 
 open Automaton
 
+data  StatesQ   : Set  where
+   q1 : StatesQ
+   q2 : StatesQ
+   q3 : StatesQ
+
+data  In2   : Set  where
+   i0 : In2
+   i1 : In2
+
+transitionQ : StatesQ  → In2 → StatesQ
+transitionQ q1 i0 = q1
+transitionQ q1 i1 = q2
+transitionQ q2 i0 = q3
+transitionQ q2 i1 = q2
+transitionQ q3 i0 = q2
+transitionQ q3 i1 = q2
+
+aendQ : StatesQ → Bool
+aendQ q2 = true
+aendQ _ = false
+
+a1 : Automaton StatesQ In2
+a1 = record {
+       δ = transitionQ
+     ; aend = aendQ
+   }
+
+accept : { Q : Set } { Σ : Set  }
+    → Automaton Q  Σ
+    → (astart : Q)
+    → List  Σ → Bool
+accept {Q} { Σ} M q [] = aend M q
+accept {Q} { Σ} M q ( H  ∷ T ) = accept M ( (δ M) q H ) T
+
+test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false
+test1 = refl
+test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) 
+
 data  States1   : Set  where
    sr : States1
    ss : States1
    st : States1
 
-data  In2   : Set  where
-   i0 : In2
-   i1 : In2
-
 moves : { Q : Set } { Σ : Set  }
     → Automaton Q  Σ
     → Q → List  Σ → Q
@@ -36,16 +70,6 @@
       move q [] = q
       move q ( H  ∷ T ) = move ( δ M q H)  T
 
-accept : { Q : Set } { Σ : Set  }
-    → Automaton Q  Σ
-    → (astart : Q)
-    → List  Σ → Bool
-accept {Q} { Σ} M astart L = move astart L
-   where
-      move : (q : Q ) ( L : List  Σ ) → Bool
-      move q [] = aend M q
-      move q ( H  ∷ T ) = move (  (δ M) q H ) T
-
 transition1 : States1  → In2  → States1
 transition1 sr i0  = sr
 transition1 sr i1  = ss
@@ -87,5 +111,53 @@
 -- 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
+
+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 = {!!}
+    lemma8 : aend M (r an (length t) lemma5 ) ≡ true → aend M (get (trace M q (h ∷ t) eq) (r1 lemma5)) ≡ true
+    lemma8 eq1 with trace-lemma M q ( h ∷ t ) eq
+    ... | eq2 = subst (λ k → aend M k ≡ true ) (lemma9 {!!} ) eq1
diff -r 475923938f50 -r 293a2075514b agda/logic.agda
--- a/agda/logic.agda	Wed Oct 30 14:03:37 2019 +0900
+++ b/agda/logic.agda	Thu Oct 31 10:08:55 2019 +0900
@@ -60,5 +60,10 @@
 not true = false
 not false = true 
 
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
 infixr  130 _\/_
 infixr  140 _/\_
diff -r 475923938f50 -r 293a2075514b agda/regular-language.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/regular-language.agda	Thu Oct 31 10:08:55 2019 +0900
@@ -0,0 +1,84 @@
+module regular-language where
+
+open import Level renaming ( suc to Suc ; zero to Zero )
+open import Data.List 
+open import Data.Nat hiding ( _≟_ )
+open import Data.Fin
+open import Data.Product
+-- open import Data.Maybe
+open import  Relation.Nullary
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import logic
+open import automaton
+open import finiteSet
+
+language : { Σ : Set } → Set
+language {Σ} = List Σ → Bool
+
+language-L : { Σ : Set } → Set
+language-L {Σ} = List (List Σ)
+
+open Automaton
+
+record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
+   field
+      states : Set 
+      astart : states 
+      automaton : Automaton states Σ
+   contain : List Σ → Bool
+   contain x = accept automaton astart x
+
+Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+Union {Σ} A B x = (A x ) \/ (B x)
+
+split : {Σ : Set} → (List Σ → Bool)
+      → ( List Σ → Bool) → 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
+
+Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
+Concat {Σ} A B = split A B
+
+{-# TERMINATING #-}
+Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
+Star {Σ} A = split A ( Star {Σ} A )
+
+open RegularLanguage 
+isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
+isRegular A x r = A x ≡ contain r x 
+
+M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
+M-Union {Σ} A B = record {
+       states =  states A × states B
+     ; astart = ( astart A , astart B )
+     ; automaton = record {
+             δ = λ 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
+   lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
+           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 ) → 
+     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))
+
+-- M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
+-- M-Concat {Σ} A B = record {
+--        states =  states A ∨ states B
+--      ; astart = case1 (astart A )
+--      ; automaton = record {
+--              δ = {!!}
+--            ; aend = {!!}
+--         }
+--    } 
+-- 
+-- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
+-- closed-in-concat = {!!}
diff -r 475923938f50 -r 293a2075514b index.ind
--- a/index.ind	Wed Oct 30 14:03:37 2019 +0900
+++ b/index.ind	Thu Oct 31 10:08:55 2019 +0900
@@ -29,6 +29,10 @@
 「やさしい Haskell 入門 (バージョン98)」
 </a> 
 
+--Agdaのinstall 方法
+
+<a href="a02/agda-install.html"> ここを参照 </a>
+
 
 -- 評価方法