Mercurial > hg > Members > kono > Proof > automaton
annotate agda/gcd.agda @ 156:91265c971200
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 02 Jan 2021 11:49:44 +0900 |
| parents | 4b6063ad6de2 |
| children | 0b74851665ee |
| 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 | |
| 155 | 120 gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1 |
| 121 gcd203 zero = refl | |
| 122 gcd203 (suc i) = gcd205 (suc i) where | |
| 123 gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1 | |
| 124 gcd205 zero = refl | |
| 125 gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j) (suc (suc i)) j (suc i)) (gcd205 j) | |
| 126 gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1 | |
| 127 gcd204 zero = refl | |
| 128 gcd204 (suc zero) = refl | |
| 129 gcd204 (suc (suc zero)) = refl | |
| 130 gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) | |
| 131 | |
| 152 | 132 gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j |
| 155 | 133 gcd2 i j = gcd200 i i j j refl refl where |
| 153 | 134 gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1) |
| 135 gcd202 zero j1 = refl | |
| 136 gcd202 (suc i) j1 = cong suc (gcd202 i j1) | |
| 137 gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0 | |
| 138 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 | |
| 139 gcd201 i i0 j j0 (suc j1) = begin | |
| 140 gcd1 (i + suc j1) (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩ | |
| 141 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩ | |
| 142 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩ | |
| 143 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning | |
| 155 | 144 gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0 |
| 145 gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl | |
| 146 gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j) | |
| 147 gcd200 zero zero (suc zero) .1 i=i0 refl = refl | |
| 148 gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin | |
| 149 gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩ | |
| 150 suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩ | |
| 151 gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning | |
| 152 gcd200 zero (suc i0) (suc j) .(suc j) () refl | |
| 153 gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin | |
| 154 gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩ | |
| 155 1 ≡⟨ sym ( gcd204 (suc j)) ⟩ | |
| 156 gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning | |
| 157 gcd200 (suc (suc i)) i0 (suc j) zero i=i0 () | |
|
154
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
158 |
| 156 | 159 gcd6 : ( i i0 j j0 n n0 : ℕ) → gcd1 i i0 j j0 ≡ gcd1 0 n 0 n0 → n ≡ n0 |
| 160 gcd6 i i0 j j0 n n0 = {!!} | |
|
154
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
161 |
| 156 | 162 gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n |
| 163 gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl where | |
| 164 gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 → gcd1 i i0 j j0 ≤ i0 | |
| 165 gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0 | |
| 166 ... | tri< a ¬b ¬c = {!!} -- ≤-refl -- j0 ≤ i0 | |
| 167 ... | tri≈ ¬a refl ¬c = ≤-refl | |
| 168 ... | tri> ¬a ¬b c = ≤-refl | |
| 169 gcd50 zero i0 (suc j) j0 0<i i<i0 j<j0 = {!!} | |
| 170 gcd50 (suc i) i0 j j0 0<i i<i0 j<j0 = {!!} | |
|
154
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
171 |
| 156 | 172 gcd4 : ( n k : ℕ ) → 1 < n → gcd n k ≡ k → k ≤ n |
| 173 gcd4 = {!!} | |
| 174 | |
| 175 gcd3 : ( n k : ℕ ) → 0 < n → n ≤ k + k → gcd n k ≡ k → n ≡ k | |
| 176 gcd3 n k 0<n n<2k gn = {!!} | |
| 177 | |
| 178 gcd23 : ( n m k : ℕ) → 0 < n → 0 < m → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m | |
|
154
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
179 gcd23 = {!!} |
| 152 | 180 |
| 142 | 181 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 ) |
| 156 | 182 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 | 183 |
| 184 record Even (i : ℕ) : Set where | |
| 185 field | |
| 186 j : ℕ | |
| 187 is-twice : i ≡ 2 * j | |
| 188 | |
| 189 e2 : (i : ℕ) → even i → Even i | |
| 190 e2 zero en = record { j = 0 ; is-twice = refl } | |
| 191 e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where | |
| 192 e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en)) | |
| 193 e21 = begin | |
| 194 suc (suc i) ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en)) ⟩ | |
| 195 suc (suc (2 * Even.j (e2 i en))) ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩ | |
| 196 2 * suc (Even.j (e2 i en)) ∎ where open ≡-Reasoning | |
| 197 | |
| 198 record Odd (i : ℕ) : Set where | |
| 199 field | |
| 200 j : ℕ | |
| 201 is-twice : i ≡ suc (2 * j ) | |
| 57 | 202 |
| 141 | 203 odd2 : (i : ℕ) → ¬ even i → even (suc i) |
| 204 odd2 zero ne = ⊥-elim ( ne tt ) | |
| 205 odd2 (suc zero) ne = tt | |
| 206 odd2 (suc (suc i)) ne = odd2 i ne | |
| 207 | |
| 208 odd3 : (i : ℕ) → ¬ even i → Odd i | |
| 209 odd3 zero ne = ⊥-elim ( ne tt ) | |
| 210 odd3 (suc zero) ne = record { j = 0 ; is-twice = refl } | |
| 211 odd3 (suc (suc i)) ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where | |
| 212 odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne))) | |
| 213 odd31 = begin | |
| 214 suc (suc i) ≡⟨ cong suc (Even.is-twice (e2 (suc i) (odd2 i ne))) ⟩ | |
| 215 suc (2 * (Even.j (e2 (suc i) (odd2 i ne)))) ∎ where open ≡-Reasoning | |
| 216 | |
| 217 odd4 : (i : ℕ) → even i → ¬ even ( suc i ) | |
| 218 odd4 (suc (suc i)) en en1 = odd4 i en en1 | |
| 219 | |
| 220 even^2 : {n : ℕ} → even ( n * n ) → even n | |
| 221 even^2 {n} en with even? n | |
| 222 ... | yes y = y | |
| 223 ... | 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 | |
| 224 m : ℕ | |
| 225 m = Odd.j ( odd3 n ne ) | |
| 226 ee3 : even (2 * m) | |
| 227 ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt ) | |
| 228 ee4 : even ((2 * m) * suc (2 * m)) | |
| 229 ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt ) | |
| 230 ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) )) | |
| 231 ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩ | |
| 232 suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩ | |
| 233 (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin | |
| 234 suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩ | |
| 235 suc m + 1 * m ≡⟨⟩ | |
| 236 suc (2 * m) | |
| 237 ∎) ⟩ suc (2 * m) + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning | |
| 57 | 238 |
| 141 | 239 open import nat |
| 240 | |
| 241 e3 : {i j : ℕ } → 2 * i ≡ 2 * j → i ≡ j | |
| 242 e3 {zero} {zero} refl = refl | |
| 243 e3 {suc x} {suc y} eq with <-cmp x y | |
| 244 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a )))))) | |
| 245 ... | tri≈ ¬a b ¬c = cong suc b | |
| 246 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c )))))) | |
| 247 |