Mercurial > hg > Papers > 2015 > atton-thesis
changeset 27:e30a02baba55
Fix function name
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 11 Feb 2015 12:37:46 +0900 |
| parents | de3397af1f8d |
| children | c684abcc781b |
| files | Makefile agda.tex src/nat_add_sym.agda src/nat_add_sym_reasoning.agda |
| diffstat | 4 files changed, 17 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/Makefile Tue Feb 10 15:30:01 2015 +0900 +++ b/Makefile Wed Feb 11 12:37:46 2015 +0900 @@ -15,7 +15,7 @@ .PHONY : clean all open remake clean: - rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt + rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol all: $(TARGET).pdf
--- a/agda.tex Tue Feb 10 15:30:01 2015 +0900 +++ b/agda.tex Wed Feb 11 12:37:46 2015 +0900 @@ -469,21 +469,21 @@ $ O + (S m) \equiv (S m) + O $ を証明することになる。 この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。 - $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/add_sym/ を実行することで証明できる。 + $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。 この2つの証明はこのような意味を持つ。 n が 0 であるとき、 m も 0 なら簡約により等式が成立する。 n が 0 であるとき、 m が 0 でないとき、 m は後続数である。 よって m が (S x) と書かれる時、 x は m の前の値である。 前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。 - ここで、 \verb/add_sym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 + ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 \item n = S n, m = O $ (S n) + O \equiv O + (S n) $ を証明する。 この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。 さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。 - よって \verb/add_sym/ により O と n を変換した後に cong で S を加えることで証明ができる。 + よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。 ここで、 $ O + n \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。 + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。
--- a/src/nat_add_sym.agda Tue Feb 10 15:30:01 2015 +0900 +++ b/src/nat_add_sym.agda Wed Feb 11 12:37:46 2015 +0900 @@ -5,10 +5,10 @@ module nat_add_sym where -add_sym : (n m : Nat) -> n + m ≡ m + n -add_sym O O = refl -add_sym O (S m) = cong S (add_sym O m) -add_sym (S n) O = cong S (add_sym n O) -add_sym (S n) (S m) = {!!} +addSym : (n m : Nat) -> n + m ≡ m + n +addSym O O = refl +addSym O (S m) = cong S (addSym O m) +addSym (S n) O = cong S (addSym n O) +addSym (S n) (S m) = {!!}
--- a/src/nat_add_sym_reasoning.agda Tue Feb 10 15:30:01 2015 +0900 +++ b/src/nat_add_sym_reasoning.agda Wed Feb 11 12:37:46 2015 +0900 @@ -5,17 +5,18 @@ module nat_add_sym_reasoning where -add_to_right : (n m : Nat) -> S (n + m) ≡ n + (S m) -add_to_right n m = {!!} +addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m) +addToRight O m = refl +addToRight (S n) m = cong S (addToRight n m) addSym : (n m : Nat) -> n + m ≡ m + n addSym O O = refl -addSym O (S m) = cong S (add_sym O m) -addSym (S n) O = cong S (add_sym n O) -add_sym (S n) (S m) = begin - S (n + S m) ≡⟨ cong S (add_sym n (S m)) ⟩ +addSym O (S m) = cong S (addSym O m) +addSym (S n) O = cong S (addSym n O) +addSym (S n) (S m) = begin + S (n + S m) ≡⟨ cong S (addSym n (S m)) ⟩ S (S (m + n)) ≡⟨ refl ⟩ - S ((S m) + n) ≡⟨ {!!} ⟩ + S ((S m) + n) ≡⟨ addToRight (S m) n ⟩ S (m + S n) ∎