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

diff -r 4a00e5f2b793 -r b065ba2f68c5 automaton-in-agda/src/gcd.agda
--- a/automaton-in-agda/src/gcd.agda	Fri Jan 14 14:39:36 2022 +0900
+++ b/automaton-in-agda/src/gcd.agda	Fri Jan 14 19:11:12 2022 +0900
@@ -700,3 +700,75 @@
 gcd-is-gratest {i} {j} {k} i>0 j>0 k>1 ki kj = div→k≤m k>1 (gcd>0 i j i>0 j>0 ) gcd001 where
     gcd001 :  Dividable k ( gcd i  j ) 
     gcd001 = gcd-div _ _ _ k>1 ki kj
+
+gcd-div-1 : {i j : ℕ } → i > 0 → j > 0  → gcd (Dividable.factor (proj1 (gcd-dividable i j))) (Dividable.factor (proj2 (gcd-dividable i j))) ≡ 1
+gcd-div-1 {suc i} {suc j} i>0 j>0 = cop where
+   d : ℕ
+   d = gcd (suc i) (suc j)
+   d>0 : gcd (suc i) (suc j) > 0
+   d>0 = gcd>0 (suc i) (suc j)  (s≤s z≤n ) (s≤s z≤n )
+   id  : Dividable d (suc i)
+   id  = proj1 (gcd-dividable (suc i) (suc j))
+   jd  : Dividable d (suc j)
+   jd  = proj2 (gcd-dividable (suc i) (suc j))
+   cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
+   cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd)
+   ... | zero | record { eq  = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (gcd>0 (Dividable.factor id) (Dividable.factor jd)
+       (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) ))
+   ... | suc zero | record { eq  = eq1 } = refl
+   ... | suc (suc t) | record { eq  = eq1 } = ⊥-elim ( nat-≤> (gcd-is-gratest {suc i} {(suc j)} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where
+        -- gcd-is-gratest :  { i j  k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j
+        d1 : ℕ
+        d1 = gcd (Dividable.factor id) (Dividable.factor jd)
+        d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1
+        d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n))
+        mul1 :  {x : ℕ} → 1 * x ≡ x
+        mul1 {zero} = refl
+        mul1 {suc x} = begin
+              1 * suc x  ≡⟨ cong suc (+-comm x _ ) ⟩
+              suc x ∎   where open ≡-Reasoning
+        co1  : gcd (suc i) (suc j) * d1 > 1
+        co1  = begin
+              2 ≤⟨ d1>1 ⟩
+              d1  ≡⟨ sym mul1 ⟩
+              1 * d1  ≤⟨ *≤ {1} {gcd (suc i) (suc j) } {d1} d>0 ⟩
+              gcd (suc i) (suc j) * d1 ∎   where open ≤-Reasoning
+        gcdd1 = gcd-dividable (Dividable.factor id) (Dividable.factor jd)
+        gcdf1 = Dividable.factor (proj1 gcdd1)
+        gcdf2 = Dividable.factor (proj2 gcdd1)
+        d1id :  Dividable (gcd (suc i) (suc j) * d1) (suc i)
+        d1id = record { factor = gcdf1 ; is-factor = begin
+              gcdf1 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩
+              gcdf1 * (d * d1) ≡⟨ cong (λ k1 → gcdf1 * k1) (*-comm d d1) ⟩
+              gcdf1 * (d1 * d) ≡⟨ sym (*-assoc gcdf1 d1 d) ⟩
+              gcdf1 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩
+              (gcdf1 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf1 * d1) 0)) ⟩
+              (gcdf1 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj1 gcdd1) ) ⟩
+              Dividable.factor id * d + 0 ≡⟨ Dividable.is-factor id ⟩
+              suc i ∎ }  where open ≡-Reasoning
+        d1jd :  Dividable (gcd (suc i) (suc j) * d1) (suc j)
+        d1jd = record { factor = gcdf2 ; is-factor = begin
+              gcdf2 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩
+              gcdf2 * (d * d1) ≡⟨ cong (λ k1 → gcdf2 * k1) (*-comm d d1) ⟩
+              gcdf2 * (d1 * d) ≡⟨ sym (*-assoc gcdf2 d1 d) ⟩
+              gcdf2 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩
+              (gcdf2 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf2 * d1) 0)) ⟩
+              (gcdf2 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj2 gcdd1) ) ⟩
+              Dividable.factor jd * d + 0 ≡⟨ Dividable.is-factor jd ⟩
+              (suc j) ∎ }  where open ≡-Reasoning
+        mul2 : {g d1 : ℕ } → g > 0 → d1 > 1 → g < g * d1
+        mul2 {suc g} {suc zero} g>0 (s≤s ())
+        mul2 {suc g} {suc (suc d2)} g>0 d1>1 = begin
+              suc (suc g) ≡⟨ cong suc (+-comm 0 _ ) ⟩
+              suc (suc g + 0) ≤⟨ s≤s (≤-plus-0  z≤n) ⟩
+              suc (suc g + (g + d2 * suc g)) ≡⟨ cong suc (sym (+-assoc  1 g _) ) ⟩
+              suc ((1 + g) + (g + d2 * suc g)) ≡⟨  cong (λ k → suc (k + (g + d2 * suc g) )) (+-comm 1 g) ⟩
+              suc ((g + 1) + (g + d2 * suc g)) ≡⟨ cong suc (+-assoc g 1 _ )  ⟩
+              suc (g + (1 + (g + d2 * suc g))) ≡⟨⟩
+              suc (g + suc (g + d2 * suc g)) ≡⟨⟩
+              suc (suc d2) * suc g  ≡⟨ *-comm (suc (suc d2)) _ ⟩
+              suc g * suc (suc d2) ∎   where open ≤-Reasoning
+        gcd<d1 : gcd (suc i) (suc j) < gcd (suc i ) (suc j) * d1
+        gcd<d1 = mul2 (gcd>0 (suc i) (suc j) (s≤s z≤n) (s≤s z≤n) ) d1>1
+
+
diff -r 4a00e5f2b793 -r b065ba2f68c5 automaton-in-agda/src/nat.agda
--- a/automaton-in-agda/src/nat.agda	Fri Jan 14 14:39:36 2022 +0900
+++ b/automaton-in-agda/src/nat.agda	Fri Jan 14 19:11:12 2022 +0900
@@ -182,6 +182,9 @@
 *< {zero} {suc y} lt = s≤s z≤n
 *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)
 
