はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

Coq によるマッチング理論の形式化
辻 陽介
北見工業大学2023 年 10 月 30 日

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

今回話す内容この発表の話題は以下の通り :マッチングの説明
形式化の具体例まとめ

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ目標とする定理
次のような事実が知られている。

Theorem ( [ Hibi-Higashitani-Kimura-Tsuchiya, JAC (2016),
Proposition 2.1 ] )任意の G に対し

1 ≤ ind-match(G ) ≤ min-match(G ) ≤ match(G ) ≤ 2 min-match(G )が成り立つ。
この定理の ind-match(G ) ≤ min-match(G ) の証明について発表
する。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

マッチング、極大マッチング、誘導マッチング
誘導マッチング数、最小マッチング数、マッチング数

マッチング
G を有限単純グラフ、 V (G ) を G の頂点集合、E (G ) を G の辺集合とする。
Deﬁnition (マッチング)
部分集合 S ⊂ E (G ) において、任意の e, f ∈ S に対して e と f が異なるならば e と f が頂点を共有しないとき S は マッチングであるという。
Definition is_matching :=[ ∀ e in S, [ ∀ f in S, (e != f) =⇒ [disjoint ‘d(e) & ‘d(f)]%fset]].
Definition matching : {fset {fset ‘E(G)}} :=[ fset S : {fset ‘E(G)} | is_matching S].
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

マッチング、極大マッチング、誘導マッチング
誘導マッチング数、最小マッチング数、マッチング数

極大マッチング、誘導マッチング
Deﬁnition (極大マッチング)
マッチング S に対して、任意の 真に S を含む T ⊂ E (G ) がマッ
チングにならないとき S は極大マッチングという。

Deﬁnition (誘導マッチング)
任意の相異なる e, f ∈ S に対し、任意の g ∈ E (G ) が e ∩ g = ∅または f ∩ g = ∅ を満たすとき S を誘導マッチングという。
極大マッチングは、新たに辺を付け足せないマッチング。
誘導マッチングは、辺どうしをつなぐ辺が存在しないマッチング。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

マッチング、極大マッチング、誘導マッチング
誘導マッチング数、最小マッチング数、マッチング数

Definition is_maximal_matching :=(S \in matching G) &&[ ∀ T : {fset ‘E(G)},(S ‘<‘ T) =⇒ (T \notin matching G)].
Definition is_induced_matching :=[ ∀ e in S, [ ∀ f in S, (e != f)=⇒ [ ∀g, [ disjoint ‘d(e) & ‘d(g)] || [ disjoint ‘d(f) & ‘d(g)]]]].

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

マッチング、極大マッチング、誘導マッチング
誘導マッチング数、最小マッチング数、マッチング数

マッチングに関する不変量
G のマッチング数 match(G )、 最小マッチング数 min-match(G )、誘導マッチング数 ind-match(G ) を以下のように定める :match(G ) = max{|M| : M は G のマッチング }min-match(G ) = min{|M| : M は G の極大マッチング }ind-match(G ) = max{|M| : M は G の誘導マッチング }Definition nmatch := \max_(S in matching) #|‘ S |.
Definition nminmatch :=\big[Order.min/nmaxmatch]_(S in maximal_matching) #|‘ S |.
Definition nindmatch := \max_(S in induced_matching) #|‘ S |.

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

マッチング、極大マッチング、誘導マッチング
誘導マッチング数、最小マッチング数、マッチング数

match(G ) = max{|M| : M は G のマッチング }min-match(G ) = min{|M| : M は G の極大マッチング }ind-match(G ) = max{|M| : M は G の誘導マッチング }これら 3 種のグラフ理論的不変量に関して、以下の事実が知られている。

Theorem ( [ Hibi-Higashitani-Kimura-Tsuchiya, JAC (2016),
Proposition 2.1 ] (再掲) )任意の G に対し

1 ≤ ind-match(G ) ≤ min-match(G ) ≤ match(G ) ≤ 2 min-match(G )が成り立つ。
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ind-match(G ) ≤ min-match(G ) の証明

N を |N| = ind-match(G ) となる誘導マッチング、M を|M| = min-match(G ) となる極大マッチングとする。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ind-match(G ) ≤ min-match(G ) の証明

N を |N| = ind-match(G ) となる誘導マッチング、M を|M| = min-match(G ) となる極大マッチングとする。
任意の e ∈ N に対してある h ∈ M が存在して e ∩ h ̸= ∅ となる。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ind-match(G ) ≤ min-match(G ) の証明

