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

# はじめに

前回、[Coq/SSReflectでperm_eqが不変条件となるような命題を証明するための帰納原理](https://qiita.com/nekonibox/items/233d23bf0fb7cad79e01)を掲載しましたが、`perm_eq`以外の仮定がある状態で帰納法を適用したいとき、この帰納原理`perm_ind`をそのまま使うと証明が困難になります。

そこで本記事では、他の仮定がある状態で`perm_eq`が不変条件となるような命題を証明するときの別の帰納原理を紹介します。

ソースコードは[こちら](https://github.com/nekonistyle/Qiita_example/blob/main/perm_ind/perm_ind.v)です。


# 仮定付きの`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.
```

`s`と`t`が`perm_eq s t`であり、仮定`P s t`の下で`Q s t`が成り立つような命題です。
これを証明する際に使う帰納原理を見ていきます。

まず、通常の`perm_eq`の帰納原理を確認します。


# `perm_eq`の帰納原理とは

`perm_eq`の帰納原理は以下になります。(詳細は[前回の記事](https://qiita.com/nekonibox/items/233d23bf0fb7cad79e01)で解説しています)

```coq
  Lemma perm_ind (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.
```

これは、任意の置換が互換の積で表せることを利用した帰納原理になっています。


## 仮定付きの命題を`perm_ind`で証明するのが困難な理由


しかしながら、この帰納原理で以下のような命題を証明しようとしたとき、その仮定を示すのが困難になります。

先ほどの示したい命題を再掲します。

```coq
T : eqType
P, Q : seq T -> seq T -> Prop
==============================
forall s t, perm_eq s t -> P s t -> Q s t.
```

この命題に対して、以下のように単純に`perm_ind`を適用すると、

```coq
    apply : perm_ind.
 (* apply : (@perm_ind (fun s t => P s t -> Q s t)). *)
```

以下の命題を全て示すことになります。

```coq
T : eqType
P, Q : seq T -> seq T -> Prop
==============================
P [::] [::] -> R [::] [::]

subgoal 2 is:
  forall u s t, (P s u -> Q s u) -> (P u t -> Q u t) -> P s t -> Q s t
subgoal 3 is:
  forall a s t, (P s t -> Q s t) -> P (a :: s) (a :: t) -> Q (a :: s) (a :: t)
subgoal 4 is:
  forall a b s, P [:: a, b & s] [:: b, a & s] -> Q [:: a, b & s] [:: b, a & s]
```

特に`subgoal 2`を示すのが困難になります。

なぜなら、`Q s t`を示すのに`Q s u`と`Q u t`が欲しい場合、`P s u`と`P u t`が必要ですが、これを`P s t`から示さないといけません。
今、`u`は任意の変数なので、もし`P s t`から`P s u`と`P u t`が示せるとすると、`forall u, P s t -> P s u`と`forall u, P s t -> P u t`が示せることになりますが、ここで`s`と`t`も任意の変数であることを考えると、実質的には`forall s t, P s t -> forall s t, P s t`が成り立っていることになります。

一見するとこの命題はトートロジーですが、実際にはそうではなく、排中律を仮定すると`(forall s t, P s t) \/ forall s t, ~ P s t`と同値になります。
つまり、これが成り立つのは`P s t`が恒等的に`True`か`False`の場合のみです。

それ以外の場合は、`Q s u`か`Q u t`のどちらかの仮定は使えないので、この命題を示すのは困難になります。

なぜこのようなことが起こっているかというと、元々2番目の仮定は`Q`の推移性を言っているだけで、再帰部分というよりは`Q`の満たす性質に対する仮定だからです。
したがって、その性質には登場しない仮定`P`がむしろ邪魔をしているわけです。

そこで、この問題を解決するような帰納原理を考えてみます。


# 仮定付きの`perm_eq`の帰納原理

以下のような帰納原理を使います。

```coq
  Lemma perm_imply_ind (P Q:seq T -> seq T -> Prop) :
    (forall s t, perm_eq s t -> forall u, P s u -> P t u) ->
    (forall s t, perm_eq s t -> forall u, P u s -> P u t) ->
    (forall a s t, P (a :: s) (a :: t) -> P s t) ->
    (P [::] [::] -> Q [::] [::]) ->
    (forall u s t, Q s u -> Q u t -> Q s t) ->
    (forall a s t, P (a :: s) (a :: t) -> Q s t -> Q (a :: s) (a :: t)) ->
    (forall a b s,
        P [:: a, b & s] [:: b, a & s] -> Q [:: a, b & s] [:: b, a & s]) ->
    forall s t, perm_eq s t -> P s t -> Q s t.
```

7つある仮定のうち、上3つが`P`に関する仮定で、下4つは元々の`perm_eq`の帰納原理の一部に`P`に関する仮定を追加したものです。

具体的には、上3つのうち、
1つ目と2つ目は`P`の第1引数、第2引数はそれぞれ置換であるような変数と入れ替えても`P`が成り立つこと、
3つ目は先頭要素が等しい場合はそれを除いても`P`が成り立つことを意味しています。

また、結論`Q`に関する仮定において、
5つ目の`Q`の推移性に関しては元の`perm_ind`と同じですが、
6つ目と7つ目の再帰部分は、その結論`Q (a :: s) (a :: t)`と`Q [:: b, a & s] t`と同じ引数の`P`に対する仮定が追加されています。


これにより、帰納法の仮定に`P`に関する仮定を追加しながら結論`Q`に関する命題を示すことができます。

この命題の証明自体は前回と同様、`s`の長さに関する完全帰納法で示すことができます。

```coq
  Proof.
    move => HPl HPr HPcons 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 _ HPas].
    - rewrite perm_cons => Hpst HPst.
      exact : Hcons HPst (IHn _ Hs _ Hpst (HPcons _ _ _ HPst)).
    - move : (perm_Wl HPl Hperm HPas) (perm_Wr HPr Hperm HPas) (perm_to_rem Hb)
      => HpPl HpPr Hsb.
      have Hbas : perm_eq [:: b, a & rem b s] (b :: t)
        by apply : perm_trans Hperm;
        rewrite -perm_rcons /= perm_cons perm_rcons perm_sym.
      move : (Hsb). rewrite -(perm_cons a) => Hpasr.
      move : (HpPr _ Hpasr) => HPasr.
      apply : (Htrans _ _ _
                (Hcons _ _ _ HPasr (IHn _ Hs _ Hsb (HPcons _ _ _ HPasr)))).
      apply : Htrans (Hcons2 _ _ _ _) _; [|apply : Hcons; [|apply /IHn]].
      + apply : HPl Hpasr _ (HpPr _ _).
          by rewrite perm_sym -perm_rcons /= perm_cons perm_rcons perm_sym.
      + exact : HpPl.
      + rewrite /= (size_rem Hb).
          by case : s Hb Hs {Hperm HPas HpPr Hsb Hbas Hpasr HPasr}.
      + by rewrite -(perm_cons b).
      + exact : HPcons (HpPl _ _).
  Qed.
```

ただし、

```coq
  Lemma perm_Wr (P:seq T -> seq T -> Prop):
    (forall s t, perm_eq s t -> forall u, P u s -> P u t) ->
    forall s t, perm_eq s t -> P s t -> forall u, perm_eq s u -> P s u.

  Lemma perm_Wl (P:seq T -> seq T -> Prop):
    (forall s t, perm_eq s t -> forall u, P s u -> P t u) ->
    forall s t, perm_eq s t -> P s t -> forall u, perm_eq u t -> P u t.
```

です。

帰納原理の証明ですが、
`have [n] := ubnP (size s)`をして、任意の`s`に関して`n`に関する帰納法を使うと`size s`に関する完全帰納法になります。
詳細は[Coq/SSReflectで{}を使わずに完全帰納法を適用する](https://qiita.com/nekonibox/items/8147291e9fd483e3d579)をご覧ください。


## 仮定が1変数の場合

もし、示すべき命題の仮定`P`が1変数の場合でも、その帰納原理は`perm_imply_ind`からすぐ示すことができます。

```coq
 Lemma perm_imply1l_ind (P:seq T -> Prop) (Q:seq T -> seq T -> Prop) :
    (forall s t, perm_eq s t -> P s -> P t) ->
    (forall a s, P (a :: s) -> P s) ->
    (P [::] -> Q [::] [::]) ->
    (forall u s t, Q s u -> Q u t -> Q s t) ->
    (forall a s t, P (a :: s) -> Q s t -> Q (a :: s) (a :: t)) ->
    (forall a b s, P [:: a, b & s] -> Q [:: a, b & s] [:: b, a & s]) ->
    forall s t, perm_eq s t -> P s -> Q s t.
  Proof.
    move => HP HPcons Hnil Htrans Hcons Hcons2.
    apply : (@perm_imply_ind (fun s t => P s)) =>[s t Hst _||a s _||||]//.
    - exact : HP.
    - exact : HPcons.
  Qed.
```

```coq
  Lemma perm_imply1r_ind (P:seq T -> Prop) (Q:seq T -> seq T -> Prop) :
    (forall s t, perm_eq s t -> P s -> P t) ->
    (forall a s, P (a :: s) -> P s) ->
    (P [::] -> Q [::] [::]) ->
    (forall u s t, Q s u -> Q u t -> Q s t) ->
    (forall a s t, P (a :: t) -> Q s t -> Q (a :: s) (a :: t)) ->
    (forall a b s, P [:: b, a & s] -> Q [:: a, b & s] [:: b, a & s]) ->
    forall s t, perm_eq s t -> P t -> Q s t.
  Proof.
    move => HP HPcons Hnil Htrans Hcons Hcons2.
    apply : (@perm_imply_ind (fun s t => P t)) =>[|s t Hst _|a _||||]//.
    - exact : HP.
    - exact : HPcons.
  Qed.
```


# 適用例

仮定付きで`perm_eq`が不変条件になるような命題として、例えば以下のようなものが挙げられます。

```coq
  Fixpoint spick (P:pred T) (s:seq T) : option T :=
    if s is x :: s' then if P x then Some x else spick P s' else None.
(* = ohead [seq x <- s | P x] *)

  Lemma perm_map_spick (S:eqType) (f:T -> S) (s1 s2:seq T):
    perm_eq s1 s2 -> uniq [seq f x | x <- s1] ->
    forall y, spick (eq_op^~ y \o f) s1 = spick (eq_op^~ y \o f) s2.
(* eq_op^~ y \o f = fun x => f x == y *)
```

これは、置換であるリスト`s1`、`s2`に対して、関数`f`で`s1`を写した先が`uniq`ならば、`s1`と`s2`をそれぞれ関数`f`で写した先が`y`と一致するような元1つを`spick`で取ってきたとき、その2つが一致すると言う命題です。
この命題は`uniq [seq f x | x <- s1]`の仮定がないと一般に成り立ちません。

証明ですが、先ほどの1変数の仮定があるときに使える帰納原理`perm_imply1l_ind`を使って簡単に示すことができます。

```coq
  Proof.
    move : s1 s2.
    apply : perm_imply1l_ind
    =>[s t /(perm_map f)/perm_uniq->|a s /andP[]|
       |u s t Hsu Hut y|a s t _ H y|a b s]//=.
    - by rewrite Hsu Hut.
    - by rewrite H.
    - rewrite inE negb_or eq_sym =>/and3P[/andP[Hba _] _ _] y.
      case : ifP Hba =>[/eqP->|]//. by case : ifP.
  Qed.
```


# まとめ

`perm_eq`が不変条件となるような仮定付きの命題を証明するための帰納原理を紹介しました。
帰納法を使う上で`perm_eq`以外の仮定が必要な場合は`perm_imply_ind`を使った方がいいことが分かりました。