Skip to content

Commit d6e37a2

Browse files
vlad902vlad902
committed
chore(SimpleGraph): move cycleGraph to its own file (leanprover-community#37930)
PR leanprover-community#34797 re-defined `cycleGraph` independent of `circulantGraph`. Now move the definition of `cycleGraph` to its own file so that the definition can be used without importing the algebra hierarchy.
1 parent 8ac5928 commit d6e37a2

3 files changed

Lines changed: 171 additions & 146 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3631,6 +3631,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
36313631
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
36323632
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
36333633
public import Mathlib.Combinatorics.SimpleGraph.Copy
3634+
public import Mathlib.Combinatorics.SimpleGraph.CycleGraph
36343635
public import Mathlib.Combinatorics.SimpleGraph.Dart
36353636
public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
36363637
public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges

‎Mathlib/Combinatorics/SimpleGraph/Circulant.lean‎

Lines changed: 1 addition & 146 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,8 @@ Authors: Iván Renison, Bhavik Mehta
55
-/
66
module
77

8-
public import Mathlib.Algebra.Group.Fin.Basic
9-
public import Mathlib.Combinatorics.SimpleGraph.Hasse
108
public import Mathlib.Algebra.Group.Pointwise.Set.Basic
9+
public import Mathlib.Combinatorics.SimpleGraph.CycleGraph
1110

1211
/-!
1312
# Definition of circulant graphs
@@ -19,15 +18,12 @@ are adjacent if and only if `u - v ∈ s` or `v - u ∈ s`. The elements of `s`
1918
## Main declarations
2019
2120
* `SimpleGraph.circulantGraph s`: the circulant graph over `G` with jumps `s`.
22-
* `SimpleGraph.cycleGraph n`: the cycle graph over `Fin n`.
2321
-/
2422

2523
@[expose] public section
2624

2725
namespace SimpleGraph
2826

29-
open Walk
30-
3127
/-- Circulant graph over additive group `G` with jumps `s` -/
3228
@[simps!]
3329
def circulantGraph {G : Type*} [AddGroup G] (s : Set G) : SimpleGraph G :=
@@ -60,150 +56,9 @@ instance [DecidableEq G] [DecidablePred (· ∈ s)] : DecidableRel (circulantGra
6056
theorem circulantGraph_adj_translate {s : Set G} {u v d : G} :
6157
(circulantGraph s).Adj (u + d) (v + d) ↔ (circulantGraph s).Adj u v := by simp
6258

63-
/-- Cycle graph over `Fin n` -/
64-
def cycleGraph : (n : ℕ) → SimpleGraph (Fin n)
65-
| 0 | 1 => ⊥
66-
| _ + 2 => {
67-
Adj a b := a - b = 1 ∨ b - a = 1
68-
}
69-
70-
instance : (n : ℕ) → DecidableRel (cycleGraph n).Adj
71-
| 0 | 1 => fun _ _ => inferInstanceAs (Decidable False)
72-
| _ + 2 => by unfold cycleGraph; infer_instance
73-
7459
theorem cycleGraph_eq_circulantGraph (n : ℕ) : cycleGraph (n + 1) = circulantGraph {1} := by
7560
cases n
7661
· exact edgeFinset_inj.mp rfl
7762
· aesop
7863

79-
theorem cycleGraph_zero_adj {u v : Fin 0} : ¬(cycleGraph 0).Adj u v := id
80-
81-
theorem cycleGraph_zero_eq_bot : cycleGraph 0 = ⊥ := Subsingleton.elim _ _
82-
theorem cycleGraph_one_eq_bot : cycleGraph 1 = ⊥ := Subsingleton.elim _ _
83-
theorem cycleGraph_zero_eq_top : cycleGraph 0 = ⊤ := Subsingleton.elim _ _
84-
theorem cycleGraph_one_eq_top : cycleGraph 1 = ⊤ := Subsingleton.elim _ _
85-
86-
theorem cycleGraph_two_eq_top : cycleGraph 2 = ⊤ := by
87-
simp only [SimpleGraph.ext_iff, funext_iff]
88-
decide
89-
90-
theorem cycleGraph_three_eq_top : cycleGraph 3 = ⊤ := by
91-
simp only [SimpleGraph.ext_iff, funext_iff]
92-
decide
93-
94-
theorem cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v := by
95-
simp [cycleGraph_one_eq_bot]
96-
97-
theorem cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} :
98-
(cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1 := Iff.rfl
99-
100-
theorem cycleGraph_adj' {n : ℕ} {u v : Fin n} :
101-
(cycleGraph n).Adj u v ↔ (u - v).val = 1 ∨ (v - u).val = 1 := by
102-
match n with
103-
| 0 => exact u.elim0
104-
| 1 => simp [cycleGraph_one_adj]
105-
| n + 2 => simp [cycleGraph_adj, Fin.ext_iff]
106-
107-
theorem cycleGraph_neighborSet {n : ℕ} {v : Fin (n + 2)} :
108-
(cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1} := by
109-
ext w
110-
simp only [mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff]
111-
rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]
112-
113-
theorem cycleGraph_neighborFinset {n : ℕ} {v : Fin (n + 2)} :
114-
(cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1} := by
115-
simp [neighborFinset, cycleGraph_neighborSet]
116-
117-
theorem cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} :
118-
(cycleGraph (n + 2)).degree v = Finset.card {v - 1, v + 1} := by
119-
rw [SimpleGraph.degree, cycleGraph_neighborFinset]
120-
121-
theorem cycleGraph_degree_three_le {n : ℕ} {v : Fin (n + 3)} :
122-
(cycleGraph (n + 3)).degree v = 2 := by
123-
rw [cycleGraph_degree_two_le, Finset.card_pair]
124-
simp only [ne_eq, sub_eq_iff_eq_add, add_assoc v, left_eq_add]
125-
exact ne_of_beq_false rfl
126-
127-
theorem pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n := by
128-
match n with
129-
| 0 | 1 => simp
130-
| n + 2 =>
131-
intro u v h
132-
rw [pathGraph_adj] at h
133-
rw [cycleGraph_adj']
134-
cases h with
135-
| inl h | inr h =>
136-
simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]
137-
138-
theorem cycleGraph_preconnected {n : ℕ} : (cycleGraph n).Preconnected :=
139-
(pathGraph_preconnected n).mono pathGraph_le_cycleGraph
140-
141-
theorem cycleGraph_connected {n : ℕ} : (cycleGraph (n + 1)).Connected :=
142-
(pathGraph_connected n).mono pathGraph_le_cycleGraph
143-
144-
section cycle
145-
146-
set_option backward.privateInPublic true in
147-
private def cycleGraph.cycleCons (n : ℕ) : ∀ m : Fin (n + 3), (cycleGraph (n + 3)).Walk m 0
148-
| ⟨0, h⟩ => Walk.nil
149-
| ⟨m + 1, h⟩ =>
150-
have hadj : (cycleGraph (n + 3)).Adj ⟨m + 1, h⟩ ⟨m, Nat.lt_of_succ_lt h⟩ := by
151-
simp [cycleGraph_adj, Fin.ext_iff, Fin.sub_val_of_le]
152-
Walk.cons hadj (cycleGraph.cycleCons n ⟨m, Nat.lt_of_succ_lt h⟩)
153-
154-
set_option backward.privateInPublic true in
155-
set_option backward.privateInPublic.warn false in
156-
/-- The Eulerian cycle of `cycleGraph (n + 3)` -/
157-
def cycleGraph.cycle (n : ℕ) : (cycleGraph (n + 3)).Walk 0 0 :=
158-
have hadj : (cycleGraph (n + 3)).Adj 0 (Fin.last (n + 2)) := by
159-
simp [cycleGraph_adj]
160-
Walk.cons hadj (cycleGraph.cycleCons n (Fin.last (n + 2)))
161-
162-
@[deprecated (since := "2026-02-15")]
163-
alias cycleGraph_EulerianCircuit := cycleGraph.cycle
164-
165-
private theorem cycleGraph.length_cycle_cons (n : ℕ) :
166-
∀ m : Fin (n + 3), (cycleGraph.cycleCons n m).length = m.val
167-
| ⟨0, h⟩ => by
168-
unfold cycleGraph.cycleCons
169-
rfl
170-
| ⟨m + 1, h⟩ => by
171-
unfold cycleGraph.cycleCons
172-
simp only [Walk.length_cons]
173-
rw [cycleGraph.length_cycle_cons n]
174-
175-
variable {n : ℕ}
176-
177-
@[simp, grind =]
178-
theorem cycleGraph.length_cycle : (cycleGraph.cycle n).length = n + 3 := by
179-
unfold cycleGraph.cycle
180-
simp [cycleGraph.length_cycle_cons]
181-
182-
@[deprecated (since := "2026-02-15")]
183-
alias cycleGraph_EulerianCircuit_length := cycleGraph.length_cycle
184-
185-
private theorem cycleGraph.getVert_cycleCons (m : Fin (n + 3)) (i : ℕ) (hi : i ≤ m.val) :
186-
(cycleGraph.cycleCons n m).getVert i = (m - i) % (n + 3) := by
187-
obtain ⟨m, hm⟩ := m
188-
induction i generalizing m
189-
· simp [Nat.mod_eq_of_lt hm]
190-
· cases m <;> grind +locals [getVert_cons_succ]
191-
192-
theorem cycleGraph.getVert_cycle {m : ℕ} (hm : m ≤ n + 3) :
193-
(cycleGraph.cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), Nat.mod_lt _ (by lia)⟩ := by
194-
cases m
195-
· simp
196-
· grind +locals [getVert_cons_succ, cycleGraph.getVert_cycleCons]
197-
198-
theorem cycleGraph.isPath_tail_cycle : (cycleGraph.cycle n).tail.IsPath := by
199-
refine isPath_iff_injective_get_support _ |>.mpr fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ ?_
200-
rw [support_tail_of_not_nil _ (of_decide_eq_false rfl)] at hi hj
201-
simp only [List.get_eq_getElem, support_getElem_eq_getVert, getVert_tail] at hij
202-
grind [← Nat.mod_eq_of_lt, cycleGraph.getVert_cycle]
203-
204-
theorem cycleGraph.isCycle_cycle : (cycleGraph.cycle n).IsCycle :=
205-
isCycle_iff_isPath_tail_and_le_length.mpr ⟨cycleGraph.isPath_tail_cycle, by simp⟩
206-
207-
end cycle
208-
20964
end SimpleGraph

