GraphSources.lean

1 import PaperIRelease.GraphReachability
2 import Mathlib.Order.Antisymmetrization
3 import Mathlib.Order.WellFoundedSet
4 
5 /-! Finite condensation is the actual quotient by mutual graph reachability.
6 Every vertex is proved reachable from a source component by finite minimality. -/
7 
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PaperIRelease.FiniteDigraph
12 
13 universe w
14 variable {I : Type w}
15 
16 abbrev Reach (edge : I → I → Prop) := Relation.ReflTransGen edge
17 
18 @[instance_reducible] def reachPreorder (edge : I → I → Prop) : Preorder I where
19   le := Reach edge
20   le_refl _ := .refl
21   le_trans _ _ _ := Relation.ReflTransGen.trans
22 
23 /-- Strongly connected components are classes of mutual reachability. -/
24 def SCC (edge : I → I → Prop) := Antisymmetrization I (Reach edge)
25 
26 instance sccPartialOrder (edge : I → I → Prop) : PartialOrder (SCC edge) :=
27   @instPartialOrderAntisymmetrization I (reachPreorder edge)
28 
29 def component (edge : I → I → Prop) : I → SCC edge :=
30   toAntisymmetrization (Reach edge)
31 
32 theorem component_surjective (edge : I → I → Prop) : Function.Surjective (component edge) := by
33   intro C
34   exact ⟨ofAntisymmetrization (Reach edge) C, toAntisymmetrization_ofAntisymmetrization (Reach edge) C⟩
35 
36 @[simp] theorem component_le_iff (edge : I → I → Prop) (a b : I) :
37     component edge a ≤ component edge b ↔ Reach edge a b := Iff.rfl
38 
39 @[simp] theorem component_eq_iff (edge : I → I → Prop) (a b : I) :
40     component edge a = component edge b ↔ Reach edge a b ∧ Reach edge b a :=
41   toAntisymmetrization_eq (Reach edge) a b
42 
43 instance sccFintype [Fintype I] (edge : I → I → Prop) : Fintype (SCC edge) := by
44   classical
45   exact Fintype.ofSurjective (component edge) (component_surjective edge)
46 
47 instance sccDecidableEq (edge : I → I → Prop) : DecidableEq (SCC edge) := Classical.decEq _
48 
49 /-- A source component has no strictly preceding component in condensation. -/
50 def Source (edge : I → I → Prop) (C : SCC edge) : Prop := ∀ D, D ≤ C → D = C
51 
52 abbrev Sources (edge : I → I → Prop) := {C : SCC edge // Source edge C}
53 
54 instance sourcesFintype [Fintype I] (edge : I → I → Prop) : Fintype (Sources edge) :=
55   Fintype.ofFinite _
56 
57 /-- An actual edge of the condensation graph joins distinct SCCs and is
58 witnessed by an original graph edge between their vertices. -/
59 def CondensationEdge (edge : I → I → Prop) (C D : SCC edge) : Prop :=
60   C ≠ D ∧ ∃ a b, component edge a = C ∧ component edge b = D ∧ edge a b
61 
62 /-- Order-minimal components are exactly the sources of the actual
63 condensation graph, rather than an independently supplied source set. -/
64 theorem source_iff_no_incoming_edge (edge : I → I → Prop) (C : SCC edge) :
65     Source edge C ↔ ∀ D, ¬ CondensationEdge edge D C := by
66   constructor
67   · intro hC D hDC
68     obtain ⟨hne, a, b, ha, hb, hab⟩ := hDC
69     apply hne
70     apply hC
71     rw [← ha, ← hb]
72     exact (component_le_iff edge a b).mpr (.single hab)
73   · intro hnone D hDC
74     obtain ⟨a, rfl⟩ := component_surjective edge D
75     obtain ⟨b, hb⟩ := component_surjective edge C
76     have hab : Reach edge a b := (component_le_iff edge a b).mp (hb ▸ hDC)
77     have hback : ∀ {x y : I}, Reach edge x y → component edge y = C →
78         component edge x = C := by
79       intro x y hxy
80       induction hxy using Relation.ReflTransGen.head_induction_on with
81       | refl => exact id
82       | @head x z hxz hzy ih =>
83         intro hy
84         have hz := ih hy
85         by_contra hx
86         exact hnone (component edge x) ⟨hx, x, z, rfl, hz, hxz⟩
87     exact hback hab hb
88 
89 /-- Every component in a finite directed graph lies above a source.
90 No topological ordering or reachability certificate is supplied as a premise. -/
91 theorem exists_source_le [Fintype I] (edge : I → I → Prop) (C : SCC edge) :
92     ∃ D : Sources edge, D.val ≤ C := by
93   obtain ⟨D, hDC, hD⟩ := (Set.finite_univ : (Set.univ : Set (SCC edge)).Finite).isPWO.exists_le_minimal
94     (a := C) (Set.mem_univ C)
95   refine ⟨⟨D, ?_⟩, hDC⟩
96   intro E hED
97   exact le_antisymm hED (hD.2 (Set.mem_univ E) hED)
98 
99 /-- Every vertex is reached from an actual vertex in an actual source SCC. -/
100 theorem exists_source_reaching [Fintype I] (edge : I → I → Prop) (b : I) :
101     ∃ C : Sources edge, ∃ a : I, component edge a = C.val ∧ Reach edge a b := by
102   obtain ⟨C, hC⟩ := exists_source_le edge (component edge b)
103   obtain ⟨a, ha⟩ := component_surjective edge C.val
104   refine ⟨C, a, ha, ?_⟩
105   exact (component_le_iff edge a b).mp (ha ▸ hC)
106 
107 /-- A path entering a source SCC must have started in that same SCC. -/
108 theorem no_reach_into_source (edge : I → I → Prop) (C : Sources edge)
109     {a b : I} (hb : component edge b = C.val) (hab : Reach edge a b) :
110     component edge a = C.val := by
111   apply C.property
112   rw [← hb]
113   exact (component_le_iff edge a b).mpr hab
114 
115 theorem source_vertex_iff (edge : I → I → Prop) (a : I) :
116     Source edge (component edge a) ↔ ∀ b, Reach edge b a → Reach edge a b := by
117   constructor
118   · intro h b hba
119     exact ((component_eq_iff edge b a).mp (h _ hba)).2
120   · intro h C hC
121     obtain ⟨b, rfl⟩ := component_surjective edge C
122     exact (component_eq_iff edge b a).mpr ⟨hC, h b hC⟩
123 
124 /-- Paths between vertices of one SCC stay in that SCC at every intermediate vertex. -/
125 theorem intermediate_same_component (edge : I → I → Prop) {a b c : I}
126     (hac : component edge a = component edge c)
127     (hab : Reach edge a b) (hbc : Reach edge b c) :
128     component edge b = component edge a := by
129   have hca := ((component_eq_iff edge a c).mp hac).2
130   exact (component_eq_iff edge b a).mpr ⟨hbc.trans hca, hab⟩
131 
132 end Komorebi.PaperIRelease.FiniteDigraph

Back to source controls