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

はじめに

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

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

ソースコードはこちらです。

仮定付きのperm_eqが不変条件になる命題

本記事で示したい命題は以下のような形で書けるものです。

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の帰納原理は以下になります。(詳細は前回の記事で解説しています)

  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で証明するのが困難な理由

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

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

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

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

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

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

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の帰納原理

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

  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の長さに関する完全帰納法で示すことができます。

  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.

ただし、

  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で{}を使わずに完全帰納法を適用するをご覧ください。

仮定が1変数の場合

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

 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.

  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が不変条件になるような命題として、例えば以下のようなものが挙げられます。

  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を使って簡単に示すことができます。

  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を使った方がいいことが分かりました。