Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 281:8b437dd616dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix gcd and root
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Dec 2021 10:29:59 +0900
parents 4e4e148eb7e5
children 4a00e5f2b793
comparison
equal deleted inserted replaced
280:681df12f0edc 281:8b437dd616dd
6 open import Data.Unit using (⊤ ; tt) 6 open import Data.Unit using (⊤ ; tt)
7 open import Relation.Nullary 7 open import Relation.Nullary
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 open import Relation.Binary.Definitions 9 open import Relation.Binary.Definitions
10 10
11 open import gcd 11 import gcd as GCD
12 open import even 12 open import even
13 open import nat 13 open import nat
14 open import logic 14 open import logic
15 15
16 record Rational : Set where 16 record Rational : Set where
17 field 17 field
18 i j : ℕ 18 i j : ℕ
19 coprime : gcd i j ≡ 1 19 coprime : GCD.gcd i j ≡ 1
20
21 -- record Dividable (n m : ℕ ) : Set where
22 -- field
23 -- factor : ℕ
24 -- is-factor : factor * n + 0 ≡ m
25
26 gcd : (i j : ℕ) → ℕ
27 gcd = GCD.gcd
28
29 gcd-euclid : ( p a b : ℕ ) → 1 < p → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i → gcd p i ≡ 1)
30 → Dividable p (a * b) → Dividable p a ∨ Dividable p b
31 gcd-euclid = GCD.gcd-euclid
32
33 gcd-div1 : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j )
34 → Dividable k ( gcd i j )
35 gcd-div1 = GCD.gcd-div
20 36
21 open _∧_ 37 open _∧_
22 38
23 open import prime 39 open import prime
24
25 -- equlid : ( n m k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * m ) → Dividable k n ∨ Dividable k m
26 40
27 divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n 41 divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
28 divdable^2 zero zero () 1<n pk dn2 42 divdable^2 zero zero () 1<n pk dn2
29 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k 43 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
30 ... | yes y = y 44 ... | yes y = y
31 ... | 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 45 ... | 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 ... | case1 dn = dn 46 ... | case1 dn = dn
33 ... | case2 dm = dm 47 ... | case2 dm = dm
34 48
35 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
36 -- → Dividable k ( gcd i j )
37
38 -- p * n * n ≡ m * m means (m/n)^2 = p 49 -- p * n * n ≡ m * m means (m/n)^2 = p
39 -- rational m/n requires m and n is comprime each other which contradicts the condition 50 -- rational m/n requires m and n is comprime each other which contradicts the condition
40 51
41 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1 → p * n * n ≡ m * m → ¬ (gcd n m ≡ 1) 52 root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1 → p * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
42 root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn))) 53 root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn)))
43 root-prime-irrational n m (suc p0) n>1 pn m>1 pnm = rot13 ( gcd-div n m (suc p0) 1<sp dn dm ) where 54 root-prime-irrational n m (suc p0) n>1 pn m>1 pnm = rot13 ( gcd-div1 n m (suc p0) 1<sp dn dm ) where
44 p = suc (p0) 55 p = suc p0
45 1<sp : 1 < p 56 1<sp : 1 < p
46 1<sp = Prime.p>1 pn 57 1<sp = Prime.p>1 pn
47 rot13 : {m : ℕ } → Dividable p m → m ≡ 1 → ⊥ 58 rot13 : {m : ℕ } → Dividable (suc p0) m → m ≡ 1 → ⊥
48 rot13 d refl with Dividable.factor d | Dividable.is-factor d 59 rot13 d refl with Dividable.factor d | Dividable.is-factor d
49 ... | zero | () -- gcd 0 m ≡ 1 60 ... | zero | () -- gcd 0 m ≡ 1
50 ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1 61 ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1
51 rot17 : suc n * p + 0 > 1 62 rot17 : suc n * (suc p0) + 0 > 1
52 rot17 = begin 63 rot17 = begin
53 2 ≡⟨ refl ⟩ 64 2 ≡⟨ refl ⟩
54 suc (1 * 1 ) ≤⟨ 1<sp ⟩ 65 suc (1 * 1 ) ≤⟨ 1<sp ⟩
55 suc p0 ≡⟨ cong suc (+-comm 0 _) ⟩ 66 suc p0 ≡⟨ cong suc (+-comm 0 _) ⟩
56 suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩ 67 suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩
68 df = Dividable.factor dm 79 df = Dividable.factor dm
69 dn : Dividable p n 80 dn : Dividable p n
70 dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin 81 dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin
71 df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin 82 df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin
72 (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩ 83 (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩
73 ((df * df) * p) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩ 84 ((df * df) * p ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
74 (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩ 85 (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩
75 (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩ 86 (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
76 ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p ⟩ 87 ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p ⟩
77 (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩ 88 (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩
78 (df * p + 0) * (df * p + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩ 89 (df * p + 0) * (df * p + 0) ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
79 m * m ≡⟨ sym pnm ⟩ 90 m * m ≡⟨ sym pnm ⟩
80 p * n * n ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩ 91 p * n * n ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩
81 n * p * n ≡⟨ *-assoc n p n ⟩ 92 n * p * n ≡⟨ *-assoc n p n ⟩
82 n * (p * n) ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩ 93 n * (p * n) ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩
83 n * (n * p) ≡⟨ sym (*-assoc n n p) ⟩ 94 n * (n * p) ≡⟨ sym (*-assoc n n p) ⟩
84 n * n * p ∎ ) ⟩ 95 n * n * p ∎ ) ⟩
85 n * n ∎ } where open ≡-Reasoning 96 n * n ∎ } where open ≡-Reasoning
86 97
98 Rational* : (r s : Rational) → Rational
99 Rational* r s = record { i = {!!} ; j = {!!} ; coprime = {!!} }
87 100
101 _r=_ : Rational → ℕ → Set
102 r r= n = (Rational.i r ≡ n) ∧ (Rational.j r ≡ 1)
103
104 root-prime-irrational1 : ( p : ℕ ) → Prime p → ¬ ( ( r : Rational ) → Rational* r r r= p )
105 root-prime-irrational1 = {!!}