Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 406:a60132983557

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 Wed, 08 Nov 2023 21:35:54 +0900
parents af8f630b7e60
children
comparison
equal deleted inserted replaced
405:af8f630b7e60 406:a60132983557
195 (d * d2) * i ≡⟨ *-assoc d _ _ ⟩ 195 (d * d2) * i ≡⟨ *-assoc d _ _ ⟩
196 d * (d2 * (Rational.i r * Rational.i r)) ∎ ) ⟩ 196 d * (d2 * (Rational.i r * Rational.i r)) ∎ ) ⟩
197 d2 * (Rational.i r * Rational.i r) ∎ ) ⟩ 197 d2 * (Rational.i r * Rational.i r) ∎ ) ⟩
198 Rational.i r * Rational.i r ∎ where open ≡-Reasoning 198 Rational.i r * Rational.i r ∎ where open ≡-Reasoning
199 199
200 -- data _≤_ : (i j : ℕ) → Set where
201 -- z≤n : {n : ℕ} → zero ≤ n
202 -- s≤s : {i j : ℕ} → i ≤ j → (suc i) ≤ (suc j)
203
200 *<-2 : {x y z : ℕ} → z > 0 → x < y → z * x < z * y 204 *<-2 : {x y z : ℕ} → z > 0 → x < y → z * x < z * y
201 *<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y 205 *<-2 {zero} {suc y} {suc z} (s≤s z>0) x<y = begin
206 suc (z * zero) ≡⟨ cong suc (*-comm z _) ⟩
207 suc (zero * z) ≡⟨ refl ⟩
208 suc zero ≤⟨ s≤s z≤n ⟩
209 suc (y + z * suc y) ∎ where open ≤-Reasoning
210 *<-2 {x} {y} {suc zero} (s≤s z>0) x<y = begin
211 suc (x + zero) ≡⟨ cong suc (+-comm x _) ⟩
212 suc x ≤⟨ x<y ⟩
213 y ≡⟨ +-comm zero _ ⟩
214 y + zero ∎ where open ≤-Reasoning
215 *<-2 {x} {y} {suc (suc z)} (s≤s z>0) x<y = begin
216 suc (x + (x + z * x)) <⟨ +-mono-≤-< x<y (*<-2 {x} {y} {suc z} (s≤s z≤n) x<y) ⟩
217 y + (y + z * y) ∎ where open ≤-Reasoning
202 218
203 r15 : {p : ℕ} → p > 1 → p < p * p 219 r15 : {p : ℕ} → p > 1 → p < p * p
204 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 ) 220 r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )
205 221
206 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r : Rational ) → ¬ ( Rational* r r r= p ) 222 root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r : Rational ) → ¬ ( Rational* r r r= p )