Mercurial > hg > Members > kono > Proof > prob1
changeset 7:f5828d8af20c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 26 Nov 2019 08:36:56 +0900 |
| parents | fce6cadae300 |
| children | cca92e69b629 |
| files | prob1.agda |
| diffstat | 1 files changed, 10 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/prob1.agda Tue Nov 26 02:34:34 2019 +0900 +++ b/prob1.agda Tue Nov 26 08:36:56 2019 +0900 @@ -103,14 +103,18 @@ A + M * (suc n) ≡⟨ +-comm A _ ⟩ M * (suc n) + A ∎ where open ≡-Reasoning - i<range : {n : ℕ } → A < (suc n) * M → minus A (minus k n * M) < M + i<range : {n : ℕ } → suc A < suc ((suc n) * M) → minus A (minus k n * M) < M i<range = {!!} - cc : ( n : ℕ ) → n < suc k → suc A < (suc k) * M → Cond1 A M (suc k) - cc 0 n<k lt = cck 0 n<k {!!} (i<range {!!}) + gt : {n : ℕ } → suc A < suc ((suc n) * M) → (minus k n ) * M < suc A + gt = {!!} + next-lt : (n : ℕ ) → suc A < (suc n) * M → (A > (pred n * M)) → suc A < n * M + next-lt n lt = {!!} + cc : ( n : ℕ ) → n < suc k → suc A < (suc n) * M → Cond1 A M (suc k) + cc 0 n<k lt = cck 0 n<k (gt {!!} ) (i<range {!!}) cc (suc n) n<k lt with <-cmp A (n * M) - cc (suc n ) n<k lt | tri< a ¬b ¬c = cck (suc n) n<k {!!} {!!} - cc (suc n ) n<k lt | tri≈ ¬a b ¬c = cck (suc n) n<k {!!} {!!} - cc (suc n ) n<k lt | tri> ¬a ¬b c = cc n (less-1 n<k ) {!!} + cc (suc n ) n<k lt | tri< a ¬b ¬c = cck (suc n) n<k (gt {!!} ) (i<range {!!}) + cc (suc n ) n<k lt | tri≈ ¬a b ¬c = cck (suc n) n<k (gt {!!} ) (i<range {!!}) + cc (suc n ) n<k lt | tri> ¬a ¬b c = cc n (less-1 n<k ) (next-lt (suc n) lt c ) problem0 : ( A M k : ℕ ) → M > 0 → k > 0 → (suc A < k * M ) → Cond1 A M k problem0 A (suc M) (suc k) 0<M 0<k A<kM = lemma1 k M A<kM a<sa a<sa where