Mercurial > hg > Members > kono > Proof > prob1
annotate prob1.agda @ 32:1e3130896834
maxA done (all 0,1,2 done)
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 31 Mar 2020 01:18:56 +0900 |
| parents | 908409975a5e |
| children | b5e8e6be9425 |
| 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 | |
| 29 | 40 unique-i : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.i c1 ≡ j |
| 41 unique-n : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.n c1 ≡ m1 | |
| 31 | 42 maxA : A ≤ ( k * M ) - 1 |
| 18 | 43 |
| 26 | 44 problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) |
| 45 → UCond1 A M k | |
| 46 problem1-0 zero A M () | |
| 47 problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s )) | |
| 48 problem1-0 (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where | |
| 13 | 49 M = suc m |
| 14 | 50 cck : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → Cond1 A M (suc k) |
| 51 cck n n<k gt lt = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = lt ; rule1 = lemma2 } where | |
| 52 lemma2 : A - ((k - n) * M) + suc k * M ≡ M * suc n + A | |
| 5 | 53 lemma2 = begin |
| 14 | 54 A - ((k - n) * M) + suc k * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩ |
| 55 A - ((k - n) * M) + (suc (((k - n) ) + n )) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (+-comm _ n) ⟩ | |
| 56 A - ((k - n) * M) + (suc (n + ((k - n) ) )) * M ≡⟨⟩ | |
| 57 A - ((k - n) * M) + (suc n + ((k - n) ) ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x * M ) (+-comm (suc n) _) ⟩ | |
| 58 A - ((k - n) * M) + (((k - n) ) + suc n ) * M ≡⟨ cong ( λ x → A - ((k - n) * M) + x ) (((proj₂ *-distrib-+)) M ((k - n)) _ ) ⟩ | |
| 59 A - ((k - n) * M) + (((k - n) * M) + (suc n) * M) ≡⟨ sym (+-assoc (A - ((k - n) * M)) _ ((suc n) * M)) ⟩ | |
| 60 A - ((k - n) * M) + ((k - n) * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {(k - n) * M} gt ) ⟩ | |
| 5 | 61 A + (suc n) * M ≡⟨ cong ( λ k → A + k ) (*-comm (suc n) _ ) ⟩ |
| 62 A + M * (suc n) ≡⟨ +-comm A _ ⟩ | |
| 63 M * (suc n) + A | |
| 64 ∎ where open ≡-Reasoning | |
| 26 | 65 cck-u : ( n : ℕ ) → n < suc k → (suc A > ((k - n) ) * M ) → A - ((k - n) * M) < M → UCond1 A M (suc k) |
| 66 cck-u n n<k k<A i<M = c0 where | |
| 21 | 67 c1 : Cond1 A M (suc k) |
| 26 | 68 c1 = cck n n<k k<A i<M |
| 24 | 69 lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z |
| 70 lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y) | |
| 71 lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) ) | |
| 27 | 72 lemma5 : {m1 n : ℕ} → M * suc m1 + A < M * suc n + A |
| 24 | 73 → M + (M * suc m1 + A) ≤ M * suc n + A |
| 27 | 74 lemma5 {m1} {n} lt with <-cmp m1 n |
| 75 lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin | |
| 25 | 76 M + (M * suc m1 + A) |
| 77 ≡⟨ sym (+-assoc M _ _ ) ⟩ | |
| 78 (M + M * suc m1) + A | |
| 79 ≡⟨ sym ( cong (λ k → (k + M * suc m1) + A) ((proj₂ *-identity) M )) ⟩ | |
| 80 (M * suc zero + M * suc m1) + A | |
| 81 ≡⟨ sym ( cong (λ k → k + A) (( proj₁ *-distrib-+ ) M (suc zero) _ )) ⟩ | |
| 82 M * suc (suc m1) + A | |
| 83 ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M ) (*≤ (s≤s a))) ⟩ | |
| 84 M * suc n + A | |
| 85 ∎ where open ≤-Reasoning | |
| 27 | 86 lemma5 {m1} {n} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt ) |
| 87 lemma5 {m1} {n} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c) | |
| 25 | 88 (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c))))))) |
| 24 | 89 lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i |
| 90 lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin | |
| 91 M + x + j | |
| 92 ≡⟨ +-assoc M _ _ ⟩ | |
| 93 M + (x + j ) | |
| 94 ≡⟨ cong (λ k → M + k ) (+-comm x _ ) ⟩ | |
| 95 M + (j + x) | |
| 96 ≤⟨ lt ⟩ | |
| 97 i + x | |
| 98 ∎ )) where open ≤-Reasoning | |
| 27 | 99 i : ℕ |
| 100 i = A - ((k - n) * M) | |
| 101 lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A | |
| 23 | 102 lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M |
| 24 | 103 lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = |
| 30 | 104 ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) lemma3) ) i<M ) where |
| 27 | 105 lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A -- M + j ≤ i |
| 24 | 106 lemma3 = lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM) |
| 23 | 107 lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) |
| 108 lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) | |
| 27 | 109 lemma-u2 : {j : ℕ} {m1 : ℕ} → (A - ((k - n) * M)) < j → |
| 110 j < M → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A | |
| 111 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 | |
| 112 lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j | |
| 113 lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j) | |
| 28 | 114 unique-i : {j : ℕ} {m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → i ≡ j |
| 115 unique-i {j} {m1} j<M m1<k eq with <-cmp i j | |
| 116 unique-i {j} {m1} j<M m1<k eq | tri< a ¬b ¬c = ⊥-elim ( lemma-u2 a j<M m1<k eq ) | |
| 117 unique-i {j} {m1} j<M m1<k eq | tri≈ ¬a b ¬c = b | |
| 118 unique-i {j} {m1} j<M m1<k eq | tri> ¬a ¬b c = ⊥-elim ( lemma-u1 c m1<k eq ) | |
| 119 lemma7 : {n m1 m A : ℕ} → n < m1 → suc (n + m * suc n + A) < suc (m1 + m * suc m1 + A) | |
| 120 lemma7 {n} {m1} {m} {A} n<m1 = begin | |
| 121 suc (suc (n + m * suc n + A)) | |
| 122 ≡⟨ +-assoc _ (m * suc n) A ⟩ | |
| 123 suc (suc n + (m * suc n + A)) | |
| 124 ≤⟨ s≤s (<-plus n<m1) ⟩ | |
| 125 suc (m1 + (m * suc n + A)) | |
| 126 ≡⟨ sym ( +-assoc _ (m * suc n) A) ⟩ | |
| 127 suc (m1 + m * suc n + A) | |
| 128 ≤⟨ ≤-plus {_} {_} {A} (≤-plus-0 {_} {_} {suc m1} (≤* {suc n} {suc m1} {m} (s≤s (≤to< n<m1 )))) ⟩ | |
| 129 suc (m1 + m * suc m1 + A) | |
| 130 ∎ where open ≤-Reasoning | |
| 131 unique-m : {i j : ℕ} {n m1 : ℕ} → i ≡ j → i + suc k * M ≡ M * suc n + A → j + suc k * M ≡ M * suc m1 + A → n ≡ m1 | |
| 132 unique-m {i} {_} {n} {m1} refl eqn eqm with <-cmp n m1 | |
| 133 unique-m {i} {_} {n} {m1} refl eqn eqm | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym (trans (sym eqm) eqn )) (lemma7 {n} {m1} {m} {A} a )) | |
| 134 unique-m {i} {_} {n} {m1} refl eqn eqm | tri≈ ¬a b ¬c = b | |
| 135 unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c )) | |
| 29 | 136 unique-n : {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1 |
| 137 unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq | |
|
32
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
138 lemmab : {x m : ℕ } → x < suc (m + x) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
139 lemmab {x} {zero} = a<sa |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
140 lemmab {zero} {suc m} = <to<s (lemmab {zero} {m}) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
141 lemmab {suc x} {suc m} = ( s≤s (subst (λ k → suc x ≤ k) (+-comm _ (suc m)) x≤x+y )) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
142 lemmaa : {x y : ℕ} → suc x > y → (suc x - y) + y ≡ suc ( (x - y) + y ) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
143 lemmaa {x} {y} lt = begin |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
144 (suc x - y) + y |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
145 ≡⟨ minus+n (<-trans lt a<sa ) ⟩ |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
146 suc x |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
147 ≡⟨ sym ( cong (λ k → suc k) ( minus+n {x} {y} lt ) ) ⟩ |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
148 suc (x - y) + y |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
149 ≡⟨⟩ |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
150 suc ( (x - y) + y ) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
151 ∎ where open ≡-Reasoning |
| 31 | 152 -- A < M + ((k - n) * M) |
| 153 -- A < suc k * M - n * M < suc k * M - n * M | |
| 154 lemma8 : A - ((k - n) * M) < M → A < M + ((k - n) * M) | |
|
32
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
155 lemma8 i<M with <-cmp (suc A) ( (k - n) * M ) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
156 lemma8 i<M | tri< a ¬b ¬c = <-minus-0 {A} {_} {suc zero} ( <-trans a (<to<s lemmab) ) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
157 lemma8 i<M | tri≈ ¬a b ¬c = <-minus-0 {A} {_} {suc zero} (subst (λ h → h < 1 + suc (m + minus k n * suc m)) (sym b) (<to<s lemmab)) where |
| 31 | 158 lemma8 i<M | tri> ¬a ¬b c = begin |
| 159 suc A | |
|
32
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
160 ≡⟨ sym ( minus+n {suc A} {(k - n) * M} (<-trans c a<sa) ) ⟩ |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
161 (suc A - ((k - n) * M)) + ((k - n) * M ) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
162 ≡⟨ lemmaa {A} {(k - n) * M} c ⟩ |
| 31 | 163 suc ( (A - ((k - n) * M)) + ((k - n) * M) ) |
| 164 ≤⟨ ≤-plus i<M ⟩ | |
| 165 M + ((k - n) * M) | |
| 166 ∎ where open ≤-Reasoning | |
| 167 lemma9 : {x y : ℕ } → suc x ≤ y → x ≤ y - 1 | |
| 168 lemma9 {zero} {zero} () | |
| 169 lemma9 {suc x} {zero} () | |
| 170 lemma9 {x} {suc y} (s≤s lt) = lt | |
|
32
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
171 lemmad : {n k m : ℕ} → n < suc k → n * suc m < suc ( k * suc m ) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
172 lemmad {n} {k} {m} n<k with <-cmp n k |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
173 lemmad {n} {k} {m} n<k | tri< a ¬b ¬c = <-trans ( *< a ) a<sa |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
174 lemmad {n} {k} {m} n<k | tri≈ ¬a refl ¬c = ≤-refl |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
175 lemmad {n} {k} {m} n<k | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n<k (s≤s c) ) |
| 31 | 176 maxA : A - ((k - n) * M) < M → A ≤ (suc k * M ) - 1 |
| 177 maxA i<M = begin | |
| 178 A | |
| 179 ≤⟨ lemma9 (lemma8 i<M ) ⟩ | |
| 180 (M + ((k - n) * M)) - 1 | |
| 181 ≡⟨ cong (λ k → (M + k ) - 1 ) (distr-minus-* {k} {n} {M} ) ⟩ | |
| 182 (M + ((k * M) - ( n * M))) - 1 | |
|
32
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
183 ≡⟨ cong (λ k → k - 1 ) ( minus+assoc {M} {k * M} {n * M} (lemmad n<k)) ⟩ |
| 31 | 184 ((M + (k * M) )- ( n * M)) - 1 |
| 185 ≡⟨⟩ | |
| 186 ((suc k * M )- ( n * M)) - 1 | |
|
32
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
187 ≡⟨ minus-assoc {suc k * M} {n * M} {1} ⟩ |
| 31 | 188 (suc k * M) - ((n * M) + 1) |
|
32
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
189 ≡⟨ cong (λ h → (suc k * M) - h ) (+-comm (n * M) _) ⟩ |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
190 (suc k * M) - (1 + (n * M) ) |
|
1e3130896834
maxA done (all 0,1,2 done)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
31
diff
changeset
|
191 ≤⟨ minus+< {suc k * M} {1} {n * M} ⟩ |
| 31 | 192 (suc k * M ) - 1 |
| 193 ∎ where open ≤-Reasoning | |
| 27 | 194 c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } |
| 29 | 195 ; unique-i = unique-i |
| 196 ; unique-n = unique-n | |
| 31 | 197 ; maxA = maxA i<M |
| 27 | 198 } |
| 26 | 199 -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M |
| 200 nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) | |
| 201 nextc n n<k with k - n | inspect (_-_ k) n | |
| 202 nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) ) | |
| 203 nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where | |
| 204 lemma : m ≤ m + n0 * suc m | |
| 205 lemma = x≤x+y | |
| 20 | 206 cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k) |
| 26 | 207 cc zero n<k k<A = cck-u 0 n<k k<A lemma where |
| 21 | 208 a<m : suc A < M + k * M |
| 209 a<m = A<kM | |
| 210 lemma : A - ((k - 0) * M) < M | |
| 211 lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) ) | |
| 17 | 212 cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M)) M |
| 26 | 213 cc (suc n) n<k k<A | tri< a ¬b ¬c = cck-u (suc n) n<k k<A a |
| 20 | 214 cc (suc n) n<k k<A | tri≈ ¬a b ¬c = |
| 22 | 215 cc n (less-1 n<k) (lemma1 b) where |
| 216 a=mk0 : (A - ((k - (suc n)) * M)) ≡ M → A ≡ (k - n) * M | |
| 217 a=mk0 a=mk = sym ( begin | |
| 218 (k - n) * M | |
| 26 | 219 ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩ |
| 22 | 220 ((k - n) * M ) - M + M |
| 221 ≡⟨ +-comm _ M ⟩ | |
| 222 M + (((k - n) * M ) - M) | |
| 223 ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩ | |
| 224 M + (k - (suc n) * M) | |
| 225 ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩ | |
| 226 A - ((k - (suc n)) * M) + ((k - (suc n)) * M) | |
| 227 ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩ | |
| 228 A | |
| 229 ∎ ) where open ≡-Reasoning | |
| 230 lemma1 : (A - ((k - (suc n)) * M)) ≡ M → suc A > (k - n) * M | |
| 231 lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa | |
| 20 | 232 cc (suc n) n<k k<A | tri> ¬a ¬b c = |
| 22 | 233 cc n (less-1 n<k) (lemma3 c) where |
| 234 lemma3 : (A - ((k - (suc n)) * M)) > M → suc A > (k - n) * M | |
| 235 lemma3 mk<a = <-trans lemma5 a<sa where | |
| 236 lemma6 : M + (k - (suc n)) * M ≡ (k - n) * M | |
| 237 lemma6 = begin | |
| 238 M + (k - (suc n)) * M | |
| 239 ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k)) ⟩ | |
| 240 M + (((k - n) * M ) - M ) | |
| 241 ≡⟨ +-comm M _ ⟩ | |
| 242 ((k - n) * M ) - M + M | |
| 26 | 243 ≡⟨ minus+n {_} {M} (nextc n n<k ) ⟩ |
| 22 | 244 (k - n) * M |
| 245 ∎ where open ≡-Reasoning | |
| 246 lemma4 : (M + (k - (suc n)) * M) < A | |
| 247 lemma4 = subst (λ x → (M + (k - (suc n)) * M) < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a ) | |
| 248 lemma5 : (k - n) * M < A | |
| 249 lemma5 = subst (λ x → x < A ) lemma6 lemma4 | |
| 17 | 250 start-range : (k : ℕ ) → suc A > (k - k) * M |
| 251 start-range zero = s≤s z≤n | |
| 252 start-range (suc k) = start-range k | |
| 253 |