Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/non-regular.agda @ 296:2f113cac060b

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 14:36:44 +0900
parents 99c2cbe6a862
children afc7db9b917d
comparison
equal deleted inserted replaced
295:99c2cbe6a862 296:2f113cac060b
103 → Trace fa is ( δ fa q i ) → Trace fa (i ∷ is) q 103 → Trace fa is ( δ fa q i ) → Trace fa (i ∷ is) q
104 tr-append1 fa i q is tr = tnext _ tr 104 tr-append1 fa i q is tr = tnext _ tr
105 105
106 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 106 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
107 107
108 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) ( q : Q ) (phase yeq : Bool) : Set where 108 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (phase : ℕ) ( q qd : Q ) : Set where
109 field 109 field
110 x y y1 z : List Σ 110 x y z : List Σ
111 px : phase ≡ true → x ≡ [] 111 trace-z : phase > 1 → Trace fa z qd
112 py : yeq ≡ true → y ≡ y1 112 trace-yz : phase > 0 → Trace fa (y ++ z) qd
113 trace0 : Trace fa (x ++ y ++ z) q 113 trace-xyz : phase ≡ 0 → Trace fa (x ++ y ++ z) q
114 trace1 : Trace fa (x ++ y ++ y1 ++ z) q 114 trace-xyyz : phase ≡ 0 → Trace fa (x ++ y ++ y ++ z) q
115
116 open import nat
115 117
116 make-TA : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 118 make-TA : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ)
117 → (tr : Trace fa is q ) 119 → (tr : Trace fa is q )
118 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true 120 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
119 → TA fa q false true 121 → TA fa 0 q qd
120 make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where 122 make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
121 open TA 123 open TA
122 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 124 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
123 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q 125 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q
124 ... | true = {!!} -- record { px = λ _ → refl ; x = [] ; y = i ∷ y TA0 ; z = z TA0 ; trace0 = tnext q (trace0 TA0 ) ; trace1 = tnext q (trace1 TA0) } 126 ... | true = {!!}
125 ... | false = record { px = λ _ → refl ; x = [] ; y = i ∷ y TA0 ; y1 = y1 TA0 ; z = z TA0 ; py = λ () 127 ... | false = {!!}
126 ; trace0 = tnext q (subst (λ k → Trace fa k (δ fa q i) ) (tr-01 (px TA0 refl ) ) (trace0 TA0)) 128 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
127 ; trace1 = tnext q (subst (λ k → Trace fa k (δ fa q i) ) (tr-02 (px TA0 refl )) (trace1 TA0))} where 129 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q
128 TA0 : TA fa (δ fa q i ) true false 130 ... | true = record { x = [] ; y = y TA0 ; z = z TA0 ; trace-z = λ () ; trace-yz = λ _ → trace-yz TA0 a<sa
131 ; trace-xyz = λ _ → subst (λ k → Trace fa (y TA0 ++ z TA0) k ) {!!} (trace-yz TA0 a<sa)
132 ; trace-xyyz = λ _ → {!!}} where
133 TA0 : {!!}
129 TA0 = tra-phase2 (δ fa q i ) is tr p 134 TA0 = tra-phase2 (δ fa q i ) is tr p
130 tr-01 : {x1 : List Σ} → x1 ≡ [] → x1 ++ y TA0 ++ z TA0 ≡ y TA0 ++ z TA0 135 ... | false = record { x = i ∷ x TA0 ; y = y TA0 ; z = z TA0 ; trace-z = λ () ; trace-yz = λ ()
131 tr-01 refl = refl 136 ; trace-xyz = λ _ → tnext q (trace-xyz TA0 refl ) ; trace-xyyz = λ _ → tnext q (trace-xyyz TA0 refl )} where
132 tr-02 : {x1 : List Σ} → x1 ≡ [] → x1 ++ y TA0 ++ (y1 TA0) ++ z TA0 ≡ y TA0 ++ (y1 TA0) ++ z TA0 137 TA0 : TA fa 0 (δ fa q i ) qd
133 tr-02 refl = refl
134 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
135 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q
136 ... | true = record { px = λ () ; x = i ∷ x TA0 ; y = y TA0 ; y1 = y TA0 ; z = z TA0 ; py = λ _ → refl
137 ; trace0 = tnext q (trace0 TA0 ) ; trace1 = tnext q {!!} } where
138 TA0 : TA fa (δ fa q i ) true false
139 TA0 = tra-phase2 (δ fa q i ) is tr p
140 ... | false = record { px = λ () ; x = i ∷ x TA0 ; y = y TA0 ; y1 = y TA0 ; z = z TA0 ; py = λ _ → refl ; trace0 = tnext q (trace0 TA0 )
141 ; trace1 = tnext q {!!} } where
142 TA0 : TA fa (δ fa q i ) false true
143 TA0 = tra-phase1 (δ fa q i ) is tr p 138 TA0 = tra-phase1 (δ fa q i ) is tr p
144 139
145 open RegularLanguage 140 open RegularLanguage
146 open import Data.Nat.Properties 141 open import Data.Nat.Properties
147 open import nat 142 open import nat
189 suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩ 184 suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩
190 n + n ≡⟨ sym (nn07 n) ⟩ 185 n + n ≡⟨ sym (nn07 n) ⟩
191 length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s ⟩ 186 length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s ⟩
192 {!!} ≤⟨ {!!} ⟩ 187 {!!} ≤⟨ {!!} ⟩
193 length nntrace ∎ where open ≤-Reasoning 188 length nntrace ∎ where open ≤-Reasoning
194 nn02 : TA (automaton r) {!!} {!!} {!!} 189 nn02 : {!!} -- TA (automaton r) {!!} {!!} {!!}
195 nn02 = {!!} where -- make-TA (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) ? where 190 nn02 = {!!} where -- make-TA (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) ? where
196 nn06 : Dup-in-list ( afin r) nntrace 191 nn06 : Dup-in-list ( afin r) nntrace
197 nn06 = dup-in-list>n (afin r) nntrace nn05 192 nn06 = dup-in-list>n (afin r) nntrace nn05
198 nn12 : (x y z : List In2) 193 nn12 : (x y z : List In2)
199 → ¬ y ≡ [] 194 → ¬ y ≡ []