Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/root2.agda @ 231:54977cc189e6
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 25 Jun 2021 08:49:12 +0900 (2021-06-24) |
parents | 4a83abf7b822 |
children | 327094b57ee2 |
line wrap: on
line diff
--- a/automaton-in-agda/src/root2.agda Thu Jun 24 11:02:58 2021 +0900 +++ b/automaton-in-agda/src/root2.agda Fri Jun 25 08:49:12 2021 +0900 @@ -11,19 +11,61 @@ open import gcd open import even open import nat +open import logic record Rational : Set where field i j : ℕ coprime : gcd i j ≡ 1 -even→gcd=2 : {n : ℕ} → even n → gcd n 2 ≡ 2 -even→gcd=2 {zero} en = refl -even→gcd=2 {suc (suc zero)} en = refl -even→gcd=2 {suc (suc (suc (suc n)))} en = begin - gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩ - gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en ⟩ - 2 ∎ where open ≡-Reasoning +open _∧_ + +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 + } + +-- n ≡ i * k + r +-- n^2 = (i * k)^2 + i * r * k + r^2 +-- r^2 | k yes → jj + +open import prime + +-- equlid : ( n m k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k m +-- equlid = {!!} + +-- divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n +-- divdable^2 zero zero 1<k 1<n pk dn2 = {!!} +-- divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k +-- ... | yes y = y +-- ... | no non with equlid (suc n) (suc n) (suc k) 1<k {!!} pk dn2 +-- ... | case1 dn = dn +-- ... | case2 dm = dm even^2 : {n : ℕ} → even ( n * n ) → even n even^2 {n} en with even? n