Mercurial > hg > Members > kono > Proof > automaton
changeset 387:2d3364cc88ad
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Jul 2023 02:09:27 +0900 |
| parents | 6ef927ac832c |
| children | 227f1f8f9c93 |
| files | automaton-in-agda/src/non-regular.agda |
| diffstat | 1 files changed, 65 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda Thu Jul 27 00:50:16 2023 +0900 +++ b/automaton-in-agda/src/non-regular.agda Thu Jul 27 02:09:27 2023 +0900 @@ -166,7 +166,7 @@ tann : {x y z : List In2} → ¬ y ≡ [] → x ++ y ++ z ≡ nn → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true ) - tann {x} {y} {z} ny eq axyz axyyz = ¬-bool (nn10 x y z (trans (Rg (x ++ y ++ z)) axyz ) ) (trans (Rg (x ++ y ++ y ++ z)) axyyz ) where + tann {x} {y} {z} ny eq axyz axyyz = ¬-bool (nn10 x y z ny (trans (Rg (x ++ y ++ z)) axyz ) ) (trans (Rg (x ++ y ++ y ++ z)) axyyz ) where count0 : (x : List In2) → ℕ count0 [] = 0 count0 (i0 ∷ x) = suc (count0 x) @@ -175,8 +175,22 @@ count1 [] = 0 count1 (i1 ∷ x) = suc (count1 x) count1 (i0 ∷ x) = count1 x + c0+1=n : (x : List In2 ) → count0 x + count1 x ≡ length x + c0+1=n [] = refl + c0+1=n (i0 ∷ t) = cong suc ( c0+1=n t ) + c0+1=n (i1 ∷ t) = begin + count0 t + suc (count1 t) ≡⟨ sym (+-assoc (count0 t) _ _) ⟩ + (count0 t + 1 ) + count1 t ≡⟨ cong (λ k → k + count1 t) (+-comm _ 1 ) ⟩ + suc (count0 t + count1 t) ≡⟨ cong suc ( c0+1=n t ) ⟩ + suc (length t) ∎ where open ≡-Reasoning nn15 : (x : List In2 ) → inputnn1 x ≡ true → count0 x ≡ count1 x - nn15 = ? + nn15 x eq = ? where + nn18 : inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true + nn18 = eq + nn16 : (x : List In2 ) → proj1 (inputnn1-i0 (count0 x) x ) ≡ count0 x + nn16 = ? + nn17 : (x : List In2 ) → count1 (proj2 (inputnn1-i0 (count0 x) x ) ) ≡ count1 x + nn17 = ? cong0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y cong0 [] y = refl cong0 (i0 ∷ x) y = cong suc (cong0 x y) @@ -191,8 +205,8 @@ i10 : z ≡ a ++ (i1 ∷ i0 ∷ b ) nn12 : (z : List In2 ) → inputnn1 z ≡ true → ¬ i1i0 z nn12 = ? - nn11 : (x y z : List In2 ) → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) - nn11 x y z xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where + nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) + nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where nn21 : count0 x + count0 y + count0 y + count0 z ≡ count1 x + count1 y + count1 y + count1 z nn21 = begin (count0 x + count0 y + count0 y) + count0 z ≡⟨ solve +-0-monoid ⟩ @@ -215,34 +229,61 @@ count1 x + count1 (y ++ z) ≡⟨ cong (λ k → count1 x + k) (cong1 y z) ⟩ count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩ count1 x + count1 y + count1 z ∎ where open ≡-Reasoning + -- this takes very long time to check and needs 10GB bb22 : count0 y ≡ count1 y - bb22 = begin - count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( - begin - count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ - (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ - (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ - (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ - count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z - ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ - count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ - count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z - ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ - count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ - count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ - count1 y ∎ where open ≡-Reasoning + bb22 = ? -- begin +-- count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( +-- begin +-- count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ +-- (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ +-- (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ +-- (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ +-- count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z +-- ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ +-- count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ +-- count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z +-- ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ +-- count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ +-- count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ +-- count1 y ∎ where open ≡-Reasoning bb23 : count0 y ≡ count1 y → i1i0 (y ++ y) - bb23 = ? + bb23 eq = bb25 y y bb26 (subst (λ k → 0 < k ) (sym eq) bb26) where + bb26 : 0 < count1 y + bb26 with <-cmp 0 (count1 y) + ... | tri< a ¬b ¬c = a + ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (sym bb27 ) (0<ly y ny) ) where + 0<ly : (y : List In2) → ¬ y ≡ [] → 0 < length y + 0<ly [] ne = ⊥-elim ( ne refl ) + 0<ly (x ∷ y) ne = s≤s z≤n + bb27 : length y ≡ 0 + bb27 = begin + length y ≡⟨ sym (c0+1=n y) ⟩ + count0 y + count1 y ≡⟨ cong (λ k → k + count1 y ) eq ⟩ + count1 y + count1 y ≡⟨ cong₂ _+_ (sym b) (sym b) ⟩ + 0 ∎ where open ≡-Reasoning + bb25 : (x y : List In2 ) → 0 < count1 x → 0 < count0 y → i1i0 (x ++ y) + bb25 (i0 ∷ x₁) y 0<x 0<y with bb25 x₁ y 0<x 0<y + ... | t = record { a = i0 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i0 ∷_) (i1i0.i10 t) } + bb25 (i1 ∷ []) y 0<x 0<y = bb27 y 0<y where + bb27 : (y : List In2 ) → 0 < count0 y → i1i0 (i1 ∷ y ) + bb27 (i0 ∷ y) 0<y = record { a = [] ; b = y ; i10 = refl } + bb27 (i1 ∷ y) 0<y with bb27 y 0<y + ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) } + bb25 (i1 ∷ i0 ∷ x₁) y 0<x 0<y = record { a = [] ; b = x₁ ++ y ; i10 = refl } + bb25 (i1 ∷ i1 ∷ x₁) y (s≤s z≤n) 0<y with bb25 (i1 ∷ x₁) y (s≤s z≤n) 0<y + ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) } bb24 : x ++ y ++ y ++ z ≡ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z bb24 = begin x ++ y ++ y ++ z ≡⟨ solve (++-monoid In2) ⟩ x ++ (y ++ y) ++ z ≡⟨ cong (λ k → x ++ k ++ z) (i1i0.i10 (bb23 bb22)) ⟩ - x ++ (i1i0.a (bb23 bb22) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) ++ z ≡⟨ solve (++-monoid In2) ⟩ + x ++ (i1i0.a (bb23 bb22) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) ++ z ≡⟨ cong (λ k → x ++ k) -- solver does not work here + (++-assoc (i1i0.a (bb23 bb22)) (i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) z ) ⟩ + x ++ (i1i0.a (bb23 bb22) ++ (i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z)) ≡⟨ sym (++-assoc x _ _ ) ⟩ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning - nn10 : (x y z : List In2 ) → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false - nn10 x y z eq with inputnn1 (x ++ y ++ y ++ z) | inspect inputnn1 (x ++ y ++ y ++ z) - ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z eq eq1 ) + nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false + nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) | inspect inputnn1 (x ++ y ++ y ++ z) + ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z my eq eq1 ) ... | false | _ = refl