\chapter{定理証明支援器 Agda での証明}

型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
。
型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。


本章では Agda で証明をするために必要な要素について説明し、Natural Deduction での証明とそれに対応して Agda 使って証明ができることを示す。
% 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。
% 依存型という表現力の高い型を持つ証明支援系 Agda を用いて型システムで証明が行える
% ことを示す。

%% ここではAgdaの文法に触るだけにとどめて Agdaと証明のchapを一つ追加。
% 其処に自然証明とAgdaの証明とかCurry-Howard対応の話とかを入れるときれいになるか
% も
%% 依存型を持っている言語には Agda の他に ATS 、 Coq 、 F* 、 Idris 、 Shen など
%% がある。

\section{Agda の文法}


Agda はインデントに意味を持つため、きちんと揃える必要がある。
また、スペースの有無は厳格にチェックされる。
なお、 \verb/--/ の後はコメントである。

Agda のプログラムでは全てモジュール内部に記述されるため、まずはトップレベルにモ
ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一になる。

通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。
また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。
モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードの後に
関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠
す場合は \verb/hiding/ キーワードを用いる。
なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/opestack に対する操作を定義しており、n/ キーワードを使うことで展開できる。
モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。

\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda}

% また、モジュールには値を渡すことができる。
% そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。
% 例えば、要素の型と比較する二項演算子を使って並べ替えをするモジュール\verb/Sort/ を考える。
% そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。
% \verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。

% \lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda}

Agda における型指定は $:$ を用いて行う。

例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。

データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
\verb/data/キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。
Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。
Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く。

% 含有関係と言ったほうが正しそうでは。。。？集合の集合って考えたらまあ階層なんだ
% けどさ

\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}


関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。

例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書
ける。
また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この
時の型は \verb/A -> (A -> B)/のように考えられる。
Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。

\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda}

引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。

\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}

パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。

\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}

Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、
\verb/\arg1 arg2 -> function body/ のように書くことができる。
例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。
関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。

\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}

Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。
これは \verb/f'/ と同様の動作をする。
\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。

\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}

データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。
自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。

\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}

自然数に対する演算は再帰関数として定義できる。
例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。

この二項演算子は中置関数として振る舞う。
前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくと、関数を呼ぶ
時にあたかも前置や後置演算子のように振る舞うことができる。
例えば \verb/!_/ を定義すると \verb/! true/ のように利用でき、\verb/_~/ を定義すると \verb/false ~/ のように利用できる。

また、Agda は再帰関数が停止するかを判別できる。
この加算の二項演算子は左側がゼロに対しては明らかに停止する。
左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。

\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}

次に依存型について見ていく。
依存型で最も基本的なものは関数型である。
依存型を利用した関数は引数の型に依存して返す型を決定できる。
なお、依存型の解決はモジュールのインポート時に行なわれる。

Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つ x を受け取り、Bを返す。
ここで B の中で x を扱っても良い。
例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。

\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}

この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。

多相の恒等関数では型を明示的に指定せずとも \verb/zero/ に適用した場合の型は自明に \verb/Nat -> Nat/である。
Agda はこのような推論をサポートしており、推論可能な引数は省略できる。
推論によって解決される引数を暗黙的な引数(implicit arguments) と言い、変数を
\verb/{}/ でくくることで表す。

例えば、\verb/identitiy/ の対象とする型\verb/A/を暗黙的な引数として省略するとリスト~\ref{src:agda-implicit-id}のようになる。
この恒等関数を利用する際は特定の型に属する値を渡すだけでその型が自動的に推論される。
よって関数を利用する際は \verb/id-zero/ のように型を省略して良い。
なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。

\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}

Agda のデータには C における構造体に相当するレコード型も存在する。
定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。
レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
複数の値を列挙する際は \verb/;/ で区切る。

\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}

構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。
なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。
レコード内の値は \verb/record oldRecord {field = value ; ... }/ という構文を利用し更新することができる。
Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。

\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}

% Agda における部分型のように振る舞う機能として Instance Arguments が存在する。
% これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。
% Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。
% 例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。
% 具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。

% \lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda}

% ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
% Nat 型が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。

% \lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}

% これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。
% 例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。
% 部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。
% なお、名前部分は必須である。
% 仮に変数として受けても利用しない場合は \verb/_/ で捨てると良い。
% 部分型として登録した record は関数本体において \verb/{{variableName}}/ という構文で変数に束縛できる。

% \lstinputlisting[label=src:agda-use-instance, caption=Agdaにおける部分型を使う関数の定義] {src/AgdaElem.agda}

% この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。
% Nat型の要素を持つリストの内部に4が含まれるか確認している。
% この \verb/listHas4/ は \verb/true/ に評価される。

% \lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda}

\section{Natural Deduction}
% Natural Deduction のお話。細かい規則は…書かなきゃいけないよね…
% いらない規則は省略しようと、少なくとも3段論法を証明できるだけ置く。。。？
% とりあえず証明に使えるやつは全部書いて必要あるやつを詳しく。

Natural Deduction (自然演繹)は Gentzen によって作られた論理及びその証明システムである。
% ~\cite{Girard:1989:PT:64805}。
命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。

Natural Deduction では次のように

\begin{eqnarray}
    \vdots \\ \nonumber
    A \\ \nonumber
\end{eqnarray}

と書いた時、命題Aを証明したことを意味する。証明は木構造で表わされ、葉の命題は仮
定となる。

\begin{eqnarray}
    \label{exp:a_implies_b}
    A \\ \nonumber
    \vdots \\ \nonumber
    B \\ \nonumber
\end{eqnarray}

式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。
この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。

ここで、推論規則により記号 $ \Rightarrow $ を導入する。

\begin{prooftree}
    \AxiomC{[$ A $]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \Rightarrow \mathcal{I} $}
    \UnaryInfC{$ A \Rightarrow B $}
\end{prooftree}

$ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。

alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
それを踏まえ、 natural deduction には以下のような規則が存在する。

\begin{itemize}
    \item Hypothesis

        仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。

        $ A $

    \item Introductions

        導入。証明された論理式に対して記号を導入することで新たな証明を導く。


\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A $ }
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \land \mathcal{I} $}
    \BinaryInfC{$ A \land B $}
  \end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A $ }
    \RightLabel{ $ \lor 1 \mathcal{I} $}
    \UnaryInfC{$ A \lor B $}
  \end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \lor 2 \mathcal{I} $}
    \UnaryInfC{$ A \lor B $}
  \end{prooftree}

\begin{prooftree}
    \AxiomC{[$ A $]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ B $ }
    \RightLabel{ $ \Rightarrow \mathcal{I} $}
    \UnaryInfC{$ A \Rightarrow B $}
  \end{prooftree}

\item Eliminations

    除去。ある論理記号で構成された証明から別の証明を導く。

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \land B $ }
    \RightLabel{ $ \land 1 \mathcal{E} $}
    \UnaryInfC{$ A $}
  \end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \land B $ }
    \RightLabel{ $ \land 2 \mathcal{E} $}
    \UnaryInfC{$ B $}
  \end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \lor B $ }

    \AxiomC{[$A$]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ C $ }

    \AxiomC{[$B$]}
    \noLine
    \UnaryInfC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ C $ }

    \RightLabel{ $ \lor \mathcal{E} $}
    \TrinaryInfC{ $ C $ }
  \end{prooftree}

\begin{prooftree}
    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A $ }

    \AxiomC{ $ \vdots $}
    \noLine
    \UnaryInfC{ $ A \Rightarrow B $ }

    \RightLabel{ $ \Rightarrow \mathcal{E} $}
    \BinaryInfC{$ B $}
  \end{prooftree}
  
\end{itemize}

記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。
natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。

それぞれの記号は以下のような意味を持つ
\begin{itemize}
    \item $ \land $
        conjunction。2つの命題が成り立つことを示す。
        $ A \land B $ と記述すると、 A かつ B と考えることができる。

    \item $ \lor $
        disjunction。2つの命題のうちどちらかが成り立つことを示す。
        $ A \lor B $ と記述すると、 A または B と考えることができる。

    \item $ \Rightarrow $
        implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
        $ A \Rightarrow B $ と記述すると、 A ならば B と考えることができる。
\end{itemize}

Natural Deduction では、これまでで説明したような規則を使い証明を行うことができる。

