Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 253:012f79b51dba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... prime version
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 29 Jun 2021 23:24:03 +0900
parents 9d2cba39b33c
children 24c721da4f27
comparison
equal deleted inserted replaced
252:9fc9e19f2c37 253:012f79b51dba
31 ... | yes y = y 31 ... | yes y = y
32 ... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2 32 ... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2
33 ... | case1 dn = dn 33 ... | case1 dn = dn
34 ... | case2 dm = dm 34 ... | case2 dm = dm
35 35
36 p2 : Prime 2
37 p2 = record { p>1 = a<sa ; isPrime = p22 } where
38 p22 : (j : ℕ) → j < 2 → 0 < j → gcd 2 j ≡ 1
39 p22 1 (s≤s (s≤s z≤n)) (s≤s 0<j) = refl
40
41 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j ) 36 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
42 -- → Dividable k ( gcd i j ) 37 -- → Dividable k ( gcd i j )
43 38
44 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1 → 2 * n * n ≡ m * m → ¬ (gcd n m ≡ 1) 39 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime (suc p) → m > 1 → (suc p) * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
45 root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) dn dm ) where 40 root-prime-irrational n m p n>1 pn m>1 pnm = rot13 ( gcd-div n m (suc p) 1<sp dn dm ) where
46 rot13 : {m : ℕ } → Dividable 2 m → m ≡ 1 → ⊥ 41 1<sp : 1 < suc p
42 1<sp = Prime.p>1 pn
43 rot13 : {m : ℕ } → Dividable (suc p) m → m ≡ 1 → ⊥
47 rot13 d refl with Dividable.factor d | Dividable.is-factor d 44 rot13 d refl with Dividable.factor d | Dividable.is-factor d
48 ... | zero | () 45 ... | zero | () -- gcd 0 m ≡ 1
49 ... | suc n | () 46 ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * suc p + 0) ≡ 1
50 dm : Dividable 2 m 47 rot17 : suc n * suc p + 0 > 1
51 dm = divdable^2 m 2 a<sa m>1 p2 record { factor = n * n ; is-factor = begin 48 rot17 = begin
52 (n * n) * 2 + 0 ≡⟨ +-comm _ 0 ⟩ 49 2 ≡⟨ refl ⟩
53 (n * n) * 2 ≡⟨ *-comm (n * n) 2 ⟩ 50 suc (1 * 1 ) ≤⟨ {!!} ⟩
54 2 * (n * n) ≡⟨ sym (*-assoc 2 n n) ⟩ 51 suc (1 * suc p ) <⟨ {!!} ⟩
55 (2 * n) * n ≡⟨ 2nm ⟩ 52 suc (0 + n * suc p ) ≤⟨ {!!} ⟩
53 suc (p + n * suc p ) ≡⟨ +-comm 0 _ ⟩
54 suc n * suc p + 0 ∎ where open ≤-Reasoning
55 dm : Dividable (suc p) m
56 dm = divdable^2 m (suc p) 1<sp m>1 pn record { factor = n * n ; is-factor = begin
57 (n * n) * (suc p) + 0 ≡⟨ +-comm _ 0 ⟩
58 (n * n) * (suc p) ≡⟨ *-comm (n * n) (suc p) ⟩
59 (suc p) * (n * n) ≡⟨ sym (*-assoc (suc p) n n) ⟩
60 (suc p * n) * n ≡⟨ pnm ⟩
56 m * m ∎ } where open ≡-Reasoning 61 m * m ∎ } where open ≡-Reasoning
57 -- 2 * n * n = 2m' 2m' 62 -- (suc p) * n * n = 2m' 2m'
58 -- n * n = m' 2m' 63 -- n * n = m' 2m'
59 df = Dividable.factor dm 64 df = Dividable.factor dm
60 dn : Dividable 2 n 65 dn : Dividable (suc p) n
61 dn = divdable^2 n 2 a<sa n>1 p2 record { factor = df * df ; is-factor = begin 66 dn = divdable^2 n (suc p) 1<sp n>1 pn record { factor = df * df ; is-factor = begin
62 df * df * 2 + 0 ≡⟨ *-cancelʳ-≡ _ _ {1} ( begin 67 df * df * (suc p) + 0 ≡⟨ *-cancelʳ-≡ _ _ {p} ( begin
63 (df * df * 2 + 0) * 2 ≡⟨ cong (λ k → k * 2) (+-comm (df * df * 2) 0) ⟩ 68 (df * df * (suc p) + 0) * (suc p) ≡⟨ cong (λ k → k * (suc p)) (+-comm (df * df * (suc p)) 0) ⟩
64 ((df * df) * 2) * 2 ≡⟨ cong (λ k → k * 2) (*-assoc df df 2 ) ⟩ 69 ((df * df) * (suc p)) * (suc p) ≡⟨ cong (λ k → k * (suc p)) (*-assoc df df (suc p) ) ⟩
65 (df * (df * 2)) * 2 ≡⟨ cong (λ k → (df * k ) * 2) (*-comm df 2) ⟩ 70 (df * (df * (suc p))) * (suc p) ≡⟨ cong (λ k → (df * k ) * (suc p)) (*-comm df (suc p)) ⟩
66 (df * (2 * df)) * 2 ≡⟨ sym ( cong (λ k → k * 2) (*-assoc df 2 df ) ) ⟩ 71 (df * ((suc p) * df)) * (suc p) ≡⟨ sym ( cong (λ k → k * (suc p)) (*-assoc df (suc p) df ) ) ⟩
67 ((df * 2) * df) * 2 ≡⟨ *-assoc (df * 2) df 2 ⟩ 72 ((df * (suc p)) * df) * (suc p) ≡⟨ *-assoc (df * (suc p)) df (suc p) ⟩
68 (df * 2) * (df * 2) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * 2)) (+-comm 0 _) ⟩ 73 (df * (suc p)) * (df * (suc p)) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * (suc p))) (+-comm 0 _) ⟩
69 (df * 2 + 0) * (df * 2 + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩ 74 (df * (suc p) + 0) * (df * (suc p) + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
70 m * m ≡⟨ sym 2nm ⟩ 75 m * m ≡⟨ sym pnm ⟩
71 2 * n * n ≡⟨ cong (λ k → k * n) (*-comm 2 n) ⟩ 76 (suc p) * n * n ≡⟨ cong (λ k → k * n) (*-comm (suc p) n) ⟩
72 n * 2 * n ≡⟨ *-assoc n 2 n ⟩ 77 n * (suc p) * n ≡⟨ *-assoc n (suc p) n ⟩
73 n * (2 * n) ≡⟨ cong (λ k → n * k) (*-comm 2 n) ⟩ 78 n * (suc p * n) ≡⟨ cong (λ k → n * k) (*-comm (suc p) n) ⟩
74 n * (n * 2) ≡⟨ sym (*-assoc n n 2) ⟩ 79 n * (n * suc p) ≡⟨ sym (*-assoc n n (suc p)) ⟩
75 n * n * 2 ∎ ) ⟩ 80 n * n * (suc p) ∎ ) ⟩
76 n * n ∎ } where open ≡-Reasoning 81 n * n ∎ } where open ≡-Reasoning
77 82
78 83