N を |N| = ind-match(G ) となる誘導マッチング、M を|M| = min-match(G ) となる極大マッチングとする。
任意の e ∈ N に対してある h ∈ M が存在して e ∩ h ̸= ∅ となる。
もし、任意の h ∈ M で e ∩ h = ∅ ならば M ∪ {e} はマッチングとなる。これは M が極大であることに矛盾する。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ここで誘導マッチング数を与えるマッチング N 、最小マッチング数を与えるマッチング M に対して f : N → M を e ∈ N を受け取って頂点を共有する辺 f (e) ∈ M を 1 つ返す関数とする。
例として次のグラフを考える。
e2

e0

e4

e1
e3

e6
e5

このグラフについての N, M をひとつ選ぶとすると、
N = {e0 , e6 }, M = {e2 , e5 } のようにとれる。
このとき N の要素に対して M の要素は f を使って
f (e0 ) = e2 , f (e6 ) = e5 と表せる。
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ここで誘導マッチング数を与えるマッチング N 、最小マッチング数を与えるマッチング M に対して f : N → M を e ∈ N を受け取って頂点を共有する辺 f (e) ∈ M を 1 つ返す関数とする。
任意の N の辺 e0 , e1 において e0 ̸= e1 ならば f (e0 ) ̸= f (e1 ) である。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ここで誘導マッチング数を与えるマッチング N 、最小マッチング数を与えるマッチング M に対して f : N → M を e ∈ N を受け取って頂点を共有する辺 f (e) ∈ M を 1 つ返す関数とする。
任意の N の辺 e0 , e1 において e0 ̸= e1 ならば f (e0 ) ̸= f (e1 ) である。
このことを背理法で示す。もし f (e0 ) = f (e1 ) ならば e0 と e1 をつ
なぐ辺が存在する。しかしこれは N が誘導マッチングであること
に反する。
f (e

0)

e0

辻 陽介

=f

(e6

)

e6

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ここで誘導マッチング数を与えるマッチング N 、最小マッチング数を与えるマッチング M に対して f : N → M を e ∈ N を受け取って頂点を共有する辺 f (e) ∈ M を 1 つ返す関数とする。
任意の N の辺 e0 , e1 において e0 ̸= e1 ならば f (e0 ) ̸= f (e1 ) である。
このことを背理法で示す。もし f (e0 ) = f (e1 ) ならば e0 と e1 をつ
なぐ辺が存在する。しかしこれは N が誘導マッチングであること
に反する。
f (e

0)

e0

=f

(e6

)

e6

よって f : N → M は単射であるから |N| ≤ |M|
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

N を |N| = ind-match(G ) となる誘導マッチング、M を|M| = min-match(G ) となる極大マッチングとする。
任意の e ∈ N に対してある h ∈ M が存在して e ∩ h ̸= ∅ となる。
もし、任意の h ∈ M で e ∩ h = ∅ ならば M ∪ {e} はマッチングとなる。これは M が極大であることに矛盾する。

ここで f : N → M を e ∈ N を受け取って頂点を共有する辺
f (e) ∈ M を 1 つ返す関数とする。
f : N → M は単射である。

任意の N の辺 e0 , e1 において e0 ̸= e1 ならば f (e0 ) ̸= f (e1 ) である。
背理法で示す。f (e0 ) = f (e1 ) ならば e0 と e1 をつなぐ辺が存在する。しかしこれは N が誘導マッチングであることに反する。

よって |N| ≤ |M|
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

Coq で行った証明の手順

以下の型を持つ関数を ind-match(G ) ≤ min-match(G ) の証明の前に定めた :
グラフ G において、ϕ は辺を受け取って辺とその頂点のペアを返す関数。

ψ は辺 e を受け取って ϕ e のはじめの要素 (辺) を返す関数。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ϕ の定義
補題

M がグラフ G の極大マッチングならば、任意の G の辺 e に対して M の辺 f が存在して e と f に共通の頂点 v が存在する。
Lemma maxmatch_edgeI’ (M : {fset ‘E(G)}) (e : ‘E(G)):
M \in maximal_matching G →∃ f : ‘ E(G), f \in M ∧ ∃ v : ‘ V(G), v \in ‘d(e) ∧ v\in ‘d(f).

この補題に選択公理を 2 回適用して辺 f と頂点 v を取り出す関数が ϕ である。
Let phi_ (M : {fset ‘E(G)}) (Mmax : M \in maximal_matching G) :‘ E(G) → ‘E(G) ∗ ‘ V(G).
move⇒ e; move: (maxmatch_edgeI’ e Mmax).
case/boolp.cid ⇒ f [] _; case/boolp.cid ⇒ v _.
exact: (f, v).
Defined.
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ψ の定義
ψ は ϕ の出力の片方 (辺) を出力する関数
Let psi (M : {fset ‘E(G)}) (Mmax : M \in maximal_matching G) e :=(phi Mmax e).1.