+*-cancel-left : {x y z : ℕ } → x > 0 → x * y ≡ x * z → y ≡ z
+*-cancel-left {suc x} {y} {z} x>0 eq = *-cancelˡ-≡ x eq
+
 <to<s : {x y  : ℕ } → x < y → x < suc y
 <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
 <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
diff -r 4a00e5f2b793 -r b065ba2f68c5 automaton-in-agda/src/root2.agda
--- a/automaton-in-agda/src/root2.agda	Fri Jan 14 14:39:36 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jan 14 19:11:12 2022 +0900
@@ -98,90 +98,89 @@
 
 mkRational : ( i j : ℕ ) → 0 < j → Rational
 mkRational zero j 0<j = record { i = 0 ; j = 1 ; coprime = refl  ; 0<j = s≤s z≤n } 
-mkRational (suc i) j (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where
+mkRational (suc i) (suc j) (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where
    d : ℕ
-   d = gcd (suc i) j
-   d>0 : gcd (suc i) j > 0
-   d>0 = GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n )
+   d = gcd (suc i) (suc j)
+   d>0 : gcd (suc i) (suc j) > 0
+   d>0 = GCD.gcd>0 (suc i) (suc j) (s≤s z≤n) (s≤s z≤n )
+   id  : Dividable d (suc i)
+   id  = proj1 (GCD.gcd-dividable (suc i) (suc j))
+   jd  : Dividable d (suc j) 
+   jd  = proj2 (GCD.gcd-dividable (suc i) (suc j))
    0<fj : Dividable.factor jd > 0
    0<fj = 0<factor d>0  (s≤s z≤n ) jd
-   id  : Dividable d (suc i)
-   id  = proj1 (GCD.gcd-dividable (suc i) j)
-   jd  : Dividable d j 
-   jd  = proj2 (GCD.gcd-dividable (suc i) j)
    cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
-   cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd)
-   ... | zero | record { eq  = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (GCD.gcd>0 (Dividable.factor id) (Dividable.factor jd)
-       (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) ))
-   ... | suc zero | record { eq  = eq1 } = refl
-   ... | suc (suc t) | record { eq  = eq1 } = ⊥-elim ( nat-≤> (GCD.gcd-is-gratest {suc i} {j} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where
-        -- gcd-is-gratest :  { i j  k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j
-        d1 : ℕ
-        d1 = gcd (Dividable.factor id) (Dividable.factor jd) 
-        d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1
-        d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n))
-        mul1 :  {x : ℕ} → 1 * x ≡ x
-        mul1 {zero} = refl
-        mul1 {suc x} = begin
-              1 * suc x  ≡⟨ cong suc (+-comm x _ ) ⟩ 
-              suc x ∎   where open ≡-Reasoning
-        co1  : gcd (suc i) j * d1 > 1
-        co1  = begin
-              2 ≤⟨ d1>1 ⟩ 
-              d1  ≡⟨ sym mul1 ⟩ 
-              1 * d1  ≤⟨ *≤ {1} {gcd (suc i) j } {d1} d>0 ⟩ 
-              gcd (suc i) j * d1 ∎   where open ≤-Reasoning
-        gcdd1 = GCD.gcd-dividable (Dividable.factor id) (Dividable.factor jd)
-        gcdf1 = Dividable.factor (proj1 gcdd1)
-        gcdf2 = Dividable.factor (proj2 gcdd1)
-        d1id :  Dividable (gcd (suc i) j * d1) (suc i)
-        d1id = record { factor = gcdf1 ; is-factor = begin
-              gcdf1 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ 
-              gcdf1 * (d * d1) ≡⟨ cong (λ k1 → gcdf1 * k1) (*-comm d d1) ⟩ 
-              gcdf1 * (d1 * d) ≡⟨ sym (*-assoc gcdf1 d1 d) ⟩ 
-              gcdf1 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ 
-              (gcdf1 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf1 * d1) 0)) ⟩ 
-              (gcdf1 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj1 gcdd1) ) ⟩ 
-              Dividable.factor id * d + 0 ≡⟨ Dividable.is-factor id ⟩ 
-              suc i ∎ }  where open ≡-Reasoning
-        d1jd :  Dividable (gcd (suc i) j * d1) j
-        d1jd = record { factor = gcdf2 ; is-factor = begin
-              gcdf2 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ 
-              gcdf2 * (d * d1) ≡⟨ cong (λ k1 → gcdf2 * k1) (*-comm d d1) ⟩ 
-              gcdf2 * (d1 * d) ≡⟨ sym (*-assoc gcdf2 d1 d) ⟩ 
-              gcdf2 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ 
-              (gcdf2 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf2 * d1) 0)) ⟩ 
-              (gcdf2 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj2 gcdd1) ) ⟩ 
-              Dividable.factor jd * d + 0 ≡⟨ Dividable.is-factor jd ⟩ 
-              j ∎ }  where open ≡-Reasoning
-        mul2 : {g d1 : ℕ } → g > 0 → d1 > 1 → g < g * d1
-        mul2 {suc g} {suc zero} g>0 (s≤s ())
-        mul2 {suc g} {suc (suc d2)} g>0 d1>1 = begin
-              suc (suc g) ≡⟨ cong suc (+-comm 0 _ ) ⟩ 
-              suc (suc g + 0) ≤⟨ s≤s (≤-plus-0  z≤n) ⟩ 
-              suc (suc g + (g + d2 * suc g)) ≡⟨ cong suc (sym (+-assoc  1 g _) ) ⟩ 
-              suc ((1 + g) + (g + d2 * suc g)) ≡⟨  cong (λ k → suc (k + (g + d2 * suc g) )) (+-comm 1 g) ⟩ 
-              suc ((g + 1) + (g + d2 * suc g)) ≡⟨ cong suc (+-assoc g 1 _ )  ⟩ 
-              suc (g + (1 + (g + d2 * suc g))) ≡⟨⟩ 
-              suc (g + suc (g + d2 * suc g)) ≡⟨⟩ 
-              suc (suc d2) * suc g  ≡⟨ *-comm (suc (suc d2)) _ ⟩ 
-              suc g * suc (suc d2) ∎   where open ≤-Reasoning
-        gcd<d1 : gcd (suc i) j < gcd (suc i ) j * d1
-        gcd<d1 = mul2 (GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n) ) d1>1 
+   cop = GCD.gcd-div-1 {suc i} {suc j} (s≤s z≤n) (s≤s z≤n )
 
