Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/gcd.agda @ 243:ea3d184c4b1f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 28 Jun 2021 16:26:44 +0900
parents bed5daf239cd
children 08994de7c82f
comparison
equal deleted inserted replaced
242:bed5daf239cd 243:ea3d184c4b1f
352 ; div-j = proj2 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ ) } 352 ; div-j = proj2 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }
353 353
354 gcd-next1 : {i0 j j0 : ℕ} → GCD 0 (suc i0) (suc (suc j)) j0 → GCD i0 (suc i0) (suc j) (suc (suc j)) 354 gcd-next1 : {i0 j j0 : ℕ} → GCD 0 (suc i0) (suc (suc j)) j0 → GCD i0 (suc i0) (suc j) (suc (suc j))
355 gcd-next1 {i0} {j} {j0} g = record { i<i0 = refl-≤s ; j<j0 = refl-≤s 355 gcd-next1 {i0} {j} {j0} g = record { i<i0 = refl-≤s ; j<j0 = refl-≤s
356 ; div-i = proj1 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) ; div-j = proj2 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) } 356 ; div-i = proj1 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) ; div-j = proj2 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) }
357
358 -- i<i0 : zero ≤ i0
359 -- j<j0 : 1 ≤ j0
360 -- div-i : Dividable i0 ((j0 + zero) - 1) -- fi * i0 ≡ (j0 + zero) - 1
361 -- div-j : Dividable j0 ((i0 + 1) - zero) -- fj * j0 ≡ (i0 + 1) - zero
362 gcd-01 : {i0 j0 : ℕ } → (d : GCD zero i0 1 j0 ) → Dividable.factor (GCD.div-i d) ≡ 1
363 gcd-01 {i0} {j0} d with <-cmp (Dividable.factor (GCD.div-i d)) 1
364 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< {!!} (GCD.j<j0 d)) where
365 ge003 : 0 ≡ j0
366 ge003 = sym ( begin
367 j0 ≡⟨ {!!} ⟩
368 (( j0 + 0 ) - 1) + 1 ≡⟨ {!!} ⟩
369 {!!} * i0 ≡⟨ {!!} ⟩
370 0 * i0 ≡⟨ {!!} ⟩
371 0 ∎ )
372 where open ≡-Reasoning
373 ... | tri≈ ¬a b ¬c = b
374 ... | tri> ¬a ¬b c = {!!} where -- ((j0 + zero) - 1) * fj ≡ ((i0 + 1) - zero) * fi → fi > 1 → fj ≡ 0
375 --
376 ge004 : Dividable.factor (GCD.div-i d) ≡ 0
377 ge004 = {!!}
378 ge005 : Dividable.factor (GCD.div-i d) ≡ 0 → Dividable.factor (GCD.div-j d) ≡ 0
379 ge005 = {!!}
357 380
358 -- gcd-dividable1 : ( i i0 j j0 : ℕ ) 381 -- gcd-dividable1 : ( i i0 j j0 : ℕ )
359 -- → Dividable i0 (j0 + i - j ) ∨ Dividable j0 (i0 + j - i) 382 -- → Dividable i0 (j0 + i - j ) ∨ Dividable j0 (i0 + j - i)
360 -- → Dividable ( gcd1 i i0 j j0 ) i0 ∧ Dividable ( gcd1 i i0 j j0 ) j0 383 -- → Dividable ( gcd1 i i0 j j0 ) i0 ∧ Dividable ( gcd1 i i0 j j0 ) j0
361 -- gcd-dividable1 zero i0 zero j0 with <-cmp i0 j0 384 -- gcd-dividable1 zero i0 zero j0 with <-cmp i0 j0
565 gcd-euclid1 : ( i i0 j j0 : ℕ ) → GCD i i0 j j0 → Euclid i0 j0 (gcd1 i i0 j j0) 588 gcd-euclid1 : ( i i0 j j0 : ℕ ) → GCD i i0 j j0 → Euclid i0 j0 (gcd1 i i0 j j0)
566 gcd-euclid1 zero i0 zero j0 di with <-cmp i0 j0 589 gcd-euclid1 zero i0 zero j0 di with <-cmp i0 j0
567 ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () } 590 ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () }
568 ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () } 591 ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () }
569 ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 } 592 ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 }
570 gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 593 -- i<i0 : zero ≤ i0
594 -- j<j0 : 1 ≤ j0
595 -- div-i : Dividable i0 ((j0 + zero) - 1) -- fi * i0 ≡ (j0 + zero) - 1
596 -- div-j : Dividable j0 ((i0 + 1) - zero) -- fj * j0 ≡ (i0 + 1) - zero
597 gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } where
598 ge6 : i0 > j0 → i0 - j0 ≡ gcd1 zero i0 1 j0
599 ge6 i0>j0 = begin
600 i0 - j0 ≡⟨ {!!} ⟩
601 1 ∎ where open ≡-Reasoning
571 gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} } 602 gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = {!!} ; is-equ> = {!!} }
572 gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di ) 603 gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di )
573 ... | e = record { eqa = ea + eb * f ; eqb = eb 604 ... | e = record { eqa = ea + eb * f ; eqb = eb
574 ; is-equ< = λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Euclid.is-equ< e (ge3 lt (ge1 ))) (ge1 ) 605 ; is-equ< = λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Euclid.is-equ< e (ge3 lt (ge1 ))) (ge1 )
575 ; is-equ> = λ lt → subst (λ k → (eb * j0) - ((ea + eb * f) * suc i0) ≡ k ) (Euclid.is-equ> e (ge3 lt (ge2 ))) (ge2 ) } where 606 ; is-equ> = λ lt → subst (λ k → (eb * j0) - ((ea + eb * f) * suc i0) ≡ k ) (Euclid.is-equ> e (ge3 lt (ge2 ))) (ge2 ) } where