Mercurial > hg > Members > kono > Proof > automaton

changeset 302:55f8031e4214

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 10:36:52 +0900
parents 30033f273f1d
children 5261402429f9
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 25 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Fri Dec 31 23:06:08 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sat Jan 01 10:36:52 2022 +0900
@@ -105,7 +105,7 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q qd : Q ) (is : List Σ)  : Set where
+record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
     field
        y z : List Σ
        yz=is : y ++ z ≡ is 
@@ -128,36 +128,42 @@
 make-TA {Q} {Σ} fa 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 q qd is
+       → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
    tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
    ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl
         ; trace-z  = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
    ... | false | record { eq = eq } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
        ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
-            ta : TA1 fa (δ fa q i) qd is
+            ta : TA1 fa finq (δ fa q i) qd is
             ta = tra-phase2 (δ fa q i) is tr p 
    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)
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
-           ; trace-xyyz = tnext q ( tra-02 (TA1.y ta) (δ fa q i) (sym (equal→refl finq eq)) {!!} {!!} {!!} ) } where
-              -- Trace fa ([] ++ (i ∷ TA1.y ta) ++ (i ∷ TA1.y ta) ++ TA1.z ta) q
-              -- tra-02 (i ∷  TA1.y ta) q (sym (equal→refl finq eq)) (tnext q (TA1.trace-yz ta)) {!!} {!!} } where
-        ta : TA1 fa (δ fa q i ) qd is
+           ; trace-xyyz = tnext q {!!} } where
+        ta : TA1 fa finq (δ fa q i ) qd is
         ta = tra-phase2 (δ fa q i ) is tr p 
-        tra-02 : (y1 : List Σ) → (q0 : Q) → q ≡ qd  → (tr : Trace fa (y1 ++ TA1.z ta) q0)
-            → phase2 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ true
-            → phase1 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ false
-            → Trace fa (y1 ++ i ∷ TA1.y ta ++ TA1.z ta) q0
-        tra-02 [] q0 q=qd tr p np with equal? finq qd q0 | inspect ( equal? finq qd) q0
-        ... | true  | record { eq = eq } = subst (λ k →  Trace fa (i ∷ TA1.y ta ++ TA1.z ta) k  ) {!!} (tnext q (TA1.trace-yz ta)  ) where
-            tra-03 : q ≡ q0 
-            tra-03 = trans q=qd ((equal→refl finq eq) )
-        ... | false | record { eq = ne } = {!!}
-        tra-02 (y1 ∷ ys) q0 q=qd (tnext q tr) p np with equal? finq qd q | inspect ( equal? finq qd) q
-        ... | true  | record { eq = eq } = {!!}
-        ... | false | record { eq = ne } = {!!} -- tnext q (tra-02 ys (δ fa q y1) q=qd tr p np )
+        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 = {!!} 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)
             ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
         ta : TA fa (δ fa q i ) is