Subgraph Isomorphism

Lax799700.SubgraphIso · concepts/Lax799700/SubgraphIso.lean · lax-799700

proven

Loading review…

Natural Language Statement

Theorem

SUBGRAPH ISOMORPHISM: does the host graph contain a subgraph isomorphic to the pattern graph, that is, is there an injective homomorphism of the pattern into the host (SubgraphIsoOn)? Non-edges of the pattern are unconstrained, the standard reading and the one that makes Clique a special case. An instance carries two graphs in one universe: two unary marks separate the pattern vertices from the host vertices, and two binary relations are their adjacencies; elements outside both marks are junk no condition mentions. Membership is by an existential second-order definition guessing the map; hardness is a quantifier-free first-order reduction from Clique, the host being the input graph and the pattern the complete graph on its marked set.

Concept map

7 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

Show types on hover

1	import Mathlib.ModelTheory.Syntax
2	import Mathlib.ModelTheory.Semantics
3	import Mathlib.Data.Fintype.Lattice
4	import Mathlib.ModelTheory.Order
5	import Mathlib.ModelTheory.Complexity
6	import Mathlib.Tactic.FinCases
7	import Mathlib.Logic.Equiv.Fin.Basic
8	import Mathlib.Order.PiLex
9	import Mathlib.Data.Prod.Lex
10	import Mathlib.Data.Fintype.EquivFin
11	import Mathlib.Data.Finite.Sigma
12	import Mathlib.Data.Set.Finite.Lemmas
13	import Mathlib.Data.Set.Card
14	import Mathlib.SetTheory.Cardinal.Finite
15	import Mathlib.Logic.Equiv.Prod
16	import Lax904597.Classes
17	import Lax799700.Problems
18
19	/-!
20	---
21	title: Subgraph Isomorphism
22	type: theorem
23	---
24	SUBGRAPH ISOMORPHISM: does the host graph contain a subgraph isomorphic
25	to the pattern graph, that is, is there an injective homomorphism of the
26	pattern into the host (SubgraphIsoOn)? Non-edges of the pattern are
27	unconstrained, the standard reading and the one that makes Clique a
28	special case. An instance carries two graphs in one universe: two unary
29	marks separate the pattern vertices from the host vertices, and two
30	binary relations are their adjacencies; elements outside both marks are
31	junk no condition mentions. Membership is by an existential second-order
32	definition guessing the map; hardness is a quantifier-free first-order
33	reduction from Clique, the host being the input graph and the pattern
34	the complete graph on its marked set.
35
36	-/
37
38	namespace Lax799700.SubgraphIso
39
40	open FirstOrder
41
42	open FirstOrder.Language
43
44	/-- The relation symbols of the language. -/
45	inductive twoGraphsRel : ℕ → Type where
46	/-- `patV a`: `a` is a vertex of the pattern graph. -/
47	\| patV : twoGraphsRel 1
48	/-- `hostV a`: `a` is a vertex of the host graph. -/
49	\| hostV : twoGraphsRel 1
50	/-- `patE a b`: there is an edge of the pattern from `a` to `b`. -/
51	\| patE : twoGraphsRel 2
52	/-- `hostE a b`: there is an edge of the host from `a` to `b`. -/
53	\| hostE : twoGraphsRel 2
54	deriving DecidableEq
55
56	/-- The relational language of pattern-and-host graphs: two graphs sharing a
57	universe, each with its own vertex mark and adjacency relation. -/
58	def twoGraphs : FirstOrder.Language :=
59	⟨fun _ => Empty, twoGraphsRel⟩
60
61	instance instIsRelationalTwoGraphs : FirstOrder.Language.IsRelational twoGraphs := fun _ =>
62	(inferInstance : IsEmpty Empty)
63
64	/-- `patV a`: `a` is a vertex of the pattern graph. -/
65	abbrev tgPatV : twoGraphs.Relations 1 :=
66	.patV
67
68	/-- `hostV a`: `a` is a vertex of the host graph. -/
69	abbrev tgHostV : twoGraphs.Relations 1 :=
70	.hostV
71
72	/-- `patE a b`: there is an edge of the pattern from `a` to `b`. -/
73	abbrev tgPatE : twoGraphs.Relations 2 :=
74	.patE
75
76	/-- `hostE a b`: there is an edge of the host from `a` to `b`. -/
77	abbrev tgHostE : twoGraphs.Relations 2 :=
78	.hostE
79
80	open FirstOrder
81
82	open Language Structure Lax904597.SecondOrder.SOBlock
83
84	section Generic
85
86	variable {A : Type}
87
88	/-- Some map sends the `PV`-vertices injectively into the `HV`-vertices,
89	carrying `PE`-edges to `HE`-edges: an injective homomorphism of the pattern
90	into the host. -/
91	def SubgraphIsoOn (PV HV : A → Prop) (PE HE : A → A → Prop) : Prop :=
92	∃ f : A → A, (∀ x, PV x → HV (f x)) ∧
93	(∀ x y, PV x → PV y → f x = f y → x = y) ∧
94	∀ x y, PV x → PV y → PE x y → HE (f x) (f y)
95
96	end Generic
97
98	section Problem
99
100	section Shorthands
101
102	variable {A : Type} [twoGraphs.Structure A]
103
104	/-- `patV a`: `a` is a vertex of the pattern graph. -/
105	def TGPatV {A : Type} [twoGraphs.Structure A] (a0 : A) : Prop :=
106	FirstOrder.Language.Structure.RelMap tgPatV ![a0]
107
108	/-- `hostV a`: `a` is a vertex of the host graph. -/
109	def TGHostV {A : Type} [twoGraphs.Structure A] (a0 : A) : Prop :=
110	FirstOrder.Language.Structure.RelMap tgHostV ![a0]
111
112	/-- `patE a b`: there is an edge of the pattern from `a` to `b`. -/
113	def TGPatE {A : Type} [twoGraphs.Structure A] (a0 : A) (a1 : A) : Prop :=
114	FirstOrder.Language.Structure.RelMap tgPatE ![a0, a1]
115
116	/-- `hostE a b`: there is an edge of the host from `a` to `b`. -/
117	def TGHostE {A : Type} [twoGraphs.Structure A] (a0 : A) (a1 : A) : Prop :=
118	FirstOrder.Language.Structure.RelMap tgHostE ![a0, a1]
119
120	end Shorthands
121
122	variable (A : Type) [twoGraphs.Structure A]
123
124	/-- The host graph contains a subgraph isomorphic to the pattern graph.
125	(Finiteness of the universe is required only for uniformity with the rest of
126	the catalog; the property itself makes sense in general.) -/
127	def HasSubgraphIso : Prop :=
128	Finite A ∧ SubgraphIsoOn (TGPatV (A := A)) TGHostV TGPatE TGHostE
129
130	end Problem
131
132	open Lax904597.Problems Lax904597.Classes Lax799700.Problems
133
134	/-- The property `HasSubgraphIso` is isomorphism-invariant. -/
135	axiom hasSubgraphIso_iso : ∀ {A B : Type} [Lax799700.SubgraphIso.twoGraphs.Structure A] [Lax799700.SubgraphIso.twoGraphs.Structure B],
136	(A ≃[Lax799700.SubgraphIso.twoGraphs] B) → (HasSubgraphIso A ↔ HasSubgraphIso B)
137
138	/-- The problem SubgraphIso: does the structure satisfy `HasSubgraphIso`? -/
139	def SubgraphIso : DecisionProblem Lax799700.SubgraphIso.twoGraphs :=
140	DecisionProblem.ofPred HasSubgraphIso
141
142	/-- The yes-instances of SubgraphIso are exactly the structures satisfying
143	`HasSubgraphIso`. -/
144	axiom subgraphIso_iff : ∀ (A : Type) [Lax799700.SubgraphIso.twoGraphs.Structure A], SubgraphIso A ↔ HasSubgraphIso A
145
146	/-- SubgraphIso is NP-complete. -/
147	axiom subgraphIso_NP_complete : NP.Complete SubgraphIso
148
149	end Lax799700.SubgraphIso
150

Show ProofShow ProofShow Proof

Builds on

Used by

none

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Subgraph Isomorphism

Flags

Flag this concept

Natural Language Statement

Theorem

1 `hasSubgraphIso_iso` proven

2 `subgraphIso_iff` proven

3 `subgraphIso_NP_complete` proven

Lean source view on GitHub

Discussion

Settings

Your comments

Subgraph Isomorphism

Natural Language Statement

Theorem

1 hasSubgraphIso_iso proven

2 subgraphIso_iff proven

3 subgraphIso_NP_complete proven

Lean source view on GitHub

Discussion

1 `hasSubgraphIso_iso` proven

2 `subgraphIso_iff` proven

3 `subgraphIso_NP_complete` proven