Mercurial > hg > Members > kono > Proof > automaton

changeset 47:dfc2f65b07ea

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 01:33:16 +0900
parents 964e4bd0272a
children 68e5f56cf01f
files agda/flcagl.agda
diffstat 1 files changed, 58 insertions(+), 95 deletions(-) [+]
line wrap: on
line diff
--- a/agda/flcagl.agda	Fri Apr 05 16:13:44 2019 +0900
+++ b/agda/flcagl.agda	Sat Apr 06 01:33:16 2019 +0900
@@ -162,105 +162,79 @@
             {g : A → A} (e : g x ≡ x) → P (g x)
         rewriteExample p e rewrite e = p
 
-        infixr 7 _∪_
+        infixr 6 _∪_
         infixr 7 _·_
         infix 5 _≅⟨_⟩≅_
-        concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
-        concat-union-distribl = {!!}
+        postulate
+                concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
 
         union-swap24 : {!!}
         union-swap24 = {!!}
 
         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)) ⟩
-           -- ≈⟨ ? ⟩
-           --     (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
+              δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a)
+           -- ≈⟨ union-cong (concat-union-distribr (δ k a)) ⟩
            ≈⟨ {!!} ⟩
-              {!!} -- (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
+              (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
+           ≈⟨ {!!} ⟩
+              (δ 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)
 
-        concat-congl : ∀{i} {m l k : Lang ∞}
-           → l ≅⟨ i ⟩≅ k
-           → l · m ≅⟨ i ⟩≅ k · m
-        concat-congl = {!!}
-        concat-congr : ∀{i} {m l k : Lang ∞}
-           → l ≅⟨ i ⟩≅ k
-            → m · l ≅⟨ i ⟩≅ m · k
-        concat-congr = {!!}
-
-
-        concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m)
-        concat-assoc = {!!}
-
-        concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅
-        concat-emptyl = {!!}
-        concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅
-        concat-emptyr = {!!}
-        concat-unitl : ∀{i} l → ε · l ≅⟨ i ⟩≅ l
-        concat-unitl = {!!}
-        concat-unitr : ∀{i} l → l · ε ≅⟨ i ⟩≅ l
-        concat-unitr = {!!}
-
-
-        star-empty : ∀{i} → ∅ * ≅⟨ i ⟩≅ ε
-        star-empty = {!!}
+        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 ⟩≅ ε
 
         star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
         ≅ν (star-concat-idem l) = refl
         ≅δ (star-concat-idem l) a = begin
-               {!!}
-           ≈⟨ {!!} ⟩
-               {!!}
-           --    δ l a · l * · l * ∪ δ l a · l *
-           -- ≈⟨ union-cong (concat-assoc _) ⟩
-           --≈⟨ ? ⟩
-           --    δ l a · (l * · l *) ∪ δ l a · l *
-           --≈⟨ ? ⟩
-           ---- ≈⟨ union-cong (concat-congr (star-concat-idem _)) ⟩
-           --    δ l a · l * ∪ δ l a · l *
-           --≈⟨ ? ⟩
-           ---- ≈⟨ union-idem _ ⟩
-           --    δ l a · l *
+               δ ((l *) · (l *)) a
+           ≈⟨ union-cong (concat-assoc _) ≅refl ⟩
+               δ l a · (l * · l *) ∪ δ l a · l *
+           ≈⟨ union-cong (concat-congr (star-concat-idem _)) ≅refl ⟩
+               δ l a · l * ∪ δ l a · l *
+           ≈⟨ union-idem _ ⟩
+               δ (l *) a
            ∎ where open EqR (Bis _)
 
         star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l *
         ≅ν (star-idem l) = refl
         ≅δ (star-idem l) a = begin
-                    {!!}
-                ≈⟨ {!!} ⟩
-                    {!!}
-                -- δ l a · l * · (l *) * ≈⟨ ? ⟩
-                -- δ l a · l * · l * ≈⟨ ? ⟩
-                -- δ l a · (l * · l *) ≈⟨ concat-congr (star-concat-idem l) ⟩
-                -- δ l a · l *
+                  δ ((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 *
                 ∎ where open EqR (Bis _)
 
-        star-rec : ∀{i} (l : Lang ∞) → l * ≅⟨ i ⟩≅ ε ∪ (l · l *)
-        star-rec = {!!}
+        postulate
+           star-rec : ∀{i} (l : Lang ∞) → l * ≅⟨ i ⟩≅ ε ∪ (l · l *)
 
         star-from-rec : ∀{i} (k {l m} : Lang ∞)
                 → ν k ≡ false
                 → l ≅⟨ i ⟩≅ k · l ∪ m
                 → l ≅⟨ i ⟩≅ k * · m
         ≅ν (star-from-rec k n p) with ≅ν p
-        ... | b rewrite n = {!!}
+        ... | b rewrite n = b
         ≅δ (star-from-rec k {l} {m} n p) a with ≅δ p a
         ... | q rewrite n = begin
                    (δ l a)
-                --≈⟨ q ⟩
-                --   δ k a · l ∪ δ m a
-                --≈⟨ union-cong (concat-congr (star-from-rec k {l} {m} n p)) ⟩
-                --   (δ k a · (k * · m) ∪ δ m a)
-                --≈⟨ union-cong (≅sym (concat-assoc (δ k a))) ⟩
-                --   (δ k a · k * · m ∪ δ m a)
-                ≈⟨ {!!} ⟩
-                  {!!}
+                ≈⟨ q ⟩
+                   δ k a · l ∪ δ m a
+                ≈⟨ union-cong (concat-congr (star-from-rec k {l} {m} n p)) ≅refl  ⟩
+                   (δ k a · (k * · m) ∪ δ m a)
+                ≈⟨ union-cong (≅sym (concat-assoc (δ k a))) ≅refl ⟩
+                    (δ k a · (k *)) · m ∪ δ m a
                 ∎ where open EqR (Bis _)
 
 
@@ -333,33 +307,30 @@
 ≅δ (powA-cons da) a = powA-cons da
 
 composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × List ∞ S2)
-ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ ν da2 {!!}
+ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ νs da2 ss2
 δ (composeA da1 s2 da2) (s1 , ss2) a =
-        δ da1 s1 a , {!!} -- δ da2 ? a -- (if ν da1 s1 then s2 ∷ ss2 else ss2) a
+        δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a
 
 import Relation.Binary.EqReasoning as EqR
 
 composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) →
         lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss
-≅ν (composeA-gen da1 da2 s1 s2 ss) = {!!}
+≅ν (composeA-gen da1 da2 s1 s2 ss) = refl
 ≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1
-... | false = {!!} -- composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 ss a)
+... | false = composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 ss a)
 ... | true = begin
