Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/gcd.agda @ 227:a61f121c34a4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 23 Jun 2021 18:10:18 +0900 |
| parents | 6077bdd19312 |
| children | a72bcc6eadad |
| 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 |
| 164 | 14 record Factor (n m : ℕ ) : Set where |
| 15 field | |
| 16 factor : ℕ | |
| 17 remain : ℕ | |
| 18 is-factor : factor * n + remain ≡ m | |
| 19 | |
| 165 | 20 record Dividable (n m : ℕ ) : Set where |
| 21 field | |
| 22 factor : ℕ | |
| 23 is-factor : factor * n + 0 ≡ m | |
| 24 | |
| 164 | 25 open Factor |
| 26 | |
|
193
875eb1fa9694
dividable reorganzaiton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
27 DtoF : {n m : ℕ} → Dividable n m → Factor n m |
| 195 | 28 DtoF {n} {m} record { factor = f ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa } |
|
193
875eb1fa9694
dividable reorganzaiton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
29 |
| 195 | 30 FtoD : {n m : ℕ} → (fc : Factor n m) → remain fc ≡ 0 → Dividable n m |
| 31 FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } refl = record { factor = f ; is-factor = fa } | |
| 164 | 32 |
| 199 | 33 --divdable^2 : ( n k : ℕ ) → Dividable k ( n * n ) → Dividable k n |
| 34 --divdable^2 n k dn2 = {!!} | |
| 35 | |
| 164 | 36 decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n |
| 191 | 37 decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = |
| 38 decf1 {n} {k} f r fa where | |
| 39 decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n) → Factor k n | |
| 40 decf1 {n} {k} f (suc r) fa = -- this case must be the first | |
| 187 | 41 record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n |
|
189
6945d2aeb86a
expanding record does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
42 f * k + r ≡⟨ cong pred ( begin |
|
6945d2aeb86a
expanding record does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
43 suc ( f * k + r ) ≡⟨ +-comm _ r ⟩ |
|
6945d2aeb86a
expanding record does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
44 r + suc (f * k) ≡⟨ sym (+-assoc r 1 _) ⟩ |
|
6945d2aeb86a
expanding record does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
45 (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩ |
|
6945d2aeb86a
expanding record does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
46 (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩ |
|
6945d2aeb86a
expanding record does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
188
diff
changeset
|
47 f * k + suc r ≡⟨ fa ⟩ |
| 187 | 48 suc n ∎ ) ⟩ |
| 191 | 49 n ∎ ) } where open ≡-Reasoning |
| 50 decf1 {n} {zero} (suc f) zero fa = ⊥-elim ( nat-≡< fa ( | |
| 51 begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero) ⟩ | |
| 52 suc (f * 0) ≡⟨ cong suc (*-comm f zero) ⟩ | |
| 53 suc zero ≤⟨ s≤s z≤n ⟩ | |
| 54 suc n ∎ )) where open ≤-Reasoning | |
| 55 decf1 {n} {suc k} (suc f) zero fa = | |
| 56 record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n | |
| 57 f * suc k + k ≡⟨ +-comm _ k ⟩ | |
| 58 k + f * suc k ≡⟨ +-comm zero _ ⟩ | |
| 59 (k + f * suc k) + zero ≡⟨ cong pred fa ⟩ | |
| 60 n ∎ ) } where open ≡-Reasoning | |
| 164 | 61 |
| 196 | 62 div0 : {k : ℕ} → Dividable k 0 |
| 63 div0 {k} = record { factor = 0; is-factor = refl } | |
| 64 | |
| 209 | 65 div= : {k : ℕ} → Dividable k k |
| 66 div= {k} = record { factor = 1; is-factor = ( begin | |
| 67 k + 0 * k + 0 ≡⟨ trans ( +-comm _ 0) ( +-comm _ 0) ⟩ | |
| 68 k ∎ ) } where open ≡-Reasoning | |
| 69 | |
| 165 | 70 gcd1 : ( i i0 j j0 : ℕ ) → ℕ |
| 71 gcd1 zero i0 zero j0 with <-cmp i0 j0 | |
| 72 ... | tri< a ¬b ¬c = i0 | |
| 73 ... | tri≈ ¬a refl ¬c = i0 | |
| 74 ... | tri> ¬a ¬b c = j0 | |
| 75 gcd1 zero i0 (suc zero) j0 = 1 | |
| 76 gcd1 zero zero (suc (suc j)) j0 = j0 | |
| 77 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 78 gcd1 (suc zero) i0 zero j0 = 1 | |
| 79 gcd1 (suc (suc i)) i0 zero zero = i0 | |
| 80 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0) | |
| 81 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0 | |
| 82 | |
| 83 gcd : ( i j : ℕ ) → ℕ | |
| 84 gcd i j = gcd1 i i j j | |
| 85 | |
| 209 | 86 gcd20 : (i : ℕ) → gcd i 0 ≡ i |
| 87 gcd20 zero = refl | |
| 88 gcd20 (suc i) = gcd201 (suc i) where | |
| 89 gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i | |
| 90 gcd201 zero = refl | |
| 91 gcd201 (suc zero) = refl | |
| 92 gcd201 (suc (suc i)) = refl | |
| 93 | |
| 94 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 | |
| 95 gcd22 zero i0 zero o0 = refl | |
| 96 gcd22 zero i0 (suc o) o0 = refl | |
| 97 gcd22 (suc i) i0 zero o0 = refl | |
| 98 gcd22 (suc i) i0 (suc o) o0 = refl | |
| 99 | |
| 100 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m | |
| 101 gcdmm zero m with <-cmp m m | |
| 102 ... | tri< a ¬b ¬c = refl | |
| 103 ... | tri≈ ¬a refl ¬c = refl | |
| 104 ... | tri> ¬a ¬b c = refl | |
| 105 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m ) | |
| 106 | |
| 107 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i | |
| 108 gcdsym2 i j with <-cmp i j | <-cmp j i | |
| 109 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) | |
| 110 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 111 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl | |
| 112 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 113 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | |
| 114 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) | |
| 115 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | |
| 116 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) | |
| 117 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | |
| 118 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0 | |
| 119 gcdsym1 zero zero zero zero = refl | |
| 120 gcdsym1 zero zero zero (suc j0) = refl | |
| 121 gcdsym1 zero (suc i0) zero zero = refl | |
| 122 gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0) | |
| 123 gcdsym1 zero zero (suc zero) j0 = refl | |
| 124 gcdsym1 zero zero (suc (suc j)) j0 = refl | |
| 125 gcdsym1 zero (suc i0) (suc zero) j0 = refl | |
| 126 gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 127 gcdsym1 (suc zero) i0 zero j0 = refl | |
| 128 gcdsym1 (suc (suc i)) i0 zero zero = refl | |
| 129 gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) | |
| 130 gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 ) | |
| 131 | |
| 132 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n | |
| 133 gcdsym {n} {m} = gcdsym1 n n m m | |
| 134 | |
| 135 gcd11 : ( i : ℕ ) → gcd i i ≡ i | |
| 136 gcd11 i = gcdmm i i | |
| 137 | |
| 212 | 138 |
| 139 gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1 | |
| 140 gcd203 zero = refl | |
| 141 gcd203 (suc i) = gcd205 (suc i) where | |
| 142 gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1 | |
| 143 gcd205 zero = refl | |
| 144 gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j) (suc (suc i)) j (suc i)) (gcd205 j) | |
| 145 | |
| 146 gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1 | |
| 147 gcd204 zero = refl | |
| 148 gcd204 (suc zero) = refl | |
| 149 gcd204 (suc (suc zero)) = refl | |
| 150 gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) | |
| 151 | |
| 152 gcd+j : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j | |
| 153 gcd+j i j = gcd200 i i j j refl refl where | |
| 154 gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1) | |
| 155 gcd202 zero j1 = refl | |
| 156 gcd202 (suc i) j1 = cong suc (gcd202 i j1) | |
| 157 gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0 | |
| 158 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 | |
| 159 gcd201 i i0 j j0 (suc j1) = begin | |
| 160 gcd1 (i + suc j1) (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩ | |
| 161 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩ | |
| 162 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩ | |
| 163 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning | |
| 164 gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0 | |
| 165 gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl | |
| 166 gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j) | |
| 167 gcd200 zero zero (suc zero) .1 i=i0 refl = refl | |
| 168 gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin | |
| 169 gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩ | |
| 170 suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩ | |
| 171 gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning | |
| 172 gcd200 zero (suc i0) (suc j) .(suc j) () refl | |
| 173 gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin | |
| 174 gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩ | |
| 175 1 ≡⟨ sym ( gcd204 (suc j)) ⟩ | |
| 176 gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning | |
| 177 gcd200 (suc (suc i)) i0 (suc j) zero i=i0 () | |
| 178 | |
| 196 | 179 div1 : { k : ℕ } → k > 1 → ¬ Dividable k 1 |
| 180 div1 {k} k>1 record { factor = (suc f) ; is-factor = fa } = ⊥-elim ( nat-≡< (sym fa) ( begin | |
| 181 2 ≤⟨ k>1 ⟩ | |
| 182 k ≡⟨ +-comm 0 _ ⟩ | |
| 183 k + 0 ≡⟨ refl ⟩ | |
| 184 1 * k ≤⟨ *-mono-≤ {1} {suc f} (s≤s z≤n ) ≤-refl ⟩ | |
| 185 suc f * k ≡⟨ +-comm 0 _ ⟩ | |
| 186 suc f * k + 0 ∎ )) where open ≤-Reasoning | |
| 187 | |
| 213 | 188 div+div : { i j k : ℕ } → Dividable k i → Dividable k j → Dividable k (i + j) ∧ Dividable k (j + i) |
| 189 div+div {i} {j} {k} di dj = ⟪ div+div1 , subst (λ g → Dividable k g) (+-comm i j) div+div1 ⟫ where | |
| 190 fki = Dividable.factor di | |
| 191 fkj = Dividable.factor dj | |
| 192 div+div1 : Dividable k (i + j) | |
| 193 div+div1 = record { factor = fki + fkj ; is-factor = ( begin | |
| 194 (fki + fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 195 (fki + fkj) * k ≡⟨ *-distribʳ-+ k fki _ ⟩ | |
| 196 fki * k + fkj * k ≡⟨ cong₂ ( λ i j → i + j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩ | |
| 197 (fki * k + 0) + (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i + j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩ | |
| 198 i + j ∎ ) } where | |
| 199 open ≡-Reasoning | |
| 200 | |
| 197 | 201 div-div : { i j k : ℕ } → k > 1 → Dividable k i → Dividable k j → Dividable k (i - j) ∧ Dividable k (j - i) |
| 213 | 202 div-div {i} {j} {k} k>1 di dj = ⟪ div-div1 di dj , div-div1 dj di ⟫ where |
| 203 div-div1 : {i j : ℕ } → Dividable k i → Dividable k j → Dividable k (i - j) | |
| 204 div-div1 {i} {j} di dj = record { factor = fki - fkj ; is-factor = ( begin | |
| 205 (fki - fkj) * k + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 206 (fki - fkj) * k ≡⟨ distr-minus-* {fki} {fkj} ⟩ | |
| 207 (fki * k) - (fkj * k) ≡⟨ cong₂ ( λ i j → i - j ) (+-comm 0 (fki * k)) (+-comm 0 (fkj * k)) ⟩ | |
| 208 (fki * k + 0) - (fkj * k + 0) ≡⟨ cong₂ ( λ i j → i - j ) (Dividable.is-factor di) (Dividable.is-factor dj) ⟩ | |
| 209 i - j ∎ ) } where | |
| 197 | 210 open ≡-Reasoning |
| 213 | 211 fki = Dividable.factor di |
| 212 fkj = Dividable.factor dj | |
| 197 | 213 |
| 196 | 214 open _∧_ |
| 192 | 215 |
| 215 | 216 div+1 : { i k : ℕ } → k > 1 → Dividable k i → ¬ Dividable k (suc i) |
| 217 div+1 {i} {k} k>1 d d1 = div1 k>1 div+11 where | |
| 218 div+11 : Dividable k 1 | |
| 219 div+11 = subst (λ g → Dividable k g) (minus+y-y {1} {i} ) ( proj2 (div-div k>1 d d1 ) ) | |
| 220 | |
| 221 div<k : { m k : ℕ } → k > 1 → m > 0 → m < k → ¬ Dividable k m | |
| 222 div<k {m} {k} k>1 m>0 m<k d = ⊥-elim ( nat-≤> (div<k1 (Dividable.factor d) (Dividable.is-factor d)) m<k ) where | |
| 223 div<k1 : (f : ℕ ) → f * k + 0 ≡ m → k ≤ m | |
| 224 div<k1 zero eq = ⊥-elim (nat-≡< eq m>0 ) | |
| 225 div<k1 (suc f) eq = begin | |
| 226 k ≤⟨ x≤x+y ⟩ | |
| 227 k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ | |
| 228 k + f * k + 0 ≡⟨ eq ⟩ | |
| 229 m ∎ where open ≤-Reasoning | |
| 230 | |
| 227 | 231 div→k≤m : { m k : ℕ } → k > 1 → m > 0 → Dividable k m → m ≥ k |
| 232 div→k≤m {m} {k} k>1 m>0 d with <-cmp m k | |
| 233 ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 m>0 a d ) | |
| 234 ... | tri≈ ¬a refl ¬c = ≤-refl | |
| 235 ... | tri> ¬a ¬b c = <to≤ c | |
| 236 | |
| 215 | 237 div1*k+0=k : {k : ℕ } → 1 * k + 0 ≡ k |
| 238 div1*k+0=k {k} = begin | |
| 239 1 * k + 0 ≡⟨ cong (λ g → g + 0) (+-comm _ 0) ⟩ | |
| 240 k + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 241 k ∎ where open ≡-Reasoning | |
| 242 | |
| 220 | 243 decD : {k m : ℕ} → k > 1 → Dec (Dividable k m ) |
| 244 decD {k} {m} k>1 = n-induction {_} {_} {ℕ} {λ m → Dec (Dividable k m ) } F I m where | |
| 215 | 245 F : ℕ → ℕ |
| 216 | 246 F m = m |
| 220 | 247 F0 : ( m : ℕ ) → F (m - k) ≡ 0 → Dec (Dividable k m ) |
| 248 F0 0 eq = yes record { factor = 0 ; is-factor = refl } | |
| 215 | 249 F0 (suc m) eq with <-cmp k (suc m) |
| 220 | 250 ... | tri< a ¬b ¬c = yes record { factor = 1 ; is-factor = |
| 251 subst (λ g → 1 * k + 0 ≡ g ) (sym (i-j=0→i=j (<to≤ a) eq )) div1*k+0=k } where -- (suc m - k) ≡ 0 → k ≡ suc m, k ≤ suc m | |
| 252 ... | tri≈ ¬a refl ¬c = yes record { factor = 1 ; is-factor = div1*k+0=k } | |
| 253 ... | tri> ¬a ¬b c = no ( λ d → ⊥-elim (div<k k>1 (s≤s z≤n ) c d) ) | |
| 216 | 254 decl : {m : ℕ } → 0 < m → m - k < m |
| 217 | 255 decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m |
| 220 | 256 ind : (p : ℕ ) → Dec (Dividable k (p - k) ) → Dec (Dividable k p ) |
| 257 ind p (yes y) with <-cmp p k | |
| 258 ... | tri≈ ¬a refl ¬c = yes (subst (λ g → Dividable k g) (minus+n ≤-refl ) (proj1 ( div+div y div= ))) | |
| 259 ... | tri> ¬a ¬b k<p = yes (subst (λ g → Dividable k g) (minus+n (<-trans k<p a<sa)) (proj1 ( div+div y div= ))) | |
| 221 | 260 ... | tri< a ¬b ¬c with <-cmp p 0 |
| 261 ... | tri≈ ¬a refl ¬c₁ = yes div0 | |
| 262 ... | tri> ¬a ¬b₁ c = no (λ d → not-div p (Dividable.factor d) a c (Dividable.is-factor d) ) where | |
| 263 not-div : (p f : ℕ) → p < k → 0 < p → f * k + 0 ≡ p → ⊥ | |
| 264 not-div (suc p) (suc f) p<k 0<p eq = nat-≡< (sym eq) ( begin -- ≤-trans p<k {!!}) -- suc p ≤ k | |
| 265 suc (suc p) ≤⟨ p<k ⟩ | |
| 266 k ≤⟨ x≤x+y ⟩ | |
| 267 k + (f * k + 0) ≡⟨ sym (+-assoc k _ _) ⟩ | |
| 268 suc f * k + 0 ∎ ) where open ≤-Reasoning | |
| 220 | 269 ind p (no n) = no (λ d → n (proj1 (div-div k>1 d div=)) ) |
| 216 | 270 I : Ninduction ℕ _ F |
| 215 | 271 I = record { |
| 216 | 272 pnext = λ p → p - k |
| 217 | 273 ; fzero = λ {m} eq → F0 m eq |
| 219 | 274 ; decline = λ {m} lt → decl lt |
| 217 | 275 ; ind = λ {p} prev → ind p prev |
| 215 | 276 } |
| 277 | |
|
193
875eb1fa9694
dividable reorganzaiton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
278 gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0) |
| 196 | 279 → Dividable k (i - j) ∧ Dividable k (j - i) |
| 165 | 280 → Dividable k ( gcd1 i i0 j j0 ) |
| 196 | 281 gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i-j with <-cmp i0 j0 |
| 194 | 282 ... | tri< a ¬b ¬c = i0f |
| 283 ... | tri≈ ¬a refl ¬c = i0f | |
| 284 ... | tri> ¬a ¬b c = j0f | |
| 196 | 285 gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f i-j = ⊥-elim (div1 k>1 (proj2 i-j)) -- can't happen |
| 286 gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = j0f | |
| 287 gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = | |
| 197 | 288 gcd-gt i0 (suc i0) (suc j) (suc (suc j)) k k>1 (decf (DtoF i0f)) i0f (decf jf) (proj2 i-j) (div-div k>1 i0f (proj2 i-j)) |
| 196 | 289 gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f i-j = ⊥-elim (div1 k>1 (proj1 i-j)) -- can't happen |
| 290 gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-j = i0f | |
| 291 gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-j = -- | |
| 197 | 292 gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) (proj1 i-j) (decf (DtoF j0f)) j0f (div-div k>1 (proj1 i-j) j0f ) |
| 196 | 293 gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-j = |
| 294 gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j | |
| 295 gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-j = | |
| 296 gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j | |
| 164 | 297 |
| 194 | 298 gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) |
| 186 | 299 → Dividable k ( gcd i j ) |
| 197 | 300 gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf (div-div k>1 if jf) |
| 143 | 301 |
| 227 | 302 gcd-dividable : ( i j : ℕ ) |
| 212 | 303 → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j |
| 227 | 304 gcd-dividable i j = f-induction {_} {_} {ℕ ∧ ℕ} |
| 209 | 305 {λ p → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p) (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where |
| 306 F : ℕ ∧ ℕ → ℕ | |
| 224 | 307 F ⟪ 0 , 0 ⟫ = 0 |
| 308 F ⟪ 0 , suc j ⟫ = 0 | |
| 222 | 309 F ⟪ suc i , 0 ⟫ = 0 |
| 224 | 310 F ⟪ suc i , suc j ⟫ with <-cmp i j |
| 311 ... | tri< a ¬b ¬c = suc j | |
| 209 | 312 ... | tri≈ ¬a b ¬c = 0 |
| 224 | 313 ... | tri> ¬a ¬b c = suc i |
| 209 | 314 F0 : { i j : ℕ } → F ⟪ i , j ⟫ ≡ 0 → (i ≡ j) ∨ (i ≡ 0 ) ∨ (j ≡ 0) |
| 315 F0 {zero} {zero} p = case1 refl | |
| 316 F0 {zero} {suc j} p = case2 (case1 refl) | |
| 317 F0 {suc i} {zero} p = case2 (case2 refl) | |
| 318 F0 {suc i} {suc j} p with <-cmp i j | |
| 224 | 319 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n )) |
| 320 ... | tri≈ ¬a refl ¬c = case1 refl | |
| 321 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n )) | |
| 322 F00 : {p : ℕ ∧ ℕ} → F p ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p) | |
| 323 F00 {⟪ i , j ⟫} eq with F0 {i} {j} eq | |
| 324 ... | case1 refl = ⟪ subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫ | |
| 325 ... | case2 (case1 refl) = ⟪ subst (λ k → Dividable k i) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0 | |
| 326 , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫ | |
| 327 ... | case2 (case2 refl) = ⟪ subst (λ k → Dividable k i) (sym (gcd20 i)) div= | |
| 328 , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫ | |
| 329 Fsym : {i j : ℕ } → F ⟪ i , j ⟫ ≡ F ⟪ j , i ⟫ | |
| 330 Fsym {0} {0} = refl | |
| 331 Fsym {0} {suc j} = refl | |
| 332 Fsym {suc i} {0} = refl | |
| 333 Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i | |
| 334 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) | |
| 335 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b)) | |
| 336 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl | |
| 337 ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) | |
| 338 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | |
| 339 ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) | |
| 340 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | |
| 341 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b)) | |
| 342 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | |
| 343 | |
| 344 record Fdec ( i j : ℕ ) : Set where | |
| 345 field | |
| 346 ni : ℕ | |
| 347 nj : ℕ | |
| 348 fdec : 0 < F ⟪ i , j ⟫ → F ⟪ ni , nj ⟫ < F ⟪ i , j ⟫ | |
| 214 | 349 |
| 224 | 350 fd1 : ( i j k : ℕ ) → i < j → k ≡ j - i → F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫ |
| 351 fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) | |
| 352 fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where | |
| 353 fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i → F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫ | |
| 354 fd2 i j k i<j eq with <-cmp i k | <-cmp i j | |
| 355 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where | |
| 356 fd3 : suc k < suc j -- suc j - suc i < suc j | |
| 357 fd3 = subst (λ g → g < suc j) (sym eq) (y-x<y {suc i} {suc j} (s≤s z≤n) (s≤s z≤n)) | |
| 358 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (⊥-elim (¬a i<j)) | |
| 359 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (⊥-elim (¬a i<j)) | |
| 360 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n | |
| 361 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (¬a₁ i<j) | |
| 362 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = s≤s z≤n -- i > j | |
| 363 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where | |
| 364 fd4 : suc i < suc j | |
| 365 fd4 = s≤s a | |
| 366 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬a₁ i<j) | |
| 367 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (¬a₁ i<j) | |
| 368 | |
| 369 fedc0 : (i j : ℕ ) → Fdec i j | |
| 370 fedc0 0 0 = record { ni = 0 ; nj = 0 ; fdec = λ () } | |
| 371 fedc0 (suc i) 0 = record { ni = suc i ; nj = 0 ; fdec = λ () } | |
| 372 fedc0 0 (suc j) = record { ni = 0 ; nj = suc j ; fdec = λ () } | |
| 373 fedc0 (suc i) (suc j) with <-cmp i j | |
| 374 ... | tri< i<j ¬b ¬c = record { ni = suc i ; nj = j - i ; fdec = λ lt → fd1 i j (j - i) i<j refl } | |
| 375 ... | tri≈ ¬a refl ¬c = record { ni = suc i ; nj = suc j ; fdec = λ lt → ⊥-elim (nat-≡< fd0 lt) } where | |
| 376 fd0 : {i : ℕ } → 0 ≡ F ⟪ suc i , suc i ⟫ | |
| 377 fd0 {i} with <-cmp i i | |
| 378 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) | |
| 379 ... | tri≈ ¬a b ¬c = refl | |
| 380 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) | |
| 381 ... | tri> ¬a ¬b c = record { ni = i - j ; nj = suc j ; fdec = λ lt → | |
| 382 subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } | |
| 214 | 383 |
| 384 ind3 : {i j : ℕ } → i < j | |
| 385 → Dividable (gcd (suc i) (j - i)) (suc i) | |
| 386 → Dividable (gcd (suc i) (suc j)) (suc i) | |
| 387 ind3 {i} {j} a prev = | |
| 388 subst (λ k → Dividable k (suc i)) ( begin | |
| 389 gcd (suc i) (j - i) ≡⟨ gcdsym {suc i} {j - i} ⟩ | |
| 390 gcd (j - i ) (suc i) ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩ | |
| 391 gcd ((j - i) + suc i) (suc i) ≡⟨ cong (λ k → gcd k (suc i)) ( begin | |
| 392 (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans ( s≤s a) a<sa ) ⟩ -- i ≤ n → suc (suc i) ≤ suc (suc (suc n)) | |
| 393 suc j ∎ ) ⟩ | |
| 394 gcd (suc j) (suc i) ≡⟨ gcdsym {suc j} {suc i} ⟩ | |
| 395 gcd (suc i) (suc j) ∎ ) prev where open ≡-Reasoning | |
| 396 ind7 : {i j : ℕ } → (i < j ) → (j - i) + suc i ≡ suc j | |
| 397 ind7 {i} {j} a = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa) ⟩ | |
| 398 suc j ∎ where open ≡-Reasoning | |
| 399 ind6 : {i j k : ℕ } → i < j | |
| 400 → Dividable k (j - i) | |
| 401 → Dividable k (suc i) | |
| 402 → Dividable k (suc j) | |
| 403 ind6 {i} {j} {k} i<j dj di = subst (λ g → Dividable k g ) (ind7 i<j) (proj1 (div+div dj di)) | |
| 404 ind4 : {i j : ℕ } → i < j | |
| 405 → Dividable (gcd (suc i) (j - i)) (j - i) | |
| 406 → Dividable (gcd (suc i) (suc j)) (j - i) | |
| 407 ind4 {i} {j} i<j prev = subst (λ k → k) ( begin | |
| 408 Dividable (gcd (suc i) (j - i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc i} ) ⟩ | |
| 409 Dividable (gcd (j - i ) (suc i) ) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) ( sym (gcd+j (j - i) (suc i))) ⟩ | |
| 410 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable (gcd k (suc i)) (j - i)) (ind7 i<j ) ⟩ | |
| 411 Dividable (gcd (suc j) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩ | |
| 412 Dividable (gcd (suc i) (suc j)) (j - i) ∎ ) prev where open ≡-Reasoning | |
| 413 | |
| 224 | 414 ind : ( i j : ℕ ) → |
| 415 Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j)) | |
| 416 ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j)) | |
| 417 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j | |
| 418 ind zero zero prev = ind0 where | |
| 210 | 419 ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero |
| 212 | 420 ind0 = ⟪ div0 , div0 ⟫ |
| 224 | 421 ind zero (suc j) prev = ind1 where |
| 210 | 422 ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j) |
| 212 | 423 ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div= ⟫ |
| 224 | 424 ind (suc i) zero prev = ind2 where |
| 210 | 425 ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero |
| 212 | 426 ind2 = ⟪ subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫ |
| 224 | 427 ind (suc i) (suc j) prev with <-cmp i j |
| 428 ... | tri< a ¬b ¬c = ⟪ ind3 a (proj1 prev) , ind6 a (ind4 a (proj2 prev)) (ind3 a (proj1 prev) ) ⟫ where | |
| 213 | 429 ... | tri≈ ¬a refl ¬c = ⟪ ind5 , ind5 ⟫ where |
| 430 ind5 : Dividable (gcd (suc i) (suc i)) (suc i) | |
| 431 ind5 = subst (λ k → Dividable k (suc j)) (sym (gcdmm (suc i) (suc i))) div= | |
| 224 | 432 ... | tri> ¬a ¬b c = ⟪ ind8 c (proj1 prev) (proj2 prev) , ind10 c (proj2 prev) ⟫ where |
| 214 | 433 ind9 : {i j : ℕ} → i < j → gcd (j - i) (suc i) ≡ gcd (suc j) (suc i) |
| 434 ind9 {i} {j} i<j = begin | |
| 435 gcd (j - i ) (suc i) ≡⟨ sym (gcd+j (j - i ) (suc i) ) ⟩ | |
| 436 gcd (j - i + suc i) (suc i) ≡⟨ cong (λ k → gcd k (suc i)) (ind7 i<j ) ⟩ | |
| 437 gcd (suc j) (suc i) ∎ where open ≡-Reasoning | |
| 438 ind8 : { i j : ℕ } → i < j | |
| 439 → Dividable (gcd (j - i) (suc i)) (j - i) | |
| 440 → Dividable (gcd (j - i) (suc i)) (suc i) | |
| 441 → Dividable (gcd (suc j) (suc i)) (suc j) | |
| 442 ind8 {i} {j} i<j dji di = ind6 i<j (subst (λ k → Dividable k (j - i)) (ind9 i<j) dji) (subst (λ k → Dividable k (suc i)) (ind9 i<j) di) | |
| 443 ind10 : { i j : ℕ } → j < i | |
| 444 → Dividable (gcd (i - j) (suc j)) (suc j) | |
| 445 → Dividable (gcd (suc i) (suc j)) (suc j) | |
| 446 ind10 {i} {j} j<i dji = subst (λ g → Dividable g (suc j) ) (begin | |
| 447 gcd (i - j) (suc j) ≡⟨ sym (gcd+j (i - j) (suc j)) ⟩ | |
| 448 gcd (i - j + suc j) (suc j) ≡⟨ cong (λ k → gcd k (suc j)) (ind7 j<i ) ⟩ | |
| 449 gcd (suc i) (suc j) ∎ ) dji where open ≡-Reasoning | |
| 210 | 450 |
| 224 | 451 I : Finduction (ℕ ∧ ℕ) _ F |
| 209 | 452 I = record { |
| 224 | 453 fzero = F00 |
| 454 ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) , Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ | |
| 455 ; decline = λ {p} lt → Fdec.fdec (fedc0 (proj1 p) (proj2 p)) lt | |
| 456 ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev | |
| 209 | 457 } |
| 458 | |
| 206 | 459 |
| 167 | 460 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1 |
| 461 gcdmul+1 zero n = gcd204 n | |
| 462 gcdmul+1 (suc m) n = begin | |
| 463 gcd (suc m * n + 1) n ≡⟨⟩ | |
| 464 gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin | |
| 465 n + m * n + 1 ≡⟨ cong (λ k → k + 1) (+-comm n _) ⟩ | |
| 466 m * n + n + 1 ≡⟨ +-assoc (m * n) _ _ ⟩ | |
| 467 m * n + (n + 1) ≡⟨ cong (λ k → m * n + k) (+-comm n _) ⟩ | |
| 468 m * n + (1 + n) ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩ | |
| 469 m * n + 1 + n ∎ | |
| 470 ) ⟩ | |
| 212 | 471 gcd (m * n + 1 + n) n ≡⟨ gcd+j (m * n + 1) n ⟩ |
| 167 | 472 gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩ |
| 473 1 ∎ where open ≡-Reasoning | |
| 474 | |
| 205 | 475 gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j |
| 476 gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where | |
| 477 gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0 → gcd1 i i0 j j0 > 0 | |
| 478 gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0 | |
| 479 ... | tri< a ¬b ¬c = 0<i | |
| 480 ... | tri≈ ¬a refl ¬c = 0<i | |
| 481 ... | tri> ¬a ¬b c = 0<j | |
| 482 gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n | |
| 483 gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j | |
| 484 gcd>01 zero (suc i0) (suc (suc j)) j0 0<i 0<j = gcd>01 i0 (suc i0) (suc j) (suc (suc j)) 0<i (s≤s z≤n) -- 0 < suc (suc j) | |
| 485 gcd>01 (suc zero) i0 zero j0 0<i 0<j = s≤s z≤n | |
| 486 gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i | |
| 487 gcd>01 (suc (suc i)) i0 zero (suc j0) 0<i 0<j = gcd>01 (suc i) (suc (suc i)) j0 (suc j0) (s≤s z≤n) 0<j | |
| 488 gcd>01 (suc i) i0 (suc j) j0 0<i 0<j = subst (λ k → 0 < k ) (sym (gcd033 i i0 j j0 )) (gcd>01 i i0 j j0 0<i 0<j ) where | |
| 489 gcd033 : (i i0 j j0 : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡ gcd1 i i0 j j0 | |
| 490 gcd033 zero zero zero zero = refl | |
| 491 gcd033 zero zero (suc j) zero = refl | |
| 492 gcd033 (suc i) zero j zero = refl | |
| 493 gcd033 zero zero zero (suc j0) = refl | |
| 494 gcd033 (suc i) zero zero (suc j0) = refl | |
| 495 gcd033 zero zero (suc j) (suc j0) = refl | |
| 496 gcd033 (suc i) zero (suc j) (suc j0) = refl | |
| 497 gcd033 zero (suc i0) j j0 = refl | |
| 498 gcd033 (suc i) (suc i0) j j0 = refl | |
| 227 | 499 |
| 500 --gcd-dividable : ( i j : ℕ ) | |
| 501 -- → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j | |
| 502 | |
| 503 f-div>0 : { k i : ℕ } → (d : Dividable k i ) → 0 < i → 0 < Dividable.factor d | |
| 504 f-div>0 {k} {i} d 0<i with <-cmp 0 (Dividable.factor d) | |
| 505 ... | tri< a ¬b ¬c = a | |
| 506 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (begin | |
| 507 0 * k + 0 ≡⟨ cong (λ g → g * k + 0) b ⟩ | |
| 508 Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ | |
| 509 i ∎ ) 0<i ) where open ≡-Reasoning | |
| 510 | |
| 511 gcd-≤ : ( i j : ℕ ) → i ≤ j → gcd i j ≤ j | |
| 512 gcd-≤ zero zero z≤n = ≤-refl | |
| 513 gcd-≤ 0 (suc j) z≤n = subst (λ k → k ≤ suc j ) (trans (sym (gcd20 (suc j))) (gcdsym {suc j} {zero})) ≤-refl | |
| 514 gcd-≤ (suc i) (suc j) (s≤s i<j) = begin | |
| 515 gcd (suc i) (suc j) ≡⟨ sym m*1=m ⟩ | |
| 516 gcd (suc i) (suc j) * 1 ≤⟨ *-monoʳ-≤ (gcd (suc i) (suc j)) (f-div>0 d (s≤s z≤n)) ⟩ | |
| 517 gcd (suc i) (suc j) * f ≡⟨ +-comm 0 _ ⟩ | |
| 518 gcd (suc i) (suc j) * f + 0 ≡⟨ cong (λ k → k + 0) (*-comm (gcd (suc i) (suc j)) _ ) ⟩ | |
| 519 Dividable.factor (proj2 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj2 (gcd-dividable (suc i) (suc j))) ⟩ | |
| 520 suc j ∎ where | |
| 521 d = proj2 (gcd-dividable (suc i) (suc j)) | |
| 522 f = Dividable.factor (proj2 (gcd-dividable (suc i) (suc j))) | |
| 523 open ≤-Reasoning | |
| 524 | |
| 525 m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1 | |
| 526 m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq | |
| 527 | |
| 528 gcd-< : ( i j : ℕ ) → 0 < i → i < j → gcd i j < j | |
| 529 gcd-< i j 0<i i<j with <-cmp ( gcd i j ) j | |
| 530 ... | tri< a ¬b ¬c = a | |
| 531 ... | tri≈ ¬a b ¬c = ⊥-elim (g111 (Dividable.factor (proj1 (gcd-dividable i j))) | |
| 532 (subst (λ k → (Dividable.factor (proj1 (gcd-dividable i j))) * k + 0 ≡ i ) b (Dividable.is-factor (proj1 (gcd-dividable i j))))) where | |
| 533 g111 : (f : ℕ) → f * j + 0 ≡ i → ⊥ | |
| 534 g111 zero eq = nat-≡< eq 0<i | |
| 535 g111 (suc zero) eq = nat-≡< (sym eq) (begin | |
| 536 suc i ≤⟨ i<j ⟩ | |
| 537 j ≡⟨ trans (+-comm 0 _) (+-comm 0 _) ⟩ | |
| 538 1 * j + 0 ∎ ) where open ≤-Reasoning | |
| 539 g111 (suc (suc f)) eq = nat-≡< (sym eq) ( begin | |
| 540 suc i ≤⟨ i<j ⟩ | |
| 541 j ≡⟨ +-comm 0 _ ⟩ | |
| 542 j + 0 ≤⟨ +-monoʳ-≤ j z≤n ⟩ | |
| 543 j + ((j + f * j) + 0) ≡⟨ sym (+-assoc j _ _) ⟩ | |
| 544 j + (j + f * j) + 0 ≡⟨ refl ⟩ | |
| 545 suc (suc f) * j + 0 ∎ ) where open ≤-Reasoning | |
| 546 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (gcd-≤ i j (<to≤ i<j)) c ) |