Coq/SSReflectで引数の長さが1短い任意の部分列で再帰呼び出しする関数を定義する
はじめに
Coq/SSReflectで再帰関数を定義する際には停止性の証明が必要です。本記事では、リストを引数にとる再帰関数で、長さが引数より1短い任意の部分列に対して再帰呼び出しを行う関数を定義する方法を説明します。
長さが1短い任意の部分列で再帰呼び出しする関数
該当する関数を定義する前に、まず長さが1短い任意の部分列を求める関数pick1sub : forall T:Type, seq T -> seq (T * seq T)を定義します。
FrommathcompRequireImportall_ssreflect.Fixpointpick1sub_rec(T:Type)(tops:seqT):seq(T*seqT):=matchswith|[::]=>[::]|a::s'=>(a,top++s')::sub1seqs_rec(rconstopa)s'end.Definitionpick1sub(T:Type)(s:seqT):=sub1seqs_rec[::]s.pick1subは、以下の例のように引数sに対し、sの各要素とsからそれを除いた部分列の組を返す関数です。pick1sub_recはpick1subを定義するための補助関数です。
Evalcomputeinpick1sub[::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を見ていきます。
SectionAllsubrec.VariableR:Type.Variableidx:R.Variableop:R->R->R.VariableI:Type.Variablef:I->R->R.Lemmaallsubrec_equation(s:seqI):allsubrecs=foldropidx(map(funx=>fx.1(allsubrecx.2))(pick1subs)).pcik1sub sの各要素(x.1, x.2)に対し、x.2の長さはsより1短いので、関数allsubrecは再帰するたびに引数の長さが1短くなります。一見すると常に再帰呼び出しを行う停止しない関数に見えますが、s = [::]のときはfoldrの返り値がidxになるため停止性が言えます。
再帰呼び出しの際、リストの長さが1短くなるので、そのままFunction allsubrec s {measure size s}と定義したくなるのですが、残念ながらそのままではコンパイルが通りません。
(* 定義できず *)Functionallsubrec(s:seqI){measuresizes}:=foldropidx(map(funx=>fx.1(allsubrecx.2))(pick1subs)).(* 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つの関数にまとめることを考えます。
Functionallsubrec_rec(s:seqI*seqI){measure(funs=>measures.1s.2)s}:R:=matchs.2with|[::]=>idx|a::s'=>op(fa(allsubrec_rec([::],s.1++s')))(allsubrec_rec(rconss.1a,s'))end.Proof.-move=>[tops]as'/=->.apply/ltP.exact:allsubrec_measure_lt2.-move=>[tops]as'/=->.apply/ltP.exact:allsubrec_measure_lt1.Defined.(* measure : seq I -> seq I -> natが定義されていて、引数の減少性がそれぞれallsubrec_measure_lt1, lt2で証明できていたとする *)Definitionallsubrec(s:seqI):=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を用いて減少性が証明できます。
LocalNotationmeasuretops:=((sizetop+sizes)^2+sizes).Lemmaallsubrec_measure_lt1top(a:I)s:measure([::]:seqI)(top++s)<measuretop(a::s).Proof.rewrite/=add0n!addnSsize_catltnS!expnS!expn0!muln1mulSn-!addnA.byrewriteaddnCleq_add//mulnSaddnACleq_addl.Qed.Lemmaallsubrec_measure_lt2top(a:I)s:measure(rconstopa)s<measuretop(a::s).Proof.byrewritesize_rconsaddSn/=!addnS.Qed.これで先ほどのallsubrec_rec及びallsubrecの定義が通るようになります。
元の漸化式を満たすことの証明
元の漸化式allsubrec_equationを満たすことは以下の補題から分かります。
Lemmamyallsubrec_rec_equation(tops:seqI):allsubrec_rec(top,s)=foldropidx(map(funx=>fx.1(allsubrec_rec([::],top++x.2)))(pick1subs)).Proof.elim:s=>[|asIHs]intop*=>//.rewriteallsubrec_rec_equation/=.congr(op).rewriteIHs.congr(foldr).rewrite(@map_pick1sub_rec__(funxy=>fx(allsubrec_rec([::],top++y)))).apply:eq_map=>x/=.byrewritecat_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).
*)Lemmaallsubrec_equation(s:seqI):allsubrecs=foldropidx(map(funx=>fx.1(allsubrecx.2))(pick1subs)).Proof.exact:myallsubrec_rec_equation.Qed.EndAllsubrec.使用例
与えられた列の全ての置換を返す関数mypermutations : forall T:Type, seq T -> seq (seq T)はallsubrecを用いて定義できます。
Definitionmypermutations(T:Type)(s:seqT):seq(seqT):=allsubrec[::]cat(funas=>ifsis_::_thenmap(consa)selse[::[::a]])s.Evalcomputeinmypermutations[::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を証明します。
SectionAllsubrec_com.VariableR:eqType.Variableidx:R.Variableop:Monoid.com_lawidx.VariableI:eqType.Variablef:I->R->R.LocalNotationmeasuretops:=((sizetop+sizes)^2+sizes).Lemmaallsubrec_rec_perm(topstoptst:seqI):perm_eqst->perm_eqtopstopt->allsubrec_recidxopf(tops,s)=allsubrec_recidxopf(topt,t).Proof.move:toptt.have[n]:=ubnP(measuretopss).elim:ntopss=>[|NIHn]tops[|as]//=;rewrite?addnSltnS=>Hntopt[|bt]//;trybymove=>/permP/(_predT).move=>Hst.move:{Hst}(perm_memHsta)(perm_memHstb)(Hst).rewrite!in_cons!eq_refl/=eq_sym=>/esym.case:(b=Pa)=>[->__|/=HabHaHbHstHtop].rewrite?perm_cons!allsubrec_rec_cons=>HstHtop.-congr(op(f__)_).+apply:IHn(perm_cat__)_=>//.apply:leq_transHn.rewrite-!addnSaddnS.exact:allsubrec_measure_lt1.+apply:(IHn__(leq_trans_Hn));byrewrite?perm_rcons2//size_rconsaddSn.-rewrite!allsubrec_rec_cons.rewrite(IHn_s(leq_trans_Hn)(rconstopsa)(b::rembs))//;tryexact:perm_to_rem.rewrite(IHn_t(leq_trans_Hn)(rconstoptb)(a::remat))//;tryexact:perm_to_rem.rewrite!allsubrec_rec_consMonoid.mulmCA.congr(op(f__)(op(f__)_));apply:(IHn__(leq_trans_Hn));tryexact:perm_refl.+apply:(leq_trans(allsubrec_measure_lt1_b_)).byrewrite-(perm_size(perm_to_remHb))size_rconsaddSn.+rewritecat_rconsperm_cat//-(perm_consb)(perm_trans_Hst)//.byrewrite-perm_rcons/=perm_consperm_rconsperm_symperm_to_rem.+rewrite-ltnS-![(_+sizes).+1]addnS.exact:allsubrec_measure_lt1.+rewritecat_rconsperm_cat//-(perm_consa)(perm_transHst)//.rewriteperm_sym-perm_rcons/=perm_consperm_rconsperm_sym.exact:perm_to_rem.+apply:(leq_trans(allsubrec_measure_lt2___)).byrewrite-(perm_size(perm_to_remHb))size_rconsaddSn.+rewrite-(perm_consa)(perm_trans_(perm_to_remHa))//.rewrite-(perm_consb)(perm_trans_Hst)//-perm_rcons/=perm_cons.byrewriteperm_rconsperm_symperm_to_rem.+rewriteperm_rcons-rcons_consperm_rconsperm_symperm_rconsperm_cons.byrewriteperm_rconsperm_consperm_sym.+case:(perm_sizeHst)(perm_sizeHtop)=>->->.byrewritesize_rconsaddSn.+byrewritesize_rconsaddSn.Qed.Lemmaallsubrec_permst:perm_eqst->allsubrecidxopfs=allsubrecidxopft.Proof.move=>Hst.exact:allsubrec_rec_perm.Qed.allsubrec_permを示すためには、元の関数allsubrec_recに関する命題を示す必要がありますが、allsubrec_recは2つ引数があり、そのそれぞれが置換であるときに返り値が等しいことを証明しています。
一見すると、片方だけが置換であったときの命題をそれぞれ示せば良さそうですが、今回のケースでは2つの引数が相互に依存するため、両方同時に証明しないと帰納法が回りませんでした。
また、帰納法ですが関数の停止性と同様、measureの減少性を利用した完全帰納法を使っています。具体的には"Coq/SSReflectで{}を使わずに完全帰納法を適用する"
を応用して、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のように記述できることがわかります。
Lemmaallsubrec_rec_equation_commtops:allsubrec_recidxopf(top,s)=foldropidx(map(funa=>fa(allsubrec_recidxopf([::],top++remas)))s).Proof.elim:s=>[|asIHs]intop*=>//=.rewriteallsubrec_rec_conseq_reflIHs.congr(op_(foldr___)).apply/eq_in_map=>bHb.congr(f).apply:allsubrec_rec_perm=>//.rewritecat_rconsperm_cat?perm_refl//.bycase:ifP=>[/eqP->|];rewrite?perm_refl//perm_symperm_to_rem.Qed.Lemmaallsubrec_equation_coms:allsubrecidxopfs=foldropidx(map(funa=>fa(allsubrecidxopf(remas)))s).Proof.exact:allsubrec_rec_equation_com.Qed.rem a sはsの要素のうち、最も先頭に近いaを除く関数なので、重複がある場合は一般に任意の部分列を表現できません。しかし、列の順序に依存しない可換モノイドであれば、この命題が成り立つことがわかります。
まとめ
Coq/SSReflectで引数の長さが1短い任意の部分列で再帰呼び出しする関数の定義や、補題に関して説明しました。
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme