Mercurial > hg > Members > kono > Proof > prob1
changeset 31:908409975a5e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Mar 2020 20:22:04 +0900 |
| parents | 7256d3d032e4 |
| children | 1e3130896834 |
| files | prob1.agda |
| diffstat | 1 files changed, 37 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/prob1.agda Mon Mar 30 17:51:52 2020 +0900 +++ b/prob1.agda Mon Mar 30 20:22:04 2020 +0900 @@ -39,6 +39,7 @@ c1 : Cond1 A M k unique-i : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.i c1 ≡ j unique-n : {j : ℕ} {m1 : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.n c1 ≡ m1 + maxA : A ≤ ( k * M ) - 1 problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) → UCond1 A M k @@ -134,9 +135,45 @@ unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c )) unique-n : {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1 unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq + -- A < M + ((k - n) * M) + -- A < suc k * M - n * M < suc k * M - n * M + lemma8 : A - ((k - n) * M) < M → A < M + ((k - n) * M) + lemma8 i<M with <-cmp (suc (suc A)) ( (k - n) * M ) + lemma8 i<M | tri< a ¬b ¬c = {!!} + lemma8 i<M | tri≈ ¬a b ¬c = {!!} + lemma8 i<M | tri> ¬a ¬b c = begin + suc A + ≡⟨ sym ( minus+n {suc A} {(k - n) * M} c ) ⟩ + (suc A - ((k - n) * M)) + (k - n) * M + ≡⟨ {!!} ⟩ + suc ( (A - ((k - n) * M)) + ((k - n) * M) ) + ≤⟨ ≤-plus i<M ⟩ + M + ((k - n) * M) + ∎ where open ≤-Reasoning + lemma9 : {x y : ℕ } → suc x ≤ y → x ≤ y - 1 + lemma9 {zero} {zero} () + lemma9 {suc x} {zero} () + lemma9 {x} {suc y} (s≤s lt) = lt + maxA : A - ((k - n) * M) < M → A ≤ (suc k * M ) - 1 + maxA i<M = begin + A + ≤⟨ lemma9 (lemma8 i<M ) ⟩ + (M + ((k - n) * M)) - 1 + ≡⟨ cong (λ k → (M + k ) - 1 ) (distr-minus-* {k} {n} {M} ) ⟩ + (M + ((k * M) - ( n * M))) - 1 + ≡⟨ {!!} ⟩ + ((M + (k * M) )- ( n * M)) - 1 + ≡⟨⟩ + ((suc k * M )- ( n * M)) - 1 + ≡⟨ {!!} ⟩ + (suc k * M) - ((n * M) + 1) + ≤⟨ {!!} ⟩ + (suc k * M ) - 1 + ∎ where open ≤-Reasoning c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } ; unique-i = unique-i ; unique-n = unique-n + ; maxA = maxA i<M } -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M)