Mercurial > hg > Members > kono > Proof > automaton

changeset 71:5cf460a98937

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 00:17:16 +0900
parents 702ce92c45ab
children c75aee1d6b4b
files agda/logic.agda agda/regular-language.agda
diffstat 2 files changed, 24 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/agda/logic.agda	Wed Nov 06 23:19:53 2019 +0900
+++ b/agda/logic.agda	Thu Nov 07 00:17:16 2019 +0900
@@ -67,3 +67,14 @@
 
 infixr  130 _\/_
 infixr  140 _/\_
+
+open import Relation.Binary.PropositionalEquality
+
+≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
+≡-Bool-func {true} {true} a→b b→a = refl
+≡-Bool-func {false} {true} a→b b→a with b→a refl
+... | ()
+≡-Bool-func {true} {false} a→b b→a with a→b refl
+... | ()
+≡-Bool-func {false} {false} a→b b→a = refl
+
--- a/agda/regular-language.agda	Wed Nov 06 23:19:53 2019 +0900
+++ b/agda/regular-language.agda	Thu Nov 07 00:17:16 2019 +0900
@@ -173,8 +173,17 @@
     lemma2 [] q qab aA = {!!}
     lemma2 (h ∷ t ) q qab aA  = lemma2 t {!!} {!!} {!!}
 
--- 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 with  split {!!} {!!} x
--- closed-in-concat A B x | true = {!!}
--- closed-in-concat A B x | false = {!!}
+split-logic : {Σ : Set} → (A : List Σ → Set )
+      → ( B : List Σ → Set ) → (x :  List Σ ) → Set
+split-logic A B [] = A [] ∧ B []
+split-logic A B (h ∷ t ) = ( A [] ∧ B ( h ∷ t ) ) ∨ split-logic ( λ t1 → A ( h ∷ t1 )) ( λ t2 → B t2 ) t
+
 
+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 = {!!}
+    lemma4 : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
+    lemma4 = {!!}
+
+