Mercurial > hg > Members > kono > Proof > automaton

changeset 295:99c2cbe6a862

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 Thu, 30 Dec 2021 17:42:44 +0900
parents 248711134141
children 2f113cac060b
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 65 insertions(+), 67 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Wed Dec 29 19:08:28 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Dec 30 17:42:44 2021 +0900
@@ -54,30 +54,41 @@
 
 open _∧_
 
-data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → ( List Q) → Set where
-    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] (q ∷ [])
-    tnext : {q : Q} → {i : Σ} { is : List Σ} {qs : List Q} 
-        → Trace fa is (δ fa q i  ∷ qs) → Trace fa (i ∷ is) ( q ∷ δ fa q i  ∷ qs ) 
+data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → Q → Set where
+    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] q
+    tnext : (q : Q) → {i : Σ} { is : List Σ} 
+        → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q 
 
 tr-len :  { Q : Set } { Σ : Set  }
     → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → ( length is ≡ length qs ) ∧ (suc (length is) ≡ length (trace fa q is ) )
-tr-len {Q} {Σ} fa .[] q .[] (tend x) = ⟪ refl , refl ⟫
-tr-len {Q} {Σ} fa (i ∷ is) q (q0 ∷ qs) (tnext t) = 
-      ⟪ cong suc (proj1 (tr-len {Q} {Σ} fa is q0 qs t)) , cong suc (proj2 (tr-len {Q} {Σ} fa is q0 qs t)) ⟫
+    → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is ) 
+tr-len {Q} {Σ} fa .[] q (tend x) = refl 
+tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t)
 
 tr-accept→ : { Q : Set } { Σ : Set  }
     → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → accept fa q is ≡ true
-tr-accept→ {Q} {Σ} fa [] q [] (tend x)  = x
-tr-accept→ {Q} {Σ} fa (i ∷ is) q (x ∷ qs) (tnext tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) qs tr
+    → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
+tr-accept→ {Q} {Σ} fa [] q (tend x)  = x
+tr-accept→ {Q} {Σ} fa (i ∷ is) q  (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr
 
 tr-accept← : { Q : Set } { Σ : Set  }
     → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is (trace fa q is)
+    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is q
 tr-accept← {Q} {Σ} fa [] q ac = tend ac
-tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext (tend ac )
-tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 
+tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac )
+tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 
+
+tr→qs : { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q) → Trace fa is q → List Q
+tr→qs fa [] q (tend x) = []
+tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr 
+
+tr→qs=is : { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡  length (tr→qs fa is q tr)
+tr→qs=is fa .[] q (tend x) = refl
+tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is  (δ fa q i) tr)
 
 open Data.Maybe
 
@@ -87,60 +98,49 @@
 
 tr-append1 : { Q : Set } { Σ : Set  }
     → (fa : Automaton Q  Σ )
-    → (i : Σ) → ( q : Q)  → (q0 : Q)
+    → (i : Σ) → ( q : Q)  
     → (is : List Σ)
-    →  head (trace fa q is) ≡ just ( δ fa q0 i )
-    → (tr : Trace fa is (trace fa q is) ) →  Trace fa (i ∷ is) (q0 ∷ (trace fa q is))
-tr-append1 fa i q q0 is hd tr with trace fa q is
-tr-append1 fa i q q0 is () tr | []
-... | q₁ ∷ qs = tr01 hd where
-      tr01 : just q₁ ≡ just (δ fa q0 i) → Trace fa (i ∷ is) (q0 ∷ q₁ ∷ qs)
-      tr01 refl = tnext tr
+    → Trace fa is ( δ fa q i )  →  Trace fa (i ∷ is) q
+tr-append1 fa i q is tr = tnext _ tr 
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) {is : List Σ} { qs : List Q } (tr : Trace fa is qs) : Set where
+record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )  ( q : Q ) (phase yeq : Bool)  : Set where
     field
-       x y z : List Σ
-       qx qy qz : List Q
-       non-nil-y : ¬ y ≡ []
-       trace0 : Trace fa (x ++ y ++ z) (qx ++ qy ++ qz) 
-       trace1 : Trace fa (x ++ y ++ y ++ z) (qx ++ qy ++ qy ++ qz) 
-       trace-eq : trace0 ≅ tr
+       x y y1 z : List Σ
+       px : phase ≡ true → x ≡ []
+       py : yeq ≡ true → y ≡ y1
+       trace0 : Trace fa (x ++ y ++ z)  q
+       trace1 : Trace fa (x ++ y ++ y1 ++ z) q
 
-tr-append : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q )
-     →  dup-in-list finq q qs ≡ true
-     →  (tr : Trace fa is qs ) → TA fa tr
-tr-append {Q} {Σ} fa finq q is qs dup tr = tra-phase1 qs is tr dup where
+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 q false true
+make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
    open TA
