Mercurial > hg > Papers > 2015 > atton-thesis
diff agda.tex @ 27:e30a02baba55
Fix function name
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 11 Feb 2015 12:37:46 +0900 (2015-02-11) |
parents | de3397af1f8d |
children | c684abcc781b |
line wrap: on
line diff
--- 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 を右側の項への移すだけであるため、右側の項への演算はしない。