Mercurial > hg > Members > kono > Proof > automaton

changeset 323:7f806a28a866

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Jan 2022 22:39:40 +0900
parents 596913103389
children 329adb1b71c7
files automaton-in-agda/src/root2.agda
diffstat 1 files changed, 14 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/root2.agda	Fri Jan 14 21:47:24 2022 +0900
+++ b/automaton-in-agda/src/root2.agda	Fri Jan 14 22:39:40 2022 +0900
@@ -200,15 +200,23 @@
      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 = {!!}
+     r01 = begin
+      p  ≡⟨ sym m*1=m  ⟩
+      p * 1  ≡⟨ sym m*1=m ⟩
+      p * 1 * 1   ≡⟨ cong (λ k → p * k * k ) (sym b) ⟩
+      p * j * j   ≡⟨ r00 ⟩
+      i * i  ∎ where open ≡-Reasoning
      r03 : p ≡ i * i → i > 1
-     r03 = {!!}
+     r03 eq with <-cmp i 1
+     ... | tri< a ¬b ¬c = {!!}
+     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri> ¬a ¬b c = c
+     r02 : p ≡ i * i → gcd p i ≡ i 
+     r02 eq = GCD.div→gcd (r03 r01) record { factor = i ; is-factor = trans  (+-comm _ 0 ) (sym r01) }
      r04 :  1 ≡ i
      r04 = begin
-      1 ≡⟨ {!!} ⟩
-      gcd p i   ≡⟨ {!!} ⟩
+      1 ≡⟨ sym (Prime.isPrime pr _ {!!} {!!} ) ⟩
+      gcd p i   ≡⟨ r02 r01 ⟩
       i ∎ where open ≡-Reasoning
 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
 ... | tri< a ¬b₁ ¬c = {!!} where