Mercurial > hg > Members > kono > Proof > automaton

changeset 48:68e5f56cf01f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix coinduction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Apr 2019 08:35:29 +0900
parents dfc2f65b07ea
children 4135d56b8120
files agda/flcagl.agda
diffstat 1 files changed, 11 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/agda/flcagl.agda	Sat Apr 06 01:33:16 2019 +0900
+++ b/agda/flcagl.agda	Sat Apr 06 08:35:29 2019 +0900
@@ -147,11 +147,6 @@
         ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q)
         ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)
 
-        -- union-union-distr : ∀{i} (k {l m} : Lang ∞) → ( ( k ∪ l ) ∪ m ) ≅⟨ i ⟩≅ ( ( k ∪ m ) ∪ ( l ∪ m ) )
-        -- ≅ν (union-union-distr k) = {!!}
-        -- ≅δ (union-union-distr k) 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
@@ -167,19 +162,17 @@
         infix 5 _≅⟨_⟩≅_
         postulate
                 concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
-
-        union-swap24 : {!!}
-        union-swap24 = {!!}
+                union-swap24 :   ∀{i} (k {l m} : Lang ∞) (a : A ) →  (δ k a · l ∪ δ k a · m) ∪ δ l a ∪ δ m a
+                     ≅⟨ i ⟩≅ ((δ k a · l ∪ δ l a) ∪ δ k a · m ∪ δ m a)
 
         concat-union-distribr : ∀{i} (k {l m} : Lang ∞) → k · ( l ∪ m ) ≅⟨ i ⟩≅ ( k · l ) ∪ ( k · m )
-        ≅ν (concat-union-distribr k) =  {!!} -- ∧-distribʳ-∨ (ν k) _ _ 
+        ≅ν (concat-union-distribr k) =  ∧-distribˡ-∨ (ν k) _ _ 
         ≅δ (concat-union-distribr k) a with ν k
         ≅δ (concat-union-distribr k {l} {m}) a | true = begin
               δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a)
-           -- ≈⟨ union-cong (concat-union-distribr (δ k a)) ⟩
-           ≈⟨ {!!} ⟩
+           ≈⟨ union-cong (concat-union-distribr (δ k a)) ≅refl ⟩
               (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
-           ≈⟨ {!!} ⟩
+           ≈⟨ union-swap24 k a  ⟩
               (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
            ∎
                where open EqR (Bis _)
@@ -211,9 +204,8 @@
         ≅ν (star-idem l) = refl
         ≅δ (star-idem l) a = begin
                   δ ((l *) *) a  ≈⟨ concat-assoc (δ l a)  ⟩
-                  δ l a · (l *) · ((l *) *) ≈⟨ {!!}  ⟩
-                  δ l a · l * · l * ≈⟨ {!!}  ⟩
-                  δ l a · ((l *) *) ≈⟨ concat-congr (star-idem l) ⟩
+                  δ l a · ((l *) · ((l *) *)) ≈⟨ concat-congr ( concat-congr (star-idem l )) ⟩
+                  δ l a · ((l *) · (l *)) ≈⟨  concat-congr (star-concat-idem l ) ⟩
                   δ l a · l *
                 ∎ where open EqR (Bis _)
 
@@ -322,9 +314,10 @@
        lang (composeA da1 s2 da2) (δ da1 s1 a , δ da2 s2 a ∷ δs da2 ss a)
    ≈⟨ composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 (s2 ∷ ss) a) ⟩
        lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang (powA da2) (δs da2 (s2 ∷ ss) a)
-   ≈⟨ {!!} ⟩ 
-      (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a))
-   ≈⟨ ≅sym {!!} ⟩
+   ≈⟨ union-cong ≅refl  (powA-cons da2)  ⟩ 
+       lang da1 (δ da1 s1 a) · lang da2 s2 ∪
+          (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a))
+   ≈⟨ ≅sym  (union-assoc _)  ⟩
        (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a)
    ∎ where open EqR (Bis _)