Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 405:af8f630b7e60

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 Sun, 24 Sep 2023 18:02:04 +0900
parents 407684f806e4
children a60132983557
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 module root2 where 3 module root2 where
2 4
3 open import Data.Nat 5 open import Data.Nat
4 open import Data.Nat.Properties 6 open import Data.Nat.Properties
5 open import Data.Empty 7 open import Data.Empty
84 -- p * n * n = 2m' 2m' 86 -- p * n * n = 2m' 2m'
85 -- n * n = m' 2m' 87 -- n * n = m' 2m'
86 df = Dividable.factor dm 88 df = Dividable.factor dm
87 dn : Dividable p n 89 dn : Dividable p n
88 dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin 90 dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin
89 df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin 91 df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ (suc p0) ( begin
90 (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩ 92 (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩
91 ((df * df) * p ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩ 93 ((df * df) * p ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
92 (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩ 94 (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩
93 (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩ 95 (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
94 ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p ⟩ 96 ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p ⟩
194 d * (d2 * (Rational.i r * Rational.i r)) ∎ ) ⟩ 196 d * (d2 * (Rational.i r * Rational.i r)) ∎ ) ⟩
195 d2 * (Rational.i r * Rational.i r) ∎ ) ⟩ 197 d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
196 Rational.i r * Rational.i r ∎ where open ≡-Reasoning 198 Rational.i r * Rational.i r ∎ where open ≡-Reasoning
197 199
198 *<-2 : {x y z : ℕ} → z > 0 → x < y → z * x < z * y 200 *<-2 : {x y z : ℕ} → z > 0 → x < y → z * x < z * y
199 *<-2 {x} {y} {suc z} (s≤s z>0) x<y = *-monoʳ-< z x<y 201 *<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y
200 202
201 r15 : {p : ℕ} → p > 1 → p < p * p 203 r15 : {p : ℕ} → p > 1 → p < p * p
202 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 ) 204 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )
203 205
204 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r : Rational ) → ¬ ( Rational* r r r= p ) 206 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r : Rational ) → ¬ ( Rational* r r r= p )