以下の発表を行った。
以下の発表を行った。
再帰関数に対して、その関数専用の induction principle を作る Functional Scheme というコマンドがある。
試しに使ってみよう。
まず、div2 関数を定義する。
From mathcomp Require Import all_ssreflect. Require Import FunInd. Fixpoint div2 (n:nat) : nat := match n with | O => 0 | S O => 0 | S (S n') => S (div2 n') end.
この関数はリファレンスマニュアルに書いてあるとおりの例である。
ここで、forall m, div2 m <= m という命題を証明したいとしよう。 (この命題もリファレンスマニュアルに書いてあるのとほぼ同じだが、 こっちは ssreflect なので実際には微妙に異なる)
普通に (m について) 帰納法を使うとうまくいかない。 これは、(ペアノの自然数としての) m の構造と、 div2 の再帰の構造が異なるからである。 div2 n <= n を仮定して div2 n.+1 <= n.+1 を証明しろといわれても困る。 .+1 じゃなくて .+2 ならうまくいくんだけど。
Goal forall m, div2 m <= m.
Proof.
elim.
by [].
move=> n.
(* div2 n <= n -> div2 n.+1 <= n.+1 *)
simpl.
Abort.
個人的に、こういうときには完全帰納法をつかっていた。 自然数に対する完全帰納法は Wf_nat.lt_wf_ind にあるので、 これを使えば証明できる。
Goal forall m, div2 m <= m.
Proof.
move=> m.
pattern m.
apply Wf_nat.lt_wf_ind => {m}.
case; first by [].
case; first by [].
move=> n IH /=.
apply ltnW.
apply IH.
by apply/ltP.
Qed.
まぁ、自然数の場合は完全帰納法でとくに問題はないと思うのだが、 自然数でない場合には完全帰納法 (ないし整礎帰納法) が あらかじめ用意されているとは限らない。
そういうときのために、 関数の構造にあわせた induction principle を作ってくれる Functional Scheme があるのだろう。たぶん。
というわけで、Functional Scheme を使ってみよう。 呼び出してみると、div2_equation と div2_ind が定義されたと出てくる。
Functional Scheme div2_ind := Induction for div2 Sort Prop. (* div2_equation is defined div2_ind is defined *)
div2_equation と div2_ind がどういうものか表示してみる。 div2_equation が div2 を一段階展開する書き換えに使える定理になっている。 div2_ind は div2 の構造に対応した induction principle になっている。
About div2_equation. (* div2_equation :
forall n : nat, div2 n = match n with
| n'.+2 => (div2 n').+1
| _ => 0
end
*)
About div2_ind. (* div2_ind :
forall P : nat -> nat -> Prop,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0) ->
(forall n n0 : nat,
n = n0.+1 ->
forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
forall n : nat, P n (div2 n)
*)
div2_ind を使うと、div2 m <= m は以下のように証明できる。
Goal forall m, div2 m <= m.
Proof.
move=> m.
functional induction (div2 m).
by [].
by [].
by apply ltnW.
Qed.
さて、div2_ind の中身がどんなものか表示してみると、ちょっと大きくて読みたくない感じである。
Print div2_ind. (* div2_ind =
fun (P : nat -> nat -> Prop) (f1 : forall n : nat, n = 0 -> P 0 0)
(f0 : forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0)
(f : forall n n0 : nat,
n = n0.+1 ->
forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
fix div3 (n : nat) : P n (div2 n) :=
@eq_ind_r nat match n with
| n'.+2 => (div2 n').+1
| _ => 0
end [eta P n]
(let f2 : n = 0 -> P 0 0 := f1 n in
let f3 : forall n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0 := f0 n in
let f4 :
forall n0 : nat,
n = n0.+1 ->
forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1 :=
f n in
match
n as n0
return
(n = n0 ->
(forall n1 : nat,
n0 = n1.+1 ->
forall n' : nat, n1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
(forall n1 : nat, n0 = n1.+1 -> n1 = 0 -> P 1 0) ->
(n0 = 0 -> P 0 0) ->
P n0 match n0 with
| n'.+2 => (div2 n').+1
| _ => 0
end)
with
| 0 =>
fun (_ : n = 0)
(_ : forall n0 : nat,
0 = n0.+1 ->
forall n' : nat,
n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1)
(_ : forall n0 : nat, 0 = n0.+1 -> n0 = 0 -> P 1 0)
(f7 : 0 = 0 -> P 0 0) => unkeyed (f7 (erefl 0))
| n0.+1 =>
fun (_ : n = n0.+1)
(f5 : forall n1 : nat,
n0.+1 = n1.+1 ->
forall n' : nat,
n1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1)
(f6 : forall n1 : nat, n0.+1 = n1.+1 -> n1 = 0 -> P 1 0)
(_ : n0.+1 = 0 -> P 0 0) =>
let f8 : n0 = 0 -> P 1 0 :=
let n1 := n0 in let H : n0.+1 = n1.+1 := erefl n0.+1 in f6 n1 H in
let f9 :
forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1 :=
let n1 := n0 in let H : n0.+1 = n1.+1 := erefl n0.+1 in f5 n1 H in
match
n0 as n1
return
(n0 = n1 ->
(n1 = 0 -> P 1 0) ->
(forall n' : nat,
n1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
P n1.+1 match n1 with
| 0 => 0
| n'.+1 => (div2 n').+1
end)
with
| 0 =>
fun (_ : n0 = 0) (f10 : 0 = 0 -> P 1 0)
(_ : forall n' : nat,
0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
unkeyed (f10 (erefl 0))
| n1.+1 =>
fun (_ : n0 = n1.+1) (_ : n1.+1 = 0 -> P 1 0)
(f11 : forall n' : nat,
n1.+1 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) =>
let f12 : P n1 (div2 n1) -> P n1.+2 (div2 n1).+1 :=
let n' := n1 in let H : n1.+1 = n'.+1 := erefl n1.+1 in f11 n' H
in
unkeyed (let Hrec : P n1 (div2 n1) := div3 n1 in f12 Hrec)
end (erefl n0) f8 f9
end (erefl n) f4 f3 f2) (div2 n) (div2_equation n)
: forall P : nat -> nat -> Prop,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0) ->
(forall n n0 : nat,
n = n0.+1 ->
forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
forall n : nat, P n (div2 n)
*)
とりあえず Print Assumptions div2_ind. として公理に依存していないことは確認できる。
Print Assumptions div2_ind. (* Closed under the global context *)
div2_equation も表示してみると、こちらはそれほど大きくない。
Print div2_equation. (* div2_equation =
fun n : nat =>
match
n as n0 return (div2 n0 = match n0 with
| n'.+2 => (div2 n').+1
| _ => 0
end)
with
| 0 => erefl 0
| n0.+1 => erefl match n0 with
| 0 => 0
| n'.+1 => (div2 n').+1
end
end
: forall n : nat, div2 n = match n with
| n'.+2 => (div2 n').+1
| _ => 0
end
*)
div2_equation 相当の定理を tactic で証明しなおしてみると、以下のようになる。 左辺を一段階展開したものが右辺なので、 そのまま reflexivity 一発、といきそうなものだが実際にはそうはいかない。 再帰関数 (fix項) を展開するには (展開してないものと展開したものが convertible になるという iota reduction では) decreasing argument の頭部が constructor であるという条件が必要で、 そのためには、div2 の (内部にある fix項の) 引数の n を場合分けして 頭部を constructor にする必要がある。 そうしてしまえばあとは問題ない。
Lemma div2_equation' : forall n : nat,
div2 n = match n with
| n'.+2 => (div2 n').+1
| _ => 0
end.
Proof.
by case.
Defined.
もともとの div2_equation と証明し直した div2_equation' は以下のように等しい。 (というか、等しくなるように証明を作ったのだが)
Goal div2_equation = div2_equation'. Proof. reflexivity. Qed.
div2_ind も同様に証明しなおしてみよう。 大きな証明項は読みたくないのだが、がんばって読んでやってみたところ、 証明項に比べてずいぶんと小さくなった。
Lemma div2_ind' : forall P : nat -> nat -> Prop,
(forall n : nat, n = 0 -> P 0 0) ->
(forall n n0 : nat, n = n0.+1 -> n0 = 0 -> P 1 0) ->
(forall n n0 : nat,
n = n0.+1 ->
forall n' : nat, n0 = n'.+1 -> P n' (div2 n') -> P n'.+2 (div2 n').+1) ->
forall n : nat, P n (div2 n).
Proof.
move=> P H0 H1 H2.
fix IH 1 => n.
rewrite div2_equation'.
move: (H2 n) (H1 n) (H0 n) => {H2 H1 H0}.
case_eq n => {n} [|n] _ H2 H1 H0; first by apply H0.
move: (H1 n erefl) (H2 n erefl) => {H2 H1 H0}.
case_eq n => {n} [|n] _ H1 H2; first by apply H1.
apply (H2 n erefl).
by apply IH.
Defined.
これも、元の証明 div2_ind と証明し直した div2_ind' は等しくなっていることが確認できる。
Goal div2_ind = div2_ind'. Proof. reflexivity. Qed.
div2_ind' の (tactic のほうの) 証明を見直すと、結局、 (fix tactic で作った) 再帰関数の中で、まず div2_equation で一段階 div2 を展開し、 引数を (div2 の分岐の構造と同じ構造で) 場合分けして証明を行っていることがわかる。
2019-04-26: 証明を簡単にしたり、説明を書き足したりした
どんな再帰関数でも Functional Scheme で induction principle を作れるのか、 というと、きっと無理だと思う。
で、具体的な例を作ってみた。
From mathcomp Require Import all_ssreflect. Require Import FunInd. Fixpoint div2 (n:nat) : nat := match n with | O => 0 | S O => 0 | S (S n') => S (div2 n') end.
以下の div2' が Functional Scheme が対応できない例である。
Fixpoint div2' (n:nat) : nat := let f m := match m with | O => 0 | S m' => S (div2' m') end in match n with | O => 0 | S n' => f n' end.
div2' は、じつは div2 と convertible である。 (内側の match を関数として括り出しただけなので)
Goal div2 = div2'. Proof. reflexivity. Qed.
で、div2' に Functional Scheme を適用すると、エラーになる。
Fail Functional Scheme div2'_ind := Induction for div2' Sort Prop. (* Cannot define graph(s) for div2' *)
マニュアル (5.2.2 Generation of induction principles with Functional Scheme) を 読み直してみたが、どういう場合にうまくいって、どういう場合にうまくいかないのかは 書いてないなぁ。
エラーメッセージをみると、なんかグラフを作れないみたいなので、 そのグラフがどういうものなのかわかればいいのかな。
Functional Scheme に関する論文を探してみたところ、たぶん以下だと思う。
Gilles Barthe, Pierre Courtieu. Efficient reasoning about executable specifications in Coq. Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002 Hampton, VA, USA, August 20–23, 2002 Proceedings (pp.31-46). http://cedric.cnam.fr/~courtiep/papers/barthe-courtieu-tphol2002.pdf
文法が今の Coq と違うようだ。
それはそれとして、let の束縛の中に match (古い文法では Case) が出てくる場合は 考慮されていない感じではある。
しかし、グラフについては触れてないと思う。
[latest]