Mercurial > hg > Members > kono > Proof > prob1
changeset 32:1e3130896834
maxA done (all 0,1,2 done)
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 31 Mar 2020 01:18:56 +0900 |
| parents | 908409975a5e |
| children | b5e8e6be9425 |
| files | nat.agda prob1.agda |
| diffstat | 2 files changed, 94 insertions(+), 31 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Mon Mar 30 20:22:04 2020 +0900 +++ b/nat.agda Tue Mar 31 01:18:56 2020 +0900 @@ -204,6 +204,69 @@ minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt +minus-assoc : {x y z : ℕ} → (x - y) - z ≡ x - (y + z) +minus-assoc {x} {zero} = refl +minus-assoc {zero} {suc y} {z} = begin + (zero - suc y) - z + ≡⟨ cong (λ k → k - z ) (minus<=0 {zero} {suc y} z≤n ) ⟩ + zero - z + ≡⟨ minus<=0 {zero} {z} z≤n ⟩ + zero + ≡⟨ sym ( minus<=0 {zero} {suc y + z} z≤n ) ⟩ + zero - (suc y + z) + ∎ where open ≡-Reasoning +minus-assoc {suc x} {suc y} = minus-assoc {x} {y} + +minus+assoc : {x y z : ℕ } → z < suc y → x + (y - z) ≡ (x + y) - z +minus+assoc {x} {y} {zero} z<y = refl +minus+assoc {x} {suc y} {suc z} (s≤s z<y) = begin + x + (suc y - suc z) + ≡⟨⟩ + x + (y - z) + ≡⟨ minus+assoc z<y ⟩ + (x + y) - z + ≡⟨⟩ + suc (x + y) - suc z + ≡⟨ cong (λ k → suc k - suc z) ( +-comm _ y ) ⟩ + suc (y + x) - suc z + ≡⟨⟩ + (suc y + x) - suc z + ≡⟨ cong (λ k → k - suc z) ( +-comm _ x ) ⟩ + (x + suc y) - suc z + ∎ where open ≡-Reasoning + +n+0≡n : {n : ℕ } → n + 0 ≡ n +n+0≡n {n} = trans (+-comm n 0) refl + +s-minus : {x y : ℕ } → x - y ≤ suc x - y +s-minus {zero} {y} = subst (λ k → k ≤ suc zero - y ) (sym (minus<=0 {zero} {y} z≤n) ) z≤n +s-minus {suc x} {zero} = s≤s refl-≤s +s-minus {suc x} {suc y} = s-minus {x} {y} + +minus-s : {x y : ℕ } → x - suc y ≤ x - y +minus-s {zero} {y} = begin + zero - suc y + ≡⟨ minus<=0 {zero} {suc y} z≤n ⟩ + zero + ≡⟨ sym (minus<=0 {zero} {y} z≤n) ⟩ + zero - y + ∎ where open ≤-Reasoning +minus-s {suc x} {y} = s-minus {x} {y} + +minus+< : {x y z : ℕ } → x - ( y + z ) ≤ x - y +minus+< {x} {y} {zero} = subst (λ k → x - k ≤ x - y ) (sym (n+0≡n {y})) ≤-refl +minus+< {x} {y} {suc z} = begin + x - (y + suc z) + ≡⟨ sym (minus-assoc {x} {y} {suc z} ) ⟩ + (x - y) - (suc z) + ≤⟨ minus-s {x - y} ⟩ + (x - y) - z + ≡⟨ minus-assoc {x} {y} {z} ⟩ + x - (y + z) + ≤⟨ minus+< {x} {y} {z} ⟩ + x - y + ∎ where open ≤-Reasoning + distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) distr-minus-* {x} {zero} {z} = refl distr-minus-* {x} {suc y} {z} with <-cmp x y @@ -247,28 +310,7 @@ lt {x} {y} {z} le = *≤ le minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z) -minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin - minus (minus x y) z + z - ≡⟨ minus+n {_} {z} lemma ⟩ - minus x y - ≡⟨ +m= {_} {_} {y} ( begin - minus x y + y - ≡⟨ minus+n {_} {y} lemma1 ⟩ - x - ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ - minus x (z + y) + (z + y) - ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ - minus x (z + y) + z + y - ∎ ) ⟩ - minus x (z + y) + z - ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ - minus x (y + z) + z - ∎ ) where - open ≡-Reasoning - lemma1 : suc x > y - lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt ) - lemma : suc (minus x y) > z - lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt ) +minus- {x} {y} {z} gt = minus-assoc {x} {y} {z} minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M minus-* {zero} {k} {n} lt = begin
--- a/prob1.agda Mon Mar 30 20:22:04 2020 +0900 +++ b/prob1.agda Tue Mar 31 01:18:56 2020 +0900 @@ -135,17 +135,31 @@ 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 + lemmab : {x m : ℕ } → x < suc (m + x) + lemmab {x} {zero} = a<sa + lemmab {zero} {suc m} = <to<s (lemmab {zero} {m}) + lemmab {suc x} {suc m} = ( s≤s (subst (λ k → suc x ≤ k) (+-comm _ (suc m)) x≤x+y )) + lemmaa : {x y : ℕ} → suc x > y → (suc x - y) + y ≡ suc ( (x - y) + y ) + lemmaa {x} {y} lt = begin + (suc x - y) + y + ≡⟨ minus+n (<-trans lt a<sa ) ⟩ + suc x + ≡⟨ sym ( cong (λ k → suc k) ( minus+n {x} {y} lt ) ) ⟩ + suc (x - y) + y + ≡⟨⟩ + suc ( (x - y) + y ) + ∎ where open ≡-Reasoning -- 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 with <-cmp (suc A) ( (k - n) * M ) + lemma8 i<M | tri< a ¬b ¬c = <-minus-0 {A} {_} {suc zero} ( <-trans a (<to<s lemmab) ) + lemma8 i<M | tri≈ ¬a b ¬c = <-minus-0 {A} {_} {suc zero} (subst (λ h → h < 1 + suc (m + minus k n * suc m)) (sym b) (<to<s lemmab)) where 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 - ≡⟨ {!!} ⟩ + ≡⟨ sym ( minus+n {suc A} {(k - n) * M} (<-trans c a<sa) ) ⟩ + (suc A - ((k - n) * M)) + ((k - n) * M ) + ≡⟨ lemmaa {A} {(k - n) * M} c ⟩ suc ( (A - ((k - n) * M)) + ((k - n) * M) ) ≤⟨ ≤-plus i<M ⟩ M + ((k - n) * M) @@ -154,6 +168,11 @@ lemma9 {zero} {zero} () lemma9 {suc x} {zero} () lemma9 {x} {suc y} (s≤s lt) = lt + lemmad : {n k m : ℕ} → n < suc k → n * suc m < suc ( k * suc m ) + lemmad {n} {k} {m} n<k with <-cmp n k + lemmad {n} {k} {m} n<k | tri< a ¬b ¬c = <-trans ( *< a ) a<sa + lemmad {n} {k} {m} n<k | tri≈ ¬a refl ¬c = ≤-refl + lemmad {n} {k} {m} n<k | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n<k (s≤s c) ) maxA : A - ((k - n) * M) < M → A ≤ (suc k * M ) - 1 maxA i<M = begin A @@ -161,13 +180,15 @@ (M + ((k - n) * M)) - 1 ≡⟨ cong (λ k → (M + k ) - 1 ) (distr-minus-* {k} {n} {M} ) ⟩ (M + ((k * M) - ( n * M))) - 1 - ≡⟨ {!!} ⟩ + ≡⟨ cong (λ k → k - 1 ) ( minus+assoc {M} {k * M} {n * M} (lemmad n<k)) ⟩ ((M + (k * M) )- ( n * M)) - 1 ≡⟨⟩ ((suc k * M )- ( n * M)) - 1 - ≡⟨ {!!} ⟩ + ≡⟨ minus-assoc {suc k * M} {n * M} {1} ⟩ (suc k * M) - ((n * M) + 1) - ≤⟨ {!!} ⟩ + ≡⟨ cong (λ h → (suc k * M) - h ) (+-comm (n * M) _) ⟩ + (suc k * M) - (1 + (n * M) ) + ≤⟨ minus+< {suc k * M} {1} {n * M} ⟩ (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 }