Ltac と proof term

一月の終わりごろから Coq で遊んでいます。

あまり自明でないこともだんだんできるようになってきた気がしますが，なにかがわかるようになってくるということとなにかがわからないと気付くこととはたいていの場合同時に起こることのようです。

tactic が何をやっているのかがよくわからない，ということが最近わかりはじめました。goal を変形すると言うけど，goal とかそれに対する操作は CIC の外にある概念であって，それが CIC の中で書ける proof term とどうつながってるのかがよくわからない。簡単な例ならなんとなく想像はつくけど，複雑になってくるとわからなくなります。

というわけで，それを理解するための第一歩。

Coq < Section test.

Coq < Variables A B : Prop.
A is assumed
B is assumed

Coq < Goal A /\ B -> B /\ A.
1 subgoal
  
  A : Prop
  B : Prop
  ============================
   A /\ B -> B /\ A

こんなのを解いてみます。

Unnamed_thm < intro H; destruct H; split; assumption.
Proof completed.

解けました。

そうではなくて。

Unnamed_thm < Restart.

tactic って結局なにやってるの，ということを proof term が作られる様子を観察しながら理解しようという試み。

Show Proof というコマンドをたたくと作りかけの proof term を見ることができます。

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> A /\ B -> B /\ A
Proof: ?1

?1 だそうです。つまり，まだなにもしてないので proof term はただの穴です。

Unnamed_thm < intro H.
1 subgoal
  
  A : Prop
  B : Prop
  H : A /\ B
  ============================
   B /\ A

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> A /\ B -> B /\ A
Proof: fun H : A /\ B => ?1 H

intro H しました。この証明は関数であり，仮引数の名前は H である，ということになりました。

関数の本体が新しい goal になります。だから本体が新しい穴になる……と思ったら，なんか ?1 に H が渡されてました。よく知りませんが，技術的な理由かもしれません。existential variable は束縛変数を含む式で instantiate できないとかそんなような話でしょうか。

Unnamed_thm < destruct H.
1 subgoal
  
  A : Prop
  B : Prop
  H : A
  H0 : B
  ============================
   B /\ A

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> A -> B -> B /\ A
Proof: fun H : A /\ B => match H with
                         | conj H0 H1 => ?1 H0 H1
                         end

destruct してみました。本体がパターンマッチになりました。destruct は match 式を作る操作だったようです。and にはコンストラクタがひとつしかないので，作られる subgoal もひとつだけです。

Unnamed_thm < split.
2 subgoals
  
  A : Prop
  B : Prop
  H : A
  H0 : B
  ============================
   B

subgoal 2 is:
 A

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> A -> B -> B
2 -> A -> B -> A
Proof: fun H : A /\ B =>
       match H with
       | conj H0 H1 => conj (?1 H0 H1) (?2 H0 H1)
       end

split するとゴールが二つに分かれます。これは and のコンストラクタ conj に渡す引数が二つ要るということですね。

?1 H0 H1 と ?2 H0 H1 がその引数で，それぞれが新しい subgoal に対応しています。やっぱり existential variable には local context にある仮定が明示的に渡されるようです。A, B は渡されてないのはどういうことかというと，よくわかりません。parameter だからですかね。

Unnamed_thm < assumption.
1 subgoal
  
  A : Prop
  B : Prop
  H : A
  H0 : B
  ============================
   A

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> A -> B -> A
Proof: fun H : A /\ B => match H with
                         | conj H0 H1 => conj H1 (?1 H0 H1)
                         end

subgoal がひとつ完成しました。assumption って射影を作るんですね。

Unnamed_thm < assumption.
Proof completed.

Unnamed_thm < Show Proof.
LOC: 
Subgoals
Proof: fun H : A /\ B => match H with
                         | conj H0 H1 => conj H1 H0
                         end

もうひとつの subgoal も同様です。

Unnamed_thm < Qed.

intro H.
destruct H.
split.
 assumption.
 
 assumption.
 
Unnamed_thm is defined

Coq < Print Unnamed_thm.
Unnamed_thm = 
fun H : A /\ B => match H with
                  | conj H0 H1 => conj H1 H0
                  end
     : A /\ B -> B /\ A

Print すると，さっきと同じものが出てきます。あたりまえですか。

Ltac がどんなことをするものなのか理解するための第一歩はこのあたりにあるのでしょうか。どうでしょうか。