また ill-typed term が出てくる例 - 論理とか計算機とか数学とか

証明がうまくいかなくて工夫が必要な事例を集めようとしています。今回のは Coq'Art にも似たような例が書いてあった気がしますが。

問題設定

Z -> Z な関数 f と，Z -> Prop な述語(「よい」整数の定義)が与えられます。

0 <= i < n なるすべての i に対して (f i) が「よい」整数であることの証明を受け取って，この範囲にわたる (f i) の総和を計算する関数 sum を書きましょう。
書けたら，sum の値は証明の中身には依存しないはずなので，それを証明しましょう。

あなぷるの JMO2011-3 (http://as305.dyndns.org/aps/problem/view/46) やってて出てきたものを少し変形した問題を考えます。関数の定義域が nat だと帰納法がやりやすいんですが，Z を使うと難しくなります。

sum の書き方

sum の定義は証明の構造に関する原始帰納法でできます。が，単純に match すると怒られるので補題を使ったりしてごまかします。Coq'Art のどこかに書いてあった方法です。

Require Import ZArith.

Open Scope Z_scope.

Parameter Z_ok : Z -> Prop.

Inductive ok : Z -> (Z -> Z) -> Prop :=
| ok_zero : forall f, ok 0 f
| ok_succ : forall n f, ok n f -> Z_ok (f n) -> ok (n + 1) f.

Lemma ok_inv : forall n f, ok n f -> n <> 0 -> ok (n-1) f.
  induction 1; try replace (n + 1 - 1) with n by omega; intuition.
Defined.

Fixpoint sum n f (p : ok n f) :=
  match Z_eq_dec n 0 with
    | left _ => 0
    | right ne_pf => f (n - 1) + sum _ _ (ok_inv _ _ p ne_pf)
  end.

問題は証明なのですが。

うまくいかなかったやつ

Coq < Lemma sum_proof_irrelevant : forall n f p p', sum n f p = sum n f p'.

1 subgoal
  
  ============================
   forall (n : Z) (f : Z -> Z) (p p' : ok n f), sum n f p = sum n f p'

sum_proof_irrelevant < induction p.
Toplevel input, characters 3-14:
>   induction p.
>   ^^^^^^^^^^^
Error: Abstracting over the terms "n" and "f" leads to a term
"fun (n : Z) (f : Z -> Z) => forall p' : ok n f, sum n f p = sum n f p'"
which is ill-typed.

帰納法を使おうとしたら怒られました。主張の内容が p に依存しているので，普通の induction は使えません。

sum_proof_irrelevant < Scheme ok_ind_max := Induction for ok Sort Prop.
ok_ind_max is defined
ok_ind_max is recursively defined

sum_proof_irrelevant < induction p using ok_ind_max.
2 subgoals
  
  f : Z -> Z
  ============================
   forall p' : ok 0 f, sum 0 f (ok_zero f) = sum 0 f p'

subgoal 2 is:
 forall p' : ok (n + 1) f, sum (n + 1) f (ok_succ n f p z) = sum (n + 1) f p'

これでとりあえず一つ進みました。

で，次に p' を分解しないと計算が進まないのですが，

sum_proof_irrelevant < destruct p'.
Toplevel input, characters 0-11:
> destruct p'.
> ^^^^^^^^^^^
Error: Abstracting over the terms "z", "f" and "p'" leads to a term
"fun (z : Z) (f : Z -> Z) (p' : ok z f) => sum z f (ok_zero f) = sum z f p'"
which is ill-typed.

destruct しようとしたら怒られます。確かに abstract すると (sum z f (ok_zero f)) に型がつかなくなりますね。

あれこれ試した結果，どうもこのままだとうまく証明できないらしいという結論に至りました。どうも p と p' の型に現れる n が共通なのがよくないようです。

うまくいったやつ

Lemma ok_n_nonneg : forall n f, ok n f -> n >= 0.
  induction 1; auto with zarith.
Qed.

Lemma ok_lemma : forall n f, ok n f -> n + 1 <> 0.
  intros n f p; pose proof (ok_n_nonneg n f p); omega.
Qed.

Lemma sum_proof_irrelevant' : forall n f (p : ok n f),
  forall n' (p' : ok n' f),
  n = n' -> sum n f p = sum n' f p'.
  induction p using ok_ind_max.
  destruct p'; auto.
  intro; elim (ok_lemma n f p'); auto.

  destruct p'; intuition.
  elim (ok_lemma n f); auto.

  assert (e : n = n0) by omega.
  subst; clear H.
  simpl.
  destruct (Z_eq_dec (n0 + 1) 0).
  auto.

  f_equal.
  transitivity (sum n0 f p); auto using eq_sym with zarith.
Qed.

別の変数にしておいて n = n' を仮定に付けるのがコツらしいです。これも Coq'Art に書いてあったかも。

ちなみにもとの主張の証明，

Lemma sum_proof_irrelevant : forall n f p p', sum n f p = sum n f p'.
  induction p using ok_ind_max.
  simpl.
  generalize (eq_refl 0); generalize 0 at -1.
  intros; destruct p'; auto.
  elim (ok_lemma n f p'); auto.

  (* ... *)

こんな調子でやればたぶんできるんですが，これは結局のところ goal をうまくいった方と同じ形に変形して証明してるだけですね。やっぱりこうしないと無理なんでしょうか。補題を用意すれば……と思ったんですが，補題の証明で結局同じことをやらなきゃならなかったので没にしました。