Mercurial > hg > Members > kono > Proof > prob1
annotate prob1.agda @ 27:73511e7ddf5c
u2 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Mar 2020 14:28:14 +0900 |
| parents | fd8633b6d551 |
| children | 8ef3eecd159f |
| rev | line source |
|---|---|
|
0
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module prob1 where |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Relation.Binary.PropositionalEquality |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Relation.Binary.Core |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Nat |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Data.Nat.Properties |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import logic |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import nat |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Data.Empty |
| 14 | 10 open import Data.Product |
|
0
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open import Relation.Nullary |
| 20 | 12 -- open import Relation.Binary.Definitions |
| 19 | 13 |
|
0
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 -- All variables are positive integer |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 -- A = -M*n + i +k*M - M |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 -- where n is in range (0,…,k-1) and i is in range(0,…,M-1) |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 -- Goal: Prove that A can take all values of (0,…,k*M-1) |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 -- A1 = -M*n1 + i1 +k*M M, A2 = -M*n2 + i2 +k*M - M |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 -- (1) If n1!=n2 or i1!=i2 then A1!=A2 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 -- Or its contraposition: (2) if A1=A2 then n1=n2 and i1=i2 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 -- Proof by contradiction: Suppose A1=A2 and (n1!=n2 or i1!=i2) becomes |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 -- contradiction |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 -- Induction on n and i |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 record Cond1 (A M k : ℕ ) : Set where |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 field |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 n : ℕ |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 i : ℕ |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 range-n : n < k |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 range-i : i < M |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 rule1 : i + k * M ≡ M * (suc n) + A -- A ≡ (i + k * M ) - (M * (suc n)) |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 -- k = 1 → n = 0 → ∀ M → A = i |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 -- k = 2 → n = 1 → |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 -- i + 2 * M = M * (suc n) + A i = suc n → A = 0 |
|
06002e20ce5c
incudtion selection on diophantos equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 |
| 26 | 37 record UCond1 (A M k : ℕ ) : Set where |
| 38 field | |
| 39 c1 : Cond1 A M k | |
| 40 u1 : {j m : ℕ} → j < Cond1.i c1 → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) | |
| 27 | 41 u2 : {j m : ℕ} → Cond1.i c1 < j → j < M → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) |
| 26 | 42 -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1 → ¬ ( j + k * M ≡ M * (suc m) + A ) |
| 43 -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) | |
| 18 | 44 |
| 26 | 45 problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) |
| 46 → UCond1 A M k | |
| 47 problem1-0 zero A M () | |
| 48 problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s )) | |
| 49 problem1-0 (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where | |
| 13 | 50 M = suc m |
| 14 | 51 cck : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → Cond1 A M (suc k) |
| 52 cck n n<k gt lt = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = lt ; rule1 = lemma2 } where | |
| 53 lemma2 : A - ((k - n) * M) + suc k * M ≡ M * suc n + A | |
| 5 | 54 lemma2 = begin |
| 14 | 55 A - ((k - n) * M) + suc k * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩ |
| 56 A - ((k - n) * M) + (suc (((k - n) ) + n )) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (+-comm _ n) ⟩ | |
| 57 A - ((k - n) * M) + (suc (n + ((k - n) ) )) * M ≡⟨⟩ | |
| 58 A - ((k - n) * M) + (suc n + ((k - n) ) ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x * M ) (+-comm (suc n) _) ⟩ | |
| 59 A - ((k - n) * M) + (((k - n) ) + suc n ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x ) (((proj₂ *-distrib-+)) M ((k - n)) _ ) ⟩ | |
| 60 A - ((k - n) * M) + (((k - n) * M) + (suc n) * M) ≡⟨ sym (+-assoc (A - ((k - n) * M)) _ ((suc n) * M)) ⟩ | |
| 61 A - ((k - n) * M) + ((k - n) * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {(k - n) * M} gt ) ⟩ | |
| 5 | 62 A + (suc n) * M ≡⟨ cong ( λ k → A + k ) (*-comm (suc n) _ ) ⟩ |
| 63 A + M * (suc n) ≡⟨ +-comm A _ ⟩ | |
| 64 M * (suc n) + A | |
| 65 ∎ where open ≡-Reasoning | |
| 26 | 66 cck-u : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → UCond1 A M (suc k) |
| 67 cck-u n n<k k<A i<M = c0 where | |
| 21 | 68 c1 : Cond1 A M (suc k) |
| 26 | 69 c1 = cck n n<k k<A i<M |
| 24 | 70 lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z |
| 71 lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y) | |
| 72 lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) ) | |
| 27 | 73 lemma5 : {m1 n : ℕ} → M * suc m1 + A < M * suc n + A |
| 24 | 74 → M + (M * suc m1 + A) ≤ M * suc n + A |
| 27 | 75 lemma5 {m1} {n} lt with <-cmp m1 n |
| 76 lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin | |
| 25 | 77 M + (M * suc m1 + A) |
| 78 ≡⟨ sym (+-assoc M _ _ ) ⟩ | |
| 79 (M + M * suc m1) + A | |
| 80 ≡⟨ sym ( cong (λ k → (k + M * suc m1) + A) ((proj₂ *-identity) M )) ⟩ | |
| 81 (M * suc zero + M * suc m1) + A | |
| 82 ≡⟨ sym ( cong (λ k → k + A) (( proj₁ *-distrib-+ ) M (suc zero) _ )) ⟩ | |
| 83 M * suc (suc m1) + A | |
| 84 ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M ) (*≤ (s≤s a))) ⟩ | |
| 85 M * suc n + A | |
| 86 ∎ where open ≤-Reasoning | |
| 27 | 87 lemma5 {m1} {n} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt ) |
| 88 lemma5 {m1} {n} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c) | |
| 25 | 89 (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c))))))) |
| 24 | 90 lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i |
| 91 lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin | |
| 92 M + x + j | |
| 93 ≡⟨ +-assoc M _ _ ⟩ | |
| 94 M + (x + j ) | |
| 95 ≡⟨ cong (λ k → M + k ) (+-comm x _ ) ⟩ | |
| 96 M + (j + x) | |
| 97 ≤⟨ lt ⟩ | |
| 98 i + x | |
| 99 ∎ )) where open ≤-Reasoning | |
| 27 | 100 i : ℕ |
| 101 i = A - ((k - n) * M) | |
| 102 lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A | |
| 23 | 103 lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M |
| 24 | 104 lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = |
| 105 ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) (lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM ))) ) i<M ) where | |
| 27 | 106 lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A -- M + j ≤ i |
| 24 | 107 lemma3 = lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM) |
| 23 | 108 lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) |
| 109 lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) | |
| 27 | 110 lemma-u2 : {j : ℕ} {m1 : ℕ} → (A - ((k - n) * M)) < j → |
| 111 j < M → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A | |
| 112 lemma-u2 {j} {m1} i<j j<M m1<k eq = ⊥-elim ( nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym (Cond1.rule1 c1)) (sym eq) lemma3-2)) j<M ) where | |
| 113 lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j | |
| 114 lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j) | |
| 115 c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } | |
| 116 ; u1 = lemma-u1 | |
| 117 ; u2 = lemma-u2 | |
| 118 } | |
| 26 | 119 -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M |
| 120 nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) | |
| 121 nextc n n<k with k - n | inspect (_-_ k) n | |
| 122 nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) ) | |
| 123 nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where | |
| 124 lemma : m ≤ m + n0 * suc m | |
| 125 lemma = x≤x+y | |
| 20 | 126 cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k) |
| 26 | 127 cc zero n<k k<A = cck-u 0 n<k k<A lemma where |
| 21 | 128 a<m : suc A < M + k * M |
| 129 a<m = A<kM | |
| 130 lemma : A - ((k - 0) * M) < M | |
| 131 lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) ) | |
| 17 | 132 cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M)) M |
| 26 | 133 cc (suc n) n<k k<A | tri< a ¬b ¬c = cck-u (suc n) n<k k<A a |
| 20 | 134 cc (suc n) n<k k<A | tri≈ ¬a b ¬c = |
| 22 | 135 cc n (less-1 n<k) (lemma1 b) where |
| 136 a=mk0 : (A - ((k - (suc n)) * M)) ≡ M → A ≡ (k - n) * M | |
| 137 a=mk0 a=mk = sym ( begin | |
| 138 (k - n) * M | |
| 26 | 139 ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩ |
| 22 | 140 ((k - n) * M ) - M + M |
| 141 ≡⟨ +-comm _ M ⟩ | |
| 142 M + (((k - n) * M ) - M) | |
| 143 ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩ | |
| 144 M + (k - (suc n) * M) | |
| 145 ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩ | |
| 146 A - ((k - (suc n)) * M) + ((k - (suc n)) * M) | |
| 147 ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩ | |
| 148 A | |
| 149 ∎ ) where open ≡-Reasoning | |
| 150 lemma1 : (A - ((k - (suc n)) * M)) ≡ M → suc A > (k - n) * M | |
| 151 lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa | |
| 20 | 152 cc (suc n) n<k k<A | tri> ¬a ¬b c = |
| 22 | 153 cc n (less-1 n<k) (lemma3 c) where |
| 154 lemma3 : (A - ((k - (suc n)) * M)) > M → suc A > (k - n) * M | |
| 155 lemma3 mk<a = <-trans lemma5 a<sa where | |
| 156 lemma6 : M + (k - (suc n)) * M ≡ (k - n) * M | |
| 157 lemma6 = begin | |
| 158 M + (k - (suc n)) * M | |
| 159 ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k)) ⟩ | |
| 160 M + (((k - n) * M ) - M ) | |
| 161 ≡⟨ +-comm M _ ⟩ | |
| 162 ((k - n) * M ) - M + M | |
| 26 | 163 ≡⟨ minus+n {_} {M} (nextc n n<k ) ⟩ |
| 22 | 164 (k - n) * M |
| 165 ∎ where open ≡-Reasoning | |
| 166 lemma4 : (M + (k - (suc n)) * M) < A | |
| 167 lemma4 = subst (λ x → (M + (k - (suc n)) * M) < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a ) | |
| 168 lemma5 : (k - n) * M < A | |
| 169 lemma5 = subst (λ x → x < A ) lemma6 lemma4 | |
| 17 | 170 start-range : (k : ℕ ) → suc A > (k - k) * M |
| 171 start-range zero = s≤s z≤n | |
| 172 start-range (suc k) = start-range k | |
| 173 |