Mercurial > hg > Members > kono > Proof > prob1
changeset 5:310a70c03166
cck done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 26 Nov 2019 02:08:50 +0900 |
| parents | 2a36d771d388 |
| children | fce6cadae300 |
| files | prob1.agda |
| diffstat | 1 files changed, 24 insertions(+), 36 deletions(-) [+] |
line wrap: on
line diff
--- a/prob1.agda Mon Nov 25 23:08:02 2019 +0900 +++ b/prob1.agda Tue Nov 26 02:08:50 2019 +0900 @@ -80,48 +80,36 @@ -- i + 2 * M = M * (suc n) + A i = suc n → A = 0 +open import Data.Product + problem : ( A M k : ℕ ) → Set problem A M k = (suc A < k * M ) → Cond1 A M k problem0-k=k : ( k A M : ℕ ) → problem A M k problem0-k=k zero A M () -problem0-k=k (suc k) A M A<kM = cc k {!!} where +problem0-k=k (suc k) A M A<kM = cc k where + cck : ( n : ℕ ) → n < k → (suc A > (minus k n ) * M ) → minus A (minus k n * M) < M → Cond1 A M (suc k) + cck n n<k gt lt = record { n = n ; i = minus A ((minus k n) * M ) ; range-n = <-trans n<k a<sa ; range-i = lt ; rule1 = lemma2 } where + lemma2 : minus A (minus k n * M) + suc k * M ≡ M * suc n + A + lemma2 = begin + minus A (minus k n * M) + suc k * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (sym (minus+n {k} {n} (<-trans n<k a<sa ) )) ⟩ + minus A (minus k n * M) + (suc ((minus k n ) + n )) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (+-comm _ n) ⟩ + minus A (minus k n * M) + (suc (n + (minus k n ) )) * M ≡⟨⟩ + minus A (minus k n * M) + (suc n + (minus k n ) ) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + x * M ) (+-comm (suc n) _) ⟩ + minus A (minus k n * M) + ((minus k n ) + suc n ) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + x ) (((proj₂ *-distrib-+)) M (minus k n) _ ) ⟩ + minus A (minus k n * M) + ((minus k n * M) + (suc n) * M) ≡⟨ sym (+-assoc (minus A (minus k n * M)) _ ((suc n) * M)) ⟩ + minus A (minus k n * M) + (minus k n * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {minus k n * M} gt ) ⟩ + A + (suc n) * M ≡⟨ cong ( λ k → A + k ) (*-comm (suc n) _ ) ⟩ + A + M * (suc n) ≡⟨ +-comm A _ ⟩ + M * (suc n) + A + ∎ where open ≡-Reasoning - ccn : (suc A > k * M ) → Cond1 A M (suc k) - ccn gt = record { n = 0 ; i = minus A (k * M ) ; range-n = s≤s z≤n ; range-i = A-Mk<M {k} gt A<kM ; rule1 = lemma1 } where - A-Mk<M : {k A M : ℕ } → (suc A > k * M ) → ( suc A < (suc k ) * M ) → minus A (k * M ) < M - A-Mk<M {k} {A} {M} lt1 lt2 = <-minus ( subst₂ (λ j k → j < k ) (sym (minus+n {A} {k * M} lt1 )) refl (<-trans a<sa lt2) ) - lemma1 : minus A (k * M) + suc k * M ≡ M * 1 + A - lemma1 = begin - minus A (k * M) + suc k * M - ≡⟨⟩ - minus A (k * M) + (M + k * M ) - ≡⟨ cong ( λ x → minus A (k * M) + x ) (+-comm M _ ) ⟩ - minus A (k * M) + (k * M + M ) - ≡⟨ sym ( +-assoc _ (k * M ) M ) ⟩ - (minus A (k * M) + k * M ) + M - ≡⟨ cong ( λ k → k + M ) (minus+n {A} {k * M} gt ) ⟩ - A + M - ≡⟨⟩ - A + ( 0 + M ) - ≡⟨ cong ( λ k → A + k ) (+-comm 0 _ ) ⟩ - A + ( M + 0 ) - ≡⟨⟩ - A + 1 * M - ≡⟨ cong ( λ k → A + k ) (*-comm 1 _ ) ⟩ - A + M * 1 - ≡⟨ +-comm A _ ⟩ - M * 1 + A - ∎ where open ≡-Reasoning - cck : ( n : ℕ ) → n < k → (suc A > (minus k n ) * M ) → Cond1 A M (suc k) - cck n n<k gt = record { n = n ; i = minus A ((minus k n) * M ) ; range-n = {!!} ; range-i = {!!} ; rule1 = {!!} } - - cc : ( n : ℕ ) → (suc A > (minus k n ) * M) → Cond1 A M (suc k) - cc 0 lt = {!!} - cc (suc n) lt with <-cmp A ((minus k (suc n) ) * M) - cc (suc n ) lt | tri< a ¬b ¬c = cck (suc n) {!!} {!!} - cc (suc n ) lt | tri≈ ¬a b ¬c = cck (suc n) {!!} {!!} - cc (suc n ) lt | tri> ¬a ¬b c = cc n {!!} + cc : ( n : ℕ ) → Cond1 A M (suc k) + cc 0 = cck 0 ? ? ? + cc (suc n) with <-cmp A ((minus k (suc n) ) * M) + cc (suc n ) | tri< a ¬b ¬c = cck (suc n) {!!} {!!} {!!} + cc (suc n ) | tri≈ ¬a b ¬c = cck (suc n) {!!} {!!} {!!} + cc (suc n ) | tri> ¬a ¬b c = cc n 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