Mercurial > hg > Members > kono > Proof > prob1
changeset 10:c0d3c5a821dd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 26 Nov 2019 14:44:34 +0900 |
| parents | e0811846b265 |
| children | ee2309eb1f5d |
| files | prob1.agda |
| diffstat | 1 files changed, 14 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/prob1.agda Tue Nov 26 12:42:13 2019 +0900 +++ b/prob1.agda Tue Nov 26 14:44:34 2019 +0900 @@ -71,24 +71,29 @@ distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) distr-minus-* = {!!} -minus- : {x y z : ℕ } → minus (minus x y) z ≡ minus x (y + z) -minus- {x} {y} {z} = +m= {_} {_} {z} ( begin +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} {!!} ⟩ minus x y ≡⟨ +m= {_} {_} {y} ( begin minus x y + y - ≡⟨ {!!} ⟩ + ≡⟨ minus+n {_} {y} {!!} ⟩ 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 + ∎ ) where + open ≡-Reasoning + lemma : suc (minus x y) > z + lemma = <-minus {_} {_} {y} ? + lemma1 : suc x > y + lemma1 = {!!} minus-* : {M k n : ℕ } → minus k (suc n) * M ≡ minus (minus k n * M ) M minus-* {M} {k} {n} = begin @@ -99,7 +104,7 @@ minus (k * M ) (M + n * M ) ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩ minus (k * M ) ((n * M) + M ) - ≡⟨ sym ( minus- {k * M} {n * M} ) ⟩ + ≡⟨ sym ( minus- {k * M} {n * M} {!!} ) ⟩ minus (minus (k * M ) (n * M)) M ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩ minus (minus k n * M ) M