Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/pumping.agda @ 405:af8f630b7e60
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 18:02:04 +0900 |
| parents | c298981108c1 |
| children |
line wrap: on
line diff
--- a/automaton-in-agda/src/pumping.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/pumping.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module pumping where open import Data.Nat @@ -115,10 +117,10 @@ open TA 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 ; q=qd = qd-nil q (tnext q tr) eq + tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq + ... | true = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) 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 = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) + ... | false = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) ; q=qd = tra-08 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where ta : TA1 fa finq (δ fa q i) qd is @@ -126,10 +128,10 @@ tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i) tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta)) - tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) ne (TA1.q=qd ta) + tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) eq (TA1.q=qd ta) 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 - ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta) + tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq + ... | true = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta) ; non-nil-y = λ () ; trace-xyz = tnext q (TA1.trace-yz ta) ; trace-xyyz = tnext q tra-05 } where @@ -145,16 +147,16 @@ tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → QDSEQ finq qd z1 {q} {y2} tr → Trace fa (y2 ++ (i ∷ y1) ++ z1) q - tra-04 [] q tr (qd-nil q _ x₁) 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 } = ⊥-elim ( ¬-bool refl x₁ ) - tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q - ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) - ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) + tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q in eq + ... | true = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz + ... | false = ⊥-elim ( ¬-bool refl x₁ ) + tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q in eq + ... | true = ⊥-elim ( ¬-bool x₁ refl ) + ... | false = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i) tra-05 with equal→refl finq eq ... | refl = tra-04 y1 (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta) - ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) + ... | false = 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 ta : TA fa (δ fa q i ) is