Mercurial > hg > Papers > 2015 > atton-thesis

comparison agda.tex @ 27:e30a02baba55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
26:de3397af1f8d 27:e30a02baba55
467 467
468 \item n = O, m = S m 468 \item n = O, m = S m
469 469
470 $ O + (S m) \equiv (S m) + O $ を証明することになる。 470 $ O + (S m) \equiv (S m) + O $ を証明することになる。
471 この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。 471 この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
472 $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/add_sym/ を実行することで証明できる。 472 $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。
473 473
474 この2つの証明はこのような意味を持つ。 474 この2つの証明はこのような意味を持つ。
475 n が 0 であるとき、 m も 0 なら簡約により等式が成立する。 475 n が 0 であるとき、 m も 0 なら簡約により等式が成立する。
476 n が 0 であるとき、 m が 0 でないとき、 m は後続数である。 476 n が 0 であるとき、 m が 0 でないとき、 m は後続数である。
477 よって m が (S x) と書かれる時、 x は m の前の値である。 477 よって m が (S x) と書かれる時、 x は m の前の値である。
478 前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。 478 前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。
479 ここで、 \verb/add_sym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 479 ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。
480 480
481 \item n = S n, m = O 481 \item n = S n, m = O
482 482
483 $ (S n) + O \equiv O + (S n) $ を証明する。 483 $ (S n) + O \equiv O + (S n) $ を証明する。
484 この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。 484 この等式は + の定義により $ S (n + O) \equiv (S n) $ と変形できる。
485 さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。 485 さらに変形すれば $ S (n + O) \equiv S (O + n) $ となる。
486 よって \verb/add_sym/ により O と n を変換した後に cong で S を加えることで証明ができる。 486 よって \verb/addSym/ により O と n を変換した後に cong で S を加えることで証明ができる。
487 487
488 ここで、 $ O + n \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。 488 ここで、 $ O + n \equiv n $ は + の定義により自明であるが、$ n + O \equiv n $ をそのまま導出できないことに注意して欲しい。
489 + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。 489 + の定義は左側の項から S を右側の項への移すだけであるため、右側の項への演算はしない。
490 490
491 \item n = S n, m = S m 491 \item n = S n, m = S m