Coq/SSReflectでperm_eqが不変条件であるような命題を証明するための帰納原理

# はじめに

Coq/SSReflectにおいて、perm_eqの2つ引数、すなわち置換の関係にある2つの列に対し、ある二項関係が成り立つような命題を帰納法で示したいときの証明方法を説明します。


# `perm_eq`が不変条件であるような命題

例えば以下のような命題です。[^1]

[^1]: この命題自体は`foldrE`で`bigop`に書き換えて`perm_big`を使っても示せますが、一般的な方法についての例として考えていただけると幸いです。

```coq
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に関する帰納原理

```coq
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`の長さに関する完全帰納法を使います。

```coq
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]`の部分です。(詳細は[こちらの記事](https://qiita.com/nekonibox/items/8147291e9fd483e3d579)で説明しています。)

証明の流れとしては、まず`s = [::]`のときは`perm_eq s t`より`t = [::]`が分かるので、1つ目の仮定から示せます。
`s = a :: s'`のときは`t = [::]`ではないことが分かるので、いったん`t = b :: t'`とします。[^2] ここで`a = b`のときは仮定3と帰納法の仮定からすぐ示せるので、`a <> b`のときを考えます。

[^2]: この時点で`a \in t`ですが、`size t = size s`よりこのままでは帰納法の仮定が使えないため、いったん`t = b :: t'`とする必要があります。

今`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`を加えてあげれば仮定より示せます。


## 応用例

上で示したのは一般の二項関係に関する命題ですが、示したい命題が等式の場合、もう少し帰納原理が簡単になります。

```coq
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`を示してみます。

```coq
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`の帰納原理自体は本記事の通りなのですが、以下のような命題を示すときには別の帰納原理を使った方がいいです。

```coq
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が不変条件となるような命題を示すための帰納原理](https://qiita.com/nekonibox/items/72ba7c69ac117195af2e)"をご覧ください。

# まとめ

`perm_eq`が不変条件であるような命題を証明するときに使用する帰納原理について説明しました。この帰納原理の仮定には`cons`しか表れず、`simpl`しただけで示すべき命題が表れるような形になりやすいのが特徴です。