Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/gcd.agda @ 289:c9802aa2a8c9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Dec 2021 15:25:22 +0900 |
| parents | 8b437dd616dd |
| children | 4a00e5f2b793 |
| 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 open Factor |
| 15 | |
| 165 | 16 gcd1 : ( i i0 j j0 : ℕ ) → ℕ |
| 17 gcd1 zero i0 zero j0 with <-cmp i0 j0 | |
| 18 ... | tri< a ¬b ¬c = i0 | |
| 19 ... | tri≈ ¬a refl ¬c = i0 | |
| 20 ... | tri> ¬a ¬b c = j0 | |
| 21 gcd1 zero i0 (suc zero) j0 = 1 | |
| 22 gcd1 zero zero (suc (suc j)) j0 = j0 | |
| 23 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 24 gcd1 (suc zero) i0 zero j0 = 1 | |
| 25 gcd1 (suc (suc i)) i0 zero zero = i0 | |
| 26 gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i)) j0 (suc j0) | |
| 27 gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0 | |
| 28 | |
| 29 gcd : ( i j : ℕ ) → ℕ | |
| 30 gcd i j = gcd1 i i j j | |
| 31 | |
| 209 | 32 gcd20 : (i : ℕ) → gcd i 0 ≡ i |
| 33 gcd20 zero = refl | |
| 34 gcd20 (suc i) = gcd201 (suc i) where | |
| 35 gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i | |
| 36 gcd201 zero = refl | |
| 37 gcd201 (suc zero) = refl | |
| 38 gcd201 (suc (suc i)) = refl | |
| 39 | |
| 40 gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0 | |
| 41 gcd22 zero i0 zero o0 = refl | |
| 42 gcd22 zero i0 (suc o) o0 = refl | |
| 43 gcd22 (suc i) i0 zero o0 = refl | |
| 44 gcd22 (suc i) i0 (suc o) o0 = refl | |
| 45 | |
| 46 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m | |
| 47 gcdmm zero m with <-cmp m m | |
| 48 ... | tri< a ¬b ¬c = refl | |
| 49 ... | tri≈ ¬a refl ¬c = refl | |
| 50 ... | tri> ¬a ¬b c = refl | |
| 51 gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m ) | |
| 52 | |
| 53 gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i | |
| 54 gcdsym2 i j with <-cmp i j | <-cmp j i | |
| 55 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) | |
| 56 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 57 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl | |
| 58 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) | |
| 59 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | |
| 60 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) | |
| 61 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | |
| 62 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) | |
| 63 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | |
| 64 gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0 | |
| 65 gcdsym1 zero zero zero zero = refl | |
| 66 gcdsym1 zero zero zero (suc j0) = refl | |
| 67 gcdsym1 zero (suc i0) zero zero = refl | |
| 68 gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0) | |
| 69 gcdsym1 zero zero (suc zero) j0 = refl | |
| 70 gcdsym1 zero zero (suc (suc j)) j0 = refl | |
| 71 gcdsym1 zero (suc i0) (suc zero) j0 = refl | |
| 72 gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j)) | |
| 73 gcdsym1 (suc zero) i0 zero j0 = refl | |
| 74 gcdsym1 (suc (suc i)) i0 zero zero = refl | |
| 75 gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) | |
| 76 gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 ) | |
| 77 | |
| 78 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n | |
| 79 gcdsym {n} {m} = gcdsym1 n n m m | |
| 80 | |
| 81 gcd11 : ( i : ℕ ) → gcd i i ≡ i | |
| 82 gcd11 i = gcdmm i i | |
| 83 | |
| 212 | 84 |
| 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 | |
| 92 gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1 | |
| 93 gcd204 zero = refl | |
| 94 gcd204 (suc zero) = refl | |
| 95 gcd204 (suc (suc zero)) = refl | |
| 96 gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) | |
| 97 | |
| 98 gcd+j : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j | |
| 99 gcd+j i j = gcd200 i i j j refl refl where | |
| 100 gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1) | |
| 101 gcd202 zero j1 = refl | |
| 102 gcd202 (suc i) j1 = cong suc (gcd202 i j1) | |
| 103 gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0 | |
| 104 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 | |
| 105 gcd201 i i0 j j0 (suc j1) = begin | |
| 106 gcd1 (i + suc j1) (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩ | |
| 107 gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩ | |
| 108 gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩ | |
| 109 gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning | |
| 110 gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0 | |
| 111 gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl | |
| 112 gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j) | |
| 113 gcd200 zero zero (suc zero) .1 i=i0 refl = refl | |
| 114 gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin | |
| 115 gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩ | |
| 116 suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩ | |
| 117 gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning | |
| 118 gcd200 zero (suc i0) (suc j) .(suc j) () refl | |
| 119 gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin | |
| 120 gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩ | |
| 121 1 ≡⟨ sym ( gcd204 (suc j)) ⟩ | |
| 122 gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning | |
| 123 gcd200 (suc (suc i)) i0 (suc j) zero i=i0 () | |
| 124 | |
| 196 | 125 open _∧_ |
| 192 | 126 |
|
193
875eb1fa9694
dividable reorganzaiton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
127 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 | 128 → Dividable k (i - j) ∧ Dividable k (j - i) |
| 165 | 129 → Dividable k ( gcd1 i i0 j j0 ) |
| 196 | 130 gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f i-j with <-cmp i0 j0 |
| 194 | 131 ... | tri< a ¬b ¬c = i0f |
| 132 ... | tri≈ ¬a refl ¬c = i0f | |
| 133 ... | tri> ¬a ¬b c = j0f | |
| 196 | 134 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 |
| 135 gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = j0f | |
| 136 gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f i-j = | |
| 197 | 137 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 | 138 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 |
| 139 gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f i-j = i0f | |
| 140 gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f i-j = -- | |
| 197 | 141 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 | 142 gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f i-j = |
| 143 gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j | |
| 144 gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f i-j = | |
| 145 gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f i-j | |
| 164 | 146 |
| 194 | 147 gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) |
| 186 | 148 → Dividable k ( gcd i j ) |
| 197 | 149 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 | 150 |
| 235 | 151 di-next : {i i0 j j0 : ℕ} → Dividable i0 ((j0 + suc i) - suc j ) ∧ Dividable j0 ((i0 + suc j) - suc i) → |
| 152 Dividable i0 ((j0 + i) - j ) ∧ Dividable j0 ((i0 + j) - i) | |
| 153 di-next {i} {i0} {j} {j0} x = | |
| 154 ⟪ ( subst (λ k → Dividable i0 (k - suc j)) ( begin | |
| 155 j0 + suc i ≡⟨ sym (+-assoc j0 1 i ) ⟩ | |
| 156 (j0 + 1) + i ≡⟨ cong (λ k → k + i) (+-comm j0 _ ) ⟩ | |
| 157 suc (j0 + i) ∎ ) (proj1 x) ) , | |
| 158 ( subst (λ k → Dividable j0 (k - suc i)) ( begin | |
| 159 i0 + suc j ≡⟨ sym (+-assoc i0 1 j ) ⟩ | |
| 160 (i0 + 1) + j ≡⟨ cong (λ k → k + j) (+-comm i0 _ ) ⟩ | |
| 161 suc (i0 + j) ∎ ) (proj2 x) ) ⟫ | |
| 162 where open ≡-Reasoning | |
| 163 | |
| 164 di-next1 : {i0 j j0 : ℕ} → Dividable (suc i0) ((j0 + 0) - (suc (suc j))) ∧ Dividable j0 (suc (i0 + suc (suc j))) | |
| 165 → Dividable (suc i0) ((suc (suc j) + i0) - suc j) ∧ Dividable (suc (suc j)) ((suc i0 + suc j) - i0) | |
| 166 di-next1 {i0} {j} {j0} x = | |
| 167 ⟪ record { factor = 1 ; is-factor = begin | |
| 168 1 * suc i0 + 0 ≡⟨ cong suc ( trans (+-comm _ 0) (+-comm _ 0) ) ⟩ | |
| 169 suc i0 ≡⟨ sym (minus+y-y {suc i0} {j}) ⟩ | |
| 170 (suc i0 + j) - j ≡⟨ cong (λ k → k - j ) (+-comm (suc i0) _ ) ⟩ | |
| 171 (suc j + suc i0 ) - suc j ≡⟨ cong (λ k → k - suc j) (sym (+-assoc (suc j) 1 i0 )) ⟩ | |
| 172 ((suc j + 1) + i0) - suc j ≡⟨ cong (λ k → (k + i0) - suc j) (+-comm _ 1) ⟩ | |
| 173 (suc (suc j) + i0) - suc j ∎ } , | |
| 174 subst (λ k → Dividable (suc (suc j)) k) ( begin | |
| 175 suc (suc j) ≡⟨ sym ( minus+y-y {suc (suc j)}{i0} ) ⟩ | |
| 176 (suc (suc j) + i0 ) - i0 ≡⟨ cong (λ k → (k + i0) - i0) (cong suc (+-comm 1 _ )) ⟩ | |
| 177 ((suc j + 1) + i0 ) - i0 ≡⟨ cong (λ k → k - i0) (+-assoc (suc j) 1 _ ) ⟩ | |
| 178 (suc j + suc i0 ) - i0 ≡⟨ cong (λ k → k - i0) (+-comm (suc j) _) ⟩ | |
| 179 ((suc i0 + suc j) - i0) ∎ ) div= ⟫ | |
| 180 where open ≡-Reasoning | |
| 181 | |
| 245 | 182 gcd>0 : ( i j : ℕ ) → 0 < i → 0 < j → 0 < gcd i j |
| 183 gcd>0 i j 0<i 0<j = gcd>01 i i j j 0<i 0<j where | |
| 184 gcd>01 : ( i i0 j j0 : ℕ ) → 0 < i0 → 0 < j0 → gcd1 i i0 j j0 > 0 | |
| 185 gcd>01 zero i0 zero j0 0<i 0<j with <-cmp i0 j0 | |
| 186 ... | tri< a ¬b ¬c = 0<i | |
| 187 ... | tri≈ ¬a refl ¬c = 0<i | |
| 188 ... | tri> ¬a ¬b c = 0<j | |
| 189 gcd>01 zero i0 (suc zero) j0 0<i 0<j = s≤s z≤n | |
| 190 gcd>01 zero zero (suc (suc j)) j0 0<i 0<j = 0<j | |
| 191 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) | |
| 192 gcd>01 (suc zero) i0 zero j0 0<i 0<j = s≤s z≤n | |
| 193 gcd>01 (suc (suc i)) i0 zero zero 0<i 0<j = 0<i | |
| 194 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 | |
| 195 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 | |
| 196 gcd033 : (i i0 j j0 : ℕ) → gcd1 (suc i) i0 (suc j) j0 ≡ gcd1 i i0 j j0 | |
| 197 gcd033 zero zero zero zero = refl | |
| 198 gcd033 zero zero (suc j) zero = refl | |
| 199 gcd033 (suc i) zero j zero = refl | |
| 200 gcd033 zero zero zero (suc j0) = refl | |
| 201 gcd033 (suc i) zero zero (suc j0) = refl | |
| 202 gcd033 zero zero (suc j) (suc j0) = refl | |
| 203 gcd033 (suc i) zero (suc j) (suc j0) = refl | |
| 204 gcd033 zero (suc i0) j j0 = refl | |
| 205 gcd033 (suc i) (suc i0) j j0 = refl | |
| 206 | |
| 238 | 207 -- gcd loop invariant |
| 208 -- | |
| 209 record GCD ( i i0 j j0 : ℕ ) : Set where | |
| 210 field | |
| 211 i<i0 : i ≤ i0 | |
| 212 j<j0 : j ≤ j0 | |
| 213 div-i : Dividable i0 ((j0 + i) - j) | |
| 214 div-j : Dividable j0 ((i0 + j) - i) | |
| 215 | |
| 245 | 216 div-11 : {i j : ℕ } → Dividable i ((j + i) - j) |
| 217 div-11 {i} {j} = record { factor = 1 ; is-factor = begin | |
| 218 1 * i + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 219 i + 0 ≡⟨ +-comm _ 0 ⟩ | |
| 220 i ≡⟨ sym (minus+y-y {i} {j}) ⟩ | |
| 221 (i + j ) - j ≡⟨ cong (λ k → k - j ) (+-comm i j ) ⟩ | |
| 222 (j + i) - j ∎ } where open ≡-Reasoning | |
| 223 | |
| 247 | 224 div→gcd : {n k : ℕ } → k > 1 → Dividable k n → gcd n k ≡ k |
| 225 div→gcd {n} {k} k>1 = n-induction {_} {_} {ℕ} {λ m → Dividable k m → gcd m k ≡ k } (λ x → x) I n where | |
| 226 decl : {m : ℕ } → 0 < m → m - k < m | |
| 227 decl {m} 0<m = y-x<y (<-trans a<sa k>1 ) 0<m | |
| 228 ind : (m : ℕ ) → (Dividable k (m - k) → gcd (m - k) k ≡ k) → Dividable k m → gcd m k ≡ k | |
| 229 ind m prev d with <-cmp (suc m) k | |
| 230 ... | tri≈ ¬a refl ¬c = ⊥-elim ( div+1 k>1 d div= ) | |
| 231 ... | tri> ¬a ¬b c = subst (λ g → g ≡ k) ind1 ( prev (proj2 (div-div k>1 div= d))) where | |
| 232 ind1 : gcd (m - k) k ≡ gcd m k | |
| 233 ind1 = begin | |
| 234 gcd (m - k) k ≡⟨ sym (gcd+j (m - k) _) ⟩ | |
| 235 gcd (m - k + k) k ≡⟨ cong (λ g → gcd g k) (minus+n {m} {k} c) ⟩ | |
| 236 gcd m k ∎ where open ≡-Reasoning | |
| 237 ... | tri< a ¬b ¬c with <-cmp 0 m | |
| 238 ... | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim ( div<k k>1 a₁ (<-trans a<sa a) d ) | |
| 239 ... | tri≈ ¬a refl ¬c₁ = subst (λ g → g ≡ k ) (gcdsym {k} {0} ) (gcd20 k) | |
| 240 fzero : (m : ℕ) → (m - k) ≡ zero → Dividable k m → gcd m k ≡ k | |
| 241 fzero 0 eq d = trans (gcdsym {0} {k} ) (gcd20 k) | |
| 242 fzero (suc m) eq d with <-cmp (suc m) k | |
| 243 ... | tri< a ¬b ¬c = ⊥-elim ( div<k k>1 (s≤s z≤n) a d ) | |
| 244 ... | tri≈ ¬a refl ¬c = gcdmm k k | |
| 245 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (minus>0 c) ) | |
| 246 I : Ninduction ℕ _ (λ x → x) | |
| 247 I = record { | |
| 248 pnext = λ p → p - k | |
| 249 ; fzero = λ {m} eq → fzero m eq | |
| 250 ; decline = λ {m} lt → decl lt | |
| 251 ; ind = λ {p} prev → ind p prev | |
| 252 } | |
| 245 | 253 |
| 254 GCDi : {i j : ℕ } → GCD i i j j | |
| 247 | 255 GCDi {i} {j} = record { i<i0 = refl-≤ ; j<j0 = refl-≤ ; div-i = div-11 {i} {j} ; div-j = div-11 {j} {i} } |
| 245 | 256 |
| 238 | 257 GCD-sym : {i i0 j j0 : ℕ} → GCD i i0 j j0 → GCD j j0 i i0 |
| 258 GCD-sym g = record { i<i0 = GCD.j<j0 g ; j<j0 = GCD.i<i0 g ; div-i = GCD.div-j g ; div-j = GCD.div-i g } | |
| 259 | |
| 260 pred-≤ : {i i0 : ℕ } → suc i ≤ suc i0 → i ≤ suc i0 | |
| 261 pred-≤ {i} {i0} (s≤s lt) = ≤-trans lt refl-≤s | |
| 262 | |
| 263 gcd-next : {i i0 j j0 : ℕ} → GCD (suc i) i0 (suc j) j0 → GCD i i0 j j0 | |
| 264 gcd-next {i} {0} {j} {0} () | |
| 265 gcd-next {i} {suc i0} {j} {suc j0} g = record { i<i0 = pred-≤ (GCD.i<i0 g) ; j<j0 = pred-≤ (GCD.j<j0 g) | |
| 266 ; div-i = proj1 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ ) | |
| 267 ; div-j = proj2 (di-next {i} {suc i0} {j} {suc j0} ⟪ GCD.div-i g , GCD.div-j g ⟫ ) } | |
| 268 | |
| 269 gcd-next1 : {i0 j j0 : ℕ} → GCD 0 (suc i0) (suc (suc j)) j0 → GCD i0 (suc i0) (suc j) (suc (suc j)) | |
| 270 gcd-next1 {i0} {j} {j0} g = record { i<i0 = refl-≤s ; j<j0 = refl-≤s | |
| 271 ; div-i = proj1 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) ; div-j = proj2 (di-next1 ⟪ GCD.div-i g , GCD.div-j g ⟫ ) } | |
| 272 | |
| 243 | 273 |
| 231 | 274 -- gcd-dividable1 : ( i i0 j j0 : ℕ ) |
| 275 -- → Dividable i0 (j0 + i - j ) ∨ Dividable j0 (i0 + j - i) | |
| 276 -- → Dividable ( gcd1 i i0 j j0 ) i0 ∧ Dividable ( gcd1 i i0 j j0 ) j0 | |
| 277 -- gcd-dividable1 zero i0 zero j0 with <-cmp i0 j0 | |
| 278 -- ... | tri< a ¬b ¬c = ⟪ div= , {!!} ⟫ -- Dividable i0 (j0 + i - j ) ∧ Dividable j0 (i0 + j - i) | |
| 279 -- ... | tri≈ ¬a refl ¬c = {!!} | |
| 280 -- ... | tri> ¬a ¬b c = {!!} | |
| 281 -- gcd-dividable1 zero i0 (suc zero) j0 = {!!} | |
| 282 -- gcd-dividable1 i i0 j j0 = {!!} | |
| 283 | |
| 227 | 284 gcd-dividable : ( i j : ℕ ) |
| 212 | 285 → Dividable ( gcd i j ) i ∧ Dividable ( gcd i j ) j |
| 227 | 286 gcd-dividable i j = f-induction {_} {_} {ℕ ∧ ℕ} |
| 209 | 287 {λ p → Dividable ( gcd (proj1 p) (proj2 p) ) (proj1 p) ∧ Dividable ( gcd (proj1 p) (proj2 p) ) (proj2 p)} F I ⟪ i , j ⟫ where |
| 288 F : ℕ ∧ ℕ → ℕ | |
| 224 | 289 F ⟪ 0 , 0 ⟫ = 0 |
| 290 F ⟪ 0 , suc j ⟫ = 0 | |
| 222 | 291 F ⟪ suc i , 0 ⟫ = 0 |
| 224 | 292 F ⟪ suc i , suc j ⟫ with <-cmp i j |
| 293 ... | tri< a ¬b ¬c = suc j | |
| 209 | 294 ... | tri≈ ¬a b ¬c = 0 |
| 224 | 295 ... | tri> ¬a ¬b c = suc i |
| 209 | 296 F0 : { i j : ℕ } → F ⟪ i , j ⟫ ≡ 0 → (i ≡ j) ∨ (i ≡ 0 ) ∨ (j ≡ 0) |
| 297 F0 {zero} {zero} p = case1 refl | |
| 298 F0 {zero} {suc j} p = case2 (case1 refl) | |
| 299 F0 {suc i} {zero} p = case2 (case2 refl) | |
| 300 F0 {suc i} {suc j} p with <-cmp i j | |
| 224 | 301 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n )) |
| 302 ... | tri≈ ¬a refl ¬c = case1 refl | |
| 303 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym p) (s≤s z≤n )) | |
| 304 F00 : {p : ℕ ∧ ℕ} → F p ≡ zero → Dividable (gcd (proj1 p) (proj2 p)) (proj1 p) ∧ Dividable (gcd (proj1 p) (proj2 p)) (proj2 p) | |
| 305 F00 {⟪ i , j ⟫} eq with F0 {i} {j} eq | |
| 306 ... | case1 refl = ⟪ subst (λ k → Dividable k i) (sym (gcdmm i i)) div= , subst (λ k → Dividable k i) (sym (gcdmm i i)) div= ⟫ | |
| 307 ... | case2 (case1 refl) = ⟪ subst (λ k → Dividable k i) (sym (trans (gcdsym {0} {j} ) (gcd20 j)))div0 | |
| 308 , subst (λ k → Dividable k j) (sym (trans (gcdsym {0} {j}) (gcd20 j))) div= ⟫ | |
| 309 ... | case2 (case2 refl) = ⟪ subst (λ k → Dividable k i) (sym (gcd20 i)) div= | |
| 310 , subst (λ k → Dividable k j) (sym (gcd20 i)) div0 ⟫ | |
| 311 Fsym : {i j : ℕ } → F ⟪ i , j ⟫ ≡ F ⟪ j , i ⟫ | |
| 312 Fsym {0} {0} = refl | |
| 313 Fsym {0} {suc j} = refl | |
| 314 Fsym {suc i} {0} = refl | |
| 315 Fsym {suc i} {suc j} with <-cmp i j | <-cmp j i | |
| 316 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) | |
| 317 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b)) | |
| 318 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl | |
| 319 ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) | |
| 320 ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl | |
| 321 ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) | |
| 322 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl | |
| 323 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b)) | |
| 324 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) | |
| 325 | |
| 326 record Fdec ( i j : ℕ ) : Set where | |
| 327 field | |
| 328 ni : ℕ | |
| 329 nj : ℕ | |
| 330 fdec : 0 < F ⟪ i , j ⟫ → F ⟪ ni , nj ⟫ < F ⟪ i , j ⟫ | |
| 214 | 331 |
| 224 | 332 fd1 : ( i j k : ℕ ) → i < j → k ≡ j - i → F ⟪ suc i , k ⟫ < F ⟪ suc i , suc j ⟫ |
| 333 fd1 i j 0 i<j eq = ⊥-elim ( nat-≡< eq (minus>0 {i} {j} i<j )) | |
| 334 fd1 i j (suc k) i<j eq = fd2 i j k i<j eq where | |
| 335 fd2 : ( i j k : ℕ ) → i < j → suc k ≡ j - i → F ⟪ suc i , suc k ⟫ < F ⟪ suc i , suc j ⟫ | |
| 336 fd2 i j k i<j eq with <-cmp i k | <-cmp i j | |
| 337 ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = fd3 where | |
| 338 fd3 : suc k < suc j -- suc j - suc i < suc j | |
| 339 fd3 = subst (λ g → g < suc j) (sym eq) (y-x<y {suc i} {suc j} (s≤s z≤n) (s≤s z≤n)) | |
| 340 ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (⊥-elim (¬a i<j)) | |
| 341 ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (⊥-elim (¬a i<j)) | |
| 342 ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = s≤s z≤n | |
| 343 ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (¬a₁ i<j) | |
| 344 ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = s≤s z≤n -- i > j | |
| 345 ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = fd4 where | |
| 346 fd4 : suc i < suc j | |
| 347 fd4 = s≤s a | |
| 348 ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬a₁ i<j) | |
| 349 ... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (¬a₁ i<j) | |
| 350 | |
| 351 fedc0 : (i j : ℕ ) → Fdec i j | |
| 352 fedc0 0 0 = record { ni = 0 ; nj = 0 ; fdec = λ () } | |
| 353 fedc0 (suc i) 0 = record { ni = suc i ; nj = 0 ; fdec = λ () } | |
| 354 fedc0 0 (suc j) = record { ni = 0 ; nj = suc j ; fdec = λ () } | |
| 355 fedc0 (suc i) (suc j) with <-cmp i j | |
| 356 ... | tri< i<j ¬b ¬c = record { ni = suc i ; nj = j - i ; fdec = λ lt → fd1 i j (j - i) i<j refl } | |
| 357 ... | tri≈ ¬a refl ¬c = record { ni = suc i ; nj = suc j ; fdec = λ lt → ⊥-elim (nat-≡< fd0 lt) } where | |
| 358 fd0 : {i : ℕ } → 0 ≡ F ⟪ suc i , suc i ⟫ | |
| 359 fd0 {i} with <-cmp i i | |
| 360 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) | |
| 361 ... | tri≈ ¬a b ¬c = refl | |
| 362 ... | tri> ¬a ¬b c = ⊥-elim ( ¬b refl ) | |
| 363 ... | tri> ¬a ¬b c = record { ni = i - j ; nj = suc j ; fdec = λ lt → | |
| 364 subst₂ (λ s t → s < t) (Fsym {suc j} {i - j}) (Fsym {suc j} {suc i}) (fd1 j i (i - j) c refl ) } | |
| 214 | 365 |
| 366 ind3 : {i j : ℕ } → i < j | |
| 367 → Dividable (gcd (suc i) (j - i)) (suc i) | |
| 368 → Dividable (gcd (suc i) (suc j)) (suc i) | |
| 369 ind3 {i} {j} a prev = | |
| 370 subst (λ k → Dividable k (suc i)) ( begin | |
| 371 gcd (suc i) (j - i) ≡⟨ gcdsym {suc i} {j - i} ⟩ | |
| 372 gcd (j - i ) (suc i) ≡⟨ sym (gcd+j (j - i) (suc i)) ⟩ | |
| 373 gcd ((j - i) + suc i) (suc i) ≡⟨ cong (λ k → gcd k (suc i)) ( begin | |
| 374 (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)) | |
| 375 suc j ∎ ) ⟩ | |
| 376 gcd (suc j) (suc i) ≡⟨ gcdsym {suc j} {suc i} ⟩ | |
| 377 gcd (suc i) (suc j) ∎ ) prev where open ≡-Reasoning | |
| 378 ind7 : {i j : ℕ } → (i < j ) → (j - i) + suc i ≡ suc j | |
| 379 ind7 {i} {j} a = begin (suc j - suc i) + suc i ≡⟨ minus+n {suc j} {suc i} (<-trans (s≤s a) a<sa) ⟩ | |
| 380 suc j ∎ where open ≡-Reasoning | |
| 381 ind6 : {i j k : ℕ } → i < j | |
| 382 → Dividable k (j - i) | |
| 383 → Dividable k (suc i) | |
| 384 → Dividable k (suc j) | |
| 385 ind6 {i} {j} {k} i<j dj di = subst (λ g → Dividable k g ) (ind7 i<j) (proj1 (div+div dj di)) | |
| 386 ind4 : {i j : ℕ } → i < j | |
| 387 → Dividable (gcd (suc i) (j - i)) (j - i) | |
| 388 → Dividable (gcd (suc i) (suc j)) (j - i) | |
| 389 ind4 {i} {j} i<j prev = subst (λ k → k) ( begin | |
| 390 Dividable (gcd (suc i) (j - i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc i} ) ⟩ | |
| 391 Dividable (gcd (j - i ) (suc i) ) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) ( sym (gcd+j (j - i) (suc i))) ⟩ | |
| 392 Dividable (gcd ((j - i) + suc i) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable (gcd k (suc i)) (j - i)) (ind7 i<j ) ⟩ | |
| 393 Dividable (gcd (suc j) (suc i)) (j - i) ≡⟨ cong (λ k → Dividable k (j - i)) (gcdsym {suc j} ) ⟩ | |
| 394 Dividable (gcd (suc i) (suc j)) (j - i) ∎ ) prev where open ≡-Reasoning | |
| 395 | |
| 224 | 396 ind : ( i j : ℕ ) → |
| 397 Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.ni (fedc0 i j)) | |
| 398 ∧ Dividable (gcd (Fdec.ni (fedc0 i j)) (Fdec.nj (fedc0 i j))) (Fdec.nj (fedc0 i j)) | |
| 399 → Dividable (gcd i j) i ∧ Dividable (gcd i j) j | |
| 400 ind zero zero prev = ind0 where | |
| 210 | 401 ind0 : Dividable (gcd zero zero) zero ∧ Dividable (gcd zero zero) zero |
| 212 | 402 ind0 = ⟪ div0 , div0 ⟫ |
| 224 | 403 ind zero (suc j) prev = ind1 where |
| 210 | 404 ind1 : Dividable (gcd zero (suc j)) zero ∧ Dividable (gcd zero (suc j)) (suc j) |
| 212 | 405 ind1 = ⟪ div0 , subst (λ k → Dividable k (suc j)) (sym (trans (gcdsym {zero} {suc j}) (gcd20 (suc j)))) div= ⟫ |
| 224 | 406 ind (suc i) zero prev = ind2 where |
| 210 | 407 ind2 : Dividable (gcd (suc i) zero) (suc i) ∧ Dividable (gcd (suc i) zero) zero |
| 212 | 408 ind2 = ⟪ subst (λ k → Dividable k (suc i)) (sym (trans refl (gcd20 (suc i)))) div= , div0 ⟫ |
| 224 | 409 ind (suc i) (suc j) prev with <-cmp i j |
| 281 | 410 ... | tri< a ¬b ¬c = ⟪ ind3 a (proj1 prev) , ind6 a (ind4 a (proj2 prev)) (ind3 a (proj1 prev) ) ⟫ |
| 213 | 411 ... | tri≈ ¬a refl ¬c = ⟪ ind5 , ind5 ⟫ where |
| 412 ind5 : Dividable (gcd (suc i) (suc i)) (suc i) | |
| 413 ind5 = subst (λ k → Dividable k (suc j)) (sym (gcdmm (suc i) (suc i))) div= | |
| 224 | 414 ... | tri> ¬a ¬b c = ⟪ ind8 c (proj1 prev) (proj2 prev) , ind10 c (proj2 prev) ⟫ where |
| 214 | 415 ind9 : {i j : ℕ} → i < j → gcd (j - i) (suc i) ≡ gcd (suc j) (suc i) |
| 416 ind9 {i} {j} i<j = begin | |
| 417 gcd (j - i ) (suc i) ≡⟨ sym (gcd+j (j - i ) (suc i) ) ⟩ | |
| 418 gcd (j - i + suc i) (suc i) ≡⟨ cong (λ k → gcd k (suc i)) (ind7 i<j ) ⟩ | |
| 419 gcd (suc j) (suc i) ∎ where open ≡-Reasoning | |
| 420 ind8 : { i j : ℕ } → i < j | |
| 421 → Dividable (gcd (j - i) (suc i)) (j - i) | |
| 422 → Dividable (gcd (j - i) (suc i)) (suc i) | |
| 423 → Dividable (gcd (suc j) (suc i)) (suc j) | |
| 424 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) | |
| 425 ind10 : { i j : ℕ } → j < i | |
| 426 → Dividable (gcd (i - j) (suc j)) (suc j) | |
| 427 → Dividable (gcd (suc i) (suc j)) (suc j) | |
| 428 ind10 {i} {j} j<i dji = subst (λ g → Dividable g (suc j) ) (begin | |
| 429 gcd (i - j) (suc j) ≡⟨ sym (gcd+j (i - j) (suc j)) ⟩ | |
| 430 gcd (i - j + suc j) (suc j) ≡⟨ cong (λ k → gcd k (suc j)) (ind7 j<i ) ⟩ | |
| 431 gcd (suc i) (suc j) ∎ ) dji where open ≡-Reasoning | |
| 210 | 432 |
| 224 | 433 I : Finduction (ℕ ∧ ℕ) _ F |
| 209 | 434 I = record { |
| 224 | 435 fzero = F00 |
| 436 ; pnext = λ p → ⟪ Fdec.ni (fedc0 (proj1 p) (proj2 p)) , Fdec.nj (fedc0 (proj1 p) (proj2 p)) ⟫ | |
| 437 ; decline = λ {p} lt → Fdec.fdec (fedc0 (proj1 p) (proj2 p)) lt | |
| 438 ; ind = λ {p} prev → ind (proj1 p ) ( proj2 p ) prev | |
| 209 | 439 } |
| 440 | |
| 247 | 441 f-div>0 : { k i : ℕ } → (d : Dividable k i ) → 0 < i → 0 < Dividable.factor d |
| 442 f-div>0 {k} {i} d 0<i with <-cmp 0 (Dividable.factor d) | |
| 443 ... | tri< a ¬b ¬c = a | |
| 444 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (begin | |
| 445 0 * k + 0 ≡⟨ cong (λ g → g * k + 0) b ⟩ | |
| 446 Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ | |
| 447 i ∎ ) 0<i ) where open ≡-Reasoning | |
| 448 | |
| 449 gcd-≤i : ( i j : ℕ ) → 0 < i → i ≤ j → gcd i j ≤ i | |
| 450 gcd-≤i zero _ () z≤n | |
| 451 gcd-≤i (suc i) (suc j) _ (s≤s i<j) = begin | |
| 452 gcd (suc i) (suc j) ≡⟨ sym m*1=m ⟩ | |
| 453 gcd (suc i) (suc j) * 1 ≤⟨ *-monoʳ-≤ (gcd (suc i) (suc j)) (f-div>0 d (s≤s z≤n)) ⟩ | |
| 454 gcd (suc i) (suc j) * f ≡⟨ +-comm 0 _ ⟩ | |
| 455 gcd (suc i) (suc j) * f + 0 ≡⟨ cong (λ k → k + 0) (*-comm (gcd (suc i) (suc j)) _ ) ⟩ | |
| 456 Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) * gcd (suc i) (suc j) + 0 ≡⟨ Dividable.is-factor (proj1 (gcd-dividable (suc i) (suc j))) ⟩ | |
| 457 suc i ∎ where | |
| 458 d = proj1 (gcd-dividable (suc i) (suc j)) | |
| 459 f = Dividable.factor (proj1 (gcd-dividable (suc i) (suc j))) | |
| 460 open ≤-Reasoning | |
| 461 | |
| 462 gcd-≤ : { i j : ℕ } → 0 < i → 0 < j → gcd i j ≤ i | |
| 463 gcd-≤ {i} {j} 0<i 0<j with <-cmp i j | |
| 464 ... | tri< a ¬b ¬c = gcd-≤i i j 0<i (<to≤ a) | |
| 465 ... | tri≈ ¬a refl ¬c = gcd-≤i i j 0<i refl-≤ | |
| 466 ... | tri> ¬a ¬b c = ≤-trans (subst (λ k → k ≤ j) (gcdsym {j} {i}) (gcd-≤i j i 0<j (<to≤ c))) (<to≤ c) | |
| 467 | |
| 241 | 468 record Euclid (i j gcd : ℕ ) : Set where |
| 233 | 469 field |
| 470 eqa : ℕ | |
| 471 eqb : ℕ | |
| 250 | 472 is-equ< : eqa * i > eqb * j → (eqa * i) - (eqb * j) ≡ gcd |
| 473 is-equ> : eqb * j > eqa * i → (eqb * j) - (eqa * i) ≡ gcd | |
| 474 is-equ= : eqa * i ≡ eqb * j → 0 ≡ gcd | |
| 234 | 475 |
| 235 | 476 ge3 : {a b c d : ℕ } → b > a → b - a ≡ d - c → d > c |
| 477 ge3 {a} {b} {c} {d} b>a eq = minus>0→x<y (subst (λ k → 0 < k ) eq (minus>0 b>a)) | |
| 234 | 478 |
| 241 | 479 ge01 : ( i0 j j0 ea eb : ℕ ) |
| 239 | 480 → ( di : GCD 0 (suc i0) (suc (suc j)) j0 ) |
| 241 | 481 → (((ea + eb * (Dividable.factor (GCD.div-i di))) * suc i0) ≡ (ea * suc i0) + (eb * (Dividable.factor (GCD.div-i di)) ) * suc i0 ) |
| 482 ∧ ( (eb * j0) ≡ (eb * suc (suc j) + (eb * (Dividable.factor (GCD.div-i di)) ) * suc i0) ) | |
| 483 ge01 i0 j j0 ea eb di = ⟪ ge011 , ge012 ⟫ where | |
| 239 | 484 f = Dividable.factor (GCD.div-i di) |
| 485 ge4 : suc (j0 + 0) > suc (suc j) | |
| 486 ge4 = subst (λ k → k > suc (suc j)) (+-comm 0 _ ) ( s≤s (GCD.j<j0 di )) | |
| 241 | 487 ge011 : (ea + eb * f) * suc i0 ≡ ea * suc i0 + eb * f * suc i0 |
| 488 ge011 = begin | |
| 489 (ea + eb * f) * suc i0 ≡⟨ *-distribʳ-+ (suc i0) ea _ ⟩ | |
| 490 ea * suc i0 + eb * f * suc i0 ∎ where open ≡-Reasoning | |
| 491 ge012 : eb * j0 ≡ eb * suc (suc j) + eb * f * suc i0 | |
| 492 ge012 = begin | |
| 493 eb * j0 ≡⟨ cong (λ k → eb * k) ( begin | |
| 494 j0 ≡⟨ +-comm 0 _ ⟩ | |
| 495 j0 + 0 ≡⟨ sym (minus+n {j0 + 0} {suc (suc j)} ge4) ⟩ | |
| 496 ((j0 + 0) - (suc (suc j))) + suc (suc j) ≡⟨ +-comm _ (suc (suc j)) ⟩ | |
| 497 suc (suc j) + ((j0 + 0) - suc (suc j)) ≡⟨ cong (λ k → suc (suc j) + k ) (sym (Dividable.is-factor (GCD.div-i di))) ⟩ | |
| 498 suc (suc j) + (f * suc i0 + 0) ≡⟨ cong (λ k → suc (suc j) + k ) ( +-comm _ 0 ) ⟩ | |
| 499 suc (suc j) + (f * suc i0 ) ∎ ) ⟩ | |
| 500 eb * (suc (suc j) + (f * suc i0 ) ) ≡⟨ *-distribˡ-+ eb (suc (suc j)) (f * suc i0) ⟩ | |
| 501 eb * suc (suc j) + eb * (f * suc i0) ≡⟨ cong (λ k → eb * suc (suc j) + k ) ((sym (*-assoc eb _ _ )) ) ⟩ | |
| 502 eb * suc (suc j) + eb * f * suc i0 ∎ where open ≡-Reasoning | |
| 239 | 503 |
| 250 | 504 ge20 : {i0 j0 : ℕ } → i0 ≡ 0 → 0 ≡ gcd1 zero i0 zero j0 |
| 505 ge20 {i0} {zero} refl = refl | |
| 506 ge20 {i0} {suc j0} refl = refl | |
| 241 | 507 |
| 508 gcd-euclid1 : ( i i0 j j0 : ℕ ) → GCD i i0 j j0 → Euclid i0 j0 (gcd1 i i0 j j0) | |
| 509 gcd-euclid1 zero i0 zero j0 di with <-cmp i0 j0 | |
| 250 | 510 ... | tri< a' ¬b ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () ; is-equ= = ge21 } where |
| 511 ge21 : 1 * i0 ≡ 0 * j0 → 0 ≡ i0 | |
| 512 ge21 eq = trans (sym eq) (+-comm i0 0) | |
| 513 ... | tri≈ ¬a refl ¬c = record { eqa = 1 ; eqb = 0 ; is-equ< = λ _ → +-comm _ 0 ; is-equ> = λ () ; is-equ= = λ eq → trans (sym eq) (+-comm i0 0) } | |
| 514 ... | tri> ¬a ¬b c = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 ; is-equ= = ge22 } where | |
| 515 ge22 : 0 * i0 ≡ 1 * j0 → 0 ≡ j0 | |
| 516 ge22 eq = trans eq (+-comm j0 0) | |
| 243 | 517 -- i<i0 : zero ≤ i0 |
| 518 -- j<j0 : 1 ≤ j0 | |
| 519 -- div-i : Dividable i0 ((j0 + zero) - 1) -- fi * i0 ≡ (j0 + zero) - 1 | |
| 520 -- div-j : Dividable j0 ((i0 + 1) - zero) -- fj * j0 ≡ (i0 + 1) - zero | |
| 250 | 521 gcd-euclid1 zero i0 (suc zero) j0 di = record { eqa = 1 ; eqb = Dividable.factor (GCD.div-j di) ; is-equ< = λ lt → ⊥-elim ( ge7 lt) ; is-equ> = λ _ → ge6 |
| 522 ; is-equ= = λ eq → ⊥-elim (nat-≡< (sym (minus<=0 (subst (λ k → k ≤ 1 * i0) eq refl-≤ ))) (subst (λ k → 0 < k) (sym ge6) a<sa )) } where | |
| 244 | 523 ge6 : (Dividable.factor (GCD.div-j di) * j0) - (1 * i0) ≡ gcd1 zero i0 1 j0 |
| 524 ge6 = begin | |
| 525 (Dividable.factor (GCD.div-j di) * j0) - (1 * i0) ≡⟨ cong (λ k → k - (1 * i0)) (+-comm 0 _) ⟩ | |
| 526 (Dividable.factor (GCD.div-j di) * j0 + 0) - (1 * i0) ≡⟨ cong (λ k → k - (1 * i0)) (Dividable.is-factor (GCD.div-j di) ) ⟩ | |
| 527 ((i0 + 1) - zero) - (1 * i0) ≡⟨ refl ⟩ | |
| 528 (i0 + 1) - (i0 + 0) ≡⟨ minus+yx-yz {_} {i0} {0} ⟩ | |
| 243 | 529 1 ∎ where open ≡-Reasoning |
| 244 | 530 ge7 : ¬ ( 1 * i0 > Dividable.factor (GCD.div-j di) * j0 ) |
| 531 ge7 lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6) (s≤s z≤n))) | |
| 250 | 532 gcd-euclid1 zero zero (suc (suc j)) j0 di = record { eqa = 0 ; eqb = 1 ; is-equ< = λ () ; is-equ> = λ _ → +-comm _ 0 |
| 533 ; is-equ= = λ eq → subst (λ k → 0 ≡ k) (+-comm _ 0) eq } | |
| 241 | 534 gcd-euclid1 zero (suc i0) (suc (suc j)) j0 di with gcd-euclid1 i0 (suc i0) (suc j) (suc (suc j)) ( gcd-next1 di ) |
| 250 | 535 ... | e = record { eqa = ea + eb * f ; eqb = eb |
| 536 ; is-equ= = λ eq → Euclid.is-equ= e (ge23 eq) | |
| 241 | 537 ; is-equ< = λ lt → subst (λ k → ((ea + eb * f) * suc i0) - (eb * j0) ≡ k ) (Euclid.is-equ< e (ge3 lt (ge1 ))) (ge1 ) |
| 538 ; is-equ> = λ lt → subst (λ k → (eb * j0) - ((ea + eb * f) * suc i0) ≡ k ) (Euclid.is-equ> e (ge3 lt (ge2 ))) (ge2 ) } where | |
| 539 ea = Euclid.eqa e | |
| 540 eb = Euclid.eqb e | |
| 238 | 541 f = Dividable.factor (GCD.div-i di) |
| 241 | 542 ge1 : ((ea + eb * f) * suc i0) - (eb * j0) ≡ (ea * suc i0) - (eb * suc (suc j)) |
| 543 ge1 = begin | |
| 544 ((ea + eb * f) * suc i0) - (eb * j0) ≡⟨ cong₂ (λ j k → j - k ) (proj1 (ge01 i0 j j0 ea eb di)) (proj2 (ge01 i0 j j0 ea eb di)) ⟩ | |
| 545 (ea * suc i0 + (eb * f ) * suc i0 ) - ( eb * suc (suc j) + ((eb * f) * (suc i0)) ) ≡⟨ minus+xy-zy {ea * suc i0} {(eb * f ) * suc i0} {eb * suc (suc j)} ⟩ | |
| 546 (ea * suc i0) - (eb * suc (suc j)) ∎ where open ≡-Reasoning | |
| 547 ge2 : (eb * j0) - ((ea + eb * f) * suc i0) ≡ (eb * suc (suc j)) - (ea * suc i0) | |
| 548 ge2 = begin | |
| 549 (eb * j0) - ((ea + eb * f) * suc i0) ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01 i0 j j0 ea eb di)) (proj1 (ge01 i0 j j0 ea eb di)) ⟩ | |
| 550 ( eb * suc (suc j) + ((eb * f) * (suc i0)) ) - (ea * suc i0 + (eb * f ) * suc i0 ) ≡⟨ minus+xy-zy {eb * suc (suc j)}{(eb * f ) * suc i0} {ea * suc i0} ⟩ | |
| 551 (eb * suc (suc j)) - (ea * suc i0) ∎ where open ≡-Reasoning | |
| 250 | 552 ge23 : (ea + eb * f) * suc i0 ≡ eb * j0 → ea * suc i0 ≡ eb * suc (suc j) |
| 553 ge23 eq = begin | |
| 554 ea * suc i0 ≡⟨ sym (minus+y-y {_} {(eb * f ) * suc i0} ) ⟩ | |
| 555 (ea * suc i0 + ((eb * f ) * suc i0 )) - ((eb * f ) * suc i0 ) ≡⟨ cong (λ k → k - ((eb * f ) * suc i0 )) (sym ( proj1 (ge01 i0 j j0 ea eb di))) ⟩ | |
| 556 ((ea + eb * f) * suc i0) - ((eb * f ) * suc i0 ) ≡⟨ cong (λ k → k - ((eb * f ) * suc i0 )) eq ⟩ | |
| 557 (eb * j0) - ((eb * f ) * suc i0 ) ≡⟨ cong (λ k → k - ((eb * f ) * suc i0 )) ( proj2 (ge01 i0 j j0 ea eb di)) ⟩ | |
| 558 (eb * suc (suc j) + ((eb * f ) * suc i0 )) - ((eb * f ) * suc i0 ) ≡⟨ minus+y-y {_} {(eb * f ) * suc i0 } ⟩ | |
| 559 eb * suc (suc j) ∎ where open ≡-Reasoning | |
| 560 gcd-euclid1 (suc zero) i0 zero j0 di = record { eqb = 1 ; eqa = Dividable.factor (GCD.div-i di) ; is-equ> = λ lt → ⊥-elim ( ge7' lt) ; is-equ< = λ _ → ge6' | |
| 561 ; is-equ= = λ eq → ⊥-elim (nat-≡< (sym (minus<=0 (subst (λ k → k ≤ 1 * j0) (sym eq) refl-≤ ))) (subst (λ k → 0 < k) (sym ge6') a<sa )) } where | |
| 244 | 562 ge6' : (Dividable.factor (GCD.div-i di) * i0) - (1 * j0) ≡ gcd1 (suc zero) i0 zero j0 |
| 563 ge6' = begin | |
| 564 (Dividable.factor (GCD.div-i di) * i0) - (1 * j0) ≡⟨ cong (λ k → k - (1 * j0)) (+-comm 0 _) ⟩ | |
| 565 (Dividable.factor (GCD.div-i di) * i0 + 0) - (1 * j0) ≡⟨ cong (λ k → k - (1 * j0)) (Dividable.is-factor (GCD.div-i di) ) ⟩ | |
| 566 ((j0 + 1) - zero) - (1 * j0) ≡⟨ refl ⟩ | |
| 567 (j0 + 1) - (j0 + 0) ≡⟨ minus+yx-yz {_} {j0} {0} ⟩ | |
| 568 1 ∎ where open ≡-Reasoning | |
| 569 ge7' : ¬ ( 1 * j0 > Dividable.factor (GCD.div-i di) * i0 ) | |
| 570 ge7' lt = ⊥-elim ( nat-≡< (sym ( minus<=0 (<to≤ lt))) (subst (λ k → 0 < k) (sym ge6') (s≤s z≤n))) | |
| 250 | 571 gcd-euclid1 (suc (suc i)) i0 zero zero di = record { eqb = 0 ; eqa = 1 ; is-equ> = λ () ; is-equ< = λ _ → +-comm _ 0 |
| 572 ; is-equ= = λ eq → subst (λ k → 0 ≡ k) (+-comm _ 0) (sym eq) } | |
| 241 | 573 gcd-euclid1 (suc (suc i)) i0 zero (suc j0) di with gcd-euclid1 (suc i) (suc (suc i)) j0 (suc j0) (GCD-sym (gcd-next1 (GCD-sym di))) |
| 250 | 574 ... | e = record { eqa = ea ; eqb = eb + ea * f |
| 575 ; is-equ= = λ eq → Euclid.is-equ= e (ge24 eq) | |
| 241 | 576 ; is-equ< = λ lt → subst (λ k → ((ea * i0) - ((eb + ea * f) * suc j0)) ≡ k ) (Euclid.is-equ< e (ge3 lt ge4)) ge4 |
| 577 ; is-equ> = λ lt → subst (λ k → (((eb + ea * f) * suc j0) - (ea * i0)) ≡ k ) (Euclid.is-equ> e (ge3 lt ge5)) ge5 } where | |
| 578 ea = Euclid.eqa e | |
| 579 eb = Euclid.eqb e | |
| 242 | 580 f = Dividable.factor (GCD.div-j di) |
| 241 | 581 ge5 : (((eb + ea * f) * suc j0) - (ea * i0)) ≡ ((eb * suc j0) - (ea * suc (suc i))) |
| 242 | 582 ge5 = begin |
| 583 ((eb + ea * f) * suc j0) - (ea * i0) ≡⟨ cong₂ (λ j k → j - k ) (proj1 (ge01 j0 i i0 eb ea (GCD-sym di) )) (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )) ⟩ | |
| 584 ( eb * suc j0 + (ea * f )* suc j0) - (ea * suc (suc i) + (ea * f )* suc j0) ≡⟨ minus+xy-zy {_} {(ea * f )* suc j0} {ea * suc (suc i)} ⟩ | |
| 585 (eb * suc j0) - (ea * suc (suc i)) ∎ where open ≡-Reasoning | |
| 241 | 586 ge4 : ((ea * i0) - ((eb + ea * f) * suc j0)) ≡ ((ea * suc (suc i)) - (eb * suc j0)) |
| 242 | 587 ge4 = begin |
| 588 (ea * i0) - ((eb + ea * f) * suc j0) ≡⟨ cong₂ (λ j k → j - k ) (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) )) (proj1 (ge01 j0 i i0 eb ea (GCD-sym di) )) ⟩ | |
| 589 (ea * suc (suc i) + (ea * f )* suc j0) - ( eb * suc j0 + (ea * f )* suc j0) ≡⟨ minus+xy-zy {ea * suc (suc i)} {(ea * f )* suc j0} { eb * suc j0} ⟩ | |
| 590 (ea * suc (suc i)) - (eb * suc j0) ∎ where open ≡-Reasoning | |
| 250 | 591 ge24 : ea * i0 ≡ (eb + ea * f) * suc j0 → ea * suc (suc i) ≡ eb * suc j0 |
| 592 ge24 eq = begin | |
| 593 ea * suc (suc i) ≡⟨ sym ( minus+y-y {_} {(ea * f ) * suc j0 }) ⟩ | |
| 594 (ea * suc (suc i) + (ea * f ) * suc j0 ) - ((ea * f ) * suc j0) ≡⟨ cong (λ k → k - ((ea * f ) * suc j0 )) (sym (proj2 (ge01 j0 i i0 eb ea (GCD-sym di) ))) ⟩ | |
| 595 (ea * i0) - ((ea * f ) * suc j0) ≡⟨ cong (λ k → k - ((ea * f ) * suc j0 )) eq ⟩ | |
| 596 ((eb + ea * f) * suc j0) - ((ea * f ) * suc j0) ≡⟨ cong (λ k → k - ((ea * f ) * suc j0 )) ((proj1 (ge01 j0 i i0 eb ea (GCD-sym di)))) ⟩ | |
| 597 ( eb * suc j0 + (ea * f ) * suc j0 ) - ((ea * f ) * suc j0) ≡⟨ minus+y-y {_} {(ea * f ) * suc j0 } ⟩ | |
| 598 eb * suc j0 ∎ where open ≡-Reasoning | |
| 241 | 599 gcd-euclid1 (suc zero) i0 (suc j) j0 di = |
| 600 gcd-euclid1 zero i0 j j0 (gcd-next di) | |
| 601 gcd-euclid1 (suc (suc i)) i0 (suc j) j0 di = | |
| 602 gcd-euclid1 (suc i) i0 j j0 (gcd-next di) | |
| 233 | 603 |
| 255 | 604 ge12 : (p x : ℕ) → 0 < x → 1 < p → ((i : ℕ ) → i < p → 0 < i → gcd p i ≡ 1) → ( gcd p x ≡ 1 ) ∨ ( Dividable p x ) |
| 605 ge12 p x 0<x 1<p prime with decD {p} {x} 1<p | |
| 606 ... | yes y = case2 y | |
| 607 ... | no nx with <-cmp (gcd p x ) 1 | |
| 608 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≤> a (s≤s (gcd>0 p x (<-trans a<sa 1<p) 0<x) ) ) | |
| 609 ... | tri≈ ¬a b ¬c = case1 b | |
| 610 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (prime (gcd p x) ge13 (<to≤ c) )) ge18 ) where | |
| 247 | 611 -- 1 < gcd p x |
| 612 ge13 : gcd p x < p -- gcd p x ≡ p → ¬ nx | |
| 613 ge13 with <-cmp (gcd p x ) p | |
| 614 ... | tri< a ¬b ¬c = a | |
| 615 ... | tri≈ ¬a b ¬c = ⊥-elim ( nx (subst (λ k → Dividable k x) b (proj2 (gcd-dividable p x )))) | |
| 616 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (gcd-≤ (<-trans a<sa 1<p) 0<x) c ) | |
| 617 ge19 : Dividable (gcd p x) p | |
| 618 ge19 = proj1 (gcd-dividable p x ) | |
| 619 ge18 : 1 < gcd p (gcd p x) -- Dividable p (gcd p x) → gcd p (gcd p x) ≡ (gcd p x) > 1 | |
| 620 ge18 = subst (λ k → 1 < k ) (sym (div→gcd {p} {gcd p x} c ge19 )) c | |
| 255 | 621 |
| 622 gcd-euclid : ( p a b : ℕ ) → 1 < p → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i → gcd p i ≡ 1) → Dividable p (a * b) → Dividable p a ∨ Dividable p b | |
| 623 gcd-euclid p a b 1<p 0<a 0<b prime div-ab with decD {p} {a} 1<p | |
| 624 ... | yes y = case1 y | |
| 625 ... | no np = case2 ge16 where | |
| 626 f = Dividable.factor div-ab | |
| 245 | 627 ge10 : gcd p a ≡ 1 |
| 255 | 628 ge10 with ge12 p a 0<a 1<p prime |
| 245 | 629 ... | case1 x = x |
| 246 | 630 ... | case2 x = ⊥-elim ( np x ) |
| 245 | 631 ge11 : Euclid p a (gcd p a) |
| 632 ge11 = gcd-euclid1 p p a a GCDi | |
| 255 | 633 ea = Euclid.eqa ge11 |
| 634 eb = Euclid.eqb ge11 | |
| 635 ge18 : (f * eb) * p ≡ b * (a * eb ) | |
| 247 | 636 ge18 = begin |
| 255 | 637 (f * eb) * p ≡⟨ *-assoc (f) (eb) p ⟩ |
| 638 f * (eb * p) ≡⟨ cong (λ k → f * k) (*-comm _ p) ⟩ | |
| 639 f * (p * eb ) ≡⟨ sym (*-assoc (f) p (eb) ) ⟩ | |
| 640 (f * p ) * eb ≡⟨ cong (λ k → k * eb ) (+-comm 0 (f * p )) ⟩ | |
| 641 (f * p + 0) * eb ≡⟨ cong (λ k → k * eb) (((Dividable.is-factor div-ab))) ⟩ | |
| 642 (a * b) * eb ≡⟨ cong (λ k → k * eb) (*-comm a b) ⟩ | |
| 643 (b * a) * eb ≡⟨ *-assoc b a (eb ) ⟩ | |
| 644 b * (a * eb ) ∎ where open ≡-Reasoning | |
| 645 ge19 : ( ea * p ) ≡ ( eb * a ) → ((b * ea) - (f * eb)) * p + 0 ≡ b | |
| 250 | 646 ge19 eq = ⊥-elim ( nat-≡< (Euclid.is-equ= ge11 eq) (subst (λ k → 0 < k ) (sym ge10) a<sa ) ) |
| 255 | 647 ge14 : ( ea * p ) > ( eb * a ) → ((b * ea) - (f * eb)) * p + 0 ≡ b |
| 245 | 648 ge14 lt = begin |
| 255 | 649 (((b * ea) - (f * eb)) * p) + 0 ≡⟨ +-comm _ 0 ⟩ |
| 650 ((b * ea) - ((f * eb)) * p) ≡⟨ distr-minus-* {_} {f * eb} {p} ⟩ | |
| 651 ((b * ea) * p) - (((f * eb) * p)) ≡⟨ cong (λ k → ((b * ea) * p) - k ) ge18 ⟩ | |
| 652 ((b * ea) * p) - (b * (a * eb )) ≡⟨ cong (λ k → k - (b * (a * eb)) ) (*-assoc b _ p) ⟩ | |
| 653 (b * (ea * p)) - (b * (a * eb )) ≡⟨ sym ( distr-minus-*' {b} {ea * p} {a * eb} ) ⟩ | |
| 654 b * (( ea * p) - (a * eb) ) ≡⟨ cong (λ k → b * ( ( ea * p) - k)) (*-comm a (eb)) ⟩ | |
| 655 (b * ( (ea * p)) - (eb * a) ) ≡⟨ cong (b *_) (Euclid.is-equ< ge11 lt )⟩ | |
| 245 | 656 b * gcd p a ≡⟨ cong (b *_) ge10 ⟩ |
| 657 b * 1 ≡⟨ m*1=m ⟩ | |
| 658 b ∎ where open ≡-Reasoning | |
| 255 | 659 ge15 : ( ea * p ) < ( eb * a ) → ((f * eb) - (b * ea ) ) * p + 0 ≡ b |
| 247 | 660 ge15 lt = begin |
| 255 | 661 ((f * eb) - (b * ea) ) * p + 0 ≡⟨ +-comm _ 0 ⟩ |
| 662 ((f * eb) - (b * ea) ) * p ≡⟨ distr-minus-* {_} {b * ea} {p} ⟩ | |
| 663 ((f * eb) * p) - ((b * ea) * p) ≡⟨ cong (λ k → k - ((b * ea) * p) ) ge18 ⟩ | |
| 664 (b * (a * eb )) - ((b * ea) * p ) ≡⟨ cong (λ k → (b * (a * eb)) - k ) (*-assoc b _ p) ⟩ | |
| 665 (b * (a * eb )) - (b * (ea * p) ) ≡⟨ sym ( distr-minus-*' {b} {a * eb} {ea * p} ) ⟩ | |
| 666 b * ( (a * eb) - (ea * p) ) ≡⟨ cong (λ k → b * ( k - ( ea * p) )) (*-comm a (eb)) ⟩ | |
| 667 b * ( (eb * a) - (ea * p) ) ≡⟨ cong (b *_) (Euclid.is-equ> ge11 lt) ⟩ | |
| 247 | 668 b * gcd p a ≡⟨ cong (b *_) ge10 ⟩ |
| 669 b * 1 ≡⟨ m*1=m ⟩ | |
| 670 b ∎ where open ≡-Reasoning | |
| 246 | 671 ge17 : (x y : ℕ ) → x ≡ y → x ≤ y |
| 672 ge17 x x refl = refl-≤ | |
| 245 | 673 ge16 : Dividable p b |
| 255 | 674 ge16 with <-cmp ( ea * p ) ( eb * a ) |
| 675 ... | tri< a ¬b ¬c = record { factor = (f * eb) - (b * ea) ; is-factor = ge15 a } | |
| 676 ... | tri≈ ¬a eq ¬c = record { factor = (b * ea) - ( f * eb) ; is-factor = ge19 eq } | |
| 677 ... | tri> ¬a ¬b c = record { factor = (b * ea) - (f * eb) ; is-factor = ge14 c } | |
| 245 | 678 |
| 679 | |
| 206 | 680 |
| 167 | 681 gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1 |
| 682 gcdmul+1 zero n = gcd204 n | |
| 683 gcdmul+1 (suc m) n = begin | |
| 684 gcd (suc m * n + 1) n ≡⟨⟩ | |
| 685 gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin | |
| 686 n + m * n + 1 ≡⟨ cong (λ k → k + 1) (+-comm n _) ⟩ | |
| 687 m * n + n + 1 ≡⟨ +-assoc (m * n) _ _ ⟩ | |
| 688 m * n + (n + 1) ≡⟨ cong (λ k → m * n + k) (+-comm n _) ⟩ | |
| 689 m * n + (1 + n) ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩ | |
| 690 m * n + 1 + n ∎ | |
| 691 ) ⟩ | |
| 212 | 692 gcd (m * n + 1 + n) n ≡⟨ gcd+j (m * n + 1) n ⟩ |
| 167 | 693 gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩ |
| 694 1 ∎ where open ≡-Reasoning | |
| 695 | |
| 230 | 696 m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1 |
| 697 m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq | |
| 698 |