Mercurial > hg > Members > kono > Proof > prob1
changeset 28:8ef3eecd159f
all done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Mar 2020 17:03:01 +0900 |
| parents | 73511e7ddf5c |
| children | 24864ed3b6d3 |
| files | nat.agda prob1.agda |
| diffstat | 2 files changed, 38 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Mon Mar 30 14:28:14 2020 +0900 +++ b/nat.agda Mon Mar 30 17:03:01 2020 +0900 @@ -163,10 +163,16 @@ *≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z *≤ lt = *-mono-≤ lt ≤-refl +≤* : {x y z : ℕ } → x ≤ y → z * x ≤ z * y +≤* {x} {y} {z} lt = subst₂ (λ x y → x ≤ y ) (*-comm _ z) (*-comm _ z) (*≤ lt) + *< : {x y z : ℕ } → x < y → x * suc z < y * suc z *< {zero} {suc y} lt = s≤s z≤n *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) +<* : {x y z : ℕ } → x < y → suc z * x < suc z * y +<* {x} {y} {z} lt = subst₂ (λ x y → x < y ) (*-comm x _ ) (*-comm y (suc z)) (*< lt) + <to<s : {x y : ℕ } → x < y → x < suc y <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)
--- a/prob1.agda Mon Mar 30 14:28:14 2020 +0900 +++ b/prob1.agda Mon Mar 30 17:03:01 2020 +0900 @@ -39,8 +39,8 @@ 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 ) - -- 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 ) + 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 ) problem1-0 : (k A M : ℕ ) → (A<kM : suc A < k * M ) → UCond1 A M k @@ -112,9 +112,39 @@ 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) + unique-i : {j : ℕ} {m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → i ≡ j + unique-i {j} {m1} j<M m1<k eq with <-cmp i j + unique-i {j} {m1} j<M m1<k eq | tri< a ¬b ¬c = ⊥-elim ( lemma-u2 a j<M m1<k eq ) + unique-i {j} {m1} j<M m1<k eq | tri≈ ¬a b ¬c = b + unique-i {j} {m1} j<M m1<k eq | tri> ¬a ¬b c = ⊥-elim ( lemma-u1 c m1<k eq ) + lemma7 : {n m1 m A : ℕ} → n < m1 → suc (n + m * suc n + A) < suc (m1 + m * suc m1 + A) + lemma7 {n} {m1} {m} {A} n<m1 = begin + suc (suc (n + m * suc n + A)) + ≡⟨ +-assoc _ (m * suc n) A ⟩ + suc (suc n + (m * suc n + A)) + ≤⟨ s≤s (<-plus n<m1) ⟩ + suc (m1 + (m * suc n + A)) + ≡⟨ sym ( +-assoc _ (m * suc n) A) ⟩ + suc (m1 + m * suc n + A) + ≤⟨ ≤-plus {_} {_} {A} (≤-plus-0 {_} {_} {suc m1} (≤* {suc n} {suc m1} {m} (s≤s (≤to< n<m1 )))) ⟩ + suc (m1 + m * suc m1 + A) + ∎ where open ≤-Reasoning + 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 + unique-m {i} {_} {n} {m1} refl eqn eqm with <-cmp n m1 + 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 )) + unique-m {i} {_} {n} {m1} refl eqn eqm | tri≈ ¬a b ¬c = b + unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c )) + m1<sk : {m1 : ℕ} → m1 < n → n < suc k → m1 < suc k + m1<sk {m1} m1<n n<k = <-trans m1<n n<k + lemma-u3 : {j : ℕ} {m₁ : ℕ} → j < M → m₁ < n → ¬ j + suc k * M ≡ M * suc m₁ + A + lemma-u3 {j} {m1} j<M m1<n eq = nat-≡< (unique-m (sym (unique-i j<M (m1<sk m1<n (Cond1.range-n c1) ) eq)) eq (Cond1.rule1 c1)) m1<n + lemma-u4 : {j : ℕ} {m₁ : ℕ} → j < M → n < m₁ → m₁ < suc k → ¬ j + suc k * M ≡ M * suc m₁ + A + lemma-u4 {j} {m1} j<M n<m1 m<sk eq = nat-≡< (unique-m (unique-i j<M m<sk eq) (Cond1.rule1 c1) eq ) n<m1 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 + ; u3 = lemma-u3 + ; u4 = lemma-u4 } -- loop on range of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M)