Mercurial > hg > Members > kono > Proof > automaton
comparison automaton-in-agda/src/gcd.agda @ 214:906b43b94228
gcd-dividable done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 21 Jun 2021 09:40:52 +0900 |
| parents | 9aec75fa796c |
| children | 6474d814d9a8 |
comparison
equal
deleted
inserted
replaced
| 213:9aec75fa796c | 214:906b43b94228 |
|---|---|
| 279 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | 279 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl |
| 280 ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) | 280 ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) |
| 281 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | 281 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl |
| 282 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b)) | 282 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b)) |
| 283 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | 283 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) |
| 284 | |
| 284 record Fdec ( i j : ℕ ) : Set where | 285 record Fdec ( i j : ℕ ) : Set where |
| 285 field | 286 field |
| 286 ni : ℕ | 287 ni : ℕ |
| 287 nj : ℕ | 288 nj : ℕ |
| 288 fdec : 0 < F ⟪ i , j ⟫ → F ⟪ ni , nj ⟫ < F ⟪ i , j ⟫ | 289 fdec : 0 < F ⟪ i , j ⟫ → F ⟪ ni , nj ⟫ < F ⟪ i , j ⟫ |
| 290 | |
| 289 fd1 : ( i j k : ℕ ) → i < j → k ≡ j - i → F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫ | 291 fd1 : ( i j k : ℕ ) → i < j → k ≡ j - i → F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫ |
| 290 fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) | 292 fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) |
| 291 fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where | 293 fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where |
| 292 fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i → F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫ | 294 fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i → F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫ |
| 293 fd2 i j k i<j eq with <-cmp i k | <-cmp i j | 295 fd2 i j k i<j eq with <-cmp i k | <-cmp i j |
| 302 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where | 304 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where |
| 303 fd4 : suc i < suc j | 305 fd4 : suc i < suc j |
| 304 fd4 = s≤s a | 306 fd4 = s≤s a |
| 305 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬a₁ i<j) | 307 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬a₁ i<j) |
| 306 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (¬a₁ i<j) | 308 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (¬a₁ i<j) |
| 309 | |
| 307 fedc0 : (i j : ℕ ) → Fdec i j | 310 fedc0 : (i j : ℕ ) → Fdec i j |
| 308 fedc0 0 0 = record { ni = 0 ; nj = 0 ; fdec = λ () } | 311 fedc0 0 0 = record { ni = 0 ; nj = 0 ; fdec = λ () } |
| 309 fedc0 (suc i) 0 = record { ni = suc i ; nj = 0 ; fdec = λ () } | 312 fedc0 (suc i) 0 = record { ni = suc i ; nj = 0 ; fdec = λ () } |
| 310 fedc0 0 (suc j) = record { ni = 0 ; nj = suc j ; fdec = λ () } | 313 fedc0 0 (suc j) = record { ni = 0 ; nj = suc j ; fdec = λ () } |
| 311 fedc0 (suc i) (suc j) with <-cmp i j | 314 fedc0 (suc i) (suc j) with <-cmp i j |
| 316 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) | 319 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) |
| 317 ... | tri≈ ¬a b ¬c = refl | 320 ... | tri≈ ¬a b ¬c = refl |
| 318 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) | 321 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) |
| 319 ... | tri> ¬a ¬b c = record { ni = i - j ; nj = suc j ; fdec = λ lt → | 322 ... | tri> ¬a ¬b c = record { ni = i - j ; nj = suc j ; fdec = λ lt → |
| 320 subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } | 323 subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } |
| 324 | |
| 325 ind3 : {i j : ℕ } → i < j | |
| 326 → Dividable (gcd (suc i) (j - i)) (suc i) | |
| 327 → Dividable (gcd (suc i) (suc j)) (suc i) | |
| 328 ind3 {i} {j} a prev = | |
| 329 subst (λ k → Dividable k (suc i)) ( begin | |
| 330 gcd (suc i) (j - i) ≡⟨ gcdsym {suc i} {j - i} ⟩ | |
| 331 gcd (j - i ) (suc i) ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩ | |
| 332 gcd ((j - i) + suc i) (suc i) ≡⟨ cong (λ k → gcd k (suc i)) ( begin | |
| 333 (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n → suc (suc i) ≤ suc (suc (suc n)) | |
| 334 suc j ∎ ) ⟩ | |
| 335 gcd (suc j) (suc i) ≡⟨ gcdsym {suc j} {suc i} ⟩ | |
| 336 gcd (suc i) (suc j) ∎ ) prev where open ≡-Reasoning | |
| 337 ind7 : {i j : ℕ } → (i < j ) → (j - i) + suc i ≡ suc j | |
| 338 ind7 {i} {j} a = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa) ⟩ | |
| 339 suc j ∎ where open ≡-Reasoning | |
| 340 ind6 : {i j k : ℕ } → i < j | |
| 341 → Dividable k (j - i) | |
| 342 → Dividable k (suc i) | |
| 343 → Dividable k (suc j) | |
| 344 ind6 {i} {j} {k} i<j dj di = subst (λ g → Dividable k g ) (ind7 i<j) (proj1 (div+div dj di)) | |
| 345 ind4 : {i j : ℕ } → i < j | |
| 346 → Dividable (gcd (suc i) (j - i)) (j - i) | |
| 347 → Dividable (gcd (suc i) (suc j)) (j - i) | |
| 348 ind4 {i} {j} i<j prev = subst (λ k → k) ( begin | |
| 349 Dividable (gcd (suc i) (j - i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc i} ) ⟩ | |
| 350 Dividable (gcd (j - i ) (suc i) ) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) ( sym (gcd+j (j - i) (suc i))) ⟩ | |
| 351 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable (gcd k (suc i)) (j - i)) (ind7 i<j ) ⟩ | |
| 352 Dividable (gcd (suc j) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩ | |
| 353 Dividable (gcd (suc i) (suc j)) (j - i) ∎ ) prev where open ≡-Reasoning | |
| 354 | |
| 321 ind : ( i j : ℕ ) → | 355 ind : ( i j : ℕ ) → |
| 322 Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j)) | 356 Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j)) |
| 323 ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j)) | 357 ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j)) |
| 324 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j | 358 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j |
| 325 ind zero zero prev = ind0 where | 359 ind zero zero prev = ind0 where |
| 330 ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div= ⟫ | 364 ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div= ⟫ |
| 331 ind (suc i) zero prev = ind2 where | 365 ind (suc i) zero prev = ind2 where |
| 332 ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero | 366 ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero |
| 333 ind2 = ⟪ subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫ | 367 ind2 = ⟪ subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫ |
| 334 ind (suc i) (suc j) prev with <-cmp i j | 368 ind (suc i) (suc j) prev with <-cmp i j |
| 335 ... | tri< a ¬b ¬c = ⟪ ind3 (proj1 prev) , ind6 (ind4 (proj2 prev)) (ind3 (proj1 prev)) ⟫ where | 369 ... | tri< a ¬b ¬c = ⟪ ind3 a (proj1 prev) , ind6 a (ind4 a (proj2 prev)) (ind3 a (proj1 prev) ) ⟫ where |
| 336 ind3 : Dividable (gcd (suc i) (j - i)) (suc i) | |
| 337 → Dividable (gcd (suc i) (suc j)) (suc i) | |
| 338 ind3 prev = | |
| 339 subst (λ k → Dividable k (suc i)) ( begin | |
| 340 gcd (suc i) (j - i) ≡⟨ gcdsym {suc i} {j - i} ⟩ | |
| 341 gcd (j - i ) (suc i) ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩ | |
| 342 gcd ((j - i) + suc i) (suc i) ≡⟨ cong (λ k → gcd k (suc i)) ( begin | |
| 343 (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n → suc (suc i) ≤ suc (suc (suc n)) | |
| 344 suc j ∎ ) ⟩ | |
| 345 gcd (suc j) (suc i) ≡⟨ gcdsym {suc j} {suc i} ⟩ | |
| 346 gcd (suc i) (suc j) ∎ ) prev where open ≡-Reasoning | |
| 347 ind7 : (j - i) + suc i ≡ suc j | |
| 348 ind7 = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa) ⟩ | |
| 349 suc j ∎ where open ≡-Reasoning | |
| 350 ind6 : {k : ℕ } → Dividable k (j - i) → Dividable k (suc i) → Dividable k (suc j) | |
| 351 ind6 {k} dj di = subst (λ g → Dividable k g ) ind7 (proj1 (div+div dj di)) | |
| 352 ind4 : Dividable (gcd (suc i) (j - i)) (j - i) | |
| 353 → Dividable (gcd (suc i) (suc j)) (j - i) | |
| 354 ind4 prev = subst (λ k → k) ( begin | |
| 355 Dividable (gcd (suc i) (j - i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc i} ) ⟩ | |
| 356 Dividable (gcd (j - i ) (suc i) ) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) ( sym (gcd+j (j - i) (suc i))) ⟩ | |
| 357 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable (gcd k (suc i)) (j - i)) ind7 ⟩ | |
| 358 Dividable (gcd (suc j) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩ | |
| 359 Dividable (gcd (suc i) (suc j)) (j - i) ∎ ) prev where open ≡-Reasoning | |
| 360 ... | tri≈ ¬a refl ¬c = ⟪ ind5 , ind5 ⟫ where | 370 ... | tri≈ ¬a refl ¬c = ⟪ ind5 , ind5 ⟫ where |
| 361 ind5 : Dividable (gcd (suc i) (suc i)) (suc i) | 371 ind5 : Dividable (gcd (suc i) (suc i)) (suc i) |
| 362 ind5 = subst (λ k → Dividable k (suc j)) (sym (gcdmm (suc i) (suc i))) div= | 372 ind5 = subst (λ k → Dividable k (suc j)) (sym (gcdmm (suc i) (suc i))) div= |
| 363 ... | tri> ¬a ¬b c = {!!} | 373 ... | tri> ¬a ¬b c = ⟪ ind8 c (proj1 prev) (proj2 prev) , ind10 c (proj2 prev) ⟫ where |
| 374 ind9 : {i j : ℕ} → i < j → gcd (j - i) (suc i) ≡ gcd (suc j) (suc i) | |
| 375 ind9 {i} {j} i<j = begin | |
| 376 gcd (j - i ) (suc i) ≡⟨ sym (gcd+j (j - i ) (suc i) ) ⟩ | |
| 377 gcd (j - i + suc i) (suc i) ≡⟨ cong (λ k → gcd k (suc i)) (ind7 i<j ) ⟩ | |
| 378 gcd (suc j) (suc i) ∎ where open ≡-Reasoning | |
| 379 ind8 : { i j : ℕ } → i < j | |
| 380 → Dividable (gcd (j - i) (suc i)) (j - i) | |
| 381 → Dividable (gcd (j - i) (suc i)) (suc i) | |
| 382 → Dividable (gcd (suc j) (suc i)) (suc j) | |
| 383 ind8 {i} {j} i<j dji di = ind6 i<j (subst (λ k → Dividable k (j - i)) (ind9 i<j) dji) (subst (λ k → Dividable k (suc i)) (ind9 i<j) di) | |
| 384 ind10 : { i j : ℕ } → j < i | |
| 385 → Dividable (gcd (i - j) (suc j)) (suc j) | |
| 386 → Dividable (gcd (suc i) (suc j)) (suc j) | |
| 387 ind10 {i} {j} j<i dji = subst (λ g → Dividable g (suc j) ) (begin | |
| 388 gcd (i - j) (suc j) ≡⟨ sym (gcd+j (i - j) (suc j)) ⟩ | |
| 389 gcd (i - j + suc j) (suc j) ≡⟨ cong (λ k → gcd k (suc j)) (ind7 j<i ) ⟩ | |
| 390 gcd (suc i) (suc j) ∎ ) dji where open ≡-Reasoning | |
| 364 | 391 |
| 365 I : Finduction (ℕ ∧ ℕ) _ F | 392 I : Finduction (ℕ ∧ ℕ) _ F |
| 366 I = record { | 393 I = record { |
| 367 fzero = F00 | 394 fzero = F00 |
| 368 ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) , Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ | 395 ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) , Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ |