Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/root2.agda @ 186:08f4ec41ea93

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
even→gcd
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 14 Jun 2021 02:17:58 +0900
parents f9473f83f6e7
children 1402c5b17160
comparison
equal deleted inserted replaced
185:f9473f83f6e7 186:08f4ec41ea93
21 even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl 21 even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
22 even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin 22 even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
23 gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩ 23 gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩
24 gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩ 24 gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
25 2 ∎ where open ≡-Reasoning 25 2 ∎ where open ≡-Reasoning
26
27 even→gcd : (n m : ℕ) → even n → even m → even (gcd n m)
28 even→gcd zero zero en em = tt
29 even→gcd zero (suc (suc m)) en em = em
30 even→gcd (suc (suc n)) zero en em = en
31 even→gcd (suc (suc n)) (suc (suc m)) en em = ee2 n n (suc (suc m)) (suc (suc m)) refl refl
32 (subst (λ k → even k) (gcdsym {suc (suc m)} {n}) (ee2 m m n n refl refl (subst (λ k → even k) (gcdsym {n} {m}) ee1))) where
33 ee1 : even (gcd n m)
34 ee1 = even→gcd n m en em
35 ee2 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → even (gcd1 i i j0 j0) → even (gcd1 (suc (suc i)) (suc (suc i)) j0 j0)
36 ee2 i i0 j j0 i=i0 j=j0 e = {!!}
26 37
27 even^2 : {n : ℕ} → even ( n * n ) → even n 38 even^2 : {n : ℕ} → even ( n * n ) → even n
28 even^2 {n} en with even? n 39 even^2 {n} en with even? n
29 ... | yes y = y 40 ... | yes y = y
30 ... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where 41 ... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where
50 ... | tri≈ ¬a b ¬c = cong suc b 61 ... | tri≈ ¬a b ¬c = cong suc b
51 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c )))))) 62 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))
52 63
53 open Factor 64 open Factor
54 65
66 -- gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j )
67 -- → remain if ≡ 0 → remain jf ≡ 0
68 -- → Dividable k ( gcd i j )
69
55 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1 → 2 * n * n ≡ m * m → ¬ (gcd n m ≡ 1) 70 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1 → 2 * n * n ≡ m * m → ¬ (gcd n m ≡ 1)
56 root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-gt n n m m 2 f2 f2 f2 fm (f3 n rot7) refl f4 f4) where 71 root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 f2 fm (f3 n rot7) refl ) where
57 rot13 : {m : ℕ } → Dividable 2 m → m ≡ 1 → ⊥ 72 rot13 : {m : ℕ } → Dividable 2 m → m ≡ 1 → ⊥
58 rot13 d refl with Dividable.factor d | Dividable.is-factor d 73 rot13 d refl with Dividable.factor d | Dividable.is-factor d
59 ... | zero | () 74 ... | zero | ()
60 ... | suc n | () 75 ... | suc n | ()
61 rot11 : {m : ℕ } → even m → Factor 2 m 76 rot11 : {m : ℕ } → even m → Factor 2 m
97 f2 : Factor 2 n 112 f2 : Factor 2 n
98 f2 = rot11 rot7 113 f2 = rot11 rot7
99 f3 : ( n : ℕ) → (e : even n ) → remain (rot11 {n} e) ≡ 0 114 f3 : ( n : ℕ) → (e : even n ) → remain (rot11 {n} e) ≡ 0
100 f3 zero e = refl 115 f3 zero e = refl
101 f3 (suc (suc n)) e = f3 n e 116 f3 (suc (suc n)) e = f3 n e
102 f4 : {m : ℕ} → remain f2 + m ≡ m
103 f4 {m} = begin
104 remain f2 + m ≡⟨ cong (λ k → k + m) (f3 n rot7) ⟩
105 0 + m ≡⟨ refl ⟩
106 m ∎ where open ≡-Reasoning
107 fm : Factor 2 m 117 fm : Factor 2 m
108 fm = record { factor = Even.j E ; remain = 0 ; is-factor = fm1 } where 118 fm = record { factor = Even.j E ; remain = 0 ; is-factor = fm1 } where
109 fm1 : Even.j E * 2 + 0 ≡ m 119 fm1 : Even.j E * 2 + 0 ≡ m
110 fm1 = begin 120 fm1 = begin
111 Even.j E * 2 + 0 ≡⟨ +-comm _ 0 ⟩ 121 Even.j E * 2 + 0 ≡⟨ +-comm _ 0 ⟩