議論の構造の proof script への反映のしかた - 論理とか計算機とか数学とか

Coq の証明を書くときに，ただ tactics を一列に並べて書くと，まったく読めなかったり Coq のバージョンが上がって証明が通らなくなったときにどこでこけてるのかわからなくなったりして不都合なので，証明の構造を proof script のテキスト上にも反映させましょうという話はたぶん昔からあって，昔はインデントとかでそれをやっていたのですが最近は Coq の側でそういうことをサポートするための仕組みが入りました。具体的には bullet と brace ですが，そのあたりの話。Reference manual の 7.2.6 あたり。

bullet は場合分けして case 1, case 2, ... というときには自然に書けて，例えば簡単な例を挙げると

Goal forall n : nat, n = 0 \/ exists m, n = S m.
Proof.
  induction n as [ | n' IHn].
  - left; reflexivity.
  - right; exists n'; reflexivity.
Qed.

のようになります。

これはいいのだけど，subgoal が発生する別のパターンとして assert のような補題を宣言する tactic を使った場合があって，これも bullet を使って書くと

Variables A B C D : Prop.
Goal (A -> B) -> (B -> C) -> A -> C.
Proof.
  intros HAB HBC HA.
  assert (HB : B).
  - apply HAB.
    exact HA.
  - apply HBC.
    exact HB.
Qed.

みたいになります。

しかし，この証明の流れは場合分けとは違う構造をしているように感じるので，こう書くのはちょっと違和感があります。つまり，assert が生成する二つの subgoal は induction の場合と違って対等ではなく，もともとの goal の証明（後ろの subgoal）が主で assert された事実の証明はそのための補助的な議論という関係にあります。だから先ほどと同じように単に二つ同種のものであるかのように並べて書くのは直感に反する気がするわけです。

この手の tactic では先に来る subgoal の方が補助的なものとみてよいと思うので（特に ssreflect の have/suff は名前から判断するにそういう使い分けをさせる意図がありそう）例えば brace を使ってこう書いたらどうでしょうか。

Goal (A -> B) -> (B -> C) -> A -> C.
Proof.
  intros HAB HBC HA.
  assert (HB : B). {
    apply HAB.
    exact HA.
  }
  apply HBC.
  exact HB.
Qed.

場合によってはネストしてみたりとか。

Goal (A -> B) -> (B -> C) -> (C -> D) -> A -> D.
Proof.
  intros HAB HBC HCD HA.
  assert (HC : C). {
    assert (HB : B). {
      apply HAB.
      exact HA.
    }
    apply HBC.
    exact HB.
  }
  apply HCD.
  exact HC.
Qed.

個人的には，どちらかというと bullet よりもよさそうな気がしていますが，こういうのを見たことがないので，あんまり想定された書き方ではないのかもしれない。

一つの問題は，brace を閉じた次の行のインデントがおかしなことになるので手で直さなければならない点。あとピリオドがないと subgoal が閉じている感じがしないのですが，これは慣れの問題かもしれない。しかし慣れとか言い始めると，そもそも bullet に慣れればそれでよくなるだろうということにも。