-         {!!}
---       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 da1 (δ da1 s1 a) · lang da2 s2 ∪
---       (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a))
---   ≈⟨ ≅sym ? ⟩
---       (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a)
-   ≈⟨  {!!} ⟩
-        {!!}
+       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 {!!} ⟩
+       (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a)
    ∎ where open EqR (Bis _)
 
-composeA-correct : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) s1 s2 →
+postulate
+  composeA-correct : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) s1 s2 →
      lang (composeA da1 s2 da2) (s1 , []) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2
-composeA-correct = {!!}
 
 
 open import Data.Maybe
@@ -383,22 +354,14 @@
 starA s0 da = finalToInitial (acceptingInitial s0 da)
 
 
-acceptingInitial-just : ∀{i S} (s0 : S) (da : DA S) {s : S} →
+postulate
+ acceptingInitial-just : ∀{i S} (s0 : S) (da : DA S) {s : S} →
    lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s
-acceptingInitial-just = {!!}
-
-acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) →
+ acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) →
         lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0
-acceptingInitial-nothing = {!!}
-
-
-starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→
+ starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→
         lang (starA s0 da) ss ≅⟨ i ⟩≅ 
                 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) *
-starA-lemma = {!!}
-
+ starA-correct : ∀{i S} (da : DA S) (s0 : S) →
+   lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
 
-starA-correct : ∀{i S} (da : DA S) (s0 : S) →
-   lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
-starA-correct = {!!}
-