ψ の行先は極大マッチング M の要素であるLet psi_M (M : {fset ‘E(G)}) (Mmax : M \in maximal_matching G) e :psi Mmax e \in M.

ψ と極大マッチング M に対して、誘導マッチング N の要素が入力であるとき、入力が異なるならば出力は異なる
Lemma psi_inj (M : {fset ‘E(G)}) (Mmax : M \in maximal_matching G)(N : {fset ‘E(G)}) e0 e1 :N \in induced_matching G → e0 \in N → e1 \in N →e0 != e1 → psi Mmax e0 != psi Mmax e1.
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ind-match(G ) を与える誘導マッチング N が存在する。
min-match(G ) を与えるマッチング M が存在する。
N から M への関数 f をあらかじめ定義していた汎関数 ψ から定める。
f が単射ならば、M の濃度が N の濃度以上であるという補題
を適用する。
f が単射であることを証明する。
(∀x1 , x2 ∈ N, f (x1 ) = f (x2 ) → x1 = x2 を示す。)
全称量化子の二つの変数をそれぞれ e0 , e1 として固定して考える（仮定に加える）。
Goal を対偶に変える (e1 ̸= e2 → f (e1 ) ̸= f (e2 ) を示す)。
f の入力となる誘導マッチング N の辺が異なるならば、出力の極大マッチング M の辺が異なることを示す。
あらかじめ定めていた ψ の単射性を Goal に移動する。
f の定義を書き下す (よって f は単射である)。

証明終了
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

Lemma nindmatch_leq_nminmatch : nindmatch G <= nminmatch G.
Proof.
case: (exists_nindmatch G) ⇒ N Nind → .
case: (exists_nminmatch G) ⇒ M Mmax → .
rewrite 2!cardfE.
set f : N → M := fun n ⇒ [‘ (psi_M Mmax (val n)) ].
apply: (leq_card f).
move⇒ e0 e1.
move/eqP ⇒ fe01.
apply/eqP.
move: fe01.
apply: contraLR.
move/(psi_inj Mmax Nind).
rewrite /f.
by rewrite 2!fsvalP ⇒ /(_ erefl erefl).
Qed.
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

初めに参考にした ind-match(G ) ≤ min-match(G ) の証明
ind-match(G ) = p, min-match(G ) = q とし、 N = {e1 , . . . , ep }を誘導マッチング、 M = {e ′ 1 , ..., e ′ q } を極大マッチングとする。
任意の 1 ≤ k ≤ p に対し、ある 1 ≤ ik ≤ q が存在して
ek ∩ eik ̸= ∅ が成り立つ。背理法で示す。ある 1 ≤ j ≤ p が存在して、任意の 1 ≤ k ≤ q に対して ej ∩ ek ̸= ∅ が成り立つとすると、
M ∪ {ej } はマッチングとなるが、これは M の極大性に反する。
ここで、任意の 1 ≤ k ̸= k ′ ≤ p に対し ik ̸= ik ′ が成り立つ。背理法で示す。ある 1 ≤ k ̸= k ′ ≤ p が存在して ik = ik ′ が成り立つと仮定すると、ek ∩ eik ̸= ∅ かつ ek ′ ∩ eik ̸= ∅ となる。これは 2 辺
ek , ek ′ をつなぐ辺 eik が存在することを意味しているが、 N が誘
導マッチングであることに反する。よって、 1 ≤ i1 , i2 , . . . , ip ≤ q
は全て異なる。
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

ind-match(G ) = p, min-match(G ) = q とし、
N = {e1 , . . . , ep } を誘導マッチング、M = {e ′ 1 , ..., e ′ q } を極大マッチングとする。
任意の 1 ≤ k ≤ p に対し、ある 1 ≤ ik ≤ q が存在して
ek ∩ eik ̸= ∅ が成り立つ。
背理法で示す。ある 1 ≤ j ≤ p が存在して、任意の
1 ≤ k ≤ q に対して ej ∩ ek ̸= ∅ が成り立つとする。
M ∪ {ej } はマッチングとなるが、これは M の極大性に反する。

任意の 1 ≤ k ̸= k ′ ≤ p に対し ik ̸= ik ′ が成り立つ。

背理法で示す。ある 1 ≤ k ̸= k ′ ≤ p が存在して ik = ik ′ が成り立つと仮定する。
ek ∩ eik ̸= ∅ かつ ek ′ ∩ eik ̸= ∅ となる。
これは 2 辺 ek , ek ′ をつなぐ辺 eik が存在することを意味しているが、 N が誘導マッチングであることに反する。

