Mercurial > hg > Members > kono > Proof > automaton

changeset 49:4135d56b8120

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 06 Apr 2019 21:06:02 +0900
parents 68e5f56cf01f
children 62ad890b6cc7
files agda/flcagl.agda
diffstat 1 files changed, 77 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/agda/flcagl.agda	Sat Apr 06 08:35:29 2019 +0900
+++ b/agda/flcagl.agda	Sat Apr 06 21:06:02 2019 +0900
@@ -143,7 +143,7 @@
         ≅δ union-emptyl a = union-emptyl
 
         union-cong : ∀{i}{k k′ l l′ : Lang ∞}
-             (p : k ≅⟨ i ⟩≅ k′)(q : l ≅⟨ i ⟩≅ l′ ) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l′ )
+             (p : k ≅⟨ i ⟩≅ k′) (q : l ≅⟨ i ⟩≅ l′ ) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l′ )
         ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q)
         ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)
 
@@ -162,39 +162,103 @@
         infix 5 _≅⟨_⟩≅_
         postulate
                 concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
-                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)
+
+        union-congl : ∀{i}{k k′ l : Lang ∞}
+             (p : k ≅⟨ i ⟩≅ k′) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l )
+        union-congl eq = union-cong eq ≅refl
+
+        union-congr : ∀{i}{k l l′ : Lang ∞}
+             (p : l ≅⟨ i ⟩≅ l′) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k ∪ l′ )
+        union-congr eq = union-cong ≅refl eq
+
+        union-swap24 :   ∀{i} ({x y z w} : Lang ∞)  →  (x ∪ y) ∪ z ∪  w
+                                              ≅⟨ i ⟩≅ (x ∪ z) ∪ y ∪ w
+        union-swap24 {_} {x} {y} {z} {w} = begin
+              (x ∪ y) ∪ z ∪ w
+           ≈⟨ union-assoc x ⟩
+               x ∪ y ∪ z ∪ w
+           ≈⟨ union-congr (≅sym ( union-assoc y)) ⟩
+              x ∪ ((y ∪ z) ∪ w)
+           ≈⟨ ≅sym ( union-assoc x ) ⟩
+              (x ∪ ( y ∪ z)) ∪ w
+           ≈⟨ union-congl (union-congr (union-comm y z )) ⟩
+              ( x ∪ (z ∪ y)) ∪ w
+           ≈⟨  union-congl (≅sym ( union-assoc x )) ⟩
+              ((x ∪ z) ∪ y) ∪ w
+           ≈⟨ union-assoc (x ∪ z) ⟩
+              (x ∪ z) ∪ y ∪ w
+           ∎
+               where open EqR (Bis _)
 
         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) 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)) ≅refl ⟩
