Skip to content

Commit 5d21312

Browse files
vlad902vlad902
committed
chore(SimpleGraph): move cycleGraph to its own file
PR #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 529f8af commit 5d21312

2 files changed

Lines changed: 172 additions & 148 deletions

File tree

‎Mathlib/Combinatorics/SimpleGraph/Circulant.lean‎

Lines changed: 1 addition & 148 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.Cycle
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,152 +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-
symm _ _ := Or.symm
69-
loopless.irrefl _ h := h.elim (by simp) (by simp)
70-
}
71-
72-
instance : (n : ℕ) → DecidableRel (cycleGraph n).Adj
73-
| 0 | 1 => fun _ _ => inferInstanceAs (Decidable False)
74-
| _ + 2 => by unfold cycleGraph; infer_instance
75-
7659
theorem cycleGraph_eq_circulantGraph (n : ℕ) : cycleGraph (n + 1) = circulantGraph {1} := by
7760
cases n
7861
· exact edgeFinset_inj.mp rfl
7962
· aesop
8063

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

‎Mathlib/Combinatorics/SimpleGraph/Cycle.lean‎

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
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+
symm _ _ := Or.symm
34+
loopless.irrefl _ h := h.elim (by simp) (by simp)
35+
}
36+
37+
instance : (n : ℕ) → DecidableRel (cycleGraph n).Adj
38+
| 0 | 1 => fun _ _ => inferInstanceAs (Decidable False)
39+
| _ + 2 => by unfold cycleGraph; infer_instance
40+
41+
theorem cycleGraph_zero_adj {u v : Fin 0} : ¬(cycleGraph 0).Adj u v := id
42+
43+
theorem cycleGraph_zero_eq_bot : cycleGraph 0 = ⊥ := Subsingleton.elim _ _
44+
theorem cycleGraph_one_eq_bot : cycleGraph 1 = ⊥ := Subsingleton.elim _ _
45+
theorem cycleGraph_zero_eq_top : cycleGraph 0 = ⊤ := Subsingleton.elim _ _
46+
theorem cycleGraph_one_eq_top : cycleGraph 1 = ⊤ := Subsingleton.elim _ _
47+
48+
theorem cycleGraph_two_eq_top : cycleGraph 2 = ⊤ := by
49+
simp only [SimpleGraph.ext_iff, funext_iff]
50+
decide
51+
52+
theorem cycleGraph_three_eq_top : cycleGraph 3 = ⊤ := by
53+
simp only [SimpleGraph.ext_iff, funext_iff]
54+
decide
55+
56+
theorem cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v := by
57+
simp [cycleGraph_one_eq_bot]
58+
59+
theorem cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} :
60+
(cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1 := Iff.rfl
61+
62+
theorem cycleGraph_adj' {n : ℕ} {u v : Fin n} :
63+
(cycleGraph n).Adj u v ↔ (u - v).val = 1 ∨ (v - u).val = 1 := by
64+
match n with
65+
| 0 => exact u.elim0
66+
| 1 => simp [cycleGraph_one_adj]
67+
| n + 2 => simp [cycleGraph_adj, Fin.ext_iff]
68+
69+
theorem cycleGraph_neighborSet {n : ℕ} {v : Fin (n + 2)} :
70+
(cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1} := by
71+
ext w
72+
simp only [mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff]
73+
rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]
74+
75+
theorem cycleGraph_neighborFinset {n : ℕ} {v : Fin (n + 2)} :
76+
(cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1} := by
77+
simp [neighborFinset, cycleGraph_neighborSet]
78+
79+
theorem cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} :
80+
(cycleGraph (n + 2)).degree v = Finset.card {v - 1, v + 1} := by
81+
rw [SimpleGraph.degree, cycleGraph_neighborFinset]
82+
83+
theorem cycleGraph_degree_three_le {n : ℕ} {v : Fin (n + 3)} :
84+
(cycleGraph (n + 3)).degree v = 2 := by
85+
rw [cycleGraph_degree_two_le, Finset.card_pair]
86+
simp only [ne_eq, sub_eq_iff_eq_add, add_assoc v, left_eq_add]
87+
exact ne_of_beq_false rfl
88+
89+
theorem pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n := by
90+
match n with
91+
| 0 | 1 => simp
92+
| n + 2 =>
93+
intro u v h
94+
rw [pathGraph_adj] at h
95+
rw [cycleGraph_adj']
96+
cases h with
97+
| inl h | inr h =>
98+
simp [Fin.coe_sub_iff_le.mpr (Nat.lt_of_succ_le h.le).le, Nat.eq_sub_of_add_eq' h]
99+
100+
theorem cycleGraph_preconnected {n : ℕ} : (cycleGraph n).Preconnected :=
101+
(pathGraph_preconnected n).mono pathGraph_le_cycleGraph
102+
103+
theorem cycleGraph_connected {n : ℕ} : (cycleGraph (n + 1)).Connected :=
104+
(pathGraph_connected n).mono pathGraph_le_cycleGraph
105+
106+
section cycle
107+
108+
set_option backward.privateInPublic true in
109+
private def cycleGraph.cycleCons (n : ℕ) : ∀ m : Fin (n + 3), (cycleGraph (n + 3)).Walk m 0
110+
| ⟨0, h⟩ => Walk.nil
111+
| ⟨m + 1, h⟩ =>
112+
have hadj : (cycleGraph (n + 3)).Adj ⟨m + 1, h⟩ ⟨m, Nat.lt_of_succ_lt h⟩ := by
113+
simp [cycleGraph_adj, Fin.ext_iff, Fin.sub_val_of_le]
114+
Walk.cons hadj (cycleGraph.cycleCons n ⟨m, Nat.lt_of_succ_lt h⟩)
115+
116+
set_option backward.privateInPublic true in
117+
set_option backward.privateInPublic.warn false in
118+
/-- The Eulerian cycle of `cycleGraph (n + 3)` -/
119+
def cycleGraph.cycle (n : ℕ) : (cycleGraph (n + 3)).Walk 0 0 :=
120+
have hadj : (cycleGraph (n + 3)).Adj 0 (Fin.last (n + 2)) := by
121+
simp [cycleGraph_adj]
122+
Walk.cons hadj (cycleGraph.cycleCons n (Fin.last (n + 2)))
123+
124+
@[deprecated (since := "2026-02-15")]
125+
alias cycleGraph_EulerianCircuit := cycleGraph.cycle
126+
127+
private theorem cycleGraph.length_cycle_cons (n : ℕ) :
128+
∀ m : Fin (n + 3), (cycleGraph.cycleCons n m).length = m.val
129+
| ⟨0, h⟩ => by
130+
unfold cycleGraph.cycleCons
131+
rfl
132+
| ⟨m + 1, h⟩ => by
133+
unfold cycleGraph.cycleCons
134+
simp only [Walk.length_cons]
135+
rw [cycleGraph.length_cycle_cons n]
136+
137+
variable {n : ℕ}
138+
139+
@[simp, grind =]
140+
theorem cycleGraph.length_cycle : (cycleGraph.cycle n).length = n + 3 := by
141+
unfold cycleGraph.cycle
142+
simp [cycleGraph.length_cycle_cons]
143+
144+
@[deprecated (since := "2026-02-15")]
145+
alias cycleGraph_EulerianCircuit_length := cycleGraph.length_cycle
146+
147+
private theorem cycleGraph.getVert_cycleCons (m : Fin (n + 3)) (i : ℕ) (hi : i ≤ m.val) :
148+
(cycleGraph.cycleCons n m).getVert i = (m - i) % (n + 3) := by
149+
obtain ⟨m, hm⟩ := m
150+
induction i generalizing m
151+
· simp [Nat.mod_eq_of_lt hm]
152+
· cases m <;> grind +locals [getVert_cons_succ]
153+
154+
theorem cycleGraph.getVert_cycle {m : ℕ} (hm : m ≤ n + 3) :
155+
(cycleGraph.cycle n).getVert m = ⟨(n + 3 - m) % (n + 3), Nat.mod_lt _ (by lia)⟩ := by
156+
cases m
157+
· simp
158+
· grind +locals [getVert_cons_succ, cycleGraph.getVert_cycleCons]
159+
160+
theorem cycleGraph.isPath_tail_cycle : (cycleGraph.cycle n).tail.IsPath := by
161+
refine isPath_iff_injective_get_support _ |>.mpr fun ⟨i, hi⟩ ⟨j, hj⟩ hij ↦ ?_
162+
rw [support_tail_of_not_nil _ (of_decide_eq_false rfl)] at hi hj
163+
simp only [List.get_eq_getElem, support_getElem_eq_getVert, getVert_tail] at hij
164+
grind [← Nat.mod_eq_of_lt, cycleGraph.getVert_cycle]
165+
166+
theorem cycleGraph.isCycle_cycle : (cycleGraph.cycle n).IsCycle :=
167+
isCycle_iff_isPath_tail_and_le_length.mpr ⟨cycleGraph.isPath_tail_cycle, by simp⟩
168+
169+
end cycle
170+
171+
end SimpleGraph

0 commit comments

Comments
 (0)