Mercurial > hg > Members > kono > Proof > automaton

changeset 307:aeb805cd624a

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 Sun, 02 Jan 2022 06:04:32 +0900
parents fadb41538406
children 2effd9a23299
files automaton-in-agda/src/non-regular.agda
diffstat 1 files changed, 11 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda	Sat Jan 01 22:08:42 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Jan 02 06:04:32 2022 +0900
@@ -110,12 +110,17 @@
 get (x ∷ x₁) zero = just x
 get (x ∷ x₁) (suc n) = get x₁ n
 
+is0-bool : ( i :　ℕ ) → Bool
+is0-bool zero = true
+is0-bool (suc i) = false
+
 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 
        trace-z    : Trace fa z  qd
        trace-yz   : Trace fa (y ++ z)  q
+       q=qd : equal? finq qd q ≡ is0-bool (length y)
 
 record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
     field
@@ -134,9 +139,9 @@
    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
    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
+   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = eq
         ; 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 )
+   ... | false | record { eq = eq } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) ; q=qd = eq
        ; 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 
@@ -156,22 +161,15 @@
         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-05 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → equal? finq qd q ≡ is0-bool (length y2)
+           tra-05 = {!!}
            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 } = {!!}
+           ... | false | record { eq = ne } = ⊥-elim ( ¬-bool {!!} {!!}  )
            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
+           ... | true | record { eq = eq } = ⊥-elim ( ¬-bool {!!} {!!} ) -- 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