ある程度 Coq を使ったことがあるひとは、以下のような状況で rewrite が失敗する ことを経験しているのではないかと思う。
Require Import List. Require Import Arith. Goal forall s, map (fun n => n * 2) s = map (fun n => 2 * n) s. intros s. (* goal: map (fun n : nat => n * 2) s = map (fun n : nat => 2 * n) s *) Fail rewrite mult_comm. (* Found no subterm matching "?M1050 * ?M1051" in the current goal. *)
n * 2 と 2 * n は乗算の交換法則により等しいので、 rewrite mult_comm で証明できるはず、と思ってやってみても rewrite は失敗する。
ここで、なぜ rewrite が失敗するかというと、書き換えたい「n * 2」という項に 含まれる n はゴール中で束縛されている束縛変数だからである。
束縛変数は fun 以外にも let や match などでも発生する。 その場合でも rewrite が失敗するのは同じである。
さて、なぜ束縛変数が含まれる項を rewrite できないかというと、 rewrite は eq_ind_r を呼び出す証明項をつくるということを知っていると理解できる。 (逆方向の rewrite<- は eq_ind を使う)
eq_ind_r の型は以下のとおりである。
About eq_ind_r. (* eq_ind_r : forall (A : Type) (x : A) (P : A -> Prop), P x -> forall y : A, y = x -> P y Arguments A, x, y are implicit Argument scopes are [type_scope _ function_scope _ _ _] eq_ind_r is transparent Expands to: Constant Coq.Init.Logic.eq_ind_r *)
つまりこれは、P x と y = x という前提が成り立てば、P y という結論が成り立つという定理である。
Coq は逆向きに証明を進めていくので、P y という結論を P x と y = x という前提に置き換えるが、 ここで rewrite tactic では人間が y = x の証明を (普通は証明済みの定理の名前として) 与えるので、 ゴールは P y が P x に置き換わることになる。 P として、書き換えたいところを与えるとゴール全体を返すような関数を与えれば、 y が x に書き換わったゴールに変化して意図どおりの書き換えができることになる。
rewrite tactic はそういう動作をするため、内部で P を作るわけである。 しかし、書き換えたいところに束縛変数があると P を作れない。 正確にいえば、P y がもともとのゴールと同じ (convertible) になるような P と y を作れない。
上記の例でいえば、map (fun n : nat => n * 2) s = map (fun n : nat => 2 * n) s というゴールの n * 2 の部分を書き換えるために、n * 2 の部分を括り出して (fun z => (map (fun n : nat => z) s = map (fun n : nat => 2 * n) s)) (n * 2) としようとすると、 n * 2 の中の n がスコープから外れてしまって、正しい項にならない。
というわけで、適切な P を作れないので、rewrite できない、というわけである。
束縛変数以外に rewrite が失敗する理由としては、依存型があげられる。
まず、どうも pure Coq の rewrite は依存型に関連する部分を避ける感じの動作になっているようで、 想定どおりの失敗にならなかったので、ここでは ssreflect を使う。
From mathcomp Require Import all_ssreflect.
すごく簡単な依存型 D を定義する。 コンストラクタ d は、引数 n を受けとると、D n 型の値を返す、というこれだけである。
Inductive D : nat -> Type := | d : forall n, D n.
さて、この型に関連する簡単な命題 d n = d n を例に依存型の rewrite を考えてみよう。 ここで出てくる = は eq だが、以下では @eq の形で暗黙の引数も明示した形で示す。
Goal forall (n : nat), d n = d n. move=> n. (* goal: @eq (D n) (d n) (d n) *)
この命題はもちろん reflexivity で証明できるのだが、今はそれには興味がなく、n を rewrite することを考える。
n はゴールに 3箇所現れる。 この3箇所を同じように書き換えれば型は壊れないが、 一部だけ書き換えると型が壊れる。
というわけで、失敗すべき例として、最初の n を n + 0 に書き換えようとしてみる。 なお n + 0 は addn n 0 だが、これは n と convertible ではない。
Fail rewrite -{1}[n]addn0.
(*
Dependent type error in rewrite of (fun _pattern_value_ : nat =>
@eq (D _pattern_value_) (d n) (d n))
*)
というわけで、やはり失敗する。 エラーメッセージには、 (fun _pattern_value_ : nat => @eq (D _pattern_value_) (d n) (d n) という項が 表示されていて、まぁ、d n は D n 型であって D _pattern_value_ 型じゃないから型エラーになるのはたしかにそうだろう。
同様に、他の部分を書き換えようとしてもやはり失敗する。
Fail rewrite -{2}[n]addn0.
Fail rewrite -{3}[n]addn0.
Fail rewrite -{1 2}[n]addn0.
Fail rewrite -{1 3}[n]addn0.
Fail rewrite -{2 3}[n]addn0.
最後に、3箇所すべてを書き換えると、これは成功する。
rewrite -{1 2 3}[n]addn0.
(* @eq (D (addn n O)) (d (addn n O)) (d (addn n O)) *)
Abort.
ところで、n + 0 でなく、0 + n に rewrite で書き換えようとすると、これも失敗する。 なお、0 + n は n と convertible である。
Goal forall (n : nat), d n = d n.
move=> n.
(* goal: @eq (D n) (d n) (d n) *)
Fail rewrite -{1}[n]add0n.
(*
Dependent type error in rewrite of (fun _pattern_value_ : nat =>
@eq (D _pattern_value_) (d n) (d n))
*)
convertible なのになぜ失敗するのか、というと、 convertible かどうかという以前に、eq_ind_r/eq_ind に渡す P を作るという段階で失敗しているのである。
上記のエラーは rewrite が P として (fun _pattern_value_ : nat => @eq (D _pattern_value_) (d n) (d n)) を作ったが、 これが型検査を通らなかったということだろう。
eq_ind_r/eq_ind の呼び出しでなく、単に convertible な置換をしたいだけなら、 change tactic を使えばよく、これは次のように問題なく成功する。
change n with (0+n) at 1. (* goal: @eq (D (addn O n)) (d n) (d n) *) Abort.
ところで、goal を P y の形にするというのは、beta expansion (つまり beta reduction の逆) をする ということである。
Coq にはこの部分を行う pattern という tactic がある。
Inductive D : nat -> Type := | d : forall n, D n. Goal forall (n : nat), d n = d n. intros n. (* goal: @eq (D n) (d n) (d n) *)
pattern n at 1 は、n を引数として受け取り、最初の出現に埋め込むような関数呼び出しに ゴールを置き換えてくれる。 当然これは、依存型のせいで型エラーになるはずである。
Fail pattern n at 1.
(*
Illegal application:
The term "@eq" of type
"forall (A : Type@{Coq.Init.Logic.8}) (_ : A) (_ : A), Prop"
cannot be applied to the terms
"D n0" : "Set"
"d n" : "D n"
"d n" : "D n"
The 2nd term has type "D n" which should be coercible to
"D n0".
*)
エラーメッセージをみると、2nd term の d n が D n 型なのに、D n0 型と convertible でない、 という想定どおりのエラーになっている。
pattern で 3箇所の n を部分的に指定するものは同様にエラーとなる。
Fail pattern n at 2. Fail pattern n at 3. Fail pattern n at 1 2. Fail pattern n at 1 3. Fail pattern n at 2 3.
pattern で 3箇所の n をすべて指定すると、これは成功する。 (すべて、というのは指定しなくてもいいので、pattern n でもよい)
pattern n at 1 2 3. (* goal: (fun n0 : nat => @eq (D n0) (d n0) (d n0)) n *)
結果を見ると、3箇所の n がすべて n0 に置き換わっている。 d n0 は D n0 型なので、これは正しく型がつき、問題ない。
そういえば、束縛変数を含んだ項を rewrite したいときにどうするか書かなかった。
ひとつの方法は、関数を展開して、すべての束縛変数をどうにかして前提においやってから rewrite するという方法である。
たとえば昨日の例の map (fun n : nat => n * 2) s = map (fun n : nat => 2 * n) s なら、 induction s として帰納法を使うと、どうにかできる。
Require Import List. Require Import Arith. Goal forall s, map (fun n => n * 2) s = map (fun n => 2 * n) s. intros s. (* goal: map (fun n : nat => n * 2) s = map (fun n : nat => 2 * n) s *) induction s. reflexivity. simpl. rewrite IHs. f_equal. (* 証明するだけならこの f_equal は不要だけど、次の goal が短くなる *) (* goal: a * 2 = a + (a + 0) *) rewrite mult_comm. reflexivity. Qed.
もちろんこれは、map という関数の中身に依存した話で、 他の関数には他のやりかたが必要だし、 不可能なこともある。
不可能な例としては、(fun n : nat => n * 2) = (fun n : nat => 2 * n) というように、 関数と関数が等しいという命題の場合がある。 Coq でこれを証明するには公理を追加する必要がある。
上記の例では map を使っていたが、もし map のかわりに、第1引数をそのまま返す関数だったら、 まさに上の関数と関数が等しいという命題になってしまう。 なので、Coq で証明するには map の性質を利用した証明が必要なのはしかたがない。
ただ、これを証明できる公理を追加してよいなら、map の性質に依存せずに証明できる。
Coq の FunctionalExtensionality というライブラリは 関数の外延性の公理を追加する。 これを使うと、map の性質に依存せずに証明できる。
もちろん、公理を追加するのはできるかぎり避けたほうがいい話ではある。 しかし、ここではあえて試しにやってみる。
Require Import List. Require Import Arith. Require Import FunctionalExtensionality.
問題をすこし現実的にするため、今回は無名関数の中身は n * 2 + 1 と 2 * n + 1 とする。
Lemma L : forall s, map (fun n => n * 2 + 1) s = map (fun n => 2 * n + 1) s. intros s. (* goal: map (fun n : nat => n * 2 + 1) s = map (fun n : nat => 2 * n + 1) s *)
ここでまず、書き換えたいところ (n * 2) をボディとする関数として括り出す。
change (fun n : nat => n * 2 + 1) with
(fun n : nat => let f m := m * 2 in f n + 1).
括り出した f は (fun m : nat => m * 2) という関数で、この関数自体は自由変数を持たない。 なので、これを (fun m : nat => 2 * m) に書き換えるのは (それらが eq であるという証明があれば) 可能である。 eq であるという証明がなくても、それは後から人間が与えるということにすればとりあえず書き換えることは できて、それを行う tactic が replace である。
replace (fun m : nat => m * 2) with
(fun m : nat => 2 * m).
(* goal: map (fun n : nat => let f := fun m : nat => 2 * m in f n + 1) s =
map (fun n : nat => 2 * n + 1) s *)
(* goal: (fun m : nat => 2 * m) = (fun m : nat => m * 2) *)
replace した後は、f は期待通りに書き換えられている。 また、ゴールがひとつ増えていて、後から人間が与えるとした eq の証明も必要である。
証明項をみると、以下のようになっていて、(rewrite<- と同じく) eq_ind を使っていることが分かる。
Show Proof.
(*
(fun s : list nat =>
let H : (fun m : nat => 2 * m) = (fun m : nat => m * 2) := ?Goal in
eq_ind (fun m : nat => 2 * m)
(fun n : nat -> nat =>
map (fun n0 : nat => let f := n in f n0 + 1) s =
map (fun n0 : nat => 2 * n0 + 1) s) ?Goal0
(fun m : nat => m * 2) H)
*)
最初のゴールはとくに問題なく reflexivity で証明できる。
reflexivity.
問題は後のゴールだが、ここで functional_extensionality という公理 (を内部で利用している定理) を使う。 これを使うと、関数と関数が等しいという命題が、すべての引数について関数を呼び出した結果が等しい、という形に変化する。
(* goal: (fun m : nat => 2 * m) = (fun m : nat => m * 2) *) apply functional_extensionality. (* goal: forall x : nat, 2 * x = x * 2 *)
この形は乗算の交換法則のひとつの具体例なので、mult_comm を apply すれば証明は終わりである。
apply mult_comm. Qed.
ここで証明した定理 L がどんな公理を利用しているかは Print Assumptions L. とすると表示される。
Print Assumptions L.
(*
Axioms:
functional_extensionality_dep : forall (A : Type)
(B : A -> Type)
(f g : forall x : A, B x),
(forall x : A, f x = g x) -> f = g
*)
これにより、実際に利用している公理は functional_extensionality_dep であるということがわかる。
[latest]