Mercurial > hg > Members > atton > agda > systemT
changeset 9:8ad92d830679
Proof left-mult-distr-one. but has yellow
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 22 May 2014 21:53:48 +0900 |
| parents | e191792472f8 |
| children | c01d31399879 |
| files | int.agda |
| diffstat | 1 files changed, 14 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/int.agda Wed May 21 21:11:34 2014 +0900 +++ b/int.agda Thu May 22 21:53:48 2014 +0900 @@ -18,6 +18,9 @@ left-add-zero O = refl left-add-zero (S n) = cong S (left-add-zero n) +left-add-one : (n : Int) -> (S n) ≡ S O + n +left-add-one O = refl +left-add-one (S n) = cong S (left-add-one n) left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) left-increment n O = refl @@ -118,7 +121,17 @@ (S (S n)) + ((S (S n)) * m) ≡⟨ cong (\x -> (S (S n)) + x) (left-mult-distr-one (S n) m) ⟩ S (S n) + (m + S n * m) - ≡⟨ {!!} ⟩ + ≡⟨ cong (\x -> x + (m + S n * m)) (left-add-one (S n)) ⟩ + (S O) + (S n) + (m + S n * m) + ≡⟨ sum-assoc ((S O) + (S n)) m (S n * m) ⟩ + (S O) + (S n) + m + S n * m + ≡⟨ cong (\x -> x + m + S n * m) (sum-sym (S O) (S n)) ⟩ + (S n) + (S O) + m + S n * m + ≡⟨ cong (\x -> (S n) + x + (S n * m)) refl ⟩ + (S n) + (S m) + S n * m + ≡⟨ cong (\x -> x + S n * m) (sum-sym (S n) (S m)) ⟩ + (S m) + (S n) + S n * m + ≡⟨ cong (\x -> (S m + x)) refl ⟩ S m + S n * S m ∎