# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1700033047 -32400
# Node ID 3d0aa205edf9fc82c822a2887ac8c3e1e7087838
# Parent  c7ad8d2dc1575fe2d715fbc8ed5a8cc7adc80bc3
...

diff -r c7ad8d2dc157 -r 3d0aa205edf9 a04/lecture.ind
--- a/a04/lecture.ind	Thu Nov 09 18:04:55 2023 +0900
+++ b/a04/lecture.ind	Wed Nov 15 16:24:07 2023 +0900
@@ -25,6 +25,14 @@
 
 abcfbffbcdf は、この正規表現にマッチする。a.*fb.*f と書いても良い。
 
+Perl で書けば
+
+  perl -de 0
+  DB<14> if ($x =~ /^(a.*f)(b.*f)$/)  { print "$1 $2\n"; }
+
+  perl -e 'if ($x =~ /^(a.*f)(b.*f)$/)  { print "$1 $2\n"; }'
+
+
 a.*f は以下の状態遷移で書ける。
 
 State は a0,a1,ae,af で、ae ならば受理。
@@ -42,6 +50,7 @@
      δb b0 _ = bf
 
 これを使って、a.*fb.*f を受理してみる。
+<a href="../automaton-in-agda/src/nfa136.agda"> nfa136.agda </a>
 
 <center><img src="fig/af-concat.svg"></center>
 
diff -r c7ad8d2dc157 -r 3d0aa205edf9 automaton-in-agda/src/flcagl.agda
--- a/automaton-in-agda/src/flcagl.agda	Thu Nov 09 18:04:55 2023 +0900
+++ b/automaton-in-agda/src/flcagl.agda	Wed Nov 15 16:24:07 2023 +0900
@@ -8,6 +8,11 @@
 --          bb : (y : aaa) → aaa
 --          cc : (y : aaa) → aaa
 --
+--     Lang : {Σ : Set } → List Σ → Bool
+--     Lang [] = ?
+--     Lang (h ∷ t)  = ?
+--     
+--
 --   (x : aaa) → bb → cc → aend
 --     induction : ( P : aaa → Set ) → (x : aaa) → P x
 --     induction P aend = ?
@@ -64,6 +69,8 @@
 
         open List 
 
+        -- Lnag ≅ Bool × (Σ → Lang)
+        --
         record  Lang (i : Size)  : Set  where
            coinductive
            field
@@ -118,9 +125,11 @@
 
         _+_ : ∀{i}  (k l : Lang i) → Lang i
         ν (k + l) = ν k ∧ ν l
-        δ (k + l) x with ν k
-        ... | false = δ k x  + l 
-        ... | true  = (δ k x  + l )  ∪ δ l x 
+        δ (k + l) x with ν k | ν l
+        ... | false | true = δ k x  + l 
+        ... | false | false = δ k x  + l 
+        ... | true  | true = (δ k x  + l )  ∪ δ l x 
+        ... | true  | false = (δ k x  + l )  ∪ δ l x 
 
         language : { Σ : Set } → Set
         language {Σ}  = List ∞ Σ → Bool
@@ -130,12 +139,12 @@
         split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
           split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
-        LtoSplit : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ true →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true
+        LtoSplit : (x y : Lang ∞ ) → (z : List ∞ A) → ((x  + y ) ∋ z) ≡ true →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true
         LtoSplit x y [] xy with ν x | ν y
         ... | true | true = refl
         LtoSplit x y (h ∷ z) xy = ?
 
-        SplitoL : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ false →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false
+        SplitoL : (x y : Lang ∞ ) → (z : List ∞ A) → ((x  + y ) ∋ z) ≡ false →   split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false
         SplitoL x y [] xy with ν x | ν y 
         ... | false | false = refl
         ... | false | true = ?
@@ -217,8 +226,7 @@
         ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)
 
         withExample : (P : Bool → Set) (p : P true) (q : P false) →
-           {A : Set} (g : A → Bool) (x : A) → P (g x)
-        withExample P p q g x with g x
+           {A : Set} (g : A → Bool) (x : A) → P (g x) withExample P p q g x with g x
         ... | true = p
         ... | false = q
 
diff -r c7ad8d2dc157 -r 3d0aa205edf9 automaton-in-agda/src/halt.agda
--- a/automaton-in-agda/src/halt.agda	Thu Nov 09 18:04:55 2023 +0900
+++ b/automaton-in-agda/src/halt.agda	Wed Nov 15 16:24:07 2023 +0900
@@ -16,6 +16,9 @@
 
 open import logic
 
+--
+--     (R → Bool) <-> S 
+--
 record FBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
    field
        ffun←  :  S → R → Bool
@@ -26,6 +29,17 @@
 
 open FBijection 
 
+--  S <-> S → Bool 
+-- 
+--  S   0 1 2 3 .... 
+--  0   t f t f .... 
+--  1   t f t f .... 
+--  2   t f t f .... 
+--  3   t t t t .....
+--  ..
+-- counter exmpple
+--      f t f f ...
+
 fdiag : {S : Set }  (b : FBijection  S S) → S → Bool
 fdiag b n = not (ffun← b n n)
 
