Mercurial > hg > Members > kono > Proof > prob1
changeset 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 |
| files | prob1.agda |
| diffstat | 1 files changed, 19 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/prob1.agda Mon Mar 30 10:31:16 2020 +0900 +++ b/prob1.agda Mon Mar 30 14:28:14 2020 +0900 @@ -38,7 +38,7 @@ field c1 : Cond1 A M k u1 : {j m : ℕ} → j < Cond1.i c1 → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) - -- u2 : {j m : ℕ} → Cond1.i c1 < j → j < M → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) + u2 : {j m : ℕ} → Cond1.i c1 < j → j < M → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) -- u3 : {j m : ℕ} → j < M → m < Cond1.n c1 → ¬ ( j + k * M ≡ M * (suc m) + A ) -- u4 : {j m : ℕ} → j < M → Cond1.n c1 < m → m < k → ¬ ( j + k * M ≡ M * (suc m) + A ) @@ -70,10 +70,10 @@ lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y) lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) ) - lemma5 : {m1 : ℕ} → M * suc m1 + A < M * suc n + A + lemma5 : {m1 n : ℕ} → M * suc m1 + A < M * suc n + A → M + (M * suc m1 + A) ≤ M * suc n + A - lemma5 {m1} lt with <-cmp m1 n - lemma5 {m1} lt | tri< a ¬b ¬c = begin + lemma5 {m1} {n} lt with <-cmp m1 n + lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin M + (M * suc m1 + A) ≡⟨ sym (+-assoc M _ _ ) ⟩ (M + M * suc m1) + A @@ -84,8 +84,8 @@ ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M ) (*≤ (s≤s a))) ⟩ M * suc n + A ∎ where open ≤-Reasoning - lemma5 {m1} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt ) - lemma5 {m1} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c) + lemma5 {m1} {n} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt ) + lemma5 {m1} {n} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c) (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c))))))) lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin @@ -97,15 +97,25 @@ ≤⟨ lt ⟩ i + x ∎ )) where open ≤-Reasoning - lemma-u1 : {j : ℕ} {m1 : ℕ} → j < (A - ((k - n) * M)) → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A + i : ℕ + i = A - ((k - n) * M) + lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c = ⊥-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 - lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A + lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A -- M + j ≤ i lemma3 = lemma5 (lemma4 eq (Cond1.rule1 c1) j<akM) lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) - c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } ; u1 = lemma-u1 } + lemma-u2 : {j : ℕ} {m1 : ℕ} → (A - ((k - n) * M)) < j → + j < M → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A + 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 + lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j + lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j) + c0 = record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k ; range-i = i<M; rule1 = Cond1.rule1 c1 } + ; u1 = lemma-u1 + ; u2 = lemma-u2 + } -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) nextc n n<k with k - n | inspect (_-_ k) n