#はじめに
Coq/SSReflectで再帰関数を定義する際には停止性の証明が必要です。本記事では、リストを引数にとる再帰関数で、長さが引数より1短い任意の部分列に対して再帰呼び出しを行う関数を定義する方法を説明します。
#長さが1短い任意の部分列で再帰呼び出しする関数
該当する関数を定義する前に、まず長さが1短い任意の部分列を求める関数pick1sub : forall T:Type, seq T -> seq (T * seq T)を定義します。
From mathcomp Require Import all_ssreflect.
Fixpoint pick1sub_rec (T:Type) (top s:seq T) : seq (T * seq T) :=
match s with
| [::] => [::]
| a :: s' => (a,top ++ s') :: sub1seqs_rec (rcons top a) s'
end.
Definition pick1sub (T:Type) (s:seq T) := sub1seqs_rec [::] s.
pick1subは、以下の例のように引数sに対し、sの各要素とsからそれを除いた部分列の組を返す関数です。pick1sub_recはpick1subを定義するための補助関数です。
Eval compute in pick1sub [:: 1; 2; 3; 4].
(* = [:: (1,[:: 2; 3; 4]); (2,[:: 1; 3; 4]); (3,[:: 1; 2; 4]), (4,[:: 1; 2; 3])] *)
これを用いて、本記事で定義したい関数allsubrec : seq I -> Rが満たすべき漸化式allsubrec_equationを見ていきます。
Section Allsubrec.
Variable R:Type.
Variable idx:R.
Variable op:R -> R -> R.
Variable I:Type.
Variable f:I -> R -> R.
Lemma allsubrec_equation (s:seq I) :
allsubrec s =
foldr op idx (map (fun x => f x.1 (allsubrec x.2)) (pick1sub s)).
pcik1sub sの各要素(x.1, x.2)に対し、x.2の長さはsより1短いので、関数allsubrecは再帰するたびに引数の長さが1短くなります。一見すると常に再帰呼び出しを行う停止しない関数に見えますが、s = [::]のときはfoldrの返り値がidxになるため停止性が言えます。
再帰呼び出しの際、リストの長さが1短くなるので、そのままFunction allsubrec s {measure size s}と定義したくなるのですが、残念ながらそのままではコンパイルが通りません。
(* 定義できず *)
Function allsubrec (s:seq I) {measure size s} :=
foldr op idx (map (fun x => f x.1 (allsubrec x.2)) (pick1sub s)).
(* the term fun x : I * seq I => f x.1 (allsubrec x.2) can not contain a recursive call to allsubrec *)
これは、再帰呼び出しを行う関数allsubrecの減少する引数が内部関数(fun x => f x.1 (allsubrec x.2))のローカル変数xに依存するためです。1
それではこれを書き直して、定義が通るようにします。
#再帰関数を定義する
先ほどの例では、部分列を求めるpick1subを外に定義し、それに対してfoldrを行っていたため、引数の減少性が分からない状態になっていました。そこでpick1subとfoldrを1つの関数にまとめることを考えます。
Function allsubrec_rec (s:seq I * seq I)
{measure (fun s => measure s.1 s.2) s} : R :=
match s.2 with
| [::] => idx
| a :: s' => op (f a (allsubrec_rec ([::],s.1 ++ s')))
(allsubrec_rec (rcons s.1 a,s'))
end.
Proof.
- move =>[top s] a s' /=->. apply /ltP. exact : allsubrec_measure_lt2.
- move =>[top s] a s' /=->. apply /ltP. exact : allsubrec_measure_lt1.
Defined.
(* measure : seq I -> seq I -> natが定義されていて、引数の減少性がそれぞれallsubrec_measure_lt1, lt2で証明できていたとする *)
Definition allsubrec (s:seq I) := allsubrec_rec ([::],s).
問題は減少性をどのように証明するかです。引数は(size s.1 + size s.2, size s.2)の辞書式順序で小さくなっているので、"Coq/SSReflectで辞書式順序で引数が構成的に小さくなる再帰関数をFixpointで定義する"の手法が使えるように見えますが、size s.1 + size s.2の部分は構造的に小さくなるとは限らないためこの方法は使えません。そこで今回はFunctionで定義します。2
Functionで定義するためにはmeasure関数が必要です。しかし、一般の辞書式順序に対し、順序を保存する自然数への写像は存在しません。3 しかしながら、第二引数に上界が存在する場合は順序を保存する自然数への写像を定義することができます。
今回のケースでは、再帰を行う第二引数s.2は最大でもsize s.1 + size s.2以下の長さにしかなりません。すなわち、以下のようなmeasure : seq I -> seq I -> natを用いて減少性が証明できます。
Local Notation measure top s := ((size top + size s) ^ 2 + size s).
Lemma allsubrec_measure_lt1 top (a:I) s :
measure ([::]:seq I) (top ++ s) < measure top (a :: s).
Proof.
rewrite /= add0n !addnS size_cat ltnS !expnS !expn0 !muln1 mulSn -!addnA.
by rewrite addnC leq_add // mulnS addnAC leq_addl.
Qed.
Lemma allsubrec_measure_lt2 top (a:I) s :
measure (rcons top a) s < measure top (a :: s).
Proof.
by rewrite size_rcons addSn /= !addnS.
Qed.
これで先ほどのallsubrec_rec及びallsubrecの定義が通るようになります。
##元の漸化式を満たすことの証明
元の漸化式allsubrec_equationを満たすことは以下の補題から分かります。
Lemma myallsubrec_rec_equation (top s:seq I) :
allsubrec_rec (top,s) =
foldr op idx
(map (fun x => f x.1 (allsubrec_rec ([::],top ++ x.2)))
(pick1sub s)).
Proof.
elim : s =>[|a s IHs] in top *=>//. rewrite allsubrec_rec_equation /=.
congr(op). rewrite IHs. congr(foldr).
rewrite (@map_pick1sub_rec
_ _ (fun x y => f x (allsubrec_rec ([::], top ++ y)))).
apply : eq_map => x /=. by rewrite cat_rcons.
Qed.
(* ただし
Lemma map_pick1sub_rec (T S:Type) (f:T -> seq T -> S) top s :
map (fun x => f x.1 x.2) (pick1sub_rec top s) =
map (fun x => f x.1 (top ++ x.2)) (pick1sub s).
*)
Lemma allsubrec_equation (s:seq I) :
allsubrec s =
foldr op idx (map (fun x => f x.1 (allsubrec x.2)) (pick1sub s)).
Proof.
exact : myallsubrec_rec_equation.
Qed.
End Allsubrec.
#使用例
与えられた列の全ての置換を返す関数mypermutations : forall T:Type, seq T -> seq (seq T)はallsubrecを用いて定義できます。
Definition mypermutations (T:Type) (s:seq T) : seq (seq T) :=
allsubrec [::] cat
(fun a s => if s is _ :: _ then map (cons a) s else [:: [:: a]]) s.
Eval compute in mypermutations [:: 1; 2; 3].
(* = [[1; 2; 3]; [1; 3; 2]; [2; 1; 3]; [2; 3; 1]; [3; 1; 2]; [3; 2; 1]] *)
#応用
##可換モノイドの場合
op:R -> R -> Rが可換モノイドの演算だった場合、allsubrecの返り値は引数の列は順序によらず等しくなることが分かります。これを表す命題allsubrec_permを証明します。
Section Allsubrec_com.
Variable R:eqType.
Variable idx:R.
Variable op:Monoid.com_law idx.
Variable I:eqType.
Variable f:I -> R -> R.
Local Notation measure top s := ((size top + size s) ^ 2 + size s).
Lemma allsubrec_rec_perm (tops topt s t:seq I) :
perm_eq s t ->
perm_eq tops topt ->
allsubrec_rec idx op f (tops,s) = allsubrec_rec idx op f (topt,t).
Proof.
move : topt t.
have [n] := ubnP (measure tops s).
elim : n tops s =>[|N IHn] tops [|a s]//=; rewrite ?addnS ltnS
=> Hn topt [|b t]//; try by move =>/permP /(_ predT).
move => Hst. move : {Hst} (perm_mem Hst a) (perm_mem Hst b) (Hst).
rewrite !in_cons !eq_refl /= eq_sym =>/esym.
case : (b =P a) =>[->_ _|/= Hab Ha Hb Hst Htop].
rewrite ?perm_cons !allsubrec_rec_cons => Hst Htop.
- congr(op (f _ _) _).
+ apply : IHn (perm_cat _ _) _=>//. apply : leq_trans Hn.
rewrite -!addnS addnS. exact : allsubrec_measure_lt1.
+ apply : (IHn _ _ (leq_trans _ Hn));
by rewrite ?perm_rcons2 // size_rcons addSn.
- rewrite !allsubrec_rec_cons.
rewrite (IHn _ s (leq_trans _ Hn) (rcons tops a) (b :: rem b s)) //;
try exact : perm_to_rem.
rewrite (IHn _ t (leq_trans _ Hn) (rcons topt b) (a :: rem a t)) //;
try exact : perm_to_rem.
rewrite !allsubrec_rec_cons Monoid.mulmCA.
congr(op (f _ _) (op (f _ _) _));
apply : (IHn _ _ (leq_trans _ Hn)); try exact : perm_refl.
+ apply : (leq_trans (allsubrec_measure_lt1 _ b _)).
by rewrite -(perm_size (perm_to_rem Hb)) size_rcons addSn.
+ rewrite cat_rcons perm_cat // -(perm_cons b) (perm_trans _ Hst) //.
by rewrite -perm_rcons /= perm_cons perm_rcons perm_sym perm_to_rem.
+ rewrite -ltnS -![(_ + size s).+1]addnS. exact : allsubrec_measure_lt1.
+ rewrite cat_rcons perm_cat // -(perm_cons a) (perm_trans Hst) //.
rewrite perm_sym -perm_rcons /= perm_cons perm_rcons perm_sym.
exact : perm_to_rem.
+ apply : (leq_trans (allsubrec_measure_lt2 _ _ _)).
by rewrite -(perm_size (perm_to_rem Hb)) size_rcons addSn.
+ rewrite -(perm_cons a) (perm_trans _ (perm_to_rem Ha)) //.
rewrite -(perm_cons b) (perm_trans _ Hst) // -perm_rcons /= perm_cons.
by rewrite perm_rcons perm_sym perm_to_rem.
+ rewrite perm_rcons -rcons_cons perm_rcons perm_sym perm_rcons perm_cons.
by rewrite perm_rcons perm_cons perm_sym.
+ case : (perm_size Hst) (perm_size Htop) =>->->.
by rewrite size_rcons addSn.
+ by rewrite size_rcons addSn.
Qed.
Lemma allsubrec_perm s t :
perm_eq s t -> allsubrec idx op f s = allsubrec idx op f t.
Proof.
move => Hst. exact : allsubrec_rec_perm.
Qed.
allsubrec_permを示すためには、元の関数allsubrec_recに関する命題を示す必要がありますが、allsubrec_recは2つ引数があり、そのそれぞれが置換であるときに返り値が等しいことを証明しています。
一見すると、片方だけが置換であったときの命題をそれぞれ示せば良さそうですが、今回のケースでは2つの引数が相互に依存するため、両方同時に証明しないと帰納法が回りませんでした。
また、帰納法ですが関数の停止性と同様、measureの減少性を利用した完全帰納法を使っています。具体的には"[Coq/SSReflectで{}を使わずに完全帰納法を適用する]
(https://qiita.com/nekonibox/items/8147291e9fd483e3d579)"を応用して、`have [n] := ubnP (measure top s). elim : n tops s =>[|n IHn] tops [|a s]`のように記述します。
証明の方針ですが、perm_eqに関する証明には"Coq/SSReflectでperm_eqが不変条件であるような命題を証明するための帰納原理"のようにコツがあり、
sとtがそれぞれa :: s', b :: t'のとき、a = bのときは帰納法の仮定がそのまま使えば示せます。a <> bのときは、b \in s'かつ``a \in t'のはずなので、perm_eq s' (b :: rem b s')`かつ`perm_eq t' (a :: rem a t')`が成り立ちます。
よって、`perm_trans`より`a :: b :: rem a s'`と`b :: a :: rem b t'`に関して示せばいいので、`rem a s'`と`rem b t'`に関する帰納法の仮定を使えます。
この補題により、漸化式が以下のallsubrec_equation_commのように記述できることがわかります。
Lemma allsubrec_rec_equation_comm top s :
allsubrec_rec idx op f (top,s) =
foldr op idx
(map (fun a => f a (allsubrec_rec idx op f ([::],top ++ rem a s))) s).
Proof.
elim : s =>[|a s IHs] in top *=>//=.
rewrite allsubrec_rec_cons eq_refl IHs. congr(op _ (foldr _ _ _)).
apply /eq_in_map => b Hb. congr(f). apply : allsubrec_rec_perm =>//.
rewrite cat_rcons perm_cat ?perm_refl //.
by case : ifP =>[/eqP->|]; rewrite ?perm_refl // perm_sym perm_to_rem.
Qed.
Lemma allsubrec_equation_com s:
allsubrec idx op f s =
foldr op idx (map (fun a => f a (allsubrec idx op f (rem a s))) s).
Proof.
exact : allsubrec_rec_equation_com.
Qed.
rem a sはsの要素のうち、最も先頭に近いaを除く関数なので、重複がある場合は一般に任意の部分列を表現できません。しかし、列の順序に依存しない可換モノイドであれば、この命題が成り立つことがわかります。
#まとめ
Coq/SSReflectで引数の長さが1短い任意の部分列で再帰呼び出しする関数の定義や、補題に関して説明しました。