@@ -35,6 +49,8 @@
 --     is pointwise equal to fdiag b , which means not (ffun← b (ffun→ b (fdiag b) ) x ≡ (fdiag b) x )
 --     but is also means not (fdiag b) x ≡ (fdiag b) x , contradiction
 
+--   ¬  (S → Bool) <-> S 
+--
 fdiagonal : { S : Set } → ¬ FBijection  S S
 fdiagonal {S} b =  ¬t=f _ (trans ff4 (sym (ff3 _) ) ) where
     ff1 : S
diff -r c7ad8d2dc157 -r 3d0aa205edf9 automaton-in-agda/src/nfa136.agda
--- a/automaton-in-agda/src/nfa136.agda	Thu Nov 09 18:04:55 2023 +0900
+++ b/automaton-in-agda/src/nfa136.agda	Wed Nov 15 16:24:07 2023 +0900
@@ -45,7 +45,7 @@
 
 t146-1 = Ntrace nfa136 states136 exists136  start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )
 
-test111 = ?
+-- test111 = ?
 
 example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] )
 
@@ -83,29 +83,67 @@
    a0 : Q2
    a1 : Q2
    ae : Q2
+   af : Q2
    b0 : Q2
    b1 : Q2
    be : Q2
+   bf : Q2
 
 -- a.*f
 
-aδ : Q2 → Σ2 → Q2 → Bool
-aδ a0 ca a1 = true
-aδ a0 _ _ = false
-aδ a1 cf ae = true
-aδ a1 _ a1 = true
-aδ _ _ _ = false
-
 a-end : Q2 → Bool
 a-end ae = true
 a-end _ = false
 
+aδ : Q2 → Σ2 → Q2 
+aδ a0 ca = a1 
+aδ a0 _ = af 
+aδ a1 cf = ae 
+aδ a1 _ = a1 
+aδ ae cf = ae 
+aδ ae _ = a1 
+aδ _ _ = af 
+fa-a : Automaton Q2 Σ2
+fa-a = record { δ = aδ ; aend = a-end }
+
+test111 : Bool
+test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] )
+
+b-end : Q2 → Bool
+b-end be = true
+b-end _ = false
+
+bδ : Q2 → Σ2 → Q2 
+bδ b0 cb = b1 
+bδ b0 _ = bf 
+bδ b1 cf = be 
+bδ b1 _ = b1 
+bδ be cf = be 
+bδ be _ = b1 
+bδ _ _ = bf 
+fa-b : Automaton Q2 Σ2
+fa-b = record { δ = bδ ; aend = b-end }
+
+test115 : Bool
+test115 = accept fa-b b0 ( cb ∷ cf ∷ cf ∷ [] )
+
+open import regular-language
+
+test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] )
+
+naδ : Q2 → Σ2 → Q2 → Bool
+naδ a0 ca a1 = true
+naδ a0 _ _ = false
+naδ a1 cf ae = true
+naδ a1 _ a1 = true
+naδ _ _ _ = false
+
 a-start : Q2 → Bool
 a-start a0 = true
 a-start _ = false
 
 nfa-a : NAutomaton Q2 Σ2
-nfa-a = record { Nδ = aδ ; Nend = a-end }
+nfa-a = record { Nδ = naδ ; Nend = a-end }
 
 nfa-a-exists : (Q2 → Bool) → Bool
 nfa-a-exists p = p a0 \/ p a1 \/ p ae
@@ -113,27 +151,23 @@
 test-a1 : Bool
 test-a1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ [] )
 
-test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae  ∷ [])  ( ca ∷ cf ∷ cf ∷ [] ) )
+-- test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae  ∷ [])  ( ca ∷ cf ∷ cf ∷ [] ) )
 
 -- b.*f
 
-bδ : Q2 → Σ2 → Q2 → Bool
-bδ ae cb b1 = true
-bδ ae _ _ = false
-bδ b1 cf be = true
-bδ b1 _ b1 = true
-bδ _ _ _ = false
-
-b-end : Q2 → Bool
-b-end be = true
-b-end _ = false
+nbδ : Q2 → Σ2 → Q2 → Bool
+nbδ ae cb b1 = true
+nbδ ae _ _ = false
+nbδ b1 cf be = true
+nbδ b1 _ b1 = true
+nbδ _ _ _ = false
 
 b-start : Q2 → Bool
 b-start ae = true
 b-start _ = false
 
 nfa-b : NAutomaton Q2 Σ2
-nfa-b = record { Nδ = bδ ; Nend = b-end }
+nfa-b = record { Nδ = nbδ ; Nend = b-end }
 
 nfa-b-exists : (Q2 → Bool) → Bool
 nfa-b-exists p = p b0 \/ p b1 \/ p ae
