Mercurial > hg > Members > kono > Proof > automaton
annotate agda/gcd.agda @ 154:ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 02 Jan 2021 04:29:20 +0900 |
| parents | d78fc1951c26 |
| children | 4b6063ad6de2 |
| rev | line source |
|---|---|
| 148 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 2 module gcd where | |
| 57 | 3 |
| 141 | 4 open import Data.Nat |
| 5 open import Data.Nat.Properties | |
| 57 | 6 open import Data.Empty |
| 141 | 7 open import Data.Unit using (⊤ ; tt) |
| 57 | 8 open import Relation.Nullary |
| 9 open import Relation.Binary.PropositionalEquality | |
| 141 | 10 open import Relation.Binary.Definitions |
| 149 | 11 open import nat |
| 151 | 12 open import logic |
| 57 | 13 |
| 14 even : (n : ℕ ) → Set | |
| 141 | 15 even zero = ⊤ |
| 16 even (suc zero) = ⊥ | |
| 17 even (suc (suc n)) = even n | |
| 57 | 18 |
| 19 even? : (n : ℕ ) → Dec ( even n ) | |
| 141 | 20 even? zero = yes tt |
| 21 even? (suc zero) = no (λ ()) | |
| 22 even? (suc (suc n)) = even? n | |
| 23 | |
| 24 n+even : {n m : ℕ } → even n → even m → even ( n + m ) | |
| 25 n+even {zero} {zero} tt tt = tt | |
| 26 n+even {zero} {suc m} tt em = em | |
| 27 n+even {suc (suc n)} {m} en em = n+even {n} {m} en em | |
| 28 | |
| 29 n*even : {m n : ℕ } → even n → even ( m * n ) | |
| 30 n*even {zero} {n} en = tt | |
| 31 n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en) | |
| 32 | |
| 33 even*n : {n m : ℕ } → even n → even ( n * m ) | |
| 34 even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en) | |
| 35 | |
| 36 gcd1 : ( i i0 j j0 : ℕ ) → ℕ | |
| 146 | 37 gcd1 zero i0 zero j0 with <-cmp i0 j0 |
| 38 ... | tri< a ¬b ¬c = j0 | |
| 39 ... | tri≈ ¬a refl ¬c = i0 | |
| 40 ... | tri> ¬a ¬b c = i0 | |
| 141 | 41 gcd1 zero i0 (suc zero) j0 = 1 |
| 42 gcd1 zero zero (suc (suc j)) j0 = j0 | |
| 43 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 44 gcd1 (suc zero) i0 zero j0 = 1 | |
| 45 gcd1 (suc (suc i)) i0 zero zero = i0 | |
| 46 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0) | |
| 47 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0 | |
| 48 | |
| 49 gcd : ( i j : ℕ ) → ℕ | |
| 50 gcd i j = gcd1 i i j j | |
| 57 | 51 |
| 141 | 52 even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2 |
| 53 even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl | |
| 54 even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin | |
| 152 | 55 gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩ |
| 56 gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩ | |
| 57 2 ∎ where open ≡-Reasoning | |
| 57 | 58 |
| 145 | 59 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m |
| 60 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n | |
| 143 | 61 |
| 146 | 62 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 |
| 63 gcd22 zero i0 zero o0 = refl | |
| 64 gcd22 zero i0 (suc o) o0 = refl | |
| 65 gcd22 (suc i) i0 zero o0 = refl | |
| 66 gcd22 (suc i) i0 (suc o) o0 = refl | |
| 67 | |
| 152 | 68 gcd20 : (i : ℕ) → gcd i 0 ≡ i |
| 69 gcd20 zero = refl | |
| 70 gcd20 (suc i) = gcd201 (suc i) where | |
| 71 gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i | |
| 72 gcd201 zero = refl | |
| 73 gcd201 (suc zero) = refl | |
| 74 gcd201 (suc (suc i)) = refl | |
| 75 | |
| 151 | 76 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m |
| 77 gcdmm zero m with <-cmp m m | |
| 78 ... | tri< a ¬b ¬c = refl | |
| 79 ... | tri≈ ¬a refl ¬c = refl | |
| 80 ... | tri> ¬a ¬b c = refl | |
| 81 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m ) | |
| 82 | |
| 83 record Comp ( m n : ℕ ) : Set where | |
| 84 field | |
| 85 non-1 : 1 < m | |
| 86 comp : ℕ | |
| 87 is-comp : n * comp ≡ m | |
| 88 | |
| 147 | 89 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i |
| 90 gcdsym2 i j with <-cmp i j | <-cmp j i | |
| 91 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) | |
| 92 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 93 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl | |
| 94 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 95 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | |
| 96 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) | |
| 97 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | |
| 98 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) | |
| 99 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | |
| 100 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0 | |
| 101 gcdsym1 zero zero zero zero = refl | |
| 102 gcdsym1 zero zero zero (suc j0) = refl | |
| 103 gcdsym1 zero (suc i0) zero zero = refl | |
| 104 gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0) | |
| 105 gcdsym1 zero zero (suc zero) j0 = refl | |
| 106 gcdsym1 zero zero (suc (suc j)) j0 = refl | |
| 107 gcdsym1 zero (suc i0) (suc zero) j0 = refl | |
| 108 gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 109 gcdsym1 (suc zero) i0 zero j0 = refl | |
| 110 gcdsym1 (suc (suc i)) i0 zero zero = refl | |
| 111 gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) | |
| 112 gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 ) | |
| 113 | |
| 146 | 114 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n |
| 147 | 115 gcdsym {n} {m} = gcdsym1 n n m m |
| 146 | 116 |
| 152 | 117 gcd11 : ( i : ℕ ) → gcd i i ≡ i |
| 118 gcd11 i = gcdmm i i | |
| 119 | |
| 120 gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j | |
| 153 | 121 gcd2 i j = gcd200 i i j j where |
| 122 gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1) | |
| 123 gcd202 zero j1 = refl | |
| 124 gcd202 (suc i) j1 = cong suc (gcd202 i j1) | |
| 125 gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0 | |
| 126 gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl | |
| 127 gcd201 i i0 j j0 (suc j1) = begin | |
| 128 gcd1 (i + suc j1) (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩ | |
| 129 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩ | |
| 130 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩ | |
| 131 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning | |
| 132 gcd200 : (i i0 j j0 : ℕ) → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0 | |
| 133 gcd200 i i0 zero j0 = {!!} | |
| 134 gcd200 (suc (suc i)) i0 (suc j) (suc j0) = gcd201 (suc (suc i)) i0 j (suc j0) (suc j) | |
| 135 gcd200 zero zero (suc zero) j0 = {!!} | |
| 136 gcd200 zero zero (suc (suc j)) j0 = {!!} | |
| 137 gcd200 zero (suc i0) (suc j) j0 = {!!} | |
| 138 gcd200 (suc zero) i0 (suc j) j0 = {!!} | |
|
154
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
139 gcd200 (suc (suc i)) i0 (suc j) zero = {!!} |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
140 |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
141 gcd4 : ( n k : ℕ ) → gcd n k ≡ k → k ≤ n |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
142 gcd4 n k gn = gcd40 n n k k gn where |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
143 gcd40 : (i i0 j j0 : ℕ) → gcd1 i i0 j j0 ≡ j0 → j0 ≤ i0 |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
144 gcd40 zero i0 zero j0 gn = {!!} |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
145 gcd40 zero i0 (suc j) j0 gn = {!!} |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
146 gcd40 (suc i) i0 zero j0 gn = {!!} |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
147 gcd40 (suc i) i0 (suc j) j0 gn = gcd40 i i0 j j0 (subst (λ k → k ≡ j0) (gcd22 i i0 j j0) gn) |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
148 |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
149 gcd3 : ( n k : ℕ ) → n ≤ k + k → gcd n k ≡ k → n ≡ k |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
150 gcd3 n k n<2k gn = {!!} |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
151 |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
152 gcd23 : ( n m k : ℕ) → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m |
|
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
153 gcd23 = {!!} |
| 152 | 154 |
| 142 | 155 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 ) |
|
154
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
156 gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k gn gm ))) |
| 141 | 157 |
| 158 record Even (i : ℕ) : Set where | |
| 159 field | |
| 160 j : ℕ | |
| 161 is-twice : i ≡ 2 * j | |
| 162 | |
| 163 e2 : (i : ℕ) → even i → Even i | |
| 164 e2 zero en = record { j = 0 ; is-twice = refl } | |
| 165 e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where | |
| 166 e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en)) | |
| 167 e21 = begin | |
| 168 suc (suc i) ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en)) ⟩ | |
| 169 suc (suc (2 * Even.j (e2 i en))) ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩ | |
| 170 2 * suc (Even.j (e2 i en)) ∎ where open ≡-Reasoning | |
| 171 | |
| 172 record Odd (i : ℕ) : Set where | |
| 173 field | |
| 174 j : ℕ | |
| 175 is-twice : i ≡ suc (2 * j ) | |
| 57 | 176 |
| 141 | 177 odd2 : (i : ℕ) → ¬ even i → even (suc i) |
| 178 odd2 zero ne = ⊥-elim ( ne tt ) | |
| 179 odd2 (suc zero) ne = tt | |
| 180 odd2 (suc (suc i)) ne = odd2 i ne | |
| 181 | |
| 182 odd3 : (i : ℕ) → ¬ even i → Odd i | |
| 183 odd3 zero ne = ⊥-elim ( ne tt ) | |
| 184 odd3 (suc zero) ne = record { j = 0 ; is-twice = refl } | |
| 185 odd3 (suc (suc i)) ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where | |
| 186 odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne))) | |
| 187 odd31 = begin | |
| 188 suc (suc i) ≡⟨ cong suc (Even.is-twice (e2 (suc i) (odd2 i ne))) ⟩ | |
| 189 suc (2 * (Even.j (e2 (suc i) (odd2 i ne)))) ∎ where open ≡-Reasoning | |
| 190 | |
| 191 odd4 : (i : ℕ) → even i → ¬ even ( suc i ) | |
| 192 odd4 (suc (suc i)) en en1 = odd4 i en en1 | |
| 193 | |
| 194 even^2 : {n : ℕ} → even ( n * n ) → even n | |
| 195 even^2 {n} en with even? n | |
| 196 ... | yes y = y | |
| 197 ... | 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 | |
| 198 m : ℕ | |
| 199 m = Odd.j ( odd3 n ne ) | |
| 200 ee3 : even (2 * m) | |
| 201 ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt ) | |
| 202 ee4 : even ((2 * m) * suc (2 * m)) | |
| 203 ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt ) | |
| 204 ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) )) | |
| 205 ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩ | |
| 206 suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩ | |
| 207 (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin | |
| 208 suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩ | |
| 209 suc m + 1 * m ≡⟨⟩ | |
| 210 suc (2 * m) | |
| 211 ∎) ⟩ suc (2 * m) + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning | |
| 57 | 212 |
| 141 | 213 open import nat |
| 214 | |
| 215 e3 : {i j : ℕ } → 2 * i ≡ 2 * j → i ≡ j | |
| 216 e3 {zero} {zero} refl = refl | |
| 217 e3 {suc x} {suc y} eq with <-cmp x y | |
| 218 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a )))))) | |
| 219 ... | tri≈ ¬a b ¬c = cong suc b | |
| 220 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c )))))) | |
| 221 |