Mercurial > hg > Members > kono > Proof > automaton

changeset 306:fadb41538406

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 22:08:42 +0900
parents 5ef7ad34a05f
children aeb805cd624a
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 39 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Sat Jan 01 18:52:42 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sat Jan 01 22:08:42 2022 +0900
@@ -12,6 +12,8 @@
 open import finiteSet
 open import Relation.Nullary 
 open import regular-language
+open import nat
+
 
 open FiniteSet
 
@@ -92,18 +94,21 @@
 
 open Data.Maybe
 
--- head : {a : Set} → List a → Maybe a
--- head [] = nothing
--- head (h ∷ _ ) = just h
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+open import Relation.Binary.Definitions
+open import Data.Unit using (⊤ ; tt)
+open import Data.Nat.Properties
 
-tr-append1 : { Q : Set } { Σ : Set  }
-    → (fa : Automaton Q  Σ )
-    → (i : Σ) → ( q : Q)  
-    → (is : List Σ)
-    → Trace fa is ( δ fa q i )  →  Trace fa (i ∷ is) q
-tr-append1 fa i q is tr = tnext _ tr 
+sometime : { a : Set } (x : List a ) → (n : ℕ) → n ≤ length x  → (P : a → Set)  → Set
+sometime {a} [] .zero z≤n P = ⊤
+sometime {a} (x ∷ x₁) zero z≤n P = P x 
+sometime {a} (x ∷ x₁) (suc n) (s≤s lt) P = sometime {a} x₁  n lt P 
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+get : { a : Set } (x : List a ) → (n : ℕ) → Maybe a
+get [] zero = nothing
+get [] (suc n) = nothing
+get (x ∷ x₁) zero = just x
+get (x ∷ x₁) (suc n) = get x₁ n
 
 record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
     field
@@ -112,12 +117,6 @@
        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 Σ
@@ -126,8 +125,6 @@
        trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
        non-nil-y : ¬ (y ≡ [])
 
-open import nat
-
 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
@@ -143,15 +140,6 @@
        ; 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) 
@@ -161,6 +149,30 @@
            ; 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 = {!!} where
+           tryz = tnext q tr 
+           tra-05 :  (y2 : List Σ) → (q qd : Q) → (tr : Trace fa (y2 ++ z1) q) → (n : ℕ) → Set
+           tra-05 y2 q qd tr n with <-cmp n (length y2)
+           ... | tri< a ¬b ¬c = ¬ ( get (tr→qs fa (y2 ++ z1) q tr ) n ≡ just qd )
+           ... | tri≈ ¬a b ¬c = get (tr→qs fa (y2 ++ z1) q tr ) n ≡ just qd
+           ... | tri> ¬a ¬b c = ⊤
+           ep : (y2 : List Σ) → (tr : Trace fa (y2 ++ z1) q)  →  length y2 ≡ 0 → get (tr→qs fa (y2 ++ z1) q tr ) 0 ≡ just qd
+           ep = {!!}
+           np2 : (y2 : List Σ) → (tr :  Trace fa (y2 ++ z1) q) →  length y2 > 0 → ¬ (get (tr→qs fa (y2 ++ z1) q tr ) 0 ≡ just qd)
+           np2 = {!!}
+           tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
+               → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
+           tra-04 [] q tr 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 } = {!!}
+           tra-04 (y0 ∷ y2) q (tnext q tr) 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 )
    ... | 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