-
-Rational* : (r s : Rational) → Rational
-Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) ) where
-    r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0
-    r1 {x} {y} x>0 y>0 = begin
+r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0
+r1 {x} {y} x>0 y>0 = begin
         1 * 1 ≤⟨ *≤ {1} {x} {1} x>0 ⟩
         x * 1 ≡⟨ *-comm x 1  ⟩
         1 * x ≤⟨ *≤ {1} {y} {x} y>0 ⟩
         y * x ≡⟨ *-comm y x ⟩
         x * y ∎ where open ≤-Reasoning
 
+Rational* : (r s : Rational) → Rational
+Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) ) 
+
 _r=_ : Rational → ℕ → Set
-r r= n  = (Rational.i r ≡ n) ∧ (Rational.j r ≡ 1)
+r r= p  = p * Rational.j r ≡ Rational.i r 
+
+r3 : ( p : ℕ ) → p > 0 → ( r  : Rational ) →  Rational* r r r= p →  p * Rational.j r * Rational.j r ≡ Rational.i r * Rational.i r
+r3 p p>0 r rr = r4 where
+    i : ℕ
+    i = Rational.i r * Rational.i r
+    j : ℕ
+    j = Rational.j r * Rational.j r
+    0<j : 0 < j
+    0<j = r1 (Rational.0<j r) (Rational.0<j r)
+    d1 = Dividable.factor (proj1 (GCD.gcd-dividable i j)) 
+    d2 = Dividable.factor (proj2 (GCD.gcd-dividable i j)) 
+    ri=id :  ( i j : ℕ) → (0<i : 0 < i ) → (0<j : 0 < j)  
+        →  Rational.i (mkRational i j 0<j) ≡ Dividable.factor (proj1 (GCD.gcd-dividable i j))
+    ri=id (suc i₁) (suc j₁) 0<i (s≤s 0<j₁) = refl
+    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
+    d : ℕ
+    d = gcd i j
+    r7 : i > 0 → d > 0
+    r7 0<i = GCD.gcd>0 _ _ 0<i 0<j
+    r6 :  i > 0 → d2 > 0
+    r6 0<i = 0<factor (r7 0<i ) 0<j (proj2 (GCD.gcd-dividable i j)) 
+    r8 : 0 < i → d2 * p ≡ d1
+    r8 0<i = begin
+      d2 * p ≡⟨ *-comm d2 p ⟩
+      p * d2  ≡⟨ cong (λ k → p * k ) (sym (ri=jd i j 0<i 0<j ))  ⟩
+      p *  Rational.j (mkRational i j  _ ) ≡⟨ rr ⟩
+      Rational.i (Rational* r r) ≡⟨ ri=id i j 0<i 0<j ⟩
+      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 = 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 ≡⟨ 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  ≡⟨ {!!} ⟩
+      (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 ≡⟨ {!!} ⟩
+      d * (d2 * (Rational.i r * Rational.i r)) ∎ )  ⟩
+      d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
+      Rational.i r * Rational.i r  ∎ where open ≡-Reasoning
+
+    
 
 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r  : Rational ) → ¬ ( Rational* r r r= p )
-root-prime-irrational1 p pr r div = root-prime-irrational (Rational.i r) (Rational.j r) {!!} {!!} pr {!!} {!!} (Rational.coprime r) 
+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 with <-cmp (Rational.i r) 1
+... | tri< a ¬b₁ ¬c = {!!}
+... | tri≈ ¬a₁ b ¬c = {!!}
+... | 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) )