Mercurial > hg > Members > kono > Proof > automaton

changeset 73:031e00cea8f1

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 Thu, 07 Nov 2019 11:36:23 +0900
parents c75aee1d6b4b
children 762d5a6fbe09
files agda/logic.agda agda/regular-language.agda
diffstat 2 files changed, 38 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/agda/logic.agda	Thu Nov 07 10:55:22 2019 +0900
+++ b/agda/logic.agda	Thu Nov 07 11:36:23 2019 +0900
@@ -83,3 +83,23 @@
 bool-≡-? true false = no (λ ())
 bool-≡-? false true = no (λ ())
 bool-≡-? false false = yes refl
+
+¬-bool-t : {a : Bool} →  ¬ ( a ≡ true ) → a ≡ false
+¬-bool-t {true} ne = ⊥-elim ( ne refl )
+¬-bool-t {false} ne = refl
+
+¬-bool-f : {a : Bool} →  ¬ ( a ≡ false ) → a ≡ true
+¬-bool-f {true} ne = refl
+¬-bool-f {false} ne = ⊥-elim ( ne refl )
+
+lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
+lemma-∧-0 {true} {true} refl ()
+lemma-∧-0 {true} {false} ()
+lemma-∧-0 {false} {true} ()
+lemma-∧-0 {false} {false} ()
+
+lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
+lemma-∧-1 {true} {true} refl ()
+lemma-∧-1 {true} {false} ()
+lemma-∧-1 {false} {true} ()
+lemma-∧-1 {false} {false} ()
--- a/agda/regular-language.agda	Thu Nov 07 10:55:22 2019 +0900
+++ b/agda/regular-language.agda	Thu Nov 07 11:36:23 2019 +0900
@@ -60,12 +60,15 @@
 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
 isRegular A x r = A x ≡ contain r x 
 
+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 Σ
 M-Union {Σ} A B = record {
        states =  states A × states B
      ; astart = ( astart A , astart B )
-     ; aℕ = {!!}
-     ; afin = {!!}
+     ; aℕ = aℕ A * aℕ B
+     ; afin = fin-× (afin A) (afin 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) )
@@ -103,37 +106,9 @@
 open import Data.Nat.Properties
 open import Relation.Binary as B hiding (Decidable)
 
-fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
-fin-∨ {A} {B} {c} {b} fa fb = record {
-              Q←F = f0
-            ; F←Q = f1
-            ; finiso→ = f2
-            ; finiso← = f3
-   } where
-        f0 : Fin (c + b) → A ∨ B
-        f0 x with <-cmp (toℕ x) c
-        f0 x | tri< a ¬b ¬c = case1 ( Q←F fa (fromℕ≤ a ) )
-        f0 x | tri≈ ¬a b ¬c = case2 ( Q←F fb (fromℕ≤ {!!} ))
-        f0 x | tri> ¬a ¬b c = case2 ( Q←F fb (fromℕ≤ {!!} ))
-        f1 : A ∨ B → Fin (c + b)
-        f1 (case1 x) = inject+ b (F←Q fa x )
-        f1 (case2 x) = raise c (F←Q fb x )
-        f2 : (q : A ∨ B) → f0 (f1 q) ≡ q
-        f2 = {!!}
-        f3 : (f : Fin (c + b)) → f1 (f0 f) ≡ f
-        f3 = {!!}
-
-fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
-fin→ {A} {a} fa = record {
-              Q←F = f0
-            ; F←Q = {!!}
-            ; finiso→ = {!!}
-            ; finiso← = {!!}
-      } where
-          f0 : Fin (exp 2 a) → A → Bool
-          f0 = {!!}
-          f1 : (A → Bool) → Fin (exp 2 a)
-          f1 = {!!}
+postulate 
+   fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
+   fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
 
 Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 
 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend } where
@@ -189,22 +164,6 @@
 list-empty++ [] (x ∷ y) ()
 list-empty++ (x ∷ x₁) y ()
 
-split-next :  {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (h : Σ) (t :  List Σ ) → Split A B (h ∷ t)
-   → ( (A [] ≡ true ) ∧ (B (h ∷ t) ≡ true) ) ∨ Split (λ t1 → A ( h ∷ t1 )) (λ t2 → B t2) t 
-split-next A B h t S with bool-≡-? (A []) true  | bool-≡-? (B (h ∷ t)) true
-split-next A B h t S | yes eqa | yes eqb = case1 (record { proj1 = eqa ; proj2 = eqb })
-split-next A B h t S | yes p | no ¬p with sp0 S
-split-next A B h t S | yes p | no ¬p | [] = {!!} -- ⊥-elim ( ¬p (prop1 S))
-split-next {Σ} A B h t S | yes p | no ¬p | x ∷ tt =
-  case2 record { sp0 = tt ; sp1 = sp1 S ; sp-concat = lemma7 {!!} ; prop0 = lemma8 {!!} ; prop1 = prop1 S } where
-    lemma6 : {ss tt t : List Σ} {h : Σ} → (h ∷ tt ) ++ ss ≡ h ∷ t → tt ++ ss ≡ t
-    lemma6 refl = refl
-    lemma7 : (h ∷ tt ) ++ sp1 S ≡ h ∷ t → tt ++ sp1 S ≡ t
-    lemma7 eq = lemma6 {sp1 S} eq
-    lemma8 :  sp0 S ≡ h ∷ tt → A (h ∷ tt) ≡ true
-    lemma8 refl = prop0 S
-split-next A B h t S | no ¬p | eqb = {!!}
-
 open _∧_
 
 split-logic : {Σ : Set} → (A : List Σ → Bool )
@@ -230,11 +189,20 @@
     lemma4 S | x ∷ tt = NS record { sp0 = [] ; sp1 = t ; sp-concat = refl ; prop0 = {!!} ; prop1 = {!!} }
 ... | _ | no ne = no {!!}
 
+c-split :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → Concat (contain A) (contain B) x ≡ true → Split (contain A) (contain B) x
+c-split {Σ} A B [] eq with bool-≡-? (contain A []) true | bool-≡-? (contain B []) true 
+c-split {Σ} A B [] eq | yes eqa | yes eqb = 
+    record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
+c-split {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
+c-split {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
+c-split {Σ} A B (h ∷ t ) eq = {!!}
 
 closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
 closed-in-concat A B x = ≡-Bool-func lemma3 lemma4 where
     lemma3 : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
-    lemma3 = {!!}
+    lemma3 concat with split-logic (contain A) (contain B) x
+    lemma3 concat | yes p = {!!}
+    lemma3 concat | no ¬p = ⊥-elim ( ¬p {!!} )
     lemma4 : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
     lemma4 = {!!}