@@ -141,7 +175,7 @@
 -- (a.*f)(b.*f)
 
 abδ : Q2 → Σ2 → Q2 → Bool
-abδ x i y = aδ x i y \/ bδ x i y
+abδ x i y = naδ x i y \/ nbδ x i y
 
 nfa-ab : NAutomaton Q2 Σ2
 nfa-ab = record { Nδ = abδ ; Nend = b-end }
@@ -155,7 +189,7 @@
 test-ab2 : Bool
 test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
 
-test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae  ∷ b0 ∷ b1 ∷ be  ∷ [])  ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
+-- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae  ∷ b0 ∷ b1 ∷ be  ∷ [])  ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ))
 
 test112 : Automaton (Q2 → Bool) Σ2
 test112 = subset-construction nfa-ab-exists nfa-ab
@@ -165,3 +199,10 @@
 test113 : Bool
 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] )
 
+-- 
+
+
+
+
+
+
diff -r c7ad8d2dc157 -r 3d0aa205edf9 automaton-in-agda/src/regular-language.agda
--- a/automaton-in-agda/src/regular-language.agda	Thu Nov 09 18:04:55 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Nov 15 16:24:07 2023 +0900
@@ -143,8 +143,11 @@
 
 open Split
 
+AB→split1 :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → {z : List Σ} → A x ≡ true → B y ≡ true →  z ≡ x ++ y → Split A B z
+AB→split1 {Σ} A B x y {z} ax by z=xy = record { sp0 = x ; sp1 = y ; sp-concat = sym z=xy ; prop0 = ax ; prop1 = by }
+
 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
-list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
+list-empty++ [] [] _ = record { proj1 = refl ; proj2 = refl }
 list-empty++ [] (x ∷ y) ()
 list-empty++ (x ∷ x₁) y ()
 
@@ -186,30 +189,46 @@
 
 AB→split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
 AB→split {Σ} A B [] [] eqa eqb = begin
-       split A B [] 
-     ≡⟨⟩
-       A [] /\ B []
-     ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
+       split A B [] ≡⟨⟩
+       A [] /\ B [] ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
       true
      ∎  where open ≡-Reasoning
 AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
-      split A B (h ∷ y )
-     ≡⟨⟩
-      A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
-     ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
-      true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
-     ≡⟨⟩
-      true \/ split (λ t1 → A (h ∷ t1)) B y
-     ≡⟨⟩
-      true
-     ∎  where open ≡-Reasoning
+      split A B (h ∷ y ) ≡⟨⟩
+      A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
+      true /\ true \/ split (λ t1 → A (h ∷ t1)) B y ≡⟨⟩
+      true \/ split (λ t1 → A (h ∷ t1)) B y ≡⟨⟩
+      true ∎  where open ≡-Reasoning
 AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
-       split A B ((h ∷ t) ++ y)  
-     ≡⟨⟩
+       split A B ((h ∷ t) ++ y)  ≡⟨⟩
        A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
      ≡⟨ cong ( λ k →  A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
-       A [] /\ B (h ∷ t ++ y) \/ true
-     ≡⟨ bool-or-3 ⟩
-      true
-     ∎  where open ≡-Reasoning
+       A [] /\ B (h ∷ t ++ y) \/ true ≡⟨ bool-or-3 ⟩
+      true ∎  where open ≡-Reasoning
+
 
+-- plit→AB1 :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x →  split A B x ≡ true 
+-- plit→AB1 {Σ} A B [] S = begin
+--      split A B [] ≡⟨⟩
+--      A [] /\ B [] ≡⟨ cong₂ _/\_ a=t b=t  ⟩ 
+--      true  /\ true  ≡⟨ bool-and-tt refl refl ⟩
+--      true ∎  where 
+--         open ≡-Reasoning
+--         a=t : A [] ≡ true
+--         a=t = begin
+--            A [] ≡⟨ cong (λ k → A k) (sym (proj1 (list-empty++ (sp0 S) (sp1 S) (sp-concat S))))  ⟩
+--            A (sp0 S) ≡⟨ prop0 S ⟩
+--            true ∎  where open ≡-Reasoning
+--         b=t : B [] ≡ true
+--         b=t = begin
+--            B [] ≡⟨ cong (λ k → B k) (sym (proj2 (list-empty++ (sp0 S) (sp1 S) (sp-concat S))))  ⟩
+--            B (sp1 S) ≡⟨ prop1 S ⟩
+--            true ∎  where open ≡-Reasoning
+-- plit→AB1 {Σ} A B (h ∷ t ) S = begin
+--      split A B (h ∷ t ) ≡⟨⟩
+--      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t ≡⟨ cong (λ k → A [] /\ B (h ∷ t) \/ k ) 
+--         (split→AB1 {Σ} (λ t1 → A (h ∷ t1)) B t ? ) ⟩
+--      A [] /\ B (h ∷ t) \/ true ≡⟨ bool-or-3 ⟩
+--      true ∎  where open ≡-Reasoning
+-- 
+