maximal induction principle の話

前回のうまくいかない elim の続きで，Coq'Art 15 章に載っている方針による別証明について。なぜそっちはうまくいくのか。

ちなみにここに書くことが Coq'Art にきちんと解説されていたかどうかは覚えていませんが，こういうことを細かく解説したものを読んだ記憶がないので触れていなかったのかもしれません。

とりあえず定義を再掲。

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.
  intros n h; elim h.

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.

elim h は大雑把には le_ind の適当な引数に h を渡した proof term を作ろうとする tactic ですが，le_ind の型は

le_2_n_pred < 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

という形をしています。ここで P に相当する引数を作ろうとしてうまくいかない，というのが上に出てきたエラーの内容でした。

なぜうまくいかないかを考えてみると，P が h を引数にとらないせいである，というのが一つの答えとして考えられます。P が h を引数にとれないので

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

みたいなものを考えなければならなくて型がつかなくなったのですが，h も引数にとるのなら，

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

を渡せるからうまくいくはずです。

実際このような方針で証明をすることができて，それには Scheme コマンドで induction principle を生成して使います。詳細は Coq'Art を参照すればよいのですが，Prop に対するデフォルトの induction scheme はやや弱い形をしていて，証明そのものは結論に現れない場合にのみ使えるようになっています。le_ind の P が h を引数にとらなかったのはそのためです。しかし原理的には，induction をしようとしているところの証明に依存するような結論に対しても使える induction principle が考えられるはずで，Prop 以外に対しては実際にそのようなものがデフォルトになっています。

で，証明ですが，こんな感じできちんと elim が使えます。

le_2_n_pred < Scheme le_ind_max := Induction for le Sort Prop.
le_ind_max is defined
le_ind_max is recursively defined

le_2_n_pred < intros n h; elim h using le_ind_max.
2 subgoals
  
  n : nat
  h : 2 <= n
  ============================
   pred_partial 2 (le_2_n_not_zero 2 (le_n 2)) <> 0

subgoal 2 is:
 forall (m : nat) (l : 2 <= m),
 pred_partial m (le_2_n_not_zero m l) <> 0 ->
 pred_partial (S m) (le_2_n_not_zero (S m) (le_S 2 m l)) <> 0

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 m (le_2_n_not_zero m l) <> 0 ->
     pred_partial (S m) (le_2_n_not_zero (S m) (le_S 2 m l)) <> 0
Proof: fun (n : nat) (h : 2 <= n) =>
       le_ind_max 2
         (fun (n0 : nat) (h0 : 2 <= n0) =>
          pred_partial n0 (le_2_n_not_zero n0 h0) <> 0) 
         (?1 n h) (?2 n h) n h

proof term を見てやると，上に書いた通りの h に依存する述語が P 相当の部分に渡されていることがわかります。

証明の残りの部分は前回の case を使ったものと同じになるので，今回の場合にこちらの方針を選ぶメリットがあったのかどうかわかりませんが。proof term も見た目は違いますが，le_ind_max を展開してやるとだいたい同じになる気がします。