Mercurial > hg > Members > kono > Proof > automaton

changeset 74:762d5a6fbe09

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 13:16:03 +0900
parents 031e00cea8f1
children c10a8347581a
files agda/logic.agda agda/regular-language.agda
diffstat 2 files changed, 91 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/agda/logic.agda	Thu Nov 07 11:36:23 2019 +0900
+++ b/agda/logic.agda	Thu Nov 07 13:16:03 2019 +0900
@@ -103,3 +103,22 @@
 lemma-∧-1 {true} {false} ()
 lemma-∧-1 {false} {true} ()
 lemma-∧-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-and-1 : {a b : Bool} →  a ≡ false → (a /\ b ) ≡ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} →  b ≡ false → (a /\ b ) ≡ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+
--- a/agda/regular-language.agda	Thu Nov 07 11:36:23 2019 +0900
+++ b/agda/regular-language.agda	Thu Nov 07 13:16:03 2019 +0900
@@ -166,44 +166,87 @@
 
 open _∧_
 
-split-logic : {Σ : Set} → (A : List Σ → Bool )
-      → ( B : List Σ → Bool ) → (x :  List Σ ) → Dec (Split A B x)
-split-logic A B [] with bool-≡-? (A []) true  | bool-≡-? (B []) true 
-... | yes eqa | yes eqb  = yes record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
-... | no ne  | _ = no lemma0 where
-    lemma0 : Split A B [] → ⊥
-    lemma0 S with proj1 (list-empty++ (Split.sp0 S)(Split.sp1 S) (Split.sp-concat S))
-    lemma0 S | refl = ne ( Split.prop0 S )
-... | _ | no ne  = no lemma3 where
-    lemma3 : Split A B [] → ⊥
-    lemma3 S with proj2 (list-empty++ (Split.sp0 S)(Split.sp1 S) (Split.sp-concat S))
-    lemma3 S | refl = ne ( Split.prop1 S )
-split-logic A B (h ∷ t ) with split-logic (λ t1 → A (h ∷ t1)) (λ t2 → B t2) t
-... | yes S = yes record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ t → h ∷ t) (sp-concat S); prop0 = prop0 S ; prop1 = prop1 S }
-... | no NS with bool-≡-? (A []) true  | bool-≡-? (B (h ∷ t)) true 
-... | yes eqa | yes eqb = yes record { sp0 = [] ; sp1 = (h ∷ t) ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
-... | no ne | _ = no lemma4 where
-    lemma4 :  Split A B (h ∷ t ) → ⊥
-    lemma4 S with sp0 S
-    lemma4 S | [] = ne {!!}
-    lemma4 S | x ∷ tt = NS record { sp0 = [] ; sp1 = t ; sp-concat = refl ; prop0 = {!!} ; prop1 = {!!} }
-... | _ | no ne = no {!!}
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
 
-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-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
+   → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
+   → split (λ t1 → A (h ∷ t1)) B t ≡ true
+c-split-lemma {Σ} A B h t eq (case1 ¬p ) = sym ( begin
+      true
+  ≡⟨  sym eq  ⟩
+      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 ) (bool-and-1 (¬-bool-t ¬p)) ⟩
+      false \/ split (λ t1 → A (h ∷ t1)) B t
+  ≡⟨ bool-or-1 refl ⟩
+      split (λ t1 → A (h ∷ t1)) B t
+  ∎ ) where open ≡-Reasoning
+c-split-lemma {Σ} A B h t eq (case2 ¬p ) = sym ( begin
+      true
+  ≡⟨  sym eq  ⟩
+      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 ) (bool-and-2 (¬-bool-t ¬p)) ⟩
+      false \/ split (λ t1 → A (h ∷ t1)) B t
+  ≡⟨ bool-or-1 refl ⟩
+      split (λ t1 → A (h ∷ t1)) B t
+  ∎ ) where open ≡-Reasoning
+
+c-split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
+c-split {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (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 = {!!}
+c-split {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
+... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
+... | no px | _ with c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
+... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
+c-split {Σ} A B (h ∷ t ) eq  | _ | no px with c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
+... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
+
+split++ :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
+split++ {Σ} A B [] [] eqa eqb = begin
+       split A B [] 
+     ≡⟨⟩
+       A [] /\ B []
+     ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
+      true
+     ∎  where open ≡-Reasoning
+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 ∷ t) y eqa eqb = begin
+       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 ) ( begin
+          split (λ t1 → A (h ∷ t1)) B (t ++ y) 
+        ≡⟨ split++ {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩
+          true 
+        ∎ ) ⟩
+       A [] /\ B (h ∷ t ++ y) \/ true
+     ≡⟨ bool-or-3 ⟩
+      true
+     ∎  where open ≡-Reasoning
+
 
 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 concat with split-logic (contain A) (contain B) x
-    lemma3 concat | yes p = {!!}
-    lemma3 concat | no ¬p = ⊥-elim ( ¬p {!!} )
+    lemma3 concat with c-split (contain A) (contain B) x concat
+    ... | S = {!!}
     lemma4 : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
-    lemma4 = {!!}
+    lemma4 C = {!!} -- split++ (contain A) (contain B) x y (accept ?) (accept ?)