はじめに
Coq/SSReflectにおいて、perm_eqの2つ引数、すなわち置換の関係にある2つの列に対し、ある二項関係が成り立つような命題を帰納法で示したいときの証明方法を説明します。
perm_eqが不変条件であるような命題
例えば以下のような命題です。1
Lemma foldr_addn_perm s t:
perm_eq s t -> foldr addn 0 s = foldr addn 0 t.
foldrはsの構造に関して再帰呼び出しを行う関数なので、単純にsまたはtの構造で帰納法を回したくなりますが、一般にsとtの要素の順番がバラバラなので、帰納法の仮定を使おうとすると仮定にあるperm_eqを示すことが難しい状況になります。
そこで、以下のような帰納原理を考えます。
perm_eqに関する帰納原理
From mathcomp Require Import all_ssreflect.
Lemma perm_ind (T:eqType) (P:seq T -> seq T -> Prop) :
P [::] [::] ->
(forall u s t, P s u -> P u t -> P s t) ->
(forall a s t, P s t -> P (a :: s) (a :: t)) ->
(forall a b s, P [:: a, b & s] [:: b, a & s]) ->
forall s t, perm_eq s t -> P s t.
Pが二項関係を表していて、forall s t, perm_eq s t -> P s tを示すための仮定が並んでいます。
この4つの仮定は任意の置換は互換の積で表せることを表していて、1つ目、3つ目の仮定は置換であるようなs, tの各列に同じ要素を追加しても置換であること、4つ目の仮定が互換を表しています。2つ目の仮定はPの推移性、すなわちここでは複数の互換の組み合わせで記述できることを表しています。
この帰納原理は、仮定に表れるPの引数がconsのみを使って記述されているため、Pが引数の構造に対して再帰的に定義されている場合は示しやすい命題になりやすいという特徴があります。
帰納原理の証明
ではこの帰納原理をどうやって示すかというと、sの長さに関する完全帰納法を使います。
Proof.
move => Hnil Htrans Hcons Hcons2 s.
have [n] := ubnP (size s).
elim : n s =>[|n IHn][|a s]//=;
[by move =>_ t; rewrite perm_sym =>/perm_nilP->|].
rewrite ltnS => Hs [/permP /(_ predT)|b t]// Hperm.
move : (perm_mem Hperm b) (Hperm).
rewrite !in_cons eq_refl =>/=/orP[/eqP->|Hb _].
- rewrite perm_cons =>/(IHn _ Hs). exact : Hcons.
- apply : Htrans (Htrans _ _ _ (Hcons a _ _ (IHn _ Hs _ (perm_to_rem Hb)))
(Hcons2 _ _ _)) (Hcons _ _ _ (IHn _ _ _ _)).
+ rewrite /= size_rem //. by case : s Hs Hb {Hperm}.
+ rewrite -(perm_cons b). apply : perm_trans Hperm.
by rewrite -perm_rcons /= perm_cons perm_rcons perm_sym perm_to_rem.
Qed.
完全帰納法を使っている部分はhave [n] := ubnP (size s). elim n s =>[|n IHn][|a s]の部分です。(詳細はこちらの記事で説明しています。)
証明の流れとしては、まずs = [::]のときはperm_eq s tよりt = [::]が分かるので、1つ目の仮定から示せます。
s = a :: s'のときはt = [::]ではないことが分かるので、いったんt = b :: t'とします。2 ここでa = bのときは仮定3と帰納法の仮定からすぐ示せるので、a <> bのときを考えます。
今a <> bかつperm_eq (a :: s') (b :: t')であるので、b \in s'かつa \in t'が分かります。よって、perm_eq s' (b :: rem b s')が成り立ちます。
すると帰納法の仮定よりP s' (b :: rem b s')とP が成り立ち、仮定3からP (a :: s') [:: a, b & rem b s']が言えます。
仮定4からP [:: a, b & rem b s'] [:: b, a & rem b s']が言えるので、仮定2のPの推移性からP (a :: s') [b :: a & rem b s']が成り立ちます。
あとはP [b :: a & rem b s'] (b :: t')を示せばPの推移性からゴールが示せますが、これは仮定2と帰納法の仮定からperm_eq (a :: rem b s') t'が示せれば良いです。これは両辺にbを加えてあげれば仮定より示せます。
応用例
上で示したのは一般の二項関係に関する命題ですが、示したい命題が等式の場合、もう少し帰納原理が簡単になります。
Lemma perm_eqind (T:eqType) (S:Type) (f:seq T -> S) :
(forall a s t, f s = f t -> f (a :: s) = f (a :: t)) ->
(forall a b s, f [:: a, b & s] = f [:: b, a & s]) ->
forall s t, perm_eq s t -> f s = f t.
Proof.
move => Hcons Hcons2. by apply : perm_ind =>[|u s t->||].
Qed.
この命題も仮定のfの引数にconsしか表れないため、fが引数の列に対して構造的に再帰呼び出しを行う関数である場合に真価を発揮すると思います。実際にこの帰納原理を適用したときはsimplするだけで示すべき等式が表れるはずです。
使用例
最初に例として挙げたfoldr_addn_permを示してみます。
Lemma foldr_addn_perm s t:
perm_eq s t -> foldr addn 0 s = foldr addn 0 t.
Proof.
move : s t. apply : perm_eqind =>[a s t/=->|a b s]//=.
by rewrite addnCA.
Qed.
注意
perm_eqの帰納原理自体は本記事の通りなのですが、以下のような命題を示すときには別の帰納原理を使った方がいいです。
T : eqType
P, Q : seq T -> seq T -> Prop
==============================
forall s t, perm_eq s t -> P s t -> Q s t.
詳細は続編の記事"Coq/SSReflectで"仮定付き"でperm_eqが不変条件となるような命題を示すための帰納原理"をご覧ください。
まとめ
perm_eqが不変条件であるような命題を証明するときに使用する帰納原理について説明しました。この帰納原理の仮定にはconsしか表れず、simplしただけで示すべき命題が表れるような形になりやすいのが特徴です。