Coq で、関数の中を rewrite するにはどうしたらいいか。 たとえば、以下で、(fun n => (n + 1) + n) という関数の中の n + 1 を n.+1 に書き換えたいとしよう
Lemma L1 s : map (fun n => (n + 1) + n) s = map (fun n => n.+1 + n) s. Proof. Fail rewrite addn1. apply: eq_map => n. by rewrite addn1. Qed.
最初に Fail rewrite addn1. 書いてあるのは、 そこでは rewrite addn1 が失敗するという意味である。 なんで失敗するかというと、n + 1 の n は (fun n => ...) というところで束縛されている変数であるため、 ゴールを P (n + 1) という形に beta expansion できないからである。
そのため、上の証明ではいきなり rewrite するのはあきらめて、まず eq_map を使って変形している。 ということは、(n + 1) という項自体の性質ではなく、 その外側にある map についての性質を利用して証明しているわけである。
しかし、eq_map みたいな補題を探すのは面倒で嫌だ、という場合を考えよう。 これは、FunctionalExtensionality という公理を使うと可能となる
Require Import FunctionalExtensionality.
Lemma L2 s : map (fun n => (n + 1) + n) s =
map (fun n => n.+1 + n) s.
Proof.
change (map (fun n => (fun x => x + 1) n + n) s =
map (fun n => n.+1 + n) s).
rewrite (_ : (fun x => x + 1) = (fun x => x.+1)).
by [].
(* (fun x : nat => x + 1) = (fun x : nat => x.+1) *)
apply functional_extensionality => x.
(* x + 1 = x.+1 *)
by rewrite addn1.
Qed.
ここでは書き換えたい n + 1 を (fun x => x + 1) n と変形して 束縛変数 n が含まれない (fun x => x + 1) という項を作り出し、 (fun x => x + 1) を (fun x => x.+1) に書き換えている
(fun x => x + 1) を (fun x => x.+1) に書き換えるのは functional_extensionality (と addn1) を使うと可能である
この証明では、eq_map のような、書き換えたいところ以外の部分の性質は使っていない。 そのため、外側に謎の関数が使ってあっても証明できる。
Parameter P : (nat -> nat) -> seq nat -> seq nat.
Lemma L3 s : P (fun n => (n + 1) + n) s =
P (fun n => n.+1 + n) s.
Proof.
change (P (fun n => (fun x => x + 1) n + n) s =
P (fun n => n.+1 + n) s).
rewrite (_ : (fun x => x + 1) = (fun x => x.+1)).
by [].
(* (fun x : nat => x + 1) = (fun x : nat => x.+1) *)
apply functional_extensionality => x.
(* x + 1 = x.+1 *)
by rewrite addn1.
Qed.
ここでは、P という中身が謎な関数を使っている中で (束縛変数 n を含む) n + 1 を n.1 に書き換えている
[latest]