Mercurial > hg > Papers > 2020 > ryokka-master
comparison paper/agda.tex @ 7:8ef64db63497
fix agda.tex
| author | ryokka |
|---|---|
| date | Thu, 06 Feb 2020 19:24:32 +0900 |
| parents | d30593612a38 |
| children | b8ff2bd1a5af |
comparison
equal
deleted
inserted
replaced
| 6:d30593612a38 | 7:8ef64db63497 |
|---|---|
| 1 \chapter{Agda} | 1 \chapter{定理証明支援系言語 Agda} |
| 2 \label{c:agda} | 2 \label{c:agda} |
| 3 Agda \cite{agda} とは定理証明支援器であり、関数型言語である。 | 3 Agda \cite{agda} とは定理証明支援器であり、関数型言語である。 |
| 4 Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱うことが可能である。 | 4 Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱うことが可能である。 |
| 5 また、型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため | 5 また、型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため |
| 6 Agda では記述したプログラムを証明することができる。 | 6 Agda では記述したプログラムを証明することができる。 |
| 7 | 7 |
| 8 本章では Agda で証明をするために必要な要素を示し。 | 8 本章では Agda で証明をするために必要な要素を示し。 |
| 9 また、Agda での証明について説明する。 | 9 また、Agda での証明について説明する。 |
| 10 | 10 |
| 11 \section{Agda の文法} | 11 \section{関数型言語としての Agda} |
| 12 | 12 Agda \cite{agda} は純粋関数型言語である。 |
| 13 Agdaはインデントが意味を持ち、スペースの有無もチェックされる。 | 13 Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。 |
| 14 コメントは \verb/-- comment/ や \verb/{-- comment --}/ のように記述される。 | 14 |
| 15 | 15 Agda の記述ではインデントが |
| 16 Agda のプログラムは全てモジュール内部に記述されるため、各ファイルのトップレベルにモ | 16 意味を持ち、スペースの有無もチェックされる。 |
| 17 ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一である。 | 17 コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。 |
| 18 | 18 また、\verb/_/でそこに入りうるすべての値を示すことができ、 |
| 19 通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。 | 19 \verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。 |
| 20 | |
| 21 Agda のプログラムは全てモジュール内部に記述される。 | |
| 22 そのため、各ファイルのトップレベルにモジュールを定義する必要がある。 | |
| 23 トップレベルのモジュールはファイル名と同一になる。 | |
| 24 | |
| 25 モジュール内で異なるモジュールをインポートする時は \verb/import/ キーワードを指定する。 | |
| 20 インポートを行なう際、モジュール内部の関数を別名に変更するには \verb/as/ キーワードを用いる。 | 26 インポートを行なう際、モジュール内部の関数を別名に変更するには \verb/as/ キーワードを用いる。 |
| 21 他にも、モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワード、 | 27 他にも、モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワード、 |
| 22 関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠 | 28 関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠 |
| 23 す場合は \verb/hiding/ キーワードを用いる。 | 29 す場合は \verb/hiding/ キーワードを用いる。 |
| 24 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open import/ キーワードを使うことで展開できる。 | 30 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open import/ キーワードを使うことで展開できる。 |
| 25 モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。 | 31 モジュールをインポートする例を\coderef{src:agda-import}に示す。 |
| 26 | 32 |
| 27 \lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda.replaced} | 33 \lstinputlisting[label=src:agda-import, caption=モジュールのインポートとオプション] {src/AgdaImport.agda.replaced} |
| 28 | 34 |
| 29 | 35 |
| 30 \section{Agda のデータ} | 36 \section{Agda のデータ} |
| 31 Agda における型指定は : を用いて行う。 変数 x が型 A を持つ、ということを表すには x : A と記述する。 | 37 Agda 型をデータや関数に記述する必要がある。 |
| 32 データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。 | 38 Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。 |
| 33 data キーワードの後に data の名前と、型、 where 句を書きインデントを深くした後、 | 39 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 |
| 40 \verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、 | |
| 34 値にコンストラクタとその型を列挙する。 | 41 値にコンストラクタとその型を列挙する。 |
| 35 | 42 |
| 36 例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。 | 43 \coderef{src:agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。 |
| 37 Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。 | 44 |
| 38 Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 | 45 \lstinputlisting[label=src:agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced} |
| 39 Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く | 46 |
| 40 | 47 \verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。 |
| 41 \lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda.replaced} | 48 \verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、 |
| 42 | 49 \verb/suc/ を連ねることで自然数全体を表現することができる。 |
| 43 | 50 |
| 44 Agda には C における構造体に相当するレコード型というデータも存在する、 | 51 $\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 |
| 45 例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。 | 52 \verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。 |
| 46 レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。 | 53 %% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。 |
| 47 複数の値を列挙する際は \verb/;/ で区切る。 | 54 |
| 48 | 55 Agda には C 言語における構造体に相当するレコード型というデータも存在する、 |
| 56 例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{src:agda-record}のようになる。 | |
| 49 \lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced} | 57 \lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced} |
| 58 レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。 | |
| 59 複数の値を列挙するには \verb/;/ で区切る必要がある。 | |
| 50 | 60 |
| 51 | 61 |
| 52 \section{Agda の関数} | 62 \section{Agda の関数} |
| 53 | 63 Agda での関数は型の定義と、関数の定義をする必要がある。 |
| 54 Agda での関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。 | 64 関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力返す型として記述される。$\rightarrow$ 、 または\verb/→/ を用いて \verb/input → output/ のように記述される。 |
| 55 関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。 | 65 関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。 |
| 56 | 66 |
| 57 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書くことができる。 | 67 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。 |
| 58 また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この | 68 また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。 |
| 59 時の型は \verb/A -> (A -> B)/のように考えられる。 | 69 この時の型は \verb/A → (A → B)/のように考えられる。 |
| 60 Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 | 70 %% 変数 \verb/x/ を取って true を返す関数 \verb/f/は\tabref{src:agda-function}のようになる。 |
| 61 | 71 例として任意の自然数$mathbb{N}$を受け取り、\verb/+1/した値を返す関数は\coderef{src:agda-function}のように定義できる。 |
| 62 \lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced} | 72 \lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} |
| 73 | |
| 63 | 74 |
| 64 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 | 75 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 |
| 65 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので | 76 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 |
| 66 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。 | 77 例として自然数$mathbb{N}$の加算を関数で書くと\coderef{agda-plus}のようになる。 |
| 67 | 78 |
| 68 \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} | 79 \lstinputlisting[label=src:agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced} |
| 69 | 80 %% \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} |
| 70 パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。 | 81 \verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味する。 |
| 71 例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。 | 82 |
| 72 なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 | 83 パターンマッチでは全てのコンストラクタのパターンを含む必要がある。 |
| 73 例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。 | 84 例えば、自然数$mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。 |
| 74 なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。 | 85 なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。 |
| 75 | 86 例えば\coderef{src:agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。 |
| 76 \lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda.replaced} | 87 |
| 77 | 88 |
| 78 Agda にはラムダ計算が存在している。ラムダ計算とは関数内で生成できる無名の関数であり、 | 89 \lstinputlisting[label=src:agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} |
| 79 \verb/\arg1 arg2 -> function body/ のように書くことができる。 | 90 |
| 80 例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ計算で書くとリスト~\ref{src:agda-lambda}のようになる。 | 91 Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、 |
| 81 関数 \verb/not-apply/ をラムダ計算を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。 | 92 \verb/\arg1 arg2 → function/ のように書くことができる。 |
| 93 \coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{src:agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。 | |
| 82 | 94 |
| 83 \lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} | 95 \lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} |
| 84 | 96 |
| 85 Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 | 97 Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 |
| 86 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 | 98 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 |
| 90 | 102 |
| 91 \lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} | 103 \lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} |
| 92 | 104 |
| 93 | 105 |
| 94 \section{定理証明支援器としての Agda} | 106 \section{定理証明支援器としての Agda} |
| 95 Agda での証明では型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明が完成する。 | 107 Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。 |
| 96 証明の例として Code \ref{proof} を見る。 | 108 証明の例として Code \coderef{proof} を見る。 |
| 97 ここでの $+zero$ は右から zero を足しても $\equiv$ の両辺は等しいことを証明している。 | 109 ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。 |
| 98 これは、引数として受けている y が Nat なので、 zero の時と suc y の二つの場合を証明する必要がある。 | 110 これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。 |
| 99 | 111 |
| 100 $y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。 | 112 \verb/y = zero/ の時は両辺が \verb/zero/ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。 |
| 101 $y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$ | 113 \verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという \verb/cong/ を使って、y の値を 1 減らしたのちに再帰的に \verb/+zero y/ |
| 102 を用いて証明している。 | 114 を用いて証明している。 |
| 103 | 115 |
| 104 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} | 116 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} |
| 105 %% \begin{lstlisting}[caption=等式変形の例,label=proof] | 117 %% \begin{lstlisting}[caption=等式変形の例,label=proof] |
| 106 %% +zero : { y : ℕ } → y + zero ≡ y | 118 %% +zero : { y : ℕ } → y + zero ≡ y |
| 107 %% +zero {zero} = refl | 119 %% +zero {zero} = refl |
| 108 %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) | 120 %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) |
| 109 %% \end{lstlisting} | 121 %% \end{lstlisting} |
| 110 | 122 |
| 111 また、他にも $\lambda$ 項部分で等式を変形する構文が存在している。 | 123 また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。 |
| 112 Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。 | 124 ここでは \verb/rewrite/ と $\equiv$\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。 |
| 113 始めに等式変形を始めたいところで $let open \equiv-Reasoning in begin$と記述する。 | 125 |
| 114 Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。 | 126 \verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。 |
| 115 $--$ は Agda 上ではコメントである。 | 127 \coderef{agda-rewrite} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。 |
| 116 | 128 ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。 |
| 117 \lstinputlisting[caption=等式変形の例1/2,label=agda-term-pre]{src/term1.agda.replaced} | 129 |
| 130 \lstinputlisting[caption=rewrite での等式変形の例,label=agda-rewrite]{src/agda-rewrite.agda.replaced} | |
| 131 | |
| 132 \coderef{agda-term-pre}、\coderef{agda-term-mid}、 \coderef{agda-term-post} は$\equiv$\verb/-Reasoning/を用いた等式変形の流れである。 | |
| 133 始めに等式変形を始めたいところで \verb/let open/ $\equiv$ \verb/-Reasoning in begin/と記述し、 | |
| 134 \verb/変形前/ $\equiv$ $\langle$ \verb/変形規則/ $\rangle$ \verb/変形後/ の形で記述して、 | |
| 135 最後に $\blacksquare$ をつけて変形を終える。 | |
| 136 この \verb/let open/ から $\blacksquare$ までの流れは1行で記述しても良いし、改行やインデントを含めても良い。 | |
| 137 \coderef{agda-term-pre}の例では分からないところを \verb/?/ と置いておき、 | |
| 138 \verb/?/ の中で示されている値は下にコメントで示しておく。 | |
| 139 | |
| 140 \lstinputlisting[caption=等式変形の例1/3,label=agda-term-pre]{src/agda-term1.agda.replaced} | |
| 118 %% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre] | 141 %% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre] |
| 119 %% stmt2Cond : {c10 : ℕ} → Cond | 142 %% +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) |
| 120 %% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) | 143 %% +-suc {zero} {y} = refl |
| 121 | 144 %% +-suc {suc x} {y} = cong suc (+-suc {x} {y}) |
| 122 %% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ | 145 |
| 123 %% 10}) | 146 %% +-comm : (x y : ℕ) → x + y ≡ y + x |
| 124 %% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in | 147 %% +-comm zero y rewrite (+zero {y}) = refl |
| 148 %% +-comm (suc x) y = let open ≡-Reasoning in | |
| 125 %% begin | 149 %% begin |
| 126 %% ? -- ?0 | 150 %% ?0 ≡⟨ ?1 ⟩ |
| 127 %% ≡⟨ ? ⟩ -- ?1 | 151 %% ?2 ∎ |
| 128 %% ? -- ?2 | 152 |
| 129 %% ∎ ) | 153 %% -- ?0 : (suc x) + y |
| 130 | 154 %% -- ?1 : suc x + y ≡ y + suc x |
| 131 %% -- ?0 : Bool | 155 %% -- ?2 : y + (suc x) |
| 132 %% -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true | |
| 133 %% -- ?2 : Bool | |
| 134 %% \end{lstlisting} | 156 %% \end{lstlisting} |
| 135 | 157 |
| 136 この状態で実行すると ? 部分に入る型を Agda が示してくれる。 | 158 この状態で実行すると \verb/?/ 部分に入る型を Agda が示してくれる。 |
| 137 始めに変形する等式を ?0 に記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。 | 159 始めに変形する等式を ?0 に記述し、?1 の中に変形規則を使用することで等式を変形できる。 |
| 138 | 160 ここでの方針は \verb/(suc x) + y/ を \verb/suc (x + y)/ 変形してやり、 |
| 139 ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。 | 161 \verb/y + (suc x)/ も同様に \verb/ suc (x + y)/ の形に変形することで等しさを証明する。 |
| 140 \lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced} | 162 Agda の加算では左側に \verb/suc/ がついていた場合外に \verb/suc/ を出して再帰的に中身と足し算を行うため、 |
| 163 何もせずに \verb/(suc x) + y/ は \verb/suc (x + y)/ に変換できる。 | |
| 164 \coderef{agda-term-mid} では \verb/suc (x + y)/ に対して \verb/cong/ で \verb/suc/ を外に出し \verb/+comm/ を再帰的に利用することで \verb/suc (y + x)/ へ変換している。 | |
| 165 | |
| 166 \lstinputlisting[caption=等式変形の例2/3,label=agda-term-mid]{src/agda-term2.agda.replaced} | |
| 141 %% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid] | 167 %% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid] |
| 142 %% ∧true : { x : Bool } → x ∧ true ≡ x | 168 %% +-comm : (x y : ℕ) → x + y ≡ y + x |
| 143 %% ∧true {x} with x | 169 %% +-comm zero y rewrite (+zero {y}) = refl |
| 144 %% ∧true {x} | false = refl | 170 %% +-comm (suc x) y = let open ≡-Reasoning in |
| 145 %% ∧true {x} | true = refl | 171 %% begin |
| 146 | 172 %% (suc x) + y ≡⟨⟩ |
| 147 %% stmt1Cond : {c10 : ℕ} → Cond | 173 %% suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ |
| 148 %% stmt1Cond {c10} env = Equal (varn env) c10 | 174 %% suc (y + x) ≡⟨ ?0 ⟩ |
| 175 %% ?1 ∎ | |
| 176 | |
| 177 %% -- ?0 : suc (y + x) ≡ y + suc x | |
| 178 %% -- ?1 : y + suc x | |
| 179 | |
| 149 %% \end{lstlisting} | 180 %% \end{lstlisting} |
| 150 | 181 |
| 151 最終的な証明は\ref{agda-term-post} のようになる。 | 182 |
| 152 \lstinputlisting[caption=等式変形の例2/2,label=agda-term-post]{src/term3.agda.replaced} | 183 |
| 184 \coderef{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。 | |
| 185 これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。 | |
| 186 \lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced} | |
| 153 %% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post] | 187 %% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post] |
| 154 %% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ | 188 %% +-comm : (x y : ℕ) → x + y ≡ y + x |
| 155 %% 10}) | 189 %% +-comm zero y rewrite (+zero {y}) = refl |
| 156 %% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in | 190 %% +-comm (suc x) y = let open ≡-Reasoning in |
| 157 %% begin | 191 %% begin |
| 158 %% (Equal (varn env) c10 ) ∧ true | 192 %% suc (x + y) ≡⟨⟩ |
| 159 %% ≡⟨ ∧true ⟩ | 193 %% suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ |
| 160 %% Equal (varn env) c10 | 194 %% suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ |
| 161 %% ≡⟨ cond ⟩ | 195 %% y + suc x ∎ |
| 162 %% true | 196 |
| 163 %% ∎ ) | 197 %% -- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) |
| 198 %% -- +-suc {zero} {y} = refl | |
| 199 %% -- +-suc {suc x} {y} = cong suc (+-suc {x} {y}) | |
| 164 %% \end{lstlisting} | 200 %% \end{lstlisting} |
| 165 | 201 Agda ではこのような形で等式を変形しながら証明を行う事ができる。 |
| 166 | 202 |
| 203 %% 例として先程の \verb/+-comm/ を rewrite で証明した \verb/rewrite-+-comm/ を \coderef{agda-rewrite} を載せる。 | |
| 204 |