依存関係のある値のうちの一部をrewriteしようとしたときの問題

この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。

最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。

問題の概要は表題の通り。シンプルな問題なので、レガシーCoq (version 8.4pl2) で説明する。

簡単のため、やや人工的な例を紹介する。 まず、正の自然数を引数にとる関数fを仮定し、その関数は引数が偶数のときは、戻り値はその半分になるとする。深い意味は無いので考えてはいけない。

Variable f : forall n : nat, n > 0 -> nat.
Hypothesis h : forall (n : nat) (H : 2 * n > 0), f (2 * n) H = n.

さて、ここで ある変数xが 2*1 と等しいことがわかっているとき、f x H = 1 であることを証明したいとする。 仮定hから f (2*1) H = 1 なんだから、超簡単に示せそうだが、そうでもなかった。

具体的には

  eq : x = 2 * 1
  ============================
   f x H = 1

から普通に rewrite eq. しようとすると次のように怒られた。

Error: Abstracting over the term "x" leads to a term
"fun x : nat => f x H = 1" which is ill-typed.

どうやら、Hはxに依存した型をもつのに、勝手にxの方だけを別のものに差し替えちゃいかんということらしい。 とりあえず generalizeタクティックでHについてゴールを一般化することで、rewriteできるようになった。

< generalize H as H.

  x : nat
  eq : x = 2 * 1
  ============================
   forall H : x > 0, f x H = 1

< rewrite eq.

  x : nat
  eq : x = 2 * 1
  ============================
   forall H : 2 * 1 > 0, f (2 * 1) H = 1

そして、あとは普通に仮定を使って証明できる。

とりあえず今回はこれでできたが、Hの部分がとても長い具体的な証明だった場合、それ全部を入力するのは大変だし、ちょっといやだ。 何かより良い方法があるものだろうか。また、依存型に定評のあるAgdaではどうなるかなども興味深い。

参考: 私の証明のコードは以下の通り

Variable f : forall n : nat, n > 0 -> nat.
Hypothesis h : forall (n : nat) (H : 2 * n > 0), f (2 * n) H = n.

Variable x : nat.
Axiom H : x > 0.

Goal x = 2*1 -> f x H = 1.
Proof.
 intro eq.
 generalize H as H.
 rewrite eq.
 intro H. rewrite h. reflexivity.
Qed.