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

diff -r 012f79b51dba -r 24c721da4f27 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Tue Jun 29 23:24:03 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Tue Jun 29 23:53:19 2021 +0900
@@ -36,48 +36,50 @@
 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
 --    → Dividable k ( gcd i  j )
 
-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
+root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1  →  p * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
+root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn))) 
+root-prime-irrational n m (suc p0) n>1 pn m>1 pnm = rot13 ( gcd-div n m (suc p0) 1<sp dn dm ) where 
+    p = suc (p0)
+    1<sp : 1 < p
     1<sp = Prime.p>1 pn
-    rot13 : {m : ℕ } → Dividable (suc p) m →  m ≡ 1 → ⊥
+    rot13 : {m : ℕ } → Dividable p m →  m ≡ 1 → ⊥
     rot13 d refl with Dividable.factor d | Dividable.is-factor d
     ... | 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
+    ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1 
+        rot17 : suc n * 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 ⟩
+           suc (1 * 1 ) ≤⟨ 1<sp  ⟩
+           suc p0  ≡⟨ cong suc (+-comm 0 _) ⟩ 
+           suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩ 
+           suc (p0 + n * p )  ≡⟨ +-comm 0 _ ⟩
+           suc n * p + 0 ∎   where open ≤-Reasoning
+    dm : Dividable p m
+    dm = divdable^2 m p 1<sp m>1 pn record { factor = n * n ; is-factor = begin
+       (n * n) * p + 0 ≡⟨  +-comm _ 0 ⟩
+       (n * n) * p  ≡⟨ *-comm (n * n) p ⟩
+       p * (n * n)  ≡⟨ sym (*-assoc p n n)  ⟩
+       (p * n) * n ≡⟨ pnm ⟩
        m * m ∎ }  where open ≡-Reasoning
-     -- (suc p) * n * n = 2m' 2m'
+     -- p * n * n = 2m' 2m'
      --  n * n = m' 2m'
     df = Dividable.factor dm
-    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 )⟩
+    dn : Dividable p n
+    dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df  ; is-factor = begin
+        df * df * p + 0  ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin 
+          (df * df * p + 0) * p ≡⟨  cong (λ k → k * p)  (+-comm (df * df * p) 0)  ⟩
+            ((df * df) * p) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
+            (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p)  ⟩
+            (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
+            ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p  ⟩
+            (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩
+          (df * p + 0) * (df * 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) ∎  ) ⟩
+          p * n * n   ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩
+            n * p * n   ≡⟨ *-assoc n p n ⟩
+            n * (p * n)   ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩
+            n * (n * p)   ≡⟨ sym (*-assoc n n p) ⟩
+          n * n * p ∎  ) ⟩
        n * n ∎ }  where open ≡-Reasoning