Mercurial > hg > Papers > 2015 > atton-thesis
comparison agda.tex @ 28:c684abcc781b
Add agda-resoning
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 11 Feb 2015 13:12:38 +0900 |
| parents | e30a02baba55 |
| children | 2ff5acb0d2e9 |
comparison
equal
deleted
inserted
replaced
| 27:e30a02baba55 | 28:c684abcc781b |
|---|---|
| 359 \verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。 | 359 \verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。 |
| 360 そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。 | 360 そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。 |
| 361 | 361 |
| 362 % }}} | 362 % }}} |
| 363 | 363 |
| 364 % {{{ Reasoning | |
| 365 | |
| 364 \section{Reasoning} | 366 \section{Reasoning} |
| 365 \label{section:reasoning} | 367 \label{section:reasoning} |
| 366 \ref{section:agda} 節ではAgdaにおける証明の手法について解説した。 | 368 \ref{section:agda} 節ではAgdaにおける証明の手法について解説した。 |
| 367 \ref{section:reasoning}節では Agda における証明の例として、自然数の加法の交換法則を証明する。 | 369 \ref{section:reasoning}節では Agda における証明の例として、自然数の加法の交換法則を証明する。 |
| 368 | 370 |
| 494 \end{itemize} | 496 \end{itemize} |
| 495 | 497 |
| 496 3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。 | 498 3 つのパターンにおいては refl や cong といった単純な項で証明を行なうことができた。 |
| 497 しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。 | 499 しかし長い証明になると refl や cong といった式を trans で大量に繋げていく必要性がある。 |
| 498 長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。 | 500 長い証明を分かりやすく記述するために $ \equiv $-Reasoning を用いる。 |
| 501 | |
| 502 $ \equiv $-Reasoning では等式の左辺を begin の後に記述し、等式の変形を $ \equiv \langle expression \rangle $ に記述することで変形していく。 | |
| 503 最終的に等式の左辺を $ \blacksquare $ の項へと変形することで等式の証明が得られる。 | |
| 504 | |
| 505 自然数の加法の交換法則を $ \equiv $-Reasoning を用いて証明した例がリスト\ref{src:nat_add_sym_reasoning}である。 | |
| 506 特に n と m が1以上である時の証明に注目する。 | |
| 507 | |
| 508 % TODO: FIXME: unicode char | |
| 509 \begin{table}[html] | |
| 510 \lstinputlisting[label=src:nat_add_sym_reasoning, caption= $ \equiv $ - Reasoning を用いた証明の例] {src/nat_add_sym_reasoning.agda} | |
| 511 \end{table} | |
| 512 | |
| 513 まず \verb/ (S n) + (S m)/ は + の定義により \verb/ S (n + (S m)) / に等しい。 | |
| 514 よって refl で導かれる。 | |
| 515 なお、基本的に定義などで同じ項に簡約される時は refl によって記述することが多い。 | |
| 516 | |
| 517 次に \verb/S (n + (S m)) / に対して addSym を用いて交換し、 cong によって S を追加することで \verb/ S ((S m) + n) / を得る。 | |
| 518 これは、前3パターンにおいて + の右辺の項が 1以上であっても上手く交換法則が定義できたことを利用して項を変形している。 | |
| 519 このように同じ法則の中でも、違うパターンで証明できた部分を用いて別パターンの証明を行なうこともある。 | |
| 520 | |
| 521 最後に \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得なくてはならない。 | |
| 522 しかし、 + の定義には右辺に対して S を移動する演算が含まれていない。 | |
| 523 よってこのままでは証明することができない。 | |
| 524 そのため、等式 $ S (m + n) \equiv m + (S n) $ を addToRight として定義する。 | |
| 525 addToRight の証明の解説は省略する。 | |
| 526 addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。 | |
| 527 これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $ の証明が完了した。 | |
| 528 | |
| 529 自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。 | |
| 530 また、定義した + の演算のみでは加法の交換法則は証明できず、さらに等式を証明する必要があった。 | |
| 531 | |
| 532 このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。 | |
| 533 | |
| 534 % }}} |