Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/pumping.agda @ 405:af8f630b7e60

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, 24 Sep 2023 18:02:04 +0900
parents c298981108c1
children
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 module pumping where 3 module pumping where
2 4
3 open import Data.Nat 5 open import Data.Nat
4 open import Data.Empty 6 open import Data.Empty
5 open import Data.List 7 open import Data.List
113 → TA fa q is 115 → TA fa q is
114 pumping-lemma {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where 116 pumping-lemma {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
115 open TA 117 open TA
116 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) 118 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q )
117 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is 119 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
118 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q 120 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq
119 ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq 121 ... | true = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
120 ; trace-z = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr } 122 ; trace-z = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
121 ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) 123 ... | false = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
122 ; q=qd = tra-08 124 ; q=qd = tra-08
123 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where 125 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
124 ta : TA1 fa finq (δ fa q i) qd is 126 ta : TA1 fa finq (δ fa q i) qd is
125 ta = tra-phase2 (δ fa q i) is tr p 127 ta = tra-phase2 (δ fa q i) is tr p
126 tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i) 128 tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i)
127 tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr 129 tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr
128 tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta)) 130 tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta))
129 tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) ne (TA1.q=qd ta) 131 tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) eq (TA1.q=qd ta)
130 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 132 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
131 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q 133 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq
132 ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta) 134 ... | true = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta)
133 ; non-nil-y = λ () 135 ; non-nil-y = λ ()
134 ; trace-xyz = tnext q (TA1.trace-yz ta) 136 ; trace-xyz = tnext q (TA1.trace-yz ta)
135 ; trace-xyyz = tnext q tra-05 } where 137 ; trace-xyyz = tnext q tra-05 } where
136 ta : TA1 fa finq (δ fa q i ) qd is 138 ta : TA1 fa finq (δ fa q i ) qd is
137 ta = tra-phase2 (δ fa q i ) is tr p 139 ta = tra-phase2 (δ fa q i ) is tr p
143 tryz = tnext qd tryz0 145 tryz = tnext qd tryz0
144 -- create Trace (y ++ y ++ z) 146 -- create Trace (y ++ y ++ z)
145 tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) 147 tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
146 → QDSEQ finq qd z1 {q} {y2} tr 148 → QDSEQ finq qd z1 {q} {y2} tr
147 → Trace fa (y2 ++ (i ∷ y1) ++ z1) q 149 → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
148 tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q 150 tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q in eq
149 ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz 151 ... | true = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
150 ... | false | record { eq = ne } = ⊥-elim ( ¬-bool refl x₁ ) 152 ... | false = ⊥-elim ( ¬-bool refl x₁ )
151 tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q 153 tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q in eq
152 ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) 154 ... | true = ⊥-elim ( ¬-bool x₁ refl )
153 ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) 155 ... | false = tnext q (tra-04 y2 (δ fa q y0) tr qdseq )
154 tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i) 156 tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i)
155 tra-05 with equal→refl finq eq 157 tra-05 with equal→refl finq eq
156 ... | refl = tra-04 y1 (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta) 158 ... | refl = tra-04 y1 (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta)
157 ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) 159 ... | false = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta)
158 ; non-nil-y = non-nil-y ta 160 ; non-nil-y = non-nil-y ta
159 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where 161 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
160 ta : TA fa (δ fa q i ) is 162 ta : TA fa (δ fa q i ) is
161 ta = tra-phase1 (δ fa q i ) is tr p 163 ta = tra-phase1 (δ fa q i ) is tr p
162 164