よって、 1 ≤ i1 , i2 , . . . , ip ≤ q は全て異なる。
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq で行った証明の手順
はじめに参考にした証明

形式化した証明との違い初めに参考にした証明では、マッチングの要素に添え字をつけて、添え字同士の対応を考えている。
単射という言葉は使わず、
ind-match(G ) = p, min-match(G ) = q として、
N の辺の添え字 1, . . . , k, . . . , p に対応する M の辺の添え字を1, . . . , ik , . . . , q としている。
最終的に i1 , . . . , ip はすべて異なり、1 ≤ i1 , . . . , ip ≤ q となることを示している。

(形式化した証明では、M と N の単射を考えていた。)

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq での証明

match(G ) ≤ 2 min-match(G ) の証明
q = min-match(G ) とし、M を |M| = min-match(G ) となる極大マッチングとする。
もし、ある辺 e ∈ E (G ) が存在して e ∩ V (M) = ∅ となると仮定
すると、M ∪ {e} がマッチングとなるが、これは M の極大性に反する。従って、任意の e ∈ E (G ) に対し、e ∩ V (M) ̸= ∅ となる。|V (M)| = 2q であるから、(2q + 1) 本以上の辺からなるマッ
チングは存在しないことがわかる。従って match(G ) ≤ 2q が成
り立つ。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq での証明

より丁寧な証明
M, S をそれぞれ |M| = match(G ), |S| = min-match(G ) となる
マッチングとする。S が極大であることから、任意の G の辺e ∈ E (G ) で、e と頂点の集合 V (S) は共通部分が空でない。よって、どの M の辺 fi = {vi , wi } に対しても vi ∈ V (S) または
wi ∈ V (S) である。
ここで任意の 1 ≤ i ≤ |M| について、vi ∈ V (S) とする。
M がマッチングであるから、1 ≤ i ̸= j ≤ |M| となる任意の i, j において、vi ̸= vj である。したがって |V (S)| ≥ |M| = match(G )。
|V (S)| = 2|S| = 2 min-match(G ) であったから、
match(G ) ≤ 2 min-match(G ) を得る。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq での証明

Coq での証明
min-match(G ) を与えるマッチング M が存在する。
マッチング M の濃度の 2 倍は M の頂点の集合の濃度。
match(G ) を与えるマッチング N が存在する。
列の長さ (size) の比較を要素の濃度の比較に変換する。
N から M の頂点への関数 f を仮定に加える。
f が単射ならば、M の濃度が N の濃度以上であるという補題
を適用する。
f が単射であることを示す(∀x1 , x2 ∈ N, f (x1 ) = f (x2 ) → x1 = x2 を示す)。
全称量化子の二つの変数をそれぞれ e0, e1 として固定して考える (仮定に加える)
ゴールを対偶に変える (e1 ≠ e2 → f (e1 ) ̸= f (e2 ) を示す)。
N から M への単射が存在し、頂点が異なるならば、辺が異なることを示す。
ϕ の単射性をゴールに移動する。

証明終了
辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

日本語での証明
Coq での証明

Proof.
case: (exists_nminmatch G) ⇒ M Mmax → .
rewrite −matching_double_card;last by case/maximal_matchingP: Mmax.
case: (exists_nmatch G) ⇒ N Nm → .
rewrite 2!cardfE.
set f : N → VofESet M := fun n ⇒ [‘ (phi_VofESet Mmax (val n)) ].
apply: (leq_card f).
move ⇒ e0 e1.
move/eqP ⇒ H; apply/eqP; move: H.
apply: contraLR.
move/(phi_inj Mmax Nm).
by rewrite 2!fsvalP ⇒ /(_ erefl erefl).
Qed.

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

まとめ
グラフのマッチングに関する理論を Coq で形式化した。

Theorem ( [ Hibi-Higashitani-Kimura-Tsuchiya, JAC (2016),
Proposition 2.1 ] (再掲) )任意の G に対し

1 ≤ ind-match(G ) ≤ min-match(G ) ≤ match(G ) ≤ 2 min-match(G )が成り立つ。
この定理の ind-match(G ) ≤ min-match(G ) の証明について発表
した。

辻 陽介

Coq によるマッチング理論の形式化

はじめに誘導マッチング数、最小マッチング数およびマッチング数
ind-match(G ) ≤ min-match(G ) の証明
match(G ) ≤ 2 min-match(G ) の証明
まとめ

T. Hibi, A. Higashitani, K. Kimura and A. Tsuchiya,
Dominating induced matching of ﬁnite graphs and regularity ofedge ideals, J. Algebraic Combin. 43 (2016), 173 ‒ 198.

辻 陽介

Coq によるマッチング理論の形式化