-   tra-phase3 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → {!!}
-        → (qy : List Q) → (iy : List Σ)  → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true → {!!}
-        → Trace fa (iy ++ is) (qy ++ qs)
-   tra-phase3 = {!!}
-   tra-phase2 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → phase2 finq q qs ≡ true
-        → (qy : List Q) → (iy : List Σ)  → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true
-        → TA fa tr
-   tra-phase2 (q0 ∷ []) is (tend x₁) p qy iy ty py = {!!}
-   tra-phase2 (q0 ∷ (q₁ ∷ qs)) (x ∷ is) (tnext tr) p qy iy ty py with equal? finq q q0
-   ... | true = {!!}
-   ... | false = {!!} where
-       tr1 : TA fa tr
-       tr1 = tra-phase2 (q₁ ∷ qs) is tr p qy iy ty py
-   tra-phase1 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → phase1 finq q qs ≡ true  → TA fa tr
-   tra-phase1 (q0 ∷ []) is (tend x₁) p = {!!}
-   tra-phase1 (q0 ∷ (q₁ ∷ qs)) (i ∷ is) (tnext tr) p with equal? finq q q0
-   ... | true = record { x = i ∷ x tr2 ; y = y tr2 ; z = z tr2
-          ; qx = q0 ∷ qx tr2 ; qy = qy tr2 ;qz = qz  tr2
-          ; trace0 = {!!}
-          ; trace1 = {!!}
-          ; non-nil-y = non-nil-y tr2 ; trace-eq = {!!} } where
-       tr2 : TA fa tr
-       tr2 = tra-phase2 (q₁ ∷ qs) is tr p (q₁ ∷ qs) is tr p
-       -- tr3 : Trace fa (x tr2 ++ y tr2 ++ z tr2) (qx tr2 ++ qy tr2 ++ qz tr2) →  Trace fa ((i ∷ x tr2) ++ y tr2 ++ z tr2)  (q0 ∷ qx tr2 ++ qy tr2 ++ qz tr2)
-       -- tr3 tr = tnext {!!}
-   ... | false = {!!} where
-       tr1 : TA fa tr
-       tr1 = tra-phase1 (q₁ ∷ qs) is tr p
+   tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase2 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q true false
+   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q
+   ... | true = {!!} -- record { px = λ _ → refl ; x = [] ; y = i ∷ y TA0 ; z = z TA0 ; trace0 = tnext q (trace0 TA0 ) ; trace1 = tnext q (trace1 TA0) } 
+   ... | false = record { px = λ _ → refl ; x = [] ; y = i ∷ y TA0 ; y1 = y1 TA0 ; z = z TA0 ; py = λ ()
+      ; trace0 = tnext q (subst (λ k → Trace fa k (δ fa q i) ) (tr-01 (px TA0 refl ) ) (trace0 TA0))
+      ; trace1 = tnext q (subst (λ k → Trace fa k (δ fa q i) ) (tr-02 (px TA0 refl )) (trace1 TA0))} where
+        TA0 : TA fa (δ fa q i ) true false
+        TA0 = tra-phase2 (δ fa q i ) is tr p
+        tr-01 : {x1 : List Σ} → x1 ≡ [] → x1 ++ y TA0 ++ z TA0 ≡ y TA0 ++ z TA0
+        tr-01 refl = refl 
+        tr-02 : {x1 : List Σ} → x1 ≡ [] → x1 ++ y TA0  ++ (y1 TA0) ++ z TA0 ≡ y TA0  ++ (y1 TA0) ++ z TA0
+        tr-02 refl = refl 
+   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q false true
+   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q
+   ... | true = record { px = λ () ; x = i ∷ x TA0 ; y = y TA0 ; y1 = y TA0 ; z = z TA0 ; py = λ _ → refl
+           ; trace0 = tnext q (trace0 TA0 ) ; trace1 = tnext q {!!} } where
+        TA0 : TA fa (δ fa q i ) true false
+        TA0 = tra-phase2 (δ fa q i ) is tr p
+   ... | false = record { px = λ () ; x = i ∷ x TA0 ; y = y TA0 ; y1 = y TA0 ; z = z TA0 ; py = λ _ → refl ; trace0 = tnext q (trace0 TA0 )
+           ; trace1 = tnext q {!!} } where
+        TA0 : TA fa (δ fa q i ) false true
+        TA0 = tra-phase1 (δ fa q i ) is tr p
 
 open RegularLanguage
 open import Data.Nat.Properties
@@ -167,7 +167,7 @@
     nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
     nn11 = {!!}
     nntrace = trace (automaton r) (astart r) nn
-    nn04 :  Trace (automaton r) nn nntrace
+    nn04 :  Trace (automaton r) nn (astart r)
     nn04 = tr-accept← (automaton r) nn (astart r) nn03 
     nn07 : (n : ℕ) →  length (inputnn0 n i0 i1 []) ≡ n + n 
     nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where
@@ -189,12 +189,10 @@
          suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
          n + n   ≡⟨ sym (nn07 n) ⟩
          length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
-         suc (length (inputnn0 (suc (finite (afin r))) i0 i1 [])) ≡⟨ proj2 (tr-len (automaton r) (inputnn0 n i0 i1 []) (astart r)
-                  (trace (automaton r) (δ (automaton r) (astart r) i0) (inputnn0 (finite (afin r)) i0 i1 (i1 ∷ [])))
-                  (tr-accept← (automaton r) _ _ nn03 )) ⟩
+         {!!} ≤⟨ {!!} ⟩
          length nntrace ∎  where open ≤-Reasoning
-    nn02 : TA (automaton r) nn04
-    nn02 = tr-append (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) nn04 where
+    nn02 : TA (automaton r) {!!} {!!} {!!}
+    nn02 = {!!} where -- make-TA (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) ? where
         nn06 : Dup-in-list ( afin r) nntrace
         nn06 = dup-in-list>n (afin r) nntrace nn05
     nn12 : (x y z : List In2)