coqの基本tacticと生成コードとその解釈

例としてand除去を含む証明。

Coq < Goal forall A B : Prop, A /\ B -> B.
...
Unnamed_thm < intros.
1 subgoal

  A : Prop
  B : Prop
  H : A /\ B
  ============================
   B

Unnamed_thm < elim H.
1 subgoal

  A : Prop
  B : Prop
  H : A /\ B
  ============================
   A -> B -> B

...
Unnamed_thm < Save andelim.
intros.
elim H.
intros.
exact H1.
andelim is defined

これによってできる式を表示すると、

Coq < Print andelim.
andelim =
fun (A B : Prop) (H : A /\ B) => and_ind (fun (_ : A) (H1 : B) => H1) H
     : forall A B : Prop, A /\ B -> B


Argument scopes are [type_scope type_scope _]

Coq <

型関係を除去すると、amdelim = fun H => and_ind (fun _ H1 => H1) H というand_indに関数と引数のHを渡した式になっている。introsはfunをつけるものなので、戦略elim Hは、and_ind _ H.を生成するもののようだ。

and_indとはなにか。

Coq < Print and_ind.
and_ind =
fun A B P : Prop => and_rect (A:=A) (B:=B) (P:=P)
     : forall A B P : Prop, (A -> B -> P) -> A /\ B -> P


Arguments A, B, P are implicit
Argument scopes are [type_scope type_scope type_scope _ _]

Coq <

and_rectを呼んでいるだけの関数だが、コード上で明示されている引数は3つなので、さらに(A->B->P)とA/\Bの二つを引数に受け取ってPを返す関数を返しているとみなせる。で、and_rectは、

Coq < Print and_rect.
and_rect =
fun (A B : Prop) (P : Type) (f : A -> B -> P) (a : A /\ B) =>
match a with
| conj x x0 => f x x0
end
     : forall (A B : Prop) (P : Type), (A -> B -> P) -> A /\ B -> P


Arguments A, B, P are implicit
Argument scopes are [type_scope type_scope type_scope _ _]

Coq <

and_rectは、最後の引数aがconjパターンだったら、そのメンバー二つを引数にしてその前の引数の関数fを適用するものになっている。conjは

Coq < Print conj.
Inductive and (A : Prop) (B : Prop) : Prop :=  conj : A -> B -> A /\ B
For conj: Arguments A, B are implicit
For and: Argument scopes are [type_scope type_scope]
For conj: Argument scopes are [type_scope type_scope _ _]

Coq <

と、ここでand型が出てくる。conjはandのデータコンストラクタだった。これまでの関数や戦略は、以下のように解釈できる

• and_rect: 引数A Bの関数をA/\Bを引数にとる関数に変える。いわば逆カリー化
• and_ind: 戻り値もPropである and_rect
• elim H: 二引数の関数goal:A->B->Pに、H: A /\ Bを分解して適用する。and型を2引数に分解する

逆にand導入を見てみる:

Coq < Goal forall A B : Prop, A -> B -> A /\ B.
...
Unnamed_thm < Save andintro.
intros.
split.
 exact H.
exact H0.
andintro is defined

でPrint

Coq < Print andintro.
andintro =
fun (A B : Prop) (H : A) (H0 : B) => conj H H0
     : forall A B : Prop, A -> B -> A /\ B


Argument scopes are [type_scope type_scope _ _]

Coq <

and導入のためのsplit戦略は、単にand型のコンストラクタコードconj _ _を生成するものだった。