Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 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
comparison
equal deleted inserted replaced
322:596913103389 323:7f806a28a866
198 i = Rational.i r 198 i = Rational.i r
199 j = Rational.j r 199 j = Rational.j r
200 r00 : p * j * j ≡ i * i 200 r00 : p * j * j ≡ i * i
201 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div 201 r00 = r3 p (<-trans a<sa (Prime.p>1 pr )) r div
202 r01 : p ≡ i * i 202 r01 : p ≡ i * i
203 r01 = {!!} 203 r01 = begin
204 r02 : (i : ℕ) → p ≡ i * i → gcd p i ≡ i 204 p ≡⟨ sym m*1=m ⟩
205 r02 = {!!} 205 p * 1 ≡⟨ sym m*1=m ⟩
206 p * 1 * 1 ≡⟨ cong (λ k → p * k * k ) (sym b) ⟩
207 p * j * j ≡⟨ r00 ⟩
208 i * i ∎ where open ≡-Reasoning
206 r03 : p ≡ i * i → i > 1 209 r03 : p ≡ i * i → i > 1
207 r03 = {!!} 210 r03 eq with <-cmp i 1
211 ... | tri< a ¬b ¬c = {!!}
212 ... | tri≈ ¬a b ¬c = {!!}
213 ... | tri> ¬a ¬b c = c
214 r02 : p ≡ i * i → gcd p i ≡ i
215 r02 eq = GCD.div→gcd (r03 r01) record { factor = i ; is-factor = trans (+-comm _ 0 ) (sym r01) }
208 r04 : 1 ≡ i 216 r04 : 1 ≡ i
209 r04 = begin 217 r04 = begin
210 1 ≡⟨ {!!} ⟩ 218 1 ≡⟨ sym (Prime.isPrime pr _ {!!} {!!} ) ⟩
211 gcd p i ≡⟨ {!!} ⟩ 219 gcd p i ≡⟨ r02 r01 ⟩
212 i ∎ where open ≡-Reasoning 220 i ∎ where open ≡-Reasoning
213 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1 221 ... | tri> ¬a ¬b c with <-cmp (Rational.i r) 1
214 ... | tri< a ¬b₁ ¬c = {!!} where 222 ... | tri< a ¬b₁ ¬c = {!!} where
215 i = Rational.i r 223 i = Rational.i r
216 j = Rational.j r 224 j = Rational.j r