Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/non-regular.agda @ 388:227f1f8f9c93
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Jul 2023 03:36:06 +0900 |
| parents | 2d3364cc88ad |
| children | 5264070ddd2d |
| rev | line source |
|---|---|
| 141 | 1 module non-regular where |
| 2 | |
| 3 open import Data.Nat | |
| 274 | 4 open import Data.Empty |
| 141 | 5 open import Data.List |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
277
diff
changeset
|
6 open import Data.Maybe hiding ( map ) |
| 141 | 7 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 8 open import logic | |
| 9 open import automaton | |
| 274 | 10 open import automaton-ex |
|
278
e89957b99662
dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
277
diff
changeset
|
11 open import finiteSetUtil |
| 141 | 12 open import finiteSet |
| 13 open import Relation.Nullary | |
| 274 | 14 open import regular-language |
| 306 | 15 open import nat |
| 385 | 16 open import pumping |
| 306 | 17 |
| 141 | 18 |
| 274 | 19 open FiniteSet |
| 20 | |
| 385 | 21 list-eq : List In2 → List In2 → Bool |
| 22 list-eq [] [] = true | |
| 23 list-eq [] (x ∷ s1) = false | |
| 24 list-eq (x ∷ s) [] = false | |
| 25 list-eq (i0 ∷ s) (i0 ∷ s1) = false | |
| 26 list-eq (i0 ∷ s) (i1 ∷ s1) = false | |
| 27 list-eq (i1 ∷ s) (i0 ∷ s1) = false | |
| 28 list-eq (i1 ∷ s) (i1 ∷ s1) = list-eq s s1 | |
| 29 | |
| 30 input-addi0 : ( n : ℕ ) → List In2 → List In2 | |
| 31 input-addi0 zero x = x | |
| 32 input-addi0 (suc i) x = i0 ∷ input-addi0 i x | |
| 33 | |
| 34 input-addi1 : ( n : ℕ ) → List In2 | |
| 35 input-addi1 zero = [] | |
| 36 input-addi1 (suc i) = i1 ∷ input-addi1 i | |
| 274 | 37 |
| 385 | 38 inputnn0 : ( n : ℕ ) → List In2 |
| 39 inputnn0 n = input-addi0 n (input-addi1 n) | |
| 40 | |
| 41 inputnn1-i1 : (i : ℕ) → List In2 → Bool | |
| 42 inputnn1-i1 zero [] = true | |
| 43 inputnn1-i1 (suc _) [] = false | |
| 44 inputnn1-i1 zero (i1 ∷ x) = false | |
| 45 inputnn1-i1 (suc i) (i1 ∷ x) = inputnn1-i1 i x | |
| 46 inputnn1-i1 zero (i0 ∷ x) = false | |
| 47 inputnn1-i1 (suc _) (i0 ∷ x) = false | |
| 48 | |
| 49 inputnn1-i0 : (i : ℕ) → List In2 → ℕ ∧ List In2 | |
| 50 inputnn1-i0 i [] = ⟪ i , [] ⟫ | |
| 51 inputnn1-i0 i (i1 ∷ x) = ⟪ i , (i1 ∷ x) ⟫ | |
| 52 inputnn1-i0 i (i0 ∷ x) = inputnn1-i0 (suc i) x | |
| 53 | |
| 54 open _∧_ | |
| 55 | |
| 56 inputnn1 : List In2 → Bool | |
| 57 inputnn1 x = inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) | |
| 274 | 58 |
| 59 t1 = inputnn1 ( i0 ∷ i1 ∷ [] ) | |
| 60 t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) | |
| 277 | 61 t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) |
| 274 | 62 |
| 385 | 63 t4 : inputnn1 ( inputnn0 5 ) ≡ true |
| 274 | 64 t4 = refl |
| 65 | |
| 291 | 66 t5 : ( n : ℕ ) → Set |
| 385 | 67 t5 n = inputnn1 ( inputnn0 n ) ≡ true |
| 68 | |
| 69 cons-inject : {A : Set} {x1 x2 : List A } { a : A } → a ∷ x1 ≡ a ∷ x2 → x1 ≡ x2 | |
| 70 cons-inject refl = refl | |
| 71 | |
| 72 append-[] : {A : Set} {x1 : List A } → x1 ++ [] ≡ x1 | |
| 73 append-[] {A} {[]} = refl | |
| 74 append-[] {A} {x ∷ x1} = cong (λ k → x ∷ k) (append-[] {A} {x1} ) | |
| 75 | |
| 76 open import Data.Nat.Properties | |
| 77 open import Relation.Binary.Definitions | |
| 78 open import Relation.Binary.PropositionalEquality | |
| 291 | 79 |
| 388 | 80 nn30 : (y : List In2) → (j : ℕ) → proj2 (inputnn1-i0 (suc j) y) ≡ proj2 (inputnn1-i0 j y ) |
| 81 nn30 [] _ = refl | |
| 82 nn30 (i0 ∷ y) j = nn30 y (suc j) | |
| 83 nn30 (i1 ∷ y) _ = refl | |
| 84 | |
| 85 nn31 : (y : List In2) → (j : ℕ) → proj1 (inputnn1-i0 (suc j) y) ≡ suc (proj1 (inputnn1-i0 j y )) | |
| 86 nn31 [] _ = refl | |
| 87 nn31 (i0 ∷ y) j = nn31 y (suc j) | |
| 88 nn31 (i1 ∷ y) _ = refl | |
| 89 | |
| 385 | 90 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i ) ≡ true |
| 91 nn01 i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i) where | |
| 92 nn07 : (j x : ℕ) → x + j ≡ i → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j | |
| 93 nn07 zero x eq with input-addi1 i | inspect input-addi1 i | |
| 94 ... | [] | _ = +-comm 0 _ | |
| 95 ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where | |
| 96 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) | |
| 97 nn08 zero () | |
| 98 nn08 (suc i) () | |
| 99 ... | i1 ∷ t | _ = +-comm 0 _ | |
| 100 nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) ) | |
| 101 (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) )) | |
| 102 nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i | |
| 103 nn09 zero with input-addi1 i | inspect input-addi1 i | |
| 104 ... | [] | _ = refl | |
| 105 ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where | |
| 106 nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) | |
| 107 nn08 zero () | |
| 108 nn08 (suc i) () | |
| 109 ... | i1 ∷ t | _ = refl | |
| 388 | 110 nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) |
| 385 | 111 nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true |
| 112 nn04 zero = refl | |
| 113 nn04 (suc i) = nn04 i | |
| 114 | |
| 274 | 115 -- |
| 116 -- if there is an automaton with n states , which accespt inputnn1, it has a trasition function. | |
| 117 -- The function is determinted by inputs, | |
| 118 -- | |
| 119 | |
| 120 open RegularLanguage | |
| 121 open Automaton | |
| 122 | |
| 123 open _∧_ | |
| 141 | 124 |
| 277 | 125 |
| 280 | 126 open RegularLanguage |
| 294 | 127 open import Data.Nat.Properties |
|
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
128 open import Data.List.Properties |
| 294 | 129 open import nat |
| 280 | 130 |
| 274 | 131 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) |
| 332 | 132 lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) (TA.xyz=is TAnn) (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyz TAnn) ) |
| 317 | 133 (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyyz TAnn) ) where |
| 280 | 134 n : ℕ |
| 135 n = suc (finite (afin r)) | |
| 385 | 136 nn = inputnn0 n |
| 280 | 137 nn03 : accept (automaton r) (astart r) nn ≡ true |
| 294 | 138 nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n) |
| 304 | 139 nn09 : (n m : ℕ) → n ≤ n + m |
| 140 nn09 zero m = z≤n | |
| 141 nn09 (suc n) m = s≤s (nn09 n m) | |
| 295 | 142 nn04 : Trace (automaton r) nn (astart r) |
| 280 | 143 nn04 = tr-accept← (automaton r) nn (astart r) nn03 |
| 315 | 144 nntrace = tr→qs (automaton r) nn (astart r) nn04 |
| 385 | 145 nn07 : (n : ℕ) → length (inputnn0 n ) ≡ n + n |
| 146 nn07 i = nn19 i where | |
| 147 nn17 : (i : ℕ) → length (input-addi1 i) ≡ i | |
| 148 nn17 zero = refl | |
| 149 nn17 (suc i)= cong suc (nn17 i) | |
| 150 nn18 : (i j : ℕ) → length (input-addi0 j (input-addi1 i)) ≡ j + length (input-addi1 i ) | |
| 151 nn18 i zero = refl | |
| 152 nn18 i (suc j)= cong suc (nn18 i j) | |
| 153 nn19 : (i : ℕ) → length (input-addi0 i ( input-addi1 i )) ≡ i + i | |
| 154 nn19 i = begin | |
| 155 length (input-addi0 i ( input-addi1 i )) ≡⟨ nn18 i i ⟩ | |
| 156 i + length (input-addi1 i) ≡⟨ cong (λ k → i + k) ( nn17 i) ⟩ | |
| 157 i + i ∎ where open ≡-Reasoning | |
| 294 | 158 nn05 : length nntrace > finite (afin r) |
| 159 nn05 = begin | |
| 160 suc (finite (afin r)) ≤⟨ nn09 _ _ ⟩ | |
| 161 n + n ≡⟨ sym (nn07 n) ⟩ | |
| 385 | 162 length (inputnn0 n ) ≡⟨ tr→qs=is (automaton r) (inputnn0 n ) (astart r) nn04 ⟩ |
| 294 | 163 length nntrace ∎ where open ≤-Reasoning |
| 315 | 164 nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04) |
| 304 | 165 nn06 = dup-in-list>n (afin r) nntrace nn05 |
| 332 | 166 |
| 304 | 167 TAnn : TA (automaton r) (astart r) nn |
| 317 | 168 TAnn = pumping-lemma (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06) |
| 332 | 169 |
| 385 | 170 open import Tactic.MonoidSolver using (solve; solve-macro) |
| 171 | |
| 317 | 172 tann : {x y z : List In2} → ¬ y ≡ [] |
| 173 → x ++ y ++ z ≡ nn | |
| 174 → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true ) | |
| 387 | 175 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 |
| 385 | 176 count0 : (x : List In2) → ℕ |
| 177 count0 [] = 0 | |
| 178 count0 (i0 ∷ x) = suc (count0 x) | |
| 179 count0 (i1 ∷ x) = count0 x | |
| 180 count1 : (x : List In2) → ℕ | |
| 181 count1 [] = 0 | |
| 182 count1 (i1 ∷ x) = suc (count1 x) | |
| 183 count1 (i0 ∷ x) = count1 x | |
| 387 | 184 c0+1=n : (x : List In2 ) → count0 x + count1 x ≡ length x |
| 185 c0+1=n [] = refl | |
| 186 c0+1=n (i0 ∷ t) = cong suc ( c0+1=n t ) | |
| 187 c0+1=n (i1 ∷ t) = begin | |
| 188 count0 t + suc (count1 t) ≡⟨ sym (+-assoc (count0 t) _ _) ⟩ | |
| 189 (count0 t + 1 ) + count1 t ≡⟨ cong (λ k → k + count1 t) (+-comm _ 1 ) ⟩ | |
| 190 suc (count0 t + count1 t) ≡⟨ cong suc ( c0+1=n t ) ⟩ | |
| 191 suc (length t) ∎ where open ≡-Reasoning | |
|
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
192 nn15 : (x : List In2 ) → inputnn1 x ≡ true → count0 x ≡ count1 x |
| 388 | 193 nn15 x eq = nn18 where |
| 194 nn17 : (x : List In2 ) → (count0 x ≡ proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x))) | |
| 195 ∧ (count1 x ≡ 0 + count1 (proj2 (inputnn1-i0 0 x))) | |
| 196 nn17 [] = ⟪ refl , refl ⟫ | |
| 197 nn17 (i0 ∷ t ) with nn17 t | |
| 198 ... | ⟪ eq1 , eq2 ⟫ = ⟪ begin | |
| 199 suc (count0 t ) ≡⟨ cong suc eq1 ⟩ | |
| 200 suc (proj1 (inputnn1-i0 0 t) + count0 (proj2 (inputnn1-i0 0 t))) ≡⟨ cong₂ _+_ (sym (nn31 t 0)) (cong count0 (sym (nn30 t 0))) ⟩ | |
| 201 proj1 (inputnn1-i0 1 t) + count0 (proj2 (inputnn1-i0 1 t)) ∎ | |
| 202 , trans eq2 (cong count1 (sym (nn30 t 0))) ⟫ where | |
| 203 open ≡-Reasoning | |
| 204 nn20 : proj2 (inputnn1-i0 1 t) ≡ proj2 (inputnn1-i0 0 t) | |
| 205 nn20 = nn30 t 0 | |
| 206 nn17 (i1 ∷ x₁) = ⟪ refl , refl ⟫ | |
| 207 nn19 : (n : ℕ) → (y : List In2 ) → inputnn1-i1 n y ≡ true → (count0 y ≡ 0) ∧ (count1 y ≡ n) | |
| 208 nn19 zero [] eq = ⟪ refl , refl ⟫ | |
| 209 nn19 zero (i0 ∷ y) () | |
| 210 nn19 zero (i1 ∷ y) () | |
| 211 nn19 (suc i) (i1 ∷ y) eq with nn19 i y eq | |
| 212 ... | t = ⟪ proj1 t , cong suc (proj2 t ) ⟫ | |
| 213 nn18 : count0 x ≡ count1 x | |
| 214 nn18 = begin | |
| 215 count0 x ≡⟨ proj1 (nn17 x) ⟩ | |
| 216 proj1 (inputnn1-i0 0 x) + count0 (proj2 (inputnn1-i0 0 x)) ≡⟨ cong (λ k → proj1 (inputnn1-i0 0 x) + k) | |
| 217 (proj1 (nn19 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) eq)) ⟩ | |
| 218 proj1 (inputnn1-i0 0 x) + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 219 0 + proj1 (inputnn1-i0 0 x) ≡⟨ cong (λ k → 0 + k) (sym (proj2 (nn19 _ _ eq))) ⟩ | |
| 220 0 + count1 (proj2 (inputnn1-i0 0 x)) ≡⟨ sym (proj2 (nn17 x)) ⟩ | |
| 221 count1 x ∎ where open ≡-Reasoning | |
| 385 | 222 cong0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y |
| 223 cong0 [] y = refl | |
| 224 cong0 (i0 ∷ x) y = cong suc (cong0 x y) | |
| 225 cong0 (i1 ∷ x) y = cong0 x y | |
| 226 cong1 : (x y : List In2 ) → count1 (x ++ y ) ≡ count1 x + count1 y | |
| 227 cong1 [] y = refl | |
| 228 cong1 (i1 ∷ x) y = cong suc (cong1 x y) | |
| 229 cong1 (i0 ∷ x) y = cong1 x y | |
| 230 record i1i0 (z : List In2) : Set where | |
| 231 field | |
| 232 a b : List In2 | |
| 233 i10 : z ≡ a ++ (i1 ∷ i0 ∷ b ) | |
| 388 | 234 nn12 : (x : List In2 ) → inputnn1 x ≡ true → ¬ i1i0 x |
| 235 nn12 x eq = nn18 x (nn17 x) eq where | |
| 236 nn17 : (x : List In2 ) → ¬ i1i0 (proj2 (inputnn1-i0 0 x)) | |
| 237 nn17 [] li with i1i0.a li | i1i0.i10 li | |
| 238 ... | [] | () | |
| 239 ... | x ∷ s | () | |
| 240 nn17 (i0 ∷ x₁) li = nn17 x₁ (subst (λ k → i1i0 k) (nn30 x₁ 0 ) li ) | |
| 241 nn17 (i1 ∷ x₁) li with i1i0.i10 li | |
| 242 ... | t = ? | |
| 243 nn18 : (x : List In2 ) → ¬ i1i0 (proj2 (inputnn1-i0 0 x)) | |
| 244 → inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true → ¬ i1i0 x | |
| 245 nn18 = ? | |
| 387 | 246 nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) |
| 388 | 247 nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) |
| 248 ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where | |
| 385 | 249 nn21 : count0 x + count0 y + count0 y + count0 z ≡ count1 x + count1 y + count1 y + count1 z |
| 250 nn21 = begin | |
| 251 (count0 x + count0 y + count0 y) + count0 z ≡⟨ solve +-0-monoid ⟩ | |
| 252 count0 x + (count0 y + (count0 y + count0 z)) ≡⟨ sym (cong (λ k → count0 x + (count0 y + k)) (cong0 y _ )) ⟩ | |
| 253 count0 x + (count0 y + count0 (y ++ z)) ≡⟨ sym (cong (λ k → count0 x + k) (cong0 y _ )) ⟩ | |
| 254 count0 x + (count0 (y ++ y ++ z)) ≡⟨ sym (cong0 x _ ) ⟩ | |
|
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
255 count0 (x ++ y ++ y ++ z) ≡⟨ nn15 (x ++ y ++ y ++ z) xyyz ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
256 count1 (x ++ y ++ y ++ z) ≡⟨ cong1 x _ ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
257 count1 x + (count1 (y ++ y ++ z)) ≡⟨ cong (λ k → count1 x + k) (cong1 y _ ) ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
258 count1 x + (count1 y + count1 (y ++ z)) ≡⟨ (cong (λ k → count1 x + (count1 y + k)) (cong1 y _ )) ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
259 count1 x + (count1 y + (count1 y + count1 z)) ≡⟨ solve +-0-monoid ⟩ |
| 385 | 260 count1 x + count1 y + count1 y + count1 z ∎ where open ≡-Reasoning |
| 261 nn20 : count0 x + count0 y + count0 z ≡ count1 x + count1 y + count1 z | |
|
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
262 nn20 = begin |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
263 count0 x + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
264 count0 x + (count0 y + count0 z) ≡⟨ cong (λ k → count0 x + k) (sym (cong0 y z)) ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
265 count0 x + (count0 (y ++ z)) ≡⟨ sym (cong0 x _) ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
266 count0 (x ++ (y ++ z)) ≡⟨ nn15 (x ++ y ++ z) xyz ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
267 count1 (x ++ (y ++ z)) ≡⟨ cong1 x _ ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
268 count1 x + count1 (y ++ z) ≡⟨ cong (λ k → count1 x + k) (cong1 y z) ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
269 count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
270 count1 x + count1 y + count1 z ∎ where open ≡-Reasoning |
| 387 | 271 -- this takes very long time to check and needs 10GB |
| 385 | 272 bb22 : count0 y ≡ count1 y |
| 387 | 273 bb22 = ? -- begin |
| 274 -- count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( | |
| 275 -- begin | |
| 276 -- count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ | |
| 277 -- (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ | |
| 278 -- (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ | |
| 279 -- (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ | |
| 280 -- count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z | |
| 281 -- ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ | |
| 282 -- count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ | |
| 283 -- count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z | |
| 284 -- ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ | |
| 285 -- count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ | |
| 286 -- count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ | |
| 287 -- count1 y ∎ where open ≡-Reasoning | |
| 385 | 288 bb23 : count0 y ≡ count1 y → i1i0 (y ++ y) |
| 387 | 289 bb23 eq = bb25 y y bb26 (subst (λ k → 0 < k ) (sym eq) bb26) where |
| 290 bb26 : 0 < count1 y | |
| 291 bb26 with <-cmp 0 (count1 y) | |
| 292 ... | tri< a ¬b ¬c = a | |
| 293 ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (sym bb27 ) (0<ly y ny) ) where | |
| 294 0<ly : (y : List In2) → ¬ y ≡ [] → 0 < length y | |
| 295 0<ly [] ne = ⊥-elim ( ne refl ) | |
| 296 0<ly (x ∷ y) ne = s≤s z≤n | |
| 297 bb27 : length y ≡ 0 | |
| 298 bb27 = begin | |
| 299 length y ≡⟨ sym (c0+1=n y) ⟩ | |
| 300 count0 y + count1 y ≡⟨ cong (λ k → k + count1 y ) eq ⟩ | |
| 301 count1 y + count1 y ≡⟨ cong₂ _+_ (sym b) (sym b) ⟩ | |
| 302 0 ∎ where open ≡-Reasoning | |
| 303 bb25 : (x y : List In2 ) → 0 < count1 x → 0 < count0 y → i1i0 (x ++ y) | |
| 304 bb25 (i0 ∷ x₁) y 0<x 0<y with bb25 x₁ y 0<x 0<y | |
| 305 ... | t = record { a = i0 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i0 ∷_) (i1i0.i10 t) } | |
| 306 bb25 (i1 ∷ []) y 0<x 0<y = bb27 y 0<y where | |
| 307 bb27 : (y : List In2 ) → 0 < count0 y → i1i0 (i1 ∷ y ) | |
| 308 bb27 (i0 ∷ y) 0<y = record { a = [] ; b = y ; i10 = refl } | |
| 309 bb27 (i1 ∷ y) 0<y with bb27 y 0<y | |
| 310 ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) } | |
| 311 bb25 (i1 ∷ i0 ∷ x₁) y 0<x 0<y = record { a = [] ; b = x₁ ++ y ; i10 = refl } | |
| 312 bb25 (i1 ∷ i1 ∷ x₁) y (s≤s z≤n) 0<y with bb25 (i1 ∷ x₁) y (s≤s z≤n) 0<y | |
| 313 ... | t = record { a = i1 ∷ i1i0.a t ; b = i1i0.b t ; i10 = cong (i1 ∷_) (i1i0.i10 t) } | |
|
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
314 bb24 : x ++ y ++ y ++ z ≡ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z |
| 385 | 315 bb24 = begin |
|
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
316 x ++ y ++ y ++ z ≡⟨ solve (++-monoid In2) ⟩ |
|
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
317 x ++ (y ++ y) ++ z ≡⟨ cong (λ k → x ++ k ++ z) (i1i0.i10 (bb23 bb22)) ⟩ |
| 387 | 318 x ++ (i1i0.a (bb23 bb22) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) ++ z ≡⟨ cong (λ k → x ++ k) -- solver does not work here |
| 319 (++-assoc (i1i0.a (bb23 bb22)) (i1 ∷ i0 ∷ i1i0.b (bb23 bb22)) z ) ⟩ | |
| 320 x ++ (i1i0.a (bb23 bb22) ++ (i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z)) ≡⟨ sym (++-assoc x _ _ ) ⟩ | |
|
386
6ef927ac832c
bb22 takes 10GB and 5 min
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
385
diff
changeset
|
321 (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning |
| 385 | 322 |
| 387 | 323 nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false |
| 324 nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) | inspect inputnn1 (x ++ y ++ y ++ z) | |
| 325 ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z my eq eq1 ) | |
| 385 | 326 ... | false | _ = refl |
| 327 | |
| 304 | 328 |
| 385 | 329 |
| 330 | |
| 331 | |
| 332 |