Mercurial > hg > Members > kono > Proof > automaton
changeset 386:6ef927ac832c
bb22 takes 10GB and 5 min
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Jul 2023 00:50:16 +0900 |
| parents | 101080136450 |
| children | 2d3364cc88ad |
| files | automaton-in-agda/src/non-regular.agda |
| diffstat | 1 files changed, 37 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda Wed Jul 26 21:20:16 2023 +0900 +++ b/automaton-in-agda/src/non-regular.agda Thu Jul 27 00:50:16 2023 +0900 @@ -119,6 +119,7 @@ open RegularLanguage open import Data.Nat.Properties +open import Data.List.Properties open import nat lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) @@ -174,7 +175,7 @@ count1 [] = 0 count1 (i1 ∷ x) = suc (count1 x) count1 (i0 ∷ x) = count1 x - nn15 : (x : List In2 ) → inputnn1 z ≡ true → count0 z ≡ count1 z + nn15 : (x : List In2 ) → inputnn1 x ≡ true → count0 x ≡ count1 x nn15 = ? cong0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y cong0 [] y = refl @@ -191,26 +192,53 @@ 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) ++ y ; i10 = bb24 } ) where + 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 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 ⟩ count0 x + (count0 y + (count0 y + count0 z)) ≡⟨ sym (cong (λ k → count0 x + (count0 y + k)) (cong0 y _ )) ⟩ count0 x + (count0 y + count0 (y ++ z)) ≡⟨ sym (cong (λ k → count0 x + k) (cong0 y _ )) ⟩ count0 x + (count0 (y ++ y ++ z)) ≡⟨ sym (cong0 x _ ) ⟩ - count0 (x ++ y ++ y ++ z) ≡⟨ ? ⟩ - count1 (x ++ y ++ y ++ z) ≡⟨ ? ⟩ + count0 (x ++ y ++ y ++ z) ≡⟨ nn15 (x ++ y ++ y ++ z) xyyz ⟩ + count1 (x ++ y ++ y ++ z) ≡⟨ cong1 x _ ⟩ + count1 x + (count1 (y ++ y ++ z)) ≡⟨ cong (λ k → count1 x + k) (cong1 y _ ) ⟩ + count1 x + (count1 y + count1 (y ++ z)) ≡⟨ (cong (λ k → count1 x + (count1 y + k)) (cong1 y _ )) ⟩ + count1 x + (count1 y + (count1 y + count1 z)) ≡⟨ solve +-0-monoid ⟩ count1 x + count1 y + count1 y + count1 z ∎ where open ≡-Reasoning nn20 : count0 x + count0 y + count0 z ≡ count1 x + count1 y + count1 z - nn20 = ? + nn20 = begin + count0 x + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ + count0 x + (count0 y + count0 z) ≡⟨ cong (λ k → count0 x + k) (sym (cong0 y z)) ⟩ + count0 x + (count0 (y ++ z)) ≡⟨ sym (cong0 x _) ⟩ + count0 (x ++ (y ++ z)) ≡⟨ nn15 (x ++ y ++ z) xyz ⟩ + count1 (x ++ (y ++ z)) ≡⟨ cong1 x _ ⟩ + 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 bb22 : count0 y ≡ count1 y - bb22 = ? + 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 = ? - bb24 : x ++ y ++ y ++ z ≡ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ y + bb24 : x ++ y ++ y ++ z ≡ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z bb24 = begin - x ++ y ++ y ++ z ≡⟨ ? ⟩ - (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ y where open ≡ + 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 ∎ 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)