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