Mercurial > hg > Members > kono > Proof > automaton
annotate agda/gcd.agda @ 159:5530b3789e0c
add even
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 Jan 2021 09:24:11 +0900 |
| parents | c332bb9dbf98 |
| children | 57f2c04eb14c |
| 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 |
| 141 | 14 gcd1 : ( i i0 j j0 : ℕ ) → ℕ |
| 146 | 15 gcd1 zero i0 zero j0 with <-cmp i0 j0 |
|
157
0b74851665ee
( n k : ℕ ) → 1 < n → gcd n k ≤ n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
16 ... | tri< a ¬b ¬c = i0 |
| 146 | 17 ... | tri≈ ¬a refl ¬c = i0 |
|
157
0b74851665ee
( n k : ℕ ) → 1 < n → gcd n k ≤ n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
156
diff
changeset
|
18 ... | tri> ¬a ¬b c = j0 |
| 141 | 19 gcd1 zero i0 (suc zero) j0 = 1 |
| 20 gcd1 zero zero (suc (suc j)) j0 = j0 | |
| 21 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 22 gcd1 (suc zero) i0 zero j0 = 1 | |
| 23 gcd1 (suc (suc i)) i0 zero zero = i0 | |
| 24 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0) | |
| 25 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0 | |
| 26 | |
| 27 gcd : ( i j : ℕ ) → ℕ | |
| 28 gcd i j = gcd1 i i j j | |
| 57 | 29 |
| 145 | 30 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m |
| 31 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n | |
| 143 | 32 |
| 146 | 33 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 |
| 34 gcd22 zero i0 zero o0 = refl | |
| 35 gcd22 zero i0 (suc o) o0 = refl | |
| 36 gcd22 (suc i) i0 zero o0 = refl | |
| 37 gcd22 (suc i) i0 (suc o) o0 = refl | |
| 38 | |
| 152 | 39 gcd20 : (i : ℕ) → gcd i 0 ≡ i |
| 40 gcd20 zero = refl | |
| 41 gcd20 (suc i) = gcd201 (suc i) where | |
| 42 gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i | |
| 43 gcd201 zero = refl | |
| 44 gcd201 (suc zero) = refl | |
| 45 gcd201 (suc (suc i)) = refl | |
| 46 | |
| 151 | 47 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m |
| 48 gcdmm zero m with <-cmp m m | |
| 49 ... | tri< a ¬b ¬c = refl | |
| 50 ... | tri≈ ¬a refl ¬c = refl | |
| 51 ... | tri> ¬a ¬b c = refl | |
| 52 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m ) | |
| 53 | |
| 147 | 54 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i |
| 55 gcdsym2 i j with <-cmp i j | <-cmp j i | |
| 56 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) | |
| 57 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 58 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl | |
| 59 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 60 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | |
| 61 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) | |
| 62 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | |
| 63 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) | |
| 64 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | |
| 65 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0 | |
| 66 gcdsym1 zero zero zero zero = refl | |
| 67 gcdsym1 zero zero zero (suc j0) = refl | |
| 68 gcdsym1 zero (suc i0) zero zero = refl | |
| 69 gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0) | |
| 70 gcdsym1 zero zero (suc zero) j0 = refl | |
| 71 gcdsym1 zero zero (suc (suc j)) j0 = refl | |
| 72 gcdsym1 zero (suc i0) (suc zero) j0 = refl | |
| 73 gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 74 gcdsym1 (suc zero) i0 zero j0 = refl | |
| 75 gcdsym1 (suc (suc i)) i0 zero zero = refl | |
| 76 gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) | |
| 77 gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 ) | |
| 78 | |
| 146 | 79 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n |
| 147 | 80 gcdsym {n} {m} = gcdsym1 n n m m |
| 146 | 81 |
| 152 | 82 gcd11 : ( i : ℕ ) → gcd i i ≡ i |
| 83 gcd11 i = gcdmm i i | |
| 84 | |
| 155 | 85 gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1 |
| 86 gcd203 zero = refl | |
| 87 gcd203 (suc i) = gcd205 (suc i) where | |
| 88 gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1 | |
| 89 gcd205 zero = refl | |
| 90 gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j) (suc (suc i)) j (suc i)) (gcd205 j) | |
| 91 gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1 | |
| 92 gcd204 zero = refl | |
| 93 gcd204 (suc zero) = refl | |
| 94 gcd204 (suc (suc zero)) = refl | |
| 95 gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) | |
| 96 | |
| 152 | 97 gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j |
| 155 | 98 gcd2 i j = gcd200 i i j j refl refl where |
| 153 | 99 gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1) |
| 100 gcd202 zero j1 = refl | |
| 101 gcd202 (suc i) j1 = cong suc (gcd202 i j1) | |
| 102 gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0 | |
| 103 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 | |
| 104 gcd201 i i0 j j0 (suc j1) = begin | |
| 105 gcd1 (i + suc j1) (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩ | |
| 106 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩ | |
| 107 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩ | |
| 108 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning | |
| 155 | 109 gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0 |
| 110 gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl | |
| 111 gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j) | |
| 112 gcd200 zero zero (suc zero) .1 i=i0 refl = refl | |
| 113 gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin | |
| 114 gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩ | |
| 115 suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩ | |
| 116 gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning | |
| 117 gcd200 zero (suc i0) (suc j) .(suc j) () refl | |
| 118 gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin | |
| 119 gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩ | |
| 120 1 ≡⟨ sym ( gcd204 (suc j)) ⟩ | |
| 121 gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning | |
| 122 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
|
123 |
| 159 | 124 gcd52 : {i : ℕ } → 1 < suc (suc i) |
| 125 gcd52 {zero} = a<sa | |
| 126 gcd52 {suc i} = <-trans (gcd52 {i}) a<sa | |
| 127 | |
| 128 gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 → gcd1 i i0 j j0 ≤ i0 | |
| 129 gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0 | |
| 130 ... | tri< a ¬b ¬c = ≤-refl | |
| 131 ... | tri≈ ¬a refl ¬c = ≤-refl | |
| 132 ... | tri> ¬a ¬b c = ≤-trans refl-≤s c | |
| 133 gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where | |
| 134 gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0 | |
| 135 gcd51 1<i = ≤to< 1<i | |
| 136 gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s | |
| 137 gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = ≤to< 0<i | |
| 138 gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl | |
| 139 gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i)) j0 (suc j0) gcd52 refl-≤s refl-≤s) i<i0 | |
| 140 gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0)) | |
| 141 (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) | |
| 142 | |
| 156 | 143 gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n |
| 159 | 144 gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl |
| 145 | |
| 146 gcd6 : ( n k : ℕ ) → 1 < n → gcd k n ≤ n | |
| 147 gcd6 n k 1<n = subst (λ m → m ≤ n) (gcdsym {n} {k}) (gcd5 n k 1<n) | |
|
154
ba7d4cc92e60
... gcd (i + j) j ≡ gcd i j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
153
diff
changeset
|
148 |
| 156 | 149 gcd4 : ( n k : ℕ ) → 1 < n → gcd n k ≡ k → k ≤ n |
| 158 | 150 gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n) |
| 156 | 151 |
| 159 | 152 record Comp ( m n : ℕ ) : Set where |
| 153 field | |
| 154 comp : ℕ | |
| 155 is-comp : n * comp ≡ m | |
| 156 | |
| 157 open Comp | |
| 158 | |
| 159 comp-n : ( m n : ℕ ) → Comp m n → Comp (m + n) n | |
| 160 comp-n m n c = record { comp = suc (comp c) ; is-comp = | |
| 161 begin | |
| 162 n * suc (comp c) ≡⟨ *-comm n (suc (comp c)) ⟩ | |
| 163 n + comp c * n ≡⟨ +-comm n (comp c * n) ⟩ | |
| 164 comp c * n + n ≡⟨ cong (λ k → k + n) ( *-comm (comp c) n) ⟩ | |
| 165 (n * comp c) + n ≡⟨ cong (λ k → k + n) (is-comp c) ⟩ | |
| 166 m + n ∎ | |
| 167 } where open ≡-Reasoning | |
| 168 | |
| 169 gcdcomp : ( m n o : ℕ ) → 0 < n → Set | |
| 170 gcdcomp m n o 0<n = gcd n m ≡ o → Comp n o | |
| 171 | |
| 172 gcdcomp-eq : ( m o : ℕ ) (0<m : 0 < m) → gcdcomp m m o 0<m | |
| 173 gcdcomp-eq m o 0<m g = record { comp = 1 ; is-comp = gcdc0 g } where | |
| 174 gcdc0 : (g : gcd m m ≡ o) → o * 1 ≡ m | |
| 175 gcdc0 g = begin | |
| 176 o * 1 ≡⟨ cong (λ k → k * 1) (sym g) ⟩ | |
| 177 gcd m m * 1 ≡⟨ *-identityʳ _ ⟩ | |
| 178 gcd m m ≡⟨ gcdmm m m ⟩ | |
| 179 m ∎ where open ≡-Reasoning | |
| 180 | |
| 181 gcd3 : Set | |
| 182 gcd3 = ( n k : ℕ ) → 1 < n → n < k + k → gcd n k ≡ k → n ≡ k | |
| 183 | |
| 184 0<gcd : {i j : ℕ} → 0 < j → 0 < gcd j i | |
| 185 0<gcd {zero} {zero} () | |
| 186 0<gcd {zero} {suc j} 0<j = subst (λ k → 0 < k ) (sym (gcd20 (suc j))) 0<j | |
| 187 0<gcd {suc i} {suc j} (s≤s 0<j) = {!!} | |
| 156 | 188 |
| 158 | 189 gcd23 : ( n m k : ℕ) → 1 < n → 1 < m → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m |
| 159 | 190 gcd23 n m k 1<n 1<m gn gm = gcd230 n n m m k k 1<n 1<m ≤-refl ≤-refl ≤-refl gn gm where |
| 191 gcd231 : (i0 k k0 : ℕ) → (1 < i0) → (suc k ≤ k0) → gcd1 0 i0 (suc k) k0 ≡ suc k → suc k ≤ i0 | |
| 192 gcd231 i0 k k0 1<i0 sk<k0 gi = subst (λ m → m ≤ i0 ) gi ( gcd50 0 i0 (suc k) k0 1<i0 z≤n sk<k0 ) | |
| 193 gcd230 : (i i0 j j0 k k0 : ℕ) → 1 < i0 → 1 < j0 → i ≤ i0 → j ≤ j0 → k ≤ k0 → gcd1 i i0 k k0 ≡ k → gcd1 j j0 k k0 ≡ k → k ≤ gcd1 i i0 j j0 | |
| 194 gcd230 j i0 i j0 zero k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!} | |
| 195 gcd230 zero i0 zero j0 (suc k) k0 1<i 1<j i<i0 j<j0 k<k0 gi gj with <-cmp i0 j0 | |
| 196 ... | tri< a ¬b ¬c = gcd231 i0 k k0 1<i k<k0 gi -- k ≤ gcd1 zero i0 (suc j) j0 | |
| 197 ... | tri≈ ¬a refl ¬c = gcd231 j0 k k0 1<i k<k0 gj | |
| 198 ... | tri> ¬a ¬b c = gcd231 j0 k k0 1<j k<k0 gj | |
| 199 gcd230 zero i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!} | |
| 200 gcd230 (suc i) i0 zero j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = {!!} | |
| 201 gcd230 (suc i) i0 (suc j) j0 (suc k) k0 1<i i<i0 1<j0 j<j0 k<k0 gi gj = subst (λ m → suc k ≤ m) (sym (gcd22 i i0 j j0)) | |
| 202 (gcd230 i i0 j j0 (suc k) k0 {!!} {!!} {!!} {!!} k<k0 {!!} {!!} ) -- gcd1 (suc i) i0 (suc k) k0 ≡ suc k → gcd1 i i0 (suc k) k0 ≡ suc k | |
| 152 | 203 |
| 142 | 204 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 ) |
| 158 | 205 gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k 1<n 1<m gn gm ))) |
| 141 | 206 |