coqでの証明戦略の引数って何？

例は、forall (A B: Prop), A->(A->B)->B。

これはintrosをすると、A, A->B ┣ Bとなる。これはcoqでは自動的に解決できるものであり、証明戦略的には、->除去である。

• http://adam.chlipala.net/itp/tactic-reference.html

によるとapplyする状況なのだが、仕組みを認識していないと引数に何を指定するかわかりにくい。

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

  A : Prop
  B : Prop
  H : A
  H0 : A -> B
  ============================
   B

Unnamed_thm < 

正解はapply H0。

Unnamed_thm < apply H0.
1 subgoal

  A : Prop
  B : Prop
  H : A
  H0 : A -> B
  ============================
   A

Unnamed_thm <

これで、左辺がgoalに入れ替わる。

結果は

intros A B H H0.
apply H0.
exact H.

これらの証明戦略とは、A,Bを変数の型、->を関数の型とみる、Curry–Howard対応でのプログラム視点では、コード生成マクロのようになっている。Ltacコマンドで定義もできる。そのtactic定義言語は以下のページに仕様がある:

• http://coq.inria.fr/doc/Reference-Manual011.html

証明結果の戦略列はそのマクロの適用順に並べてる。その適用結果後はLemmaやTheoremもDefinition同様の名前付関数になる。

	コマンド	適用結果
0	Goal 〜	_: forall (A B: Prop), A->(A->B)->B
1	intros A B	fun (A B:Prop) => _: A->(A->B)->B
2	intro H	fun (A B:Prop) => fun (H:A) => (_:(A->B)->B)
3	intro H0	fun (A B:Prop) => fun (H:A) => (fun (H0:A->B) => (_:B))
4	apply H0	fun (A B:Prop) => fun (H:A) => (fun (H0:A->B) => (H0 (_:A)))
5	exact H	fun (A B:Prop) => fun (H:A) => (fun (H0:A->B) => (H0 (H)))
6	Save myfunc	myfunc = fun (A B : Prop) (H : A) (H0 : A-> B) => H0 H

論理式分解としては逆っぽい意味にみえるのtacticも、コード生成的視点でみればそれっぽく見える点に注目したい。

GoalやLemmaで証明したものは、Printをすると、上記の関数のほうで表示される。

Coq < Print Unnamed_thm.
Unnamed_thm =
fun (A B : Prop) (H : A) (H0 : A -> B) => H0 H
     : forall A B : Prop, A -> (A -> B) -> B

Coq <

coqではGoalやLemmaやTheoremでは直接本体の式を書くことはできないが、Definitionでは本体を書かないとGoalやLemma同様の証明モードにはいり、証明によって式を定義することができる。