+           ≈⟨ union-congl (concat-union-distribr (δ k a)) ⟩
               (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
-           ≈⟨ union-swap24 k a  ⟩
+           ≈⟨ union-swap24 ⟩
               (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
            ∎
                where open EqR (Bis _)
         ≅δ (concat-union-distribr k) a | false = concat-union-distribr (δ k a)
 
         postulate
-                concat-congl : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → l · m ≅⟨ i ⟩≅ k · m
-                concat-congr : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → m · l ≅⟨ i ⟩≅ m · k
-                concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m)
                 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅
                 concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅
                 concat-unitl : ∀{i} l → ε · l ≅⟨ i ⟩≅ l
                 concat-unitr : ∀{i} l → l · ε ≅⟨ i ⟩≅ l
                 star-empty : ∀{i} → ∅ * ≅⟨ i ⟩≅ ε
 
+        concat-congl : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → l · m ≅⟨ i ⟩≅ k · m
+        ≅ν (concat-congl {i} {m} p ) =  cong (λ x →  x ∧  ( ν m ))  ( ≅ν p )
+        ≅δ (concat-congl {i} {m} {l} {k} p ) a with ν k | ν l | ≅ν p
+        ≅δ (concat-congl {i} {m} {l} {k} p) a | false | false | refl = concat-congl (≅δ p a)
+        ≅δ (concat-congl {i} {m} {l} {k} p) a | true | true | refl = union-congl (concat-congl (≅δ p a)) 
+
+        concat-congr : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → m · l ≅⟨ i ⟩≅ m · k
+        ≅ν (concat-congr {i} {m} {_} {k} p ) =  cong (λ x →  ( ν m ) ∧ x )  ( ≅ν p )
+        ≅δ (concat-congr {i} {m} {l} {k} p ) a with ν m | ν k | ν l | ≅ν p
+        ≅δ (concat-congr {i} {m} {l} {k} p) a | false | x | .x | refl = concat-congr p
+        ≅δ (concat-congr {i} {m} {l} {k} p) a | true | x | .x | refl = union-cong (concat-congr p ) ( ≅δ p a )
+
+        concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m)
+        ≅ν (concat-assoc {i} k {l} {m} ) =  ∧-assoc ( ν k ) ( ν l ) ( ν m )
+        ≅δ (concat-assoc {i} k {l} {m} ) a with  ν k 
+        ≅δ (concat-assoc {i} k {l} {m}) a | false  = concat-assoc (δ k a)
+        ≅δ (concat-assoc {i} k {l} {m}) a | true  with ν l
+        ≅δ (concat-assoc {i} k {l} {m}) a | true | false =  begin
+             ( if false then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m )
+          ≈⟨ ≅refl  ⟩
+            (δ k a · l ∪ δ l a) · m
+          ≈⟨ concat-union-distribl (δ k a · l) ⟩
+            ((δ k a · l) · m ) ∪ ( δ l a · m )
+          ≈⟨ union-congl (concat-assoc (δ k a)) ⟩
+             (δ k a · l · m ) ∪ ( δ l a · m )
+          ≈⟨ ≅refl  ⟩
+             δ k a · l · m ∪ (if false then δ l a · m ∪ δ m a else δ l a · m)
+           ∎ where open EqR (Bis _)
+        ≅δ (concat-assoc {i} k {l} {m}) a | true | true = begin
+             (if true then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m)
+          ≈⟨ ≅refl  ⟩
+             ((( δ k a · l ) ∪ δ l a) · m ) ∪ δ m a
+          ≈⟨ union-congl (concat-union-distribl (δ k a · l)   ) ⟩
+             ((δ k a · l) · m   ∪ ( δ l a · m )) ∪ δ m a
+          ≈⟨  union-congl (  union-congl (concat-assoc (δ k a)))   ⟩
+             (( δ k a · l · m ) ∪ ( δ l a · m )) ∪ δ m a 
+          ≈⟨ union-assoc ( δ k a  · l · m ) ⟩
+             ( δ k a · l · m ) ∪ ( ( δ l a · m ) ∪ δ m a )
+          ≈⟨ ≅refl  ⟩
+             δ k a · l · m ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)
+           ∎ where open EqR (Bis _)
+
         star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
         ≅ν (star-concat-idem l) = refl
         ≅δ (star-concat-idem l) a = begin
                δ ((l *) · (l *)) a
-           ≈⟨ union-cong (concat-assoc _) ≅refl ⟩
+           ≈⟨ union-congl (concat-assoc _) ⟩
                δ l a · (l * · l *) ∪ δ l a · l *
-           ≈⟨ union-cong (concat-congr (star-concat-idem _)) ≅refl ⟩
+           ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
                δ l a · l * ∪ δ l a · l *
            ≈⟨ union-idem _ ⟩
                δ (l *) a
@@ -223,9 +287,9 @@
                    (δ l a)
                 ≈⟨ q ⟩
                    δ k a · l ∪ δ m a
-                ≈⟨ union-cong (concat-congr (star-from-rec k {l} {m} n p)) ≅refl  ⟩
+                ≈⟨ union-congl (concat-congr (star-from-rec k {l} {m} n p))  ⟩
                    (δ k a · (k * · m) ∪ δ m a)
-                ≈⟨ union-cong (≅sym (concat-assoc (δ k a))) ≅refl ⟩
+                ≈⟨ union-congl (≅sym (concat-assoc (δ k a))) ⟩
                     (δ k a · (k *)) · m ∪ δ m a
                 ∎ where open EqR (Bis _)
 
@@ -314,7 +378,7 @@
        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)
-   ≈⟨ union-cong ≅refl  (powA-cons da2)  ⟩ 
+   ≈⟨ union-congr (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 _)  ⟩