Mercurial > hg > Members > kono > Proof > automaton
changeset 247:61d9fdb22f2d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 28 Jun 2021 23:01:27 +0900 |
| parents | 6cd80d8432ea |
| children | de959bb968ed |
| files | automaton-in-agda/src/gcd.agda |
| diffstat | 1 files changed, 92 insertions(+), 67 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/gcd.agda Mon Jun 28 19:28:52 2021 +0900 +++ b/automaton-in-agda/src/gcd.agda Mon Jun 28 23:01:27 2021 +0900 @@ -372,9 +372,38 @@ (i + j ) - j ≡⟨ cong (λ k → k - j ) (+-comm i j ) ⟩ (j + i) - j ∎ } where open ≡-Reasoning +div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k +div→gcd {n} {k} k>1 = n-induction {_} {_} {ℕ} {λ m → Dividable k m → gcd m k ≡ k } (λ x → x) I n where + decl : {m : ℕ } → 0 < m → m - k < m + decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m + ind : (m : ℕ ) → (Dividable k (m - k) → gcd (m - k) k ≡ k) → Dividable k m → gcd m k ≡ k + ind m prev d with <-cmp (suc m) k + ... | tri≈ ¬a refl ¬c = ⊥-elim ( div+1 k>1 d div= ) + ... | tri> ¬a ¬b c = subst (λ g → g ≡ k) ind1 ( prev (proj2 (div-div k>1 div= d))) where + ind1 : gcd (m - k) k ≡ gcd m k + ind1 = begin + gcd (m - k) k ≡⟨ sym (gcd+j (m - k) _) ⟩ + gcd (m - k + k) k ≡⟨ cong (λ g → gcd g k) (minus+n {m} {k} c) ⟩ + gcd m k ∎ where open ≡-Reasoning + ... | tri< a ¬b ¬c with <-cmp 0 m + ... | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim ( div<k k>1 a₁ (<-trans a<sa a) d ) + ... | tri≈ ¬a refl ¬c₁ = subst (λ g → g ≡ k ) (gcdsym {k} {0} ) (gcd20 k) + fzero : (m : ℕ) → (m - k) ≡ zero → Dividable k m → gcd m k ≡ k + fzero 0 eq d = trans (gcdsym {0} {k} ) (gcd20 k) + fzero (suc m) eq d with <-cmp (suc m) k + ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 (s≤s z≤n) a d ) + ... | tri≈ ¬a refl ¬c = gcdmm k k + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (minus>0 c) ) + I : Ninduction ℕ _ (λ x → x) + I = record { + pnext = λ p → p - k + ; fzero = λ {m} eq → fzero m eq + ; decline = λ {m} lt → decl lt + ; ind = λ {p} prev → ind p prev + } GCDi : {i j : ℕ } → GCD i i j j -GCDi {i} {j} = record { i<i0 = refl-≤ ; j<j0 = refl-≤ ; div-i = div-11 ; div-j = div-11 } +GCDi {i} {j} = record { i<i0 = refl-≤ ; j<j0 = refl-≤ ; div-i = div-11 {i} {j} ; div-j = div-11 {j} {i} } GCD-sym : {i i0 j j0 : ℕ} → GCD i i0 j j0 → GCD j j0 i i0 GCD-sym g = record { i<i0 = GCD.j<j0 g ; j<j0 = GCD.i<i0 g ; div-i = GCD.div-j g ; div-j = GCD.div-i g } @@ -560,6 +589,33 @@ ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev } +f-div>0 : { k i : ℕ } → (d : Dividable k i ) → 0 < i → 0 < Dividable.factor d +f-div>0 {k} {i} d 0<i with <-cmp 0 (Dividable.factor d) +... | tri< a ¬b ¬c = a +... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (begin + 0 * k + 0 ≡⟨ cong (λ g → g * k + 0) b ⟩ + Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ + i ∎ ) 0<i ) where open ≡-Reasoning + +gcd-≤i : ( i j : ℕ ) → 0 < i → i ≤ j → gcd i j ≤ i +gcd-≤i zero _ () z≤n +gcd-≤i (suc i) (suc j) _ (s≤s i<j) = begin + gcd (suc i) (suc j) ≡⟨ sym m*1=m ⟩ + gcd (suc i) (suc j) * 1 ≤⟨ *-monoʳ-≤ (gcd (suc i) (suc j)) (f-div>0 d (s≤s z≤n)) ⟩ + gcd (suc i) (suc j) * f ≡⟨ +-comm 0 _ ⟩ + gcd (suc i) (suc j) * f + 0 ≡⟨ cong (λ k → k + 0) (*-comm (gcd (suc i) (suc j)) _ ) ⟩ + Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable (suc i) (suc j))) ⟩ + suc i ∎ where + d = proj1 (gcd-dividable (suc i) (suc j)) + f = Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) + open ≤-Reasoning + +gcd-≤ : { i j : ℕ } → 0 < i → 0 < j → gcd i j ≤ i +gcd-≤ {i} {j} 0<i 0<j with <-cmp i j +... | tri< a ¬b ¬c = gcd-≤i i j 0<i (<to≤ a) +... | tri≈ ¬a refl ¬c = gcd-≤i i j 0<i refl-≤ +... | tri> ¬a ¬b c = ≤-trans (subst (λ k → k ≤ j) (gcdsym {j} {i}) (gcd-≤i j i 0<j (<to≤ c))) (<to≤ c) + record Euclid (i j gcd : ℕ ) : Set where field eqa : ℕ @@ -677,36 +733,57 @@ ... | no nx with <-cmp (gcd p x ) 1 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (s≤s (gcd>0 p x (<-trans a<sa 1<p) 0<x) ) ) ... | tri≈ ¬a b ¬c = case1 b - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (prime (gcd p x) {!!} (gcd>0 p x (<-trans a<sa 1<p) 0<x))) {!!} ) where - ge13 : gcd p (gcd p x) ≡ gcd p x - ge13 = {!!} + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (prime (gcd p x) ge13 (<to≤ c) )) ge18 ) where + -- 1 < gcd p x + ge13 : gcd p x < p -- gcd p x ≡ p → ¬ nx + ge13 with <-cmp (gcd p x ) p + ... | tri< a ¬b ¬c = a + ... | tri≈ ¬a b ¬c = ⊥-elim ( nx (subst (λ k → Dividable k x) b (proj2 (gcd-dividable p x )))) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (gcd-≤ (<-trans a<sa 1<p) 0<x) c ) + ge19 : Dividable (gcd p x) p + ge19 = proj1 (gcd-dividable p x ) + ge18 : 1 < gcd p (gcd p x) -- Dividable p (gcd p x) → gcd p (gcd p x) ≡ (gcd p x) > 1 + ge18 = subst (λ k → 1 < k ) (sym (div→gcd {p} {gcd p x} c ge19 )) c ge10 : gcd p a ≡ 1 ge10 with ge12 a 0<a ... | case1 x = x ... | case2 x = ⊥-elim ( np x ) ge11 : Euclid p a (gcd p a) ge11 = gcd-euclid1 p p a a GCDi + ge18 : (Dividable.factor div-ab * Euclid.eqb ge11) * p ≡ b * (a * Euclid.eqb ge11 ) + ge18 = begin + (Dividable.factor div-ab * Euclid.eqb ge11) * p ≡⟨ {!!} ⟩ + (Euclid.eqb ge11 * p) ≡⟨ {!!} ⟩ + (p * Euclid.eqb ge11 ) ≡⟨ {!!} ⟩ + (Dividable.factor div-ab * p ) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ + (Dividable.factor div-ab * p + 0) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ + (a * b) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ + (b * a) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ + b * (a * Euclid.eqb ge11 ) ∎ where open ≡-Reasoning ge14 : ( Euclid.eqa ge11 * p ) ≤ ( Euclid.eqb ge11 * a ) → (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p + 0 ≡ b ge14 lt = begin (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p + 0 ≡⟨ {!!} ⟩ (b * Euclid.eqa ge11 - Dividable.factor div-ab * Euclid.eqb ge11) * p ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * Euclid.eqb ge11) * p ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * Euclid.eqb ge11) * p ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - Dividable.factor div-ab * (Euclid.eqb ge11 * p) ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - Dividable.factor div-ab * (p * Euclid.eqb ge11 ) ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * p ) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - (Dividable.factor div-ab * p + 0) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - (a * b) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - (b * a) * Euclid.eqb ge11 ≡⟨ {!!} ⟩ - (b * Euclid.eqa ge11) * p - b * (a * Euclid.eqb ge11 ) ≡⟨ {!!} ⟩ - b * (Euclid.eqa ge11 * p) - b * (a * Euclid.eqb ge11 ) ≡⟨ {!!} ⟩ + (b * Euclid.eqa ge11) * p - ((Dividable.factor div-ab * Euclid.eqb ge11) * p) ≡⟨ cong (λ k → (b * Euclid.eqa ge11) * p - k ) ge18 ⟩ + (b * Euclid.eqa ge11) * p - (b * (a * Euclid.eqb ge11 )) ≡⟨ {!!} ⟩ + b * (Euclid.eqa ge11 * p) - (b * (a * Euclid.eqb ge11 )) ≡⟨ {!!} ⟩ b * ( Euclid.eqa ge11 * p - a * Euclid.eqb ge11 ) ≡⟨ {!!} ⟩ b * ( Euclid.eqa ge11 * p - Euclid.eqb ge11 * a ) ≡⟨ cong (b *_) {!!} ⟩ b * gcd p a ≡⟨ cong (b *_) ge10 ⟩ b * 1 ≡⟨ m*1=m ⟩ b ∎ where open ≡-Reasoning ge15 : ( Euclid.eqa ge11 * p ) > ( Euclid.eqb ge11 * a ) → (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11 ) * p + 0 ≡ b - ge15 = {!!} + ge15 lt = begin + (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11 ) * p + 0 ≡⟨ {!!} ⟩ + (Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11 ) * p ≡⟨ {!!} ⟩ + ((Dividable.factor div-ab * Euclid.eqb ge11) * p) - ((b * Euclid.eqa ge11) * p) ≡⟨ cong (λ k → k - ((b * Euclid.eqa ge11) * p) ) ge18 ⟩ + (b * (a * Euclid.eqb ge11 )) - ((b * Euclid.eqa ge11) * p ) ≡⟨ {!!} ⟩ + (b * (a * Euclid.eqb ge11 )) - (b * (Euclid.eqa ge11 * p) ) ≡⟨ {!!} ⟩ + b * ( a * Euclid.eqb ge11 - (Euclid.eqa ge11 * p) ) ≡⟨ {!!} ⟩ + b * ( Euclid.eqb ge11 * a - Euclid.eqa ge11 * p ) ≡⟨ cong (b *_) {!!} ⟩ + b * gcd p a ≡⟨ cong (b *_) ge10 ⟩ + b * 1 ≡⟨ m*1=m ⟩ + b ∎ where open ≡-Reasoning ge17 : (x y : ℕ ) → x ≡ y → x ≤ y ge17 x x refl = refl-≤ ge16 : Dividable p b @@ -716,35 +793,6 @@ ... | tri> ¬a ¬b c = record { factor = Dividable.factor div-ab * Euclid.eqb ge11 - b * Euclid.eqa ge11 ; is-factor = ge15 c } -div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k -div→gcd {n} {k} k>1 = n-induction {_} {_} {ℕ} {λ m → Dividable k m → gcd m k ≡ k } (λ x → x) I n where - decl : {m : ℕ } → 0 < m → m - k < m - decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m - ind : (m : ℕ ) → (Dividable k (m - k) → gcd (m - k) k ≡ k) → Dividable k m → gcd m k ≡ k - ind m prev d with <-cmp (suc m) k - ... | tri≈ ¬a refl ¬c = ⊥-elim ( div+1 k>1 d div= ) - ... | tri> ¬a ¬b c = subst (λ g → g ≡ k) ind1 ( prev (proj2 (div-div k>1 div= d))) where - ind1 : gcd (m - k) k ≡ gcd m k - ind1 = begin - gcd (m - k) k ≡⟨ sym (gcd+j (m - k) _) ⟩ - gcd (m - k + k) k ≡⟨ cong (λ g → gcd g k) (minus+n {m} {k} c) ⟩ - gcd m k ∎ where open ≡-Reasoning - ... | tri< a ¬b ¬c with <-cmp 0 m - ... | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim ( div<k k>1 a₁ (<-trans a<sa a) d ) - ... | tri≈ ¬a refl ¬c₁ = subst (λ g → g ≡ k ) (gcdsym {k} {0} ) (gcd20 k) - fzero : (m : ℕ) → (m - k) ≡ zero → Dividable k m → gcd m k ≡ k - fzero 0 eq d = trans (gcdsym {0} {k} ) (gcd20 k) - fzero (suc m) eq d with <-cmp (suc m) k - ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 (s≤s z≤n) a d ) - ... | tri≈ ¬a refl ¬c = gcdmm k k - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (minus>0 c) ) - I : Ninduction ℕ _ (λ x → x) - I = record { - pnext = λ p → p - k - ; fzero = λ {m} eq → fzero m eq - ; decline = λ {m} lt → decl lt - ; ind = λ {p} prev → ind p prev - } gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1 gcdmul+1 zero n = gcd204 n @@ -764,29 +812,6 @@ --gcd-dividable : ( i j : ℕ ) -- → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j -f-div>0 : { k i : ℕ } → (d : Dividable k i ) → 0 < i → 0 < Dividable.factor d -f-div>0 {k} {i} d 0<i with <-cmp 0 (Dividable.factor d) -... | tri< a ¬b ¬c = a -... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (begin - 0 * k + 0 ≡⟨ cong (λ g → g * k + 0) b ⟩ - Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ - i ∎ ) 0<i ) where open ≡-Reasoning - m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1 m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq -gcd-≤ : ( i j : ℕ ) → 0 < i → i ≤ j → gcd i j ≤ i -gcd-≤ zero _ () z≤n -gcd-≤ (suc i) (suc j) _ (s≤s i<j) = begin - gcd (suc i) (suc j) ≡⟨ sym m*1=m ⟩ - gcd (suc i) (suc j) * 1 ≤⟨ *-monoʳ-≤ (gcd (suc i) (suc j)) (f-div>0 d (s≤s z≤n)) ⟩ - gcd (suc i) (suc j) * f ≡⟨ +-comm 0 _ ⟩ - gcd (suc i) (suc j) * f + 0 ≡⟨ cong (λ k → k + 0) (*-comm (gcd (suc i) (suc j)) _ ) ⟩ - Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable (suc i) (suc j))) ⟩ - suc i ∎ where - d = proj1 (gcd-dividable (suc i) (suc j)) - f = Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) - open ≤-Reasoning - -gcd-≥ : ( i j : ℕ ) → 0 < i → i ≤ j → gcd j i ≤ i -gcd-≥ i j 0<i i≤j = subst (λ k → k ≤ i) (gcdsym {i} {j}) ( gcd-≤ i j 0<i i≤j )