# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1642164444 -32400
# Node ID 596913103389ec6f621dfdad6f8d0b7f87ebfe5b
# Parent  b065ba2f68c54168d52afba8078f7f6e4d83407c
...

diff -r b065ba2f68c5 -r 596913103389 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Fri Jan 14 19:11:12 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jan 14 21:47:24 2022 +0900
@@ -142,6 +142,12 @@
     ri=jd :  ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j)  
         →  Rational.j (mkRational i j 0<j) ≡ Dividable.factor (proj2 (GCD.gcd-dividable i j))
     ri=jd (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl
+    r0=id :  ( i j : ℕ) → (0=i : 0 ≡ i ) → (0<j : 0 < j)  
+        →  Rational.i (mkRational i j 0<j) ≡ 0
+    r0=id  0 j refl 0<j = refl
+    r0=jd :  ( i j : ℕ) → (0=i : 0 ≡ i ) → (0<j : 0 < j)  
+        →  Rational.j (mkRational i j 0<j) ≡ 1
+    r0=jd  0 j refl 0<j = refl
     d : ℕ
     d = gcd i j
     r7 : i > 0 → d > 0
@@ -157,18 +163,28 @@
       d1 ∎ where open ≡-Reasoning
     r4 : p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r
     r4 with <-cmp (Rational.i r * Rational.i r) 0
-    ... | tri≈ ¬a b ¬c = {!!}
+    ... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< (begin
+        0 ≡⟨ sym (r0=id i j (sym b) 0<j ) ⟩
+        Rational.i (mkRational (Rational.i r * Rational.i r) (Rational.j r * Rational.j r) _ ) ≡⟨ sym rr ⟩
+        p *  Rational.j (mkRational (Rational.i r * Rational.i r) (Rational.j r * Rational.j r) _ ) ≡⟨ cong (λ k → p * k ) (r0=jd i j (sym b) 0<j ) ⟩
+        p *  1  ≡⟨ m*1=m  ⟩
+        p ∎ ) p>0 ) where open ≡-Reasoning
     ... | tri> ¬a ¬b c = begin
       p * Rational.j r * Rational.j r  ≡⟨ *-cancel-left (r6 c) ( begin
-      d2 * (p * Rational.j r * Rational.j r)  ≡⟨ {!!} ⟩
+      d2 * ((p * Rational.j r) * Rational.j r)  ≡⟨ sym (*-assoc d2 _ _) ⟩
+      (d2 * ( p *  Rational.j r )) * Rational.j r ≡⟨ cong (λ k → k *  Rational.j r) (sym (*-assoc d2 _ _ )) ⟩
       (d2 * p) * Rational.j r * Rational.j r ≡⟨ cong (λ k → k *  Rational.j r * Rational.j r) (r8 c) ⟩
       d1 * Rational.j r * Rational.j r  ≡⟨ *-cancel-left (r7 c) ( begin 
-      d * (d1 * Rational.j r * Rational.j r)  ≡⟨ {!!} ⟩
-      d * d1 * Rational.j r * Rational.j r  ≡⟨ {!!} ⟩
+      d * ((d1 * Rational.j r) * Rational.j r)  ≡⟨ cong (λ k → d * k ) (*-assoc d1 _ _ )⟩
+      d * (d1 * (Rational.j r * Rational.j r))  ≡⟨ sym (*-assoc d _ _) ⟩
+      (d * d1) * (Rational.j r * Rational.j r)  ≡⟨ cong (λ k → k * j) (*-comm d _ ) ⟩
+      (d1 * d) * j  ≡⟨  cong (λ k → k * j) (+-comm 0 (d1 * d)  ) ⟩
       (d1 * d + 0) * j  ≡⟨ cong (λ k → k * j ) (Dividable.is-factor  (proj1 (GCD.gcd-dividable i j)) ) ⟩
       i * j ≡⟨ *-comm i j ⟩
       j * i ≡⟨ cong (λ k → k * i ) (sym (Dividable.is-factor (proj2 (GCD.gcd-dividable i j))) ) ⟩
-      (d2 * GCD.gcd i j + 0) * i ≡⟨ {!!} ⟩
+      (d2 * GCD.gcd i j + 0) * i ≡⟨  cong (λ k → k * i ) (+-comm (d2 * d )  0) ⟩
+      (d2 * d) * i ≡⟨ cong (λ k → k * i ) (*-comm d2 _ ) ⟩
+      (d * d2) * i ≡⟨ *-assoc d _ _ ⟩
       d * (d2 * (Rational.i r * Rational.i r)) ∎ )  ⟩
       d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
       Rational.i r * Rational.i r  ∎ where open ≡-Reasoning
@@ -178,9 +194,38 @@
 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r  : Rational ) → ¬ ( Rational* r r r= p )
 root-prime-irrational1 p pr r div  with <-cmp (Rational.j r) 1
 ... | tri< a ¬b ¬c = ⊥-elim (nat-≤> (Rational.0<j r) a )
-... | tri≈ ¬a b ¬c = {!!}
+... | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< r04 (r03 r01)) where
+     i = Rational.i r
+     j = Rational.j r
+     r00 : p * j * j ≡ i * i
+     r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
+     r01 : p ≡ i * i
+     r01 = {!!} 
+     r02 : (i : ℕ) → p ≡ i * i → gcd p i ≡ i 
+     r02 = {!!}
+     r03 : p ≡ i * i → i > 1
+     r03 = {!!}
+     r04 :  1 ≡ i
+     r04 = begin
+      1 ≡⟨ {!!} ⟩
+      gcd p i   ≡⟨ {!!} ⟩
+      i ∎ where open ≡-Reasoning
 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
-... | tri< a ¬b₁ ¬c = {!!}
-... | tri≈ ¬a₁ b ¬c = {!!}
+... | tri< a ¬b₁ ¬c = {!!} where
+     i = Rational.i r
+     j = Rational.j r
+     r00 : p * j * j ≡ i * i
+     r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
+     r06 : i ≡ 0
+     r06 = {!!}
+     r05 : p * j * j ≡ i * i  -- j > 0 → p * j * j > 0
+     r05 = {!!}
+... | tri≈ ¬a₁ b ¬c = {!!} where
+     i = Rational.i r
+     j = Rational.j r
+     r00 : p * j * j ≡ i * i
+     r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
+     r07 : p * j * j ≡ i * i  -- j > 0 → p * j * j > 0
+     r07 = {!!}
 ... | tri> ¬a₁ ¬b₁ c₁ = root-prime-irrational (Rational.j r) (Rational.i r) p c pr c₁ (r3 p (<-trans a<sa (Prime.p>1 pr ) ) r div)
     (trans (GCD.gcdsym {Rational.j r} {_} ) (Rational.coprime r) )