# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1624976643 -32400
# Node ID 012f79b51dba4c9add648cb0f76407278c09375a
# Parent  9fc9e19f2c37dd52106b773666541eb8ea30da97
... prime version

diff -r 9fc9e19f2c37 -r 012f79b51dba automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Tue Jun 29 20:03:32 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Tue Jun 29 23:24:03 2021 +0900
@@ -33,46 +33,51 @@
 ... | case1 dn = dn
 ... | case2 dm = dm
 
-p2 : Prime 2
-p2 = record { p>1 = a<sa ; isPrime = p22 } where
-   p22 : (j : ℕ) → j < 2 → 0 < j → gcd 2 j ≡ 1
-   p22 1 (s≤s (s≤s z≤n)) (s≤s 0<j) = refl
-
 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
 --    → Dividable k ( gcd i  j )
 
-root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
-root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) dn dm ) where 
-    rot13 : {m : ℕ } → Dividable 2 m →  m ≡ 1 → ⊥
+root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime (suc p) → m > 1  →  (suc p) * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
+root-prime-irrational n m p n>1 pn m>1 pnm = rot13 ( gcd-div n m (suc p) 1<sp dn dm ) where 
+    1<sp : 1 < suc p
+    1<sp = Prime.p>1 pn
+    rot13 : {m : ℕ } → Dividable (suc p) m →  m ≡ 1 → ⊥
     rot13 d refl with Dividable.factor d | Dividable.is-factor d
-    ... | zero | ()
-    ... | suc n | ()
-    dm : Dividable 2 m
-    dm = divdable^2 m 2 a<sa m>1 p2 record { factor = n * n ; is-factor = begin
-       (n * n) * 2 + 0 ≡⟨  +-comm _ 0 ⟩
-       (n * n) * 2  ≡⟨ *-comm (n * n) 2 ⟩
-       2 * (n * n)  ≡⟨ sym (*-assoc 2 n n)  ⟩
-       (2 * n) * n ≡⟨ 2nm  ⟩
+    ... | zero | ()   -- gcd 0 m ≡ 1
+    ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * suc p + 0) ≡ 1 
+        rot17 : suc n * suc p + 0 > 1
+        rot17 = begin
+           2 ≡⟨ refl ⟩
+           suc (1 * 1 )  ≤⟨ {!!}  ⟩
+           suc (1 * suc p )  <⟨ {!!}  ⟩
+           suc (0 + n * suc p )  ≤⟨ {!!}  ⟩
+           suc (p + n * suc p )  ≡⟨ +-comm 0 _ ⟩
+           suc n * suc p + 0 ∎   where open ≤-Reasoning
+    dm : Dividable (suc p) m
+    dm = divdable^2 m (suc p) 1<sp m>1 pn record { factor = n * n ; is-factor = begin
+       (n * n) * (suc p) + 0 ≡⟨  +-comm _ 0 ⟩
+       (n * n) * (suc p)  ≡⟨ *-comm (n * n) (suc p) ⟩
+       (suc p) * (n * n)  ≡⟨ sym (*-assoc (suc p) n n)  ⟩
+       (suc p * n) * n ≡⟨ pnm ⟩
        m * m ∎ }  where open ≡-Reasoning
-     -- 2 * n * n = 2m' 2m'
+     -- (suc p) * n * n = 2m' 2m'
      --  n * n = m' 2m'
     df = Dividable.factor dm
-    dn : Dividable 2 n
-    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = df * df  ; is-factor = begin
-        df * df * 2 + 0  ≡⟨ *-cancelʳ-≡ _ _ {1} ( begin 
-          (df * df * 2 + 0) * 2 ≡⟨  cong (λ k → k * 2)  (+-comm (df * df * 2) 0)  ⟩
-          ((df * df) * 2) * 2 ≡⟨ cong (λ k → k * 2) (*-assoc df df 2 ) ⟩
-          (df * (df * 2)) * 2 ≡⟨ cong (λ k → (df * k ) * 2) (*-comm df 2)  ⟩
-          (df * (2 * df)) * 2 ≡⟨ sym ( cong (λ k → k * 2) (*-assoc df 2 df ) ) ⟩
-          ((df * 2) * df) * 2 ≡⟨ *-assoc (df * 2) df 2  ⟩
-          (df * 2) * (df * 2) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * 2)) (+-comm 0 _) ⟩
-          (df * 2 + 0) * (df * 2 + 0)   ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
-          m * m   ≡⟨ sym 2nm ⟩
-          2 * n * n   ≡⟨ cong (λ k → k * n) (*-comm 2 n) ⟩
-          n * 2 * n   ≡⟨ *-assoc n 2 n ⟩
-          n * (2 * n)   ≡⟨ cong (λ k → n * k) (*-comm 2 n) ⟩
-          n * (n * 2)   ≡⟨ sym (*-assoc n n 2) ⟩
-          n * n * 2 ∎  ) ⟩
+    dn : Dividable (suc p) n
+    dn = divdable^2 n (suc p) 1<sp n>1 pn record { factor = df * df  ; is-factor = begin
+        df * df * (suc p) + 0  ≡⟨ *-cancelʳ-≡ _ _ {p} ( begin 
+          (df * df * (suc p) + 0) * (suc p) ≡⟨  cong (λ k → k * (suc p))  (+-comm (df * df * (suc p)) 0)  ⟩
+          ((df * df) * (suc p)) * (suc p) ≡⟨ cong (λ k → k * (suc p)) (*-assoc df df (suc p) ) ⟩
+          (df * (df * (suc p))) * (suc p) ≡⟨ cong (λ k → (df * k ) * (suc p)) (*-comm df (suc p))  ⟩
+          (df * ((suc p) * df)) * (suc p) ≡⟨ sym ( cong (λ k → k * (suc p)) (*-assoc df (suc p) df ) ) ⟩
+          ((df * (suc p)) * df) * (suc p) ≡⟨ *-assoc (df * (suc p)) df (suc p)  ⟩
+          (df * (suc p)) * (df * (suc p)) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * (suc p))) (+-comm 0 _) ⟩
+          (df * (suc p) + 0) * (df * (suc p) + 0)   ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
+          m * m   ≡⟨ sym pnm ⟩
+          (suc p) * n * n   ≡⟨ cong (λ k → k * n) (*-comm (suc p) n) ⟩
+          n * (suc p) * n   ≡⟨ *-assoc n (suc p) n ⟩
+          n * (suc p * n)   ≡⟨ cong (λ k → n * k) (*-comm (suc p) n) ⟩
+          n * (n * suc p)   ≡⟨ sym (*-assoc n n (suc p)) ⟩
+          n * n * (suc p) ∎  ) ⟩
        n * n ∎ }  where open ≡-Reasoning