GraphSourceBoundary.lean

1 import PaperIRelease.GraphSourceProjection
2 
3 set_option autoImplicit false
4 
5 namespace Komorebi.PaperIRelease.FiniteDigraph
6 
7 universe u
8 variable {I : Type u}
9 
10 /-- With no edges each vertex is a source SCC. -/
11 theorem empty_graph_source_boundary (a : I) :
12     Source (fun _ _ : I => False) (component (fun _ _ : I => False) a) := by
13   apply (source_vertex_iff _ _).mpr
14   intro b hba
15   rcases hba.cases_head with h | ⟨c, hbc, _⟩
16   · subst b; exact .refl
17   · exact hbc.elim
18 
19 def oneArrow (a b : Bool) : Prop := a = false ∧ b = true
20 
21 theorem oneArrow_no_reverse : ¬ Reach oneArrow true false := by
22   intro h
23   rcases h.cases_tail with h | ⟨c, _, hc⟩
24   · cases h
25   · cases hc.2
26 
27 /-- In the two-vertex one-arrow graph the tail is a source. -/
28 theorem oneArrow_source_boundary : Source oneArrow (component oneArrow false) := by
29   apply (source_vertex_iff _ _).mpr
30   intro b hb
31   cases b
32   · exact .refl
33   · exact (oneArrow_no_reverse hb).elim
34 
35 /-- The arrow head is not a source, and cannot be confused with its tail SCC. -/
36 theorem oneArrow_not_source_boundary : ¬ Source oneArrow (component oneArrow true) := by
37   intro h
38   exact oneArrow_no_reverse ((source_vertex_iff _ _).mp h false (.single ⟨rfl, rfl⟩))
39 
40 theorem oneArrow_components_distinct : component oneArrow false ≠ component oneArrow true := by
41   intro h
42   exact oneArrow_no_reverse ((component_eq_iff _ _ _).mp h).2
43 
44 /-- The two-vertex directed cycle contracts to one strongly connected component. -/
45 theorem twoCycle_single_component_boundary (a b : Bool) :
46     component (fun x y : Bool => x ≠ y) a = component (fun x y : Bool => x ≠ y) b := by
47   apply (component_eq_iff _ _ _).mpr
48   by_cases h : a = b
49   · subst b; exact ⟨.refl, .refl⟩
50   · exact ⟨.single h, .single (fun hba => h hba.symm)⟩
51 
52 end Komorebi.PaperIRelease.FiniteDigraph

Back to source controls