Mercurial > hg > Members > kono > Proof > automaton

changeset 305:5ef7ad34a05f

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 Sat, 01 Jan 2022 18:52:42 +0900
parents b0a88e024188
children fadb41538406
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 19 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Sat Jan 01 12:27:39 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sat Jan 01 18:52:42 2022 +0900
@@ -112,6 +112,12 @@
        trace-z    : Trace fa z  qd
        trace-yz   : Trace fa (y ++ z)  q
 
+record TA2 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (y1 is : List Σ)  : Set where
+    field
+       y z : List Σ
+       yz=is : y ++ z ≡ is 
+       trace-yyz   : Trace fa (y ++ y1 ++ z)  q
+
 record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
     field
        x y z : List Σ
@@ -122,11 +128,11 @@
 
 open import nat
 
-make-TA : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
+make-TA : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (fins : FiniteSet Σ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
      → (tr : Trace fa is q )
      → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
      → TA fa q is
-make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
+make-TA {Q} {Σ} fa fins finq q qd is tr dup = tra-phase1 q is tr dup where
    open TA
    tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q )
        → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
@@ -137,36 +143,24 @@
        ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
             ta : TA1 fa finq (δ fa q i) qd is
             ta = tra-phase2 (δ fa q i) is tr p 
+   tra-phase3 : (i : Σ) → (y1 z1 : List Σ)  → (tr : Trace fa (y1 ++ i ∷ z1)  (δ fa qd i) ) 
+       → phase1 finq qd (tr→qs fa (y1 ++ i ∷ z1)  (δ fa qd i) tr) ≡ false 
+       → phase1 finq qd (tr→qs fa (i ∷ y1 ++ i ∷ z1) qd (tnext qd tr)) ≡ true → TA2 fa finq q qd (i ∷ y1) (i ∷ y1 ++ i ∷ z1)
+   tra-phase3 i y1 z1 tr1 p = {!!} where
+       tra-phase4 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is q ) 
+          → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA2 fa finq q qd (i ∷ y1) is
+       tra-phase4 q (j ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
+          | phase1 finq qd (tr→qs fa is (δ fa q j) tr) | inspect ( phase1 finq qd)  (tr→qs fa is (δ fa q j) tr) 
+       ... | t1 | t2 | t3 | t4 = {!!}
    tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q is
    tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
           | phase1 finq qd (tr→qs fa is (δ fa q i) tr) | inspect ( phase1 finq qd)  (tr→qs fa is (δ fa q i) tr) 
    ... | true | record { eq = eq } | false | record { eq = np} = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
            ; non-nil-y = λ ()
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
-           ; trace-xyyz = tra-02 (i ∷ TA1.y ta) (TA1.z ta) q
-                    (tnext q (TA1.trace-yz ta)) (subst (λ k → Trace fa (TA1.z ta)  k) {!!} (TA1.trace-z ta)) {!!} {!!}  } where
+           ; trace-xyyz = {!!} } where 
         ta : TA1 fa finq (δ fa q i ) qd is
         ta = tra-phase2 (δ fa q i ) is tr p 
-        tra-02 : (y1 z1 : List Σ) → (qd : Q) → (tr : Trace fa (y1 ++ z1) qd) → (trz : Trace fa z1 qd)
-            → phase2 finq qd (tr→qs fa (y1 ++ z1) qd tr) ≡ true
-            → phase1 finq qd (tr→qs fa (y1 ++ z1) qd tr) ≡ false
-            → Trace fa (y1 ++ y1 ++ z1) qd
-        tra-02 [] z1 qd tryz trz p1 np1 = trz
-        tra-02 (i ∷ y1) z1 qd (tnext q tr) trz p1 np1 = tnext q (tra-04 y1 (δ fa q i) tr {!!} ( qd ∷ tr→qs fa (y1 ++ z1) (δ fa qd i) tr) {!!} np1 p1 )  where
-           tryz = tnext q tr 
-           tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
-               → (qs zqs : List Q)
-               → tr→qs fa (y2 ++ z1) q tr ≡ qs ++ zqs
-               → phase1 finq qd (qs ++ zqs)  ≡ false   -- no two qd
-               → phase2 finq qd zqs ≡ true             -- at least one od
-               → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
-           tra-04 [] q tr qs zqs eq p2 np2 with equal? finq qd q | inspect (equal? finq qd) q
-           ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
-           ... | false | record { eq = ne } = {!!} -- qs ≡ [] → ⊥
-           tra-04 (y0 ∷ y2) q (tnext q tr) [] (q' ∷ zqs) eq p2 np2 = {!!}
-           tra-04 (y0 ∷ y2) q (tnext q tr) (q' ∷ qs) zqs eq p2 np2 with equal? finq qd q | inspect (equal? finq qd) q
-           ... | true | record { eq = eq } = {!!}  -- y2 + z1 contains two qd
-           ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qs zqs {!!} {!!} np2 )
    ... | true | record { eq = eq } | true | record { eq = np} = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta)
            ; non-nil-y = non-nil-y ta
             ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
@@ -221,7 +215,7 @@
     nn06 : Dup-in-list ( afin r) nntrace
     nn06 = dup-in-list>n (afin r) nntrace nn05
     TAnn : TA (automaton r) (astart r) nn
-    TAnn = make-TA (automaton r) (afin r) (astart r) {!!} nn {!!} {!!}
+    TAnn = make-TA (automaton r) {!!} (afin r) (astart r) {!!} nn {!!} {!!}
     count : In2 → List In2 → ℕ
     count _ [] = 0
     count i0 (i0 ∷ s) = suc (count i0 s)