‎Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
/-
2+
Copyright (c) 2024 Iván Renison, Bhavik Mehta. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Iván Renison, Bhavik Mehta
5+
-/
6+
module
7+
8+
public import Mathlib.Combinatorics.SimpleGraph.Hasse
9+
10+
/-!
11+
# Definition of cycle graphs
12+
13+
This file defines and proves several fact about cycle graphs on `n` vertices and the cycle around
14+
the cycle graph when `n ≥ 3`.
15+
16+
## Main declarations
17+
18+
* `SimpleGraph.cycleGraph n`: the cycle graph over `Fin n`.
19+
* `(SimpleGraph.cycleGraph n).cycle`: the cycle around `cycleGraph (n + 3)` starting at 0.
20+
-/
21+
22+
@[expose] public section
23+
24+
namespace SimpleGraph
25+
26+
open Walk
27+
28+
/-- Cycle graph over `Fin n` -/
29+
def cycleGraph : (n : ℕ) → SimpleGraph (Fin n)
30+
| 0 | 1 => ⊥
31+
| _ + 2 => {
32+
Adj a b := a - b = 1 ∨ b - a = 1
33+
}
34+
35+
instance : (n : ℕ) → DecidableRel (cycleGraph n).Adj
36+
| 0 | 1 => fun _ _ => inferInstanceAs (Decidable False)
37+
| _ + 2 => by unfold cycleGraph; infer_instance
38+
39+
theorem cycleGraph_zero_adj {u v : Fin 0} : ¬(cycleGraph 0).Adj u v := id
40+
41+
theorem cycleGraph_zero_eq_bot : cycleGraph 0 = ⊥ := Subsingleton.elim _ _
42+
theorem cycleGraph_one_eq_bot : cycleGraph 1 = ⊥ := Subsingleton.elim _ _
43+
theorem cycleGraph_zero_eq_top : cycleGraph 0 = ⊤ := Subsingleton.elim _ _
44+
theorem cycleGraph_one_eq_top : cycleGraph 1 = ⊤ := Subsingleton.elim _ _
45+
46+
theorem cycleGraph_two_eq_top : cycleGraph 2 = ⊤ := by
47+
simp only [SimpleGraph.ext_iff, funext_iff]
48+
decide
49+
50+
theorem cycleGraph_three_eq_top : cycleGraph 3 = ⊤ := by
51+
simp only [SimpleGraph.ext_iff, funext_iff]
52+
decide
53+
54+
theorem cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v := by
55+
simp [cycleGraph_one_eq_bot]
56+
57+
theorem cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} :
58+
(cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1 := Iff.rfl
59+
60+
theorem cycleGraph_adj' {n : ℕ} {u v : Fin n} :
61+
(cycleGraph n).Adj u v ↔ (u - v).val = 1 ∨ (v - u).val = 1 := by
62+
match n with
63+
| 0 => exact u.elim0
64+
| 1 => simp [cycleGraph_one_adj]
65+
| n + 2 => simp [cycleGraph_adj, Fin.ext_iff]
66+
67+
theorem cycleGraph_neighborSet {n : ℕ} {v : Fin (n + 2)} :
68+
(cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1} := by
69+
ext w
70+
simp only [mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff]
71+
rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]
72+
73+
theorem cycleGraph_neighborFinset {n : ℕ} {v : Fin (n + 2)} :
74+
(cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1} := by
75+
simp [neighborFinset, cycleGraph_neighborSet]
76+
77+
theorem cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} :
78+
(cycleGraph (n + 2)).degree v = Finset.card {v - 1, v + 1} := by
79+
rw [SimpleGraph.degree, cycleGraph_neighborFinset]
80+
81+
theorem cycleGraph_degree_three_le {n : ℕ} {v : Fin (n + 3)} :
82+
(cycleGraph (n + 3)).degree v = 2 := by
83+
rw [cycleGraph_degree_two_le, Finset.card_pair]
84+
simp only [ne_eq, sub_eq_iff_eq_add, add_assoc v, left_eq_add]
85+
exact ne_of_beq_false rfl
86+
87+
theorem pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n := by
88+
match n with
89+
| 0 | 1 => simp
90+
| n + 2 =>
91+
intro u v h
92+
rw [pathGraph_adj] at h
93+
rw [cycleGraph_adj']
94+
cases h with
95+
| inl h | inr h =>
96+
simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]
97+
98+
theorem cycleGraph_preconnected {n : ℕ} : (cycleGraph n).Preconnected :=
99+
(pathGraph_preconnected n).mono pathGraph_le_cycleGraph
100+
101+
theorem cycleGraph_connected {n : ℕ} : (cycleGraph (n + 1)).Connected :=
102+
(pathGraph_connected n).mono pathGraph_le_cycleGraph
103+
104+
section cycle
105+
106+
set_option backward.privateInPublic true in
107+
private def cycleGraph.cycleCons (n : ℕ) : ∀ m : Fin (n + 3), (cycleGraph (n + 3)).Walk m 0
108+
| ⟨0, h⟩ => Walk.nil
109+
| ⟨m + 1, h⟩ =>
110+
have hadj : (cycleGraph (n + 3)).Adj ⟨m + 1, h⟩ ⟨m, Nat.lt_of_succ_lt h⟩ := by
111+
simp [cycleGraph_adj, Fin.ext_iff, Fin.sub_val_of_le]
112+
Walk.cons hadj (cycleGraph.cycleCons n ⟨m, Nat.lt_of_succ_lt h⟩)
113+
114+
set_option backward.privateInPublic true in
115+
set_option backward.privateInPublic.warn false in
116+
/-- The Eulerian cycle of `cycleGraph (n + 3)` -/
117+
def cycleGraph.cycle (n : ℕ) : (cycleGraph (n + 3)).Walk 0 0 :=
118+
have hadj : (cycleGraph (n + 3)).Adj 0 (Fin.last (n + 2)) := by
119+
simp [cycleGraph_adj]
120+
Walk.cons hadj (cycleGraph.cycleCons n (Fin.last (n + 2)))
121+
122+
@[deprecated (since := "2026-02-15")]
123+
alias cycleGraph_EulerianCircuit := cycleGraph.cycle
124+
125+
private theorem cycleGraph.length_cycle_cons (n : ℕ) :
126+
∀ m : Fin (n + 3), (cycleGraph.cycleCons n m).length = m.val
127+
| ⟨0, h⟩ => by
128+
unfold cycleGraph.cycleCons
129+
rfl
130+
| ⟨m + 1, h⟩ => by
131+
unfold cycleGraph.cycleCons
132+
simp only [Walk.length_cons]
133+
rw [cycleGraph.length_cycle_cons n]
134+
135+
variable {n : ℕ}
136+
137+
@[simp, grind =]
138+
theorem cycleGraph.length_cycle : (cycleGraph.cycle n).length = n + 3 := by
139+
unfold cycleGraph.cycle
140+
simp [cycleGraph.length_cycle_cons]
141+
142+
@[deprecated (since := "2026-02-15")]
143+
alias cycleGraph_EulerianCircuit_length := cycleGraph.length_cycle
144+
145+
private theorem cycleGraph.getVert_cycleCons (m : Fin (n + 3)) (i : ℕ) (hi : i ≤ m.val) :
146+
(cycleGraph.cycleCons n m).getVert i = (m - i) % (n + 3) := by
147+
obtain ⟨m, hm⟩ := m
148+
induction i generalizing m
149+
· simp [Nat.mod_eq_of_lt hm]
150+
· cases m <;> grind +locals [getVert_cons_succ]
151+
152+
theorem cycleGraph.getVert_cycle {m : ℕ} (hm : m ≤ n + 3) :
153+
(cycleGraph.cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), Nat.mod_lt _ (by lia)⟩ := by
154+
cases m
155+
· simp
156+
· grind +locals [getVert_cons_succ, cycleGraph.getVert_cycleCons]
157+
158+
theorem cycleGraph.isPath_tail_cycle : (cycleGraph.cycle n).tail.IsPath := by
159+
refine isPath_iff_injective_get_support _ |>.mpr fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ ?_
160+
rw [support_tail_of_not_nil _ (of_decide_eq_false rfl)] at hi hj
161+
simp only [List.get_eq_getElem, support_getElem_eq_getVert, getVert_tail] at hij
162+
grind [← Nat.mod_eq_of_lt, cycleGraph.getVert_cycle]
163+
164+
theorem cycleGraph.isCycle_cycle : (cycleGraph.cycle n).IsCycle :=
165+
isCycle_iff_isPath_tail_and_le_length.mpr ⟨cycleGraph.isPath_tail_cycle, by simp⟩
166+
167+
end cycle
168+
169+
end SimpleGraph

0 commit comments

Comments
 (0)