婚活パーティのカップリングアルゴリズムの正しさをCoq/SSReflectで形式検証する

#はじめに
ある婚活パーティでは、参加者はそれぞれカップルになりたい人の候補者の名前を書き、お互いに名前を書いた者同士の中からカップルが成立するという方式をとっています。

そこで本記事では、この婚活パーティにおけるカップル生成アルゴリズムが正しい仕様を満たしているかどうかを形式検証ツールの1つであるCoq/SSReflectで実装し、検証します。
特に、生成されたカップルが本当にお互いの名前を書いているのか等、カップル生成アルゴリズムが満たすべき仕様を満たしていることを数学的に証明します。

プログラム全体のソースコード及び証明は[こちら](https://github.com/nekonistyle/party-matching/blob/main/party_matching.v)にあります。


#問題設定
本記事で仮定する「婚活パーティ」のルールを以下に定義します。

##婚活パーティのルール

有限の参加者を２つのグループ`T`と`S`に分けます。
(一般的には女性と男性ですが、LGBTなどの問題を考慮し、ここでは単にグループ`T`と`S`と呼ぶことにします。)

それぞれの参加者は、一通り他の参加者と会話をしたのち、各参加者は自分が所属していないグループの中から、カップルになりたいと思う人の名前をカップリング希望用紙に複数人書き、婚活パーティの運営者に提出します。
すなわちグループ`T`に所属する人はグループ`S`に所属する人の名前を書き、グループ`S`に所属する人はグループ`T`に所属する人の名前を書きます。

ここで、名前を書く人数に制限はなく、全員でも0人でも構いません。

婚活パーティの運営者は参加者全員のカップリング希望用紙を回収したのち、これらを以下を入出力とするカップル生成アルゴリズムに入力します。


###カップル生成アルゴリズムの入出力

- **[入力]**：参加者全員のカップリング希望用紙
- **[出力]**：グループ`T`に所属する人とグループ`S`に所属する人によるペアのリスト

----

このアルゴリズムの出力として与えられた二人をカップルとして認定します。
その後、誰かとカップルになった参加者にはそれぞれカップルになった相手の名前を伝えて婚活パーティは終了です。


ここで、カップル生成アルゴリズムで出力されるカップルの組み合わせは誰でも良いわけではなく、以下の仕様を満たさなければいけません。


###カップル生成アルゴリズムの仕様

- **[健全性]** 出力されたカップルの相手は、互いにカップリング希望用紙に名前を書いた人であること。
- **[一意性]** 各参加者に対し、カップル成立する相手はたかだか1人であること。つまり2人以上の人とはカップル成立しないこと。
- **[極大性]** 互いにカップリング希望用紙に名前を書いているにも関わらず、どちらも誰ともカップル成立しないという状況にはならないこと。言い換えると、カップリング希望用紙にお互いの名前を書いている2人がいた場合、少なくてもどちらか1人は誰かとカップル成立していること。

----

本記事では、これらの仕様をそれぞれカップル生成アルゴリズムの「**健全性**」「**一意性**」「**極大性**」と呼ぶことにします。

特に**極大性**は、まさに**健全性**と**一意性**を満たすペアの部分集合の包含関係における極大性を主張しています。


さらに、場合によっては以下の仕様も仮定する場合があります。

###カップル生成アルゴリズムの追加仕様

- **[優先順位極小性]**カップリング希望用紙にカップリングしたい人の「優先順位」があり、優先順位が上位の人が優先してカップリングする。

----

ここでいう「優先順位」とは具体的には何か、また「優先順位が上位の人がカップリングする」とは何かが曖昧で、多くのこの方針の婚活パーティではこの詳細が明かされていないです。
そこで、本記事では、**この仕様を満たす「優先順位」とは何か、「優先順位が高い人がカップリングする」とは何か**を考え、数学的に証明します。


#カップル生成アルゴリズムの型

上記の問題設定をもとに、形式検証ツールの１つであるCoq/SSReflectでカップル生成アルゴリズムを実装します。
まずカップル生成アルゴリズム`mkCouple'`の型を考えます。
具体的には以下のように記述することができます。

```coq
Variable (T S:finType).

Check mkCouple'.
(* mkCouple' : (T -> seq S) -> (S -> seq T) -> seq (T * S) *)
```

`T S:finType`がグループ`T`と`S`に所属する人の型を表していて、それぞれ有限集合[^1]なので`finType`で定義しています。

[^1]: 有限性を仮定しないと無限のカップルが生成される場合が考えられるため、一般に停止しない関数になります。

また、`T -> seq S`がグループ`T`に所属する人のカップリング希望用紙を表していて、`S -> seq T`がその逆です。
具体的には、引数`ft:T -> seq S`に対し、グループ`T`に所属する参加者`t:T`がカップリング希望用紙に書いた名前のリストが`ft t:seq S`です。

これらを入力にとって、返すのが`T`と`S`のペアのリストなので、返り値の型は`seq (T * S)`になっています。

しかしながら、追加の仕様を考えるために、型を以下のように変更します。

```coq
Variable (R:rel (nat * nat)).
Variable (T S:finType).

Check mkCouple.
(* mkCouple : (T -> seq S) -> (S -> seq T) -> seq (T * S * (nat * nat)) *)
```

定数`R : rel (nat * nat)`が追加されていて、返り値が`seq (T * S)`から`(T * S * (nat * nat))`になっています。

これはマッチングする優先順位を表していて、追加の仕様である**[優先順位極小性]**を満たすアルゴリズムとして定義する場合に必要になります。

具体的には、返り値`(t,s,(nt,ns))`に対し、参加者`t`はカップリング希望用紙の`nt`番目に`s`の名前を書いていて、`s`は`ns`番目に`t`の名前を書いたことを表しています。このペア`(nt,ns)`を優先順位と見て、その上の順序関係を`R`としているわけです。

ちなみに最初の`mkCouple'`は

```coq
Definition mkCouple' ft fs := map fst (mkCouple (fun _ _ => false) ft fs)
```
と`mkCouple`から定義できます。


#カップル生成アルゴリズムの仕様を記述する

カップル生成アルゴリズム`mkCouple`は上で説明したような仕様を満たさなければいけません。そこで、それぞれの仕様を形式的に記述します。


###健全性

>- **[健全性]** 出力されたカップルの相手は、互いにカップリング希望用紙に名前を書いた人であること。

```coq
  Lemma mkCouple_kindness (ft:T -> seq S) (fs:S -> seq T) t s nt ns :
    (t,s,(nt,ns)) \in mkCouple ft fs -> (t \in fs s) && (s \in ft t).
```

`(t,s,(nt,ns)) \in mkCouple ft fs`が出力されたカップルであり、特に`t`と`s`によるカップルを表しています。
それぞれカップリング希望用紙に名前があることは、`t`の希望用紙が`ft t`であり、`s`の希望用紙が`fs s`であるため、それぞれ`t \in fs s`と`s \in ft t`で表せます。


###一意性

>- **[一意性]** 各参加者に対し、カップル成立する相手はたかだか1人であること。つまり複数人とはカップル成立しないこと。

```coq
  Lemma mkCouple_uniquel (ft:T -> seq S) (fs:S -> seq T) t s s' nt nt' ns ns':
    (t,s,(nt,ns)) \in mkCouple ft fs ->
                      (t,s',(nt',ns')) \in mkCouple ft fs ->
                                           [/\ s = s', nt = nt' & ns = ns'].

  Lemma mkCouple_uniquer (ft:T -> seq S) (fs:S -> seq T) t t' s nt nt' ns ns':
    (t,s,(nt,ns)) \in mkCouple ft fs ->
                      (t',s,(nt',ns')) \in mkCouple ft fs ->
                                           [/\ t = t', nt = nt' & ns = ns'].
```

`(t,s,(nt,ns))`と`(t,s',(nt',ns'))`が`t`に対する2つのカップルです。
これが一致することを表現すればいいので、結論が`[/\ s = s', nt = nt' & ns = ns']`になっています。

これを`s`に対しても同様に記述します。


###極大性

>- **[極大性]** 互いにカップリング希望用紙に名前を書いているにも関わらず、どちらも誰ともカップル成立しないという状況にはならないこと。言い換えると、カップリング希望用紙にお互いの名前を書いている2人がいた場合、少なくてもどちらか1人は誰かとカップル成立していること。

```coq
  Lemma mkCouple_maximal (ft:T -> seq S) (fs:S -> seq T) t s:
    (t \in fs s) && (s \in ft t) ->
    has (fun m => (m.1.1 == t) || (m.1.2 == s)) (mkCouple ft fs).
```

**[極大性]**の後者の表現で定義します。
`(t \in fs s) && (s \in ft t)`が`t`と`s`がお互いにカップリング希望用紙を名前を書いていることを表していて、このとき、`m.1.1 = t`または`m.1.2 = s`を満たすカップル`m`が出力されていること、すなわち、`t`か`s`のどちらか1人は誰かとカップルになっていることを表しています。


###優先順位極小性

>- **[優先順位極小性]**カップリング希望用紙にカップリングしたい人の「優先順位」があり、優先順位が上位の人が優先してカップリングする。

```coq
  Hypothesis (Htrans: transitive R).

  Lemma mkCouple_minimal (ft:T -> seq S) (fs:S -> seq T) t s:
    (t \in fs s) && (s \in ft t) ->
    has (fun m => ((m.1.1 == t) || (m.1.2 == s)) &&
                  let x := (index s (ft t), index t (fs s)) in
                  (R x m.2 ==> R m.2 x))
        (mkCouple ft fs).
```

命題としては極大性よりも強い主張をしています。
極大性の命題と同様に、`(t \in fs s) && (s \in ft t)`が`t`と`s`がお互いにカップリング希望用紙を名前を書いていることを表していて、
`(m.1.1 == t) || (m.1.2 == s)`すなわち、`t`か`s`のどちらかが所属するカップル`m`が出力されることを表しています。
さらにこのカップル`m`の優先順位`m.2`は、`s`と`t`同士のペアの優先順位である`x := (index s (ft t),index t (fs s))`より**真に大きくならない**ことを`R x m.2 ==> R m.2 x`によって主張しています。
つまり**優先順位が高い人がマッチングすること**を**優先順位を表す二項関係が極小であること**として定義するわけです。

ここで、**小さくなる**ことではなく、**真に大きくならないこと**と定義しているのは、優先順位を決定する二項関係`R`を広く取るためです。
小さくなること、つまり`m`が最小の優先順位であることをいうためには、少なくても最小値の存在性、すなわち任意の優先順位が比較可能でなければなりません。
しかしながら、`R`に全順序を仮定するのは強すぎます。

特に、ここで使う`R`には一般には反対称律を仮定する必要はないです。
なぜならば、`R`に反対称律を仮定したとしても、2つのカップル`c1 := (t1,s1,(nt1,ns1))`と`c2 := (t2,s2,(nt2,ns2))`に対し、それぞれの優先順位`(nt1,ns1)`と`(ns1,ns2)`が等しかったとしても`c1 = c2`は一般に成り立たたないからです。
例えば、異なる`t1`と`t2`のカップリング希望順位1位がそれぞれ異なる`s1`と`s2`でかつ`s1`と`s2`の希望順位1位がそれぞれ`t1`と`t2`であるとき、カップル`(t1,s1)`、`(t2,s2)`の優先順位はどちらも`(1,1)`になりますが、`t1 != t2`であり`s1 != s2`なので、`R`をカップル上の順序として見たときには反対称律は成り立ちません。
したがって、元々の`R`自体に反対称律を仮定することはあまり意味をなさないです。


##優先順位極小性を成り立たせるための「優先順位」の十分条件

実は、`R`は推移律だけを仮定すればこの命題を証明することができ、これを満たす任意の「優先順位」で**[優先順位極小性]**が成り立つことが言えます。

推移律だけ仮定した順序においても、任意の有限部分集合において極小値、すなわち任意の要素よりも真に大きくはない値の存在性が言えるため、こちらを表す命題`R x m.2 ==> R m.2 x`で定義しているというわけです。

ちなみに全擬順序、つまり比較可能性と推移性を満たす二項関係ならば、極小値が最小値になり、真に大きくないことと小さいことが同値になります。
(ただしペアに対する反対称律が一般に成り立たないので、最小値の一意性が一般に成り立たないことに注意。)


###優先順位極小性が成り立つ「優先順位」の例

例としては以下のようなものが挙げられます。

- 自然数上の辞書式順序。例えばグループ`T`の順位を優先し、それが等しいときにグループ`S`の順位を優先させる二項関係。全順序になる。
- 自然数上の積順序。つまり`(nt,ns) <= (nt',ns')`を`nt <= nt'`かつ`ns <= ns'`で定義する二項関係。半順序になる。
- 優先順位`(nt,ns)`に対し、それらの和`nt+ns`で比較する二項関係。反対称律は満たさないが比較可能性を満たす。
- 任意の`x y:nat * nat`に対して`R x y = false`を満たす二項関係`R`。任意のペアに対して順序がつかず、クイックソートしてもリストの並びが変わらないので、この二項関係を使うことによって事実上、優先順位極小性を仮定しないカップル生成アルゴリズムとみなすことができる。


#カップル生成アルゴリズムの実装

カップル生成アルゴリズムを実装はシンプルです。
まず、全ての互いに名前を書いたペアのリストを生成する関数`pairs`を作り、
これらを順序`R`でクイックソート関数`qsort`を使ってソートします。
最後に、同じ人がいるペアをのぞく関数`pUndup`すれば完成です。

具体的な実装は以下の通りです。


###`pairs`

```coq
  Fixpoint pairs_def (fs:S -> seq T) (t:T) (ss:seq S) (nt:nat) :
    seq (T * S * (nat * nat)) :=
    match ss with
    | [::] => [::]
    | s :: ss => let st := fs s in
                 let ns := index t st in
                 if ns < size st
                 then (t,s,(nt,ns)) :: pairs_def fs t ss nt.+1
                 else pairs_def fs t ss nt.+1
    end.

  Definition pairs (ft:T -> seq S) (fs:S -> seq T) :
    seq (T * S * (nat * nat)) :=
    flatten (codom (fun t => pairs_def fs t (ft t) 0)).
```

まず、`pairs_def`で片方(ここでは`t`)を固定したときに全てのペアになる組み合わせを求めます。ここで`ss := ft t`を表していて、`nt`を求めるための補助変数です。
具体的には、もし`s \in ss`のとき、つまり`t`のカップリング希望リストに`s`が含まれている場合、`fs s`つまり`s`におけるカップリング希望リストに`t`が含まれている場合はそれを先頭に追加して再帰します。

あとはこれを全ての`t`に対して求め、それらのリストを`flatten`で結合してしまえば関数`pairs`の完成です。


###`qsort`

実装は「[クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する](https://qiita.com/nekonibox/items/eabcbc1bb11b1a472a63)」内で紹介したのと同じなので省略します。

なぜクイックソートを使うかというと、任意の半順序、というよりも単なる推移的な二項関係であればソート可能だからです。
詳細は「[半順序でソートするためのアルゴリズムとは？](https://qiita.com/nekonibox/items/c1c7f4d1ad1695967e39)」をご覧ください。


###`pUndup`

```coq
  Variable (X:eqType).

  Function pUndup (s:seq (T * S * X)) {measure size s} : seq (T * S * X) :=
    match s with
    | [::] => [::]
    | h :: s => h :: pUndup [seq x <- s | h.1.1 != x.1.1 & h.1.2 != x.1.2 ]
    end.
  Proof.
    move => s' h s _. apply /ltP. exact : filter_size.
  Defined.
```

先頭の要素`(t,s,(nt,ns))`　を取り出し、残りの要素のうち、`t`か`s`が一致している要素を除いて再帰します。このとき、コンストラクタのみを除いて再帰するわけではなく減少性が非自明なため、`Function`コマンドを使って定義します。

また`qsort`のときと同様に、自動生成される`pUndup`における帰納原理`pUndup_ind`の使い勝手が悪いので、新たに帰納原理を証明します。

```coq
  Lemma my_pUndup_ind (P:seq (T * S * X) -> Prop) :
    P [::] ->
    (forall h s, P [seq x <- s | h.1.1 != x.1.1 & h.1.2 != x.1.2 ] ->
                 P (h :: s)) ->
    forall s, P s.
  Proof.
    move => Hnil Hcons s.
    have [n] := ubnP (size s).
    elim : n s =>[|n IH][|h s]//=. rewrite ltnS => Hsize. apply /Hcons /IH.
    exact : leq_ltn_trans (filter_size _ _) Hsize.
  Qed.
```

証明の方針は「[Coq/SSReflectで{}を使わずに完全帰納法を適用する](https://qiita.com/nekonibox/items/8147291e9fd483e3d579)」のクイックソートにおける帰納原理と同様です。


###`mkCouple`

これらを組み合わせれば、カップル生成アルゴリズム`mkCouple`の完成です。

```coq
  Definition mkCouple (ft:T -> seq S) (fs:S -> seq T) :
    seq (T * S * (nat * nat)) :=
    pUndup (qsort (fun x y => R x.2 y.2) (pairs ft fs)).
```


#仕様を満たすことを証明する

上で定義した`mkCouple`が仕様を満たすことを証明します。

そのための補題をいくつか用意します。

##`pairs`に関する補題

まず、`pairs`に関する補題です。

`pairs`の返り値のリストに入っているペアが満たすべき必要十分条件が以下の通りです。

```coq
  Lemma ex_pairsP (ft:T -> seq S) (fs:S -> seq T) (t:T) (s:S):
    reflect (exists nt ns, (t,s,(nt,ns)) \in pairs ft fs)
            ((t \in fs s) && (s \in ft t)).
```

`(t \in fs s) && (s \in ft t)`すなわち`t`と`s`がお互いにカップリング希望を出していることと`exists nt ns, (t,s,(nt,ns)) \in pairs ft fs`すなわち`pairs ft fs`のリストに含まれていることが同値になります。

ここで、「`nt`と`ns`が存在すること」とありますが、具体的な値の1つは以下のように`index s (ft t)`と`index t (fs s)`になります。

```coq
  Lemma pairs_index (ft:T -> seq S) (fs:S -> seq T) (t:T) (s:S):
    (t \in fs s) && (s \in ft t) ->
    (t,s,(index s (ft t),index t (fs s))) \in pairs ft fs.
```

ここで「１つ」と言ったのは、マッチング希望用紙に同じ名前を複数書く場合があるからです。

名前が重複しないことを仮定しても良いのですが、重複したペアはのちに`pUndup`で消えるので、ここでは仮定していません。


##`qsort`に関する補題

クイックソート`qsort`に関しては返り値がソートされていることと元のリストの置換になっていることを示せれば十分です。

```coq
  Fixpoint mysorted T (R:rel T) (s:seq T) :=
    if s is x :: s' then all (fun y => R y x ==> R x y) s' && mysorted R s'
    else true.

  Lemma qsort_sorted T (R:rel T) s : transitive R -> mysorted R (qsort R s).

  Lemma perm_qsort (T:eqType) (R:rel T) s: perm_eq (qsort R s) s.
```

ついでに、二項関係`fun _ _ => false`でソートしても元のリストと変わらないことも示しておきます。

```coq
  Lemma qsort0 T (s:seq T) : qsort (fun _ _ => false) s = s.
```


##`pUndup`に関する補題

それぞれの仕様に関する補題を示していきます。

###健全性

`pUndup`したリストが部分集合、特に部分列になっていることを示します。

```coq
  Lemma pUndup_subseq s : subseq (pUndup s) s.
```

###一意性

`pUndup`したリストが一意性を満たすことを示します。

```coq
  Lemma pUndup_uniquel s x y:
    x \in pUndup s -> y \in pUndup s -> x.1.1 = y.1.1 -> x = y.

  Lemma pUndup_uniquer s x y:
    x \in pUndup s -> y \in pUndup s -> x.1.2 = y.1.2 -> x = y.
```


###極大性

`pUndup`したリストが極大性を満たすことを示します。

```coq
  Lemma pUndup_maximal s x:
    x \in s -> has (fun m => (m.1.1 == x.1.1) || (m.1.2 == x.1.2)) (pUndup s).
```


###優先順位極小性

これは、`pundup`の定義だけでは示せないので、別の補題を示します。

まず、述語`behind`を定義します。

```coq
  Fixpoint dropuntil (X:eqType) x (s:seq X) :=
    match s with
    | [::] => [::]
    | h :: s' => if x == h then s else dropuntil x s'
    end.

  Definition behind (X:eqType) (s:seq X) f b := b \in dropuntil f s.
```

`behind s f b`が意味するところは、リスト`s`の中の最初に現れる`f`より後ろに`b`が存在することです。

特に`[:: f; b]`が`s`の部分列であるか、`f = b`かつ`f`が`s`に含まれることと同値になります。

```coq
  Lemma behindP (X:eqType) (s:seq X) f b:
    reflect (subseq [:: f; b] s || (f == b) && (f \in s)) (behind s f b).
```

`behind`を使って`pUndup`の極小性を表します。


```coq
  Lemma pUndup_minimal s x:
    x \in s ->
          has (fun m => ((m.1.1 == x.1.1) || (m.1.2 == x.1.2)) && behind s m x)
              (pUndup s).
```

つまり、`pUndup_maximal s x`が表しているのは、ペア`x = (t,s,(nt,ns))`に対し、`t`と`s`のどちらかが一致する`m`よりあとに`x`がリスト`s`に存在することを表しています。

今考えたいのはソートされたリスト`s`なので、`m`の後に`x`が存在することと`m`が`x`より真に小さくないことが言えます。


あとはこれらを組み合わせてカップル生成アルゴリズム`mkCouple`が仕様を満たすことを示します。


##`mkCouple`が仕様を満たすことを示す。

上の補題を使ってそれぞれ証明します。

###健全性

```coq
  Lemma mkCouple_kindness (ft:T -> seq S) (fs:S -> seq T) t s nt ns :
    (t,s,(nt,ns)) \in mkCouple ft fs -> (t \in fs s) && (s \in ft t).
  Proof.
    move /(mem_subseq (pUndup_subseq _)).
    by rewrite (perm_mem (perm_qsort _ _))=>/mem_pairs.
  Qed.
```

###一意性

```coq
  Lemma mkCouple_uniquel (ft:T -> seq S) (fs:S -> seq T) t s s' nt nt' ns ns':
    (t,s,(nt,ns)) \in mkCouple ft fs ->
                      (t,s',(nt',ns')) \in mkCouple ft fs ->
                                           [/\ s = s', nt = nt' & ns = ns'].
  Proof.
    move => H H'. by case : (pUndup_uniquel H H' (erefl _)).
  Qed.

  Lemma mkCouple_uniquer (ft:T -> seq S) (fs:S -> seq T) t t' s nt nt' ns ns':
    (t,s,(nt,ns)) \in mkCouple ft fs ->
                      (t',s,(nt',ns')) \in mkCouple ft fs ->
                                           [/\ t = t', nt = nt' & ns = ns'].
  Proof.
    move => H H'. by case : (pUndup_uniquer H H' (erefl _)).
  Qed.
```

###極大性

```coq
  Lemma mkCouple_maximal (ft:T -> seq S) (fs:S -> seq T) t s:
    (t \in fs s) && (s \in ft t) ->
    has (fun m => (m.1.1 == t) || (m.1.2 == s)) (mkCouple ft fs).
  Proof.
    case /ex_pairsP =>[nt][ns].
    rewrite -(perm_mem (perm_qsort (fun x y => R x.2 y.2) _)).
    exact : pUndup_maximal.
  Qed.
```

###優先順位極小性

```coq
  Hypothesis (Htrans: transitive R).

  Lemma mkCouple_minimal (ft:T -> seq S) (fs:S -> seq T) t s:
    (t \in fs s) && (s \in ft t) ->
    has (fun m => ((m.1.1 == t) || (m.1.2 == s)) &&
                  let x := (index s (ft t), index t (fs s)) in
                  (R x m.2 ==> R m.2 x))
        (mkCouple ft fs).
  Proof.
    move => /pairs_index ts. move : (ts).
    rewrite -(perm_mem (perm_qsort (fun x y => R x.2 y.2) _))
               =>/pUndup_minimal.
    apply : sub_has => m /=/andP[->]/behindP/orP[|/andP[/eqP->_]];
                         [|exact /implyP].
    have sndtrans : transitive (fun x y: (T * S * (nat * nat)) => R x.2 y.2)
      := fun _ _ _ xy yz => Htrans xy yz.
    move =>/subseq_mysorted. move =>/(_ _ (qsort_sorted _ sndtrans))/=.
      by rewrite !andbT.
  Qed.
```


#まとめ

婚活パーティにおけるカップル生成アルゴリズムを形式検証しました。

また、婚活パーティにおける「優先順位が高い人がマッチングする」ということの意味を確認しました。
具体的には、「優先順位」とは$\mathbb{N} \times \mathbb{N}$上の推移性を満たす二項関係であり、
「優先順位が高い人がマッチングすること」は優先順位による極小値をとるペアがカップルになるということがわかりました。