Mercurial > hg > Members > kono > Proof > automaton

changeset 299:841f4064e515

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 Fri, 31 Dec 2021 17:27:58 +0900
parents 1b5c09f12373
children 67d8e42b7782
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 34 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Fri Dec 31 17:02:31 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Dec 31 17:27:58 2021 +0900
@@ -105,61 +105,64 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (phase : ℕ)  ( q qd : Q ) (is : List Σ)  : Set where
+record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
+    field
+       y z : List Σ
+       yz=is : y ++ z ≡ is 
+       trace-z    : Trace fa z  q
+       trace-yz   : Trace fa (y ++ z)  q
+
+record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
     field
        x y z : List Σ
        xyz=is : x ++ y ++ z ≡ is 
-       trace-z    : phase > 1 → Trace fa z  qd
-       trace-yz   : phase > 0 → Trace fa (y ++ z)  qd
-       trace-xyz  : phase ≡ 0 → Trace fa (x ++ y ++ z)  q
-       trace-xyyz : phase ≡ 0 → Trace fa (x ++ y ++ y ++ z) q
+       trace-xyz  : Trace fa (x ++ y ++ z)  q
+       trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
 
 open import nat
 
 make-TA : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (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 0 q qd is
+     → TA fa q is
 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  → TA fa 1 q qd is
+   tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase2 finq qd (tr→qs fa is q tr) ≡ true  → TA1 fa q is
    tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
    ... | true | record { eq = eq } = {!!} 
    ... | false | record { eq = eq } = {!!} 
-   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa 0 q qd is
+   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 = y TA0 ;  z = z TA0 ; xyz=is = {!!} -- cong (i ∷_ ) 
-           ; trace-z = λ () ; trace-yz = λ _ → trace-yz TA0 a<sa 
-           ; trace-xyz  = λ _ → subst (λ k → Trace fa (y TA0 ++ z TA0) k ) (equal→refl finq eq) (trace-yz TA0 a<sa)
-           ; trace-xyyz = λ _ → subst (λ k → Trace fa (y TA0 ++ y TA0 ++ z TA0) k ) (equal→refl finq eq) (tra-02 (y TA0) qd (trace-yz TA0 a<sa) {!!} {!!}) } where
---  : phase2 finq qd (tr→qs fa (y TA0 ++ z TA0) qd (trace-yz TA0 a<sa))
+   ... | 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  = {!!}
+           ; trace-xyyz = {!!} } where
+--  : phase2 finq qd (tr→qs fa (y ta ++ z ta) qd (trace-yz ta a<sa))
 --    ≡ true
---  : phase1 finq qd (tr→qs fa (y TA0 ++ z TA0) qd (trace-yz TA0 a<sa))
+--  : phase1 finq qd (tr→qs fa (y ta ++ z ta) qd (trace-yz ta a<sa))
 --    ≡ false
-        TA0 : TA fa 1 (δ fa q i ) qd  is
-        TA0 = tra-phase2 (δ fa q i ) is tr p
-        tra-02 : (y1 : List Σ) → (q : Q) → (tr : Trace fa (y1 ++ z TA0) q)
-            → phase2 finq qd (tr→qs fa (y1 ++ z TA0) q tr) ≡ true
-            → phase1 finq qd (tr→qs fa (y1 ++ z TA0) q tr) ≡ false
-            → Trace fa (y1 ++ y TA0 ++ z TA0) q
+        ta : TA1 fa (δ fa q i ) is
+        ta = tra-phase2 (δ fa q i ) is tr p
+        tra-02 : (y1 : List Σ) → (q : Q) → (tr : Trace fa (y1 ++ TA1.z ta) q)
+            → phase2 finq qd (tr→qs fa (y1 ++ TA1.z ta) q tr) ≡ true
+            → phase1 finq qd (tr→qs fa (y1 ++ TA1.z ta) q tr) ≡ false
+            → Trace fa (y1 ++ TA1.y ta ++ TA1.z ta) q
         tra-02 [] q tr p np with equal? finq qd q | inspect ( equal? finq qd) q
-        ... | true  | record { eq = eq } = subst (λ k →  Trace fa (y TA0 ++ z TA0) k ) (equal→refl finq eq) (trace-yz TA0 a<sa )
+        ... | true  | record { eq = eq } = subst (λ k →  Trace fa (TA1.y ta ++ TA1.z ta) k ) (equal→refl finq eq) (TA1.trace-yz ta )
         ... | false | record { eq = ne } = {!!}
         tra-02 (y1 ∷ ys) q (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) tr p np )
-        tra-01 : (y1 : List Σ) → Trace fa (y1 ++ z TA0) qd → Trace fa (y1 ++ y TA0 ++ z TA0) qd
+        tra-01 : (y1 : List Σ) → Trace fa (y1 ++ TA1.z ta) qd → Trace fa (y1 ++ TA1.y ta ++ TA1.z ta) qd
         tra-01 = {!!}
-   ... | true | record { eq = eq } | true | record { eq = np} = record { x = i ∷ x TA0 ; y = y TA0 ; z = z TA0 ; xyz=is = cong (i ∷_ ) (xyz=is TA0)
-            ; trace-z = λ () ; trace-yz = λ ()
-            ; trace-xyz = λ _ → tnext q (trace-xyz TA0 refl ) ; trace-xyyz = λ _ → tnext q (trace-xyyz TA0 refl )} where
-        TA0 : TA fa 0 (δ fa q i ) qd  is
-        TA0 = tra-phase1 (δ fa q i ) is tr np
-   ... | false | _ | _ | _ = record { x = i ∷ x TA0 ; y = y TA0 ; z = z TA0 ; xyz=is = cong (i ∷_ ) (xyz=is TA0) ; trace-z = λ () ; trace-yz = λ ()
-            ; trace-xyz = λ _ → tnext q (trace-xyz TA0 refl ) ; trace-xyyz = λ _ → tnext q (trace-xyyz TA0 refl )} where
-        TA0 : TA fa 0 (δ fa q i ) qd  is
-        TA0 = tra-phase1 (δ fa q i ) is tr p
+   ... | 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
+        ta = tra-phase1 (δ fa q i ) is tr np
+   ... | false | _ | _ | _ = 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
+        ta = tra-phase1 (δ fa q i ) is tr p
 
 open RegularLanguage
 open import Data.Nat.Properties