Library curry_howard

カリーハワード対応とCoqのあいだ - Show Proof で学ぶ Coq のしくみ -

Coq はカリーハワード対応を利用して証明をプログラムによって表現しているというのはよく知られています。

カリーハワード対応というのは、命題と型、証明とプログラムが同じ構造になっているという話です。

しかし、Coq の proof editing mode で証明をしていると、証明項（プログラムのことですが、あまりプログラムとしては意識しないので証明項と呼びましょう）がどのようなものか意識することは少ないのではないでしょうか。

たとえば、intros H がなにをする（どんな証明項を構築する）のかわかるでしょうか。

ここでは Coq のいろいろなコマンドがなにをするものなのか、また、それをどうやって調べるのか説明します。