Ltac と proof term 5

tactic が proof term を生成していく様子を何度か観察しましたが，何のためにそんなことをしていたかというと，ときどき tactic が失敗してよくわからないエラーを出すことがあるのでその理由を知りたかったのです。今回はそこに近づこうとしてみます。

例として Coq'Art の chapter 10 にあるものを取り上げてみます。web から拾ってきた仏語版だと 10.2.4 節，289 ページから 290 ページにかけて書いてあります。

先に必要な定義をしておきます。

Definition pred_partial : forall n, n <> 0 -> nat.
  intro n; case n.
  intro h; elim h; reflexivity.
  intros p ?; exact p.
Defined.

Theorem le_2_n_not_zero : forall n, 2 <= n -> n <> 0.
  intros n Hle; elim Hle; discriminate.
Qed.

で，こんなことを証明しようとします。

Theorem le_2_n_pred :
  forall n (h : 2 <= n), pred_partial n (le_2_n_not_zero n h) <> 0.

テキストでは次のような証明を試みて，これは Cannot solve a second-order unification problem と言われて失敗するよと書いてあります。

  intros n h; elim h.

Coq 8.3 で試してみると

Error: Abstracting over the term "n" leads to a term
"fun n : nat => pred_partial n (le_2_n_not_zero n h) <> 0"
which is ill-typed.

というエラーになりました。たぶんこっちのほうがわかりやすくなってます。せっかくわかりやすくなっているので詳しく見てみましょう。

なぜ ill-typed か

まずは上の項が ill-typed であることから確認します。

中に現れる二つの定数の型は

Coq < Check pred_partial.
pred_partial
     : forall n : nat, n <> 0 -> nat

Coq < Check le_2_n_not_zero.
le_2_n_not_zero
     : forall n : nat, 2 <= n -> n <> 0

となっています。さらに

n : nat
h : 2 <= n

であることを考えると

n : nat, h : 2 <= n |- pred_partial n (le_2_n_not_zero n h) <> 0 : Prop

のように型がつきますが，ここで n を abstract しようとしても，n の右にまだ仮定 h が残っていて規則が適用できません。Lam 規則を使うことになるはずですが，この規則では一番右にある変数しか abstract できないからです。ここでは h が n に依存している (もうちょっと詳しく言うと，自由な n を含む型をもつ) ので n と h の順番がこうなっているのは本質的であり，ちょっとどうしようもない感じがします。

要するに，n を abstract しようとするんだけど n に依存した h が残っているから abstract してしまうと h の型の n は何者だということになってしまっておかしいよ，ということみたいです。*1

なぜそんな項が現れるのか

ill-typed であるのはどうやら間違いないようですが，じゃあなんでそんなものが現れてしまうのか，というのが次の疑問です。そのためには elim が何をしているかを知る必要があります。ちょうど le 型に対する elim を使った証明が上のほうにあったので，それを詳しく見てみましょう。

Coq < Reset le_2_n_not_zero.

Coq < Theorem le_2_n_not_zero : forall n, 2 <= n -> n <> 0.
1 subgoal
  
  ============================
   forall n : nat, 2 <= n -> n <> 0

le_2_n_not_zero < intros n Hle.
1 subgoal
  
  n : nat
  Hle : 2 <= n
  ============================
   n <> 0

le_2_n_not_zero < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat, 2 <= n -> n <> 0
Proof: fun (n : nat) (Hle : 2 <= n) => ?1 n Hle

le_2_n_not_zero < elim Hle.
2 subgoals
  
  n : nat
  Hle : 2 <= n
  ============================
   2 <> 0

subgoal 2 is:
 forall m : nat, 2 <= m -> m <> 0 -> S m <> 0

le_2_n_not_zero < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat, 2 <= n -> 2 <> 0
2 -> forall n : nat, 2 <= n -> forall m : nat, 2 <= m -> m <> 0 -> S m <> 0
Proof: fun (n : nat) (Hle : 2 <= n) =>
       le_ind 2 (fun n0 : nat => n0 <> 0) (?1 n Hle) (?2 n Hle) n Hle

大雑把にいうと le_ind を使ってるだけですね。le_ind の型は

le_2_n_not_zero < Check le_ind.
le_ind
     : forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0

なので，le_ind をそのまま適用した形のようです。induction だともうちょっと違う形になるみたいです。

で，残りはまあいいでしょう。

le_2_n_not_zero < discriminate.
1 subgoal
  
  n : nat
  Hle : 2 <= n
  ============================
   forall m : nat, 2 <= m -> m <> 0 -> S m <> 0

le_2_n_not_zero < discriminate.
Proof completed.

le_2_n_not_zero < Qed.
intros n Hle.
elim Hle.
 discriminate.
 
 discriminate.
 
le_2_n_not_zero is defined

それで元の証明に戻りますが，

Theorem le_2_n_pred :
  forall n (h : 2 <= n), pred_partial n (le_2_n_not_zero n h) <> 0.
  intros n h.

とりあえずここまでやると subgoal と proof term が

le_2_n_pred < Show.
1 subgoal
  
  n : nat
  h : 2 <= n
  ============================
   pred_partial n (le_2_n_not_zero n h) <> 0

le_2_n_pred < Show Proof.
LOC: 
Subgoals
1 -> forall (n : nat) (h : 2 <= n), pred_partial n (le_2_n_not_zero n h) <> 0
Proof: fun (n : nat) (h : 2 <= n) => ?1 n h

となってます。elim h したときに何が起きるか想像してみましょう。le_ind を適用するということが上でわかったので le_ind の型を見ると，h が 2 <= n であることから proof term は

le_ind 2 ?P (?1 : ?P 2) 
  (?2 : forall m : nat, n <= m -> ?P m -> ?P (S m))
  n h 
    : ?P n

のようなものになるはずです。?P が何になるかはすぐわからなかったのでこう書いておいたんですが，これは上の項と現在の goal とを見比べてみると，おそらく

fun n => pred_partial n (le_2_n_not_zero n h) <> 0

になるでしょう。あれ，どこかで見た形ですね。そういえばさっき見た ill-typed term がこれでした。

というわけでエラーの出所は一応わかったわけですが……理解できたようなできてないような。

別証明

ちなみに上で失敗してる証明ですが，elim ではなく case を使うとできます。

  case h.
  discriminate.
  apply le_2_n_not_zero; assumption.
Qed.

ちなみに case h した直後の proof term の形はこうなってます。

le_2_n_pred < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat,
     2 <= n -> pred_partial 2 (le_2_n_not_zero 2 (le_n 2)) <> 0
2 -> forall n : nat,
     2 <= n ->
     forall (m : nat) (l : 2 <= m),
     pred_partial (S m) (le_2_n_not_zero (S m) (le_S 2 m l)) <> 0
Proof: fun (n : nat) (h : 2 <= n) =>
       match
         h as l in (_ <= n0)
         return (pred_partial n0 (le_2_n_not_zero n0 l) <> 0)
       with
       | le_n => ?1 n h
       | le_S x x0 => ?2 n h x x0
       end

match になるんですね。でもけっこうややこしい。

Coq'Art の 15 章では，また別の証明として maximal induction principle を使う方法が紹介されています。

*1:ここのところ，型付け規則を見ると「ああそれは確かにだめに決まってるね」という気がするのですが直感的な説明をしようとするとなんだかすっきりしない。もっとよい説明があったら知りたいです。