例として Natural Deduction で三段論法の証明を行う。
このとき、「A は B であり、 B は C である。よって A は C である」 が証明するべき
命題である。

この命題では 「A は B であり」と 「B は C である」の二つの小さい命題に分けられる。
この「A は B であり」から、AからBが導出できることが分かり、これは $ A \Rightarrow B $ と表せる。
また、「B は C である」から、BからCが導出できることが分かる。これも「A は B であ
り」の時と同様に $ B \Rightarrow C $ と表せる。


\begin{prooftree}
    \AxiomC{ $ [A] $ $_{(1)}$}
    \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
    \RightLabel{ $ \land 1 \mathcal{E} $ }
    \UnaryInfC{ $ (A \Rightarrow B) $ }
    \RightLabel{ $ \Rightarrow \mathcal{E} $}
    \BinaryInfC{ $ B $ }

    \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
    \RightLabel{ $ \land 2 \mathcal{E} $ }
    \UnaryInfC{ $ (B \Rightarrow C) $ }

    \RightLabel{ $ \Rightarrow \mathcal{E} $}
    \BinaryInfC{ $ C $ }
    \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$}
    \UnaryInfC{ $ A \Rightarrow C $}
    \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$}
    \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $}
\end{prooftree}


Natural Deductionでは次のような証明木になる。


\begin{figure}[htpb]
   \begin{center}
       \includegraphics{pic/modus-ponens.pdf}
   \end{center}
   \caption{自然演繹での三段論法の証明}
   \label{fig:modus-ponens}
\end{figure}

これにより自然演繹を使って三段論法が証明できた。
%%%%%%%%%%%%%%%%%%%%%%


\section{Natural Deduction と 型付き $ \lambda $  計算}

ここでは、 Natural Deduction と型付き$ \lambda $ 計算の対応を定義する。
対応は以下の表\ref{table:curry-howard}のようになる。

\begin{center}
  \begin{table}[h]
%    \scalebox{0.75}{
      \begin{tabular}{|c|c|} \hline
        Natural Deduction           & 型付き $ \lambda $ 計算  \\ \hline \hline
        $ A $                       & 型 A を持つ変数 x \\ \hline
        $ A \Rightarrow B $         & 型 A を取り型 B の変数を返す関数 f \\ \hline
        $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline
        $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline
        $ A \land B $               & 型 A と型 B の直積型 を持つ変数 x \\ \hline
        $ \land \mathcal{I} $       & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline
        $ \land 1 \mathcal{E} $     & 直積型からの型Aを取り出す射影fst \\ \hline
        $ \land 2 \mathcal{E} $     & 直積型からの型Bを取り出す射影snd \\ \hline
      \end{tabular}
%    }
    \caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)}
    \label{table:curry-howard}
  \end{table}
\end{center}

この対応をもとに Agda で型付き $\lambda$ 計算による証明を示す。
% ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。
ここでも先程 Natural Deduction で証明した三段論法を例とする。
% この三段論法は自然演繹では\ref{fig:modus-ponens}のようになっていた。

% \begin{figure}[htpb]
%    \begin{center}
%        \includegraphics{pic/modus-ponens.pdf}
%    \end{center}
%    \caption{自然演繹での三段論法の証明}
%    \label{fig:modus-ponens}
% \end{figure}

%McCこの証明木に対応するAgdaによる証明はリスト\ref{agda-moduse-ponens}のようになる。

\begin{lstlisting}[frame=lrbt,label=agda-moduse-ponens,caption={\footnotesize Agda による
    三段論法の定義と証明}]    
data _×_ (A B : Set) : Set where
  <_,_> : A → B → A × B

fst : {A B : Set} → A × B → A
fst < a , _ > = a

snd : {A B : Set} → A × B → B
snd < _ , b > = b 


f : {A B C : Set} → ((A → B) × (B → C)) → (A → C)
f = λ p x → (snd p) ((fst p) x)
\end{lstlisting}

自然演繹での三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。

ここで $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。
よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。
これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。
仮定 $ (A \rightarrow B) \times (B \rightarrow C) $  と仮定 A から A $ \rightarrow $ C を導いている。

仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。
fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。
もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。
得られた B を snd p に適用することで最終的に C が導ける。

\lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda}

このように Agda でも自然演繹と同様に証明を記述できる。