Hamilton circuits

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

proven

Loading review…

Natural Language Statement

Theorem

DIRECTED HAMILTON CIRCUIT and HAMILTON CIRCUIT: does a graph have a circuit visiting every vertex exactly once? Both live on the vocabulary of digraphs, a single binary relation; the undirected problem reads that relation symmetrically (DGEdge). A circuit is read, after cutting it anywhere, as a linear order whose consecutive elements are adjacent and whose last element is adjacent to its first (TourOn); a relation is what an existential second-order block can guess, and the rest is first-order, so both problems are in NP. The empty graph is a yes-instance and a one-element graph is one exactly when it has a self-loop. Hardness of the undirected problem is a relativized ordered first-order reduction from Vertex Cover, the one reduction of the catalog that needs the relativized form; the directed problem is NP-hard by a first-order reduction from the undirected one.

Concept map

8 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

Lean source view on GitHub

Show types on hover

1	import Mathlib.ModelTheory.Semantics
2	import Mathlib.ModelTheory.Complexity
3	import Mathlib.Tactic.FinCases
4	import Mathlib.Algebra.BigOperators.Finprod
5	import Mathlib.Data.Set.Finite.Lemmas
6	import Mathlib.Data.Fintype.EquivFin
7	import Mathlib.Data.Set.Card
8	import Mathlib.SetTheory.Cardinal.Finite
9	import Mathlib.Logic.Equiv.Prod
10	import Mathlib.ModelTheory.Syntax
11	import Lax904597.Machines
12	import Lax904597.Classes
13	import Lax799700.Problems
14
15	/-!
16	---
17	title: Hamilton circuits
18	type: theorem
19	---
20	DIRECTED HAMILTON CIRCUIT and HAMILTON CIRCUIT: does a graph have a
21	circuit visiting every vertex exactly once? Both live on the vocabulary
22	of digraphs, a single binary relation; the undirected problem reads that
23	relation symmetrically (DGEdge). A circuit is read, after cutting it
24	anywhere, as a linear order whose consecutive elements are adjacent and
25	whose last element is adjacent to its first (TourOn); a relation is what
26	an existential second-order block can guess, and the rest is first-order,
27	so both problems are in NP. The empty graph is a yes-instance and a
28	one-element graph is one exactly when it has a self-loop. Hardness of
29	the undirected problem is a relativized ordered first-order reduction
30	from Vertex Cover, the one reduction of the catalog that needs the
31	relativized form; the directed problem is NP-hard by a first-order
32	reduction from the undirected one.
33
34	-/
35
36	namespace Lax799700.Hamilton
37
38	open Lax904597.Machines
39
40	open FirstOrder
41
42	open FirstOrder.Language
43
44	/-- The relation symbols of the language. -/
45	inductive digraphRel : ℕ → Type where
46	/-- `arc a b`: there is an arc from `a` to `b`. -/
47	\| arc : digraphRel 2
48	deriving DecidableEq
49
50	/-- The relational language of digraphs: one binary relation. The undirected
51	problem reads it symmetrically rather than on a vocabulary of its own. -/
52	def digraph : FirstOrder.Language :=
53	⟨fun _ => Empty, digraphRel⟩
54
55	instance instIsRelationalDigraph : FirstOrder.Language.IsRelational digraph := fun _ =>
56	(inferInstance : IsEmpty Empty)
57
58	/-- `arc a b`: there is an arc from `a` to `b`. -/
59	abbrev dgArc : digraph.Relations 2 :=
60	.arc
61
62	open FirstOrder
63
64	open Language Structure
65
66	section Tour
67
68	variable {A : Type}
69
70	/-- `y` is the immediate `Le`-successor of `x`: above it, distinct from it,
71	and with nothing strictly in between. -/
72	def SuccOf (Le : A → A → Prop) (x y : A) : Prop :=
73	Le x y ∧ x ≠ y ∧ ∀ z, Le x z → Le z y → z = x ∨ z = y
74
75	/-- A tour of a relation: a linear order of the universe whose
76	consecutive elements are related and whose last element is related to its
77	first. On a finite universe this is exactly a Hamilton circuit, cut open at
78	one place. -/
79	def TourOn (R : A → A → Prop) : Prop :=
80	∃ Le : A → A → Prop, IsLinOrd Le ∧ (∀ x y, SuccOf Le x y → R x y) ∧
81	∀ x y, (∀ z, Le x z) → (∀ z, Le z y) → R y x
82
83	end Tour
84
85	section Problems
86
87	variable {A : Type} [digraph.Structure A]
88
89	/-- `arc a b`: there is an arc from `a` to `b`. -/
90	def DGArc {A : Type} [digraph.Structure A] (a0 : A) (a1 : A) : Prop :=
91	FirstOrder.Language.Structure.RelMap dgArc ![a0, a1]
92
93	/-- There is an edge between `a` and `b`: the arc relation read
94	symmetrically, which is how the undirected problem reads its instance. -/
95	def DGEdge (a b : A) : Prop := DGArc a b ∨ DGArc b a
96
97	variable (A) in
98	/-- A digraph is a yes-instance of DIRECTED HAMILTON CIRCUIT when its arcs
99	carry a tour of the universe. -/
100	def HasDirHamCircuit : Prop := Finite A ∧ TourOn (DGArc (A := A))
101
102	variable (A) in
103	/-- A graph is a yes-instance of HAMILTON CIRCUIT when its edges – the arcs
104	read symmetrically – carry a tour of the universe. -/
105	def HasHamCircuit : Prop := Finite A ∧ TourOn (DGEdge (A := A))
106
107	end Problems
108
109	open Lax904597.Problems Lax904597.Classes Lax799700.Problems
110
111	/-- The property `HasHamCircuit` is isomorphism-invariant. -/
112	axiom hasHamCircuit_iso : ∀ {A B : Type} [Lax799700.Hamilton.digraph.Structure A] [Lax799700.Hamilton.digraph.Structure B],
113	(A ≃[Lax799700.Hamilton.digraph] B) → (HasHamCircuit A ↔ HasHamCircuit B)
114
115	/-- The problem HamCircuit: does the structure satisfy `HasHamCircuit`? -/
116	def HamCircuit : DecisionProblem Lax799700.Hamilton.digraph :=
117	DecisionProblem.ofPred HasHamCircuit
118
119	/-- The yes-instances of HamCircuit are exactly the structures satisfying
120	`HasHamCircuit`. -/
121	axiom hamCircuit_iff : ∀ (A : Type) [Lax799700.Hamilton.digraph.Structure A], HamCircuit A ↔ HasHamCircuit A
122
123	/-- HamCircuit is NP-complete. -/
124	axiom hamCircuit_NP_complete : NP.Complete HamCircuit
125
126	/-- The property `HasDirHamCircuit` is isomorphism-invariant. -/
127	axiom hasDirHamCircuit_iso : ∀ {A B : Type} [Lax799700.Hamilton.digraph.Structure A] [Lax799700.Hamilton.digraph.Structure B],
128	(A ≃[Lax799700.Hamilton.digraph] B) → (HasDirHamCircuit A ↔ HasDirHamCircuit B)
129
130	/-- The problem DirHamCircuit: does the structure satisfy `HasDirHamCircuit`? -/
131	def DirHamCircuit : DecisionProblem Lax799700.Hamilton.digraph :=
132	DecisionProblem.ofPred HasDirHamCircuit
133
134	/-- The yes-instances of DirHamCircuit are exactly the structures satisfying
135	`HasDirHamCircuit`. -/
136	axiom dirHamCircuit_iff : ∀ (A : Type) [Lax799700.Hamilton.digraph.Structure A], DirHamCircuit A ↔ HasDirHamCircuit A
137
138	/-- DirHamCircuit is NP-complete. -/
139	axiom dirHamCircuit_NP_complete : NP.Complete DirHamCircuit
140
141	end Lax799700.Hamilton
142

Show ProofShow ProofShow ProofShow 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

Hamilton circuits

Flags

Flag this concept

Natural Language Statement

Theorem

1 `dirHamCircuit_iff` proven

2 `dirHamCircuit_NP_complete` proven

3 `hamCircuit_iff` proven

4 `hamCircuit_NP_complete` proven

5 `hasDirHamCircuit_iso` proven

6 `hasHamCircuit_iso` proven

Lean source view on GitHub

Discussion

Settings