DirectedSeeds.lean

1 import Mathlib.Order.Antisymmetrization
2 import Mathlib.Order.Preorder.Finite
3 import Mathlib.Data.Fintype.Card
4 import Mathlib.Data.Finset.Card
5 import Mathlib.Data.Nat.Find
6 import Mathlib.SetTheory.Cardinal.Finite
7 
8 /-!
9 Paper X, 7.3: minimum generating sets for a finite directed graph.
10 Edges are supplied; reachability is the actual reflexive-transitive closure.
11 Components are the quotient by mutual reachability, not stipulated labels.
12 No decidability of the edge relation is needed for the structural theorem.
13 -/
14 set_option autoImplicit false
15 namespace PaperX.DirectedSeeds
16 
17 universe u
18 variable {V : Type u}
19 
20 abbrev Reach (E : V → V → Prop) : V → V → Prop := Relation.ReflTransGen E
21 
22 abbrev Component (E : V → V → Prop) := Antisymmetrization V (Reach E)
23 
24 def component (E : V → V → Prop) : V → Component E :=
25   toAntisymmetrization (Reach E)
26 
27 theorem component_eq_iff (E : V → V → Prop) (a b : V) :
28     component E a = component E b ↔ Reach E a b ∧ Reach E b a :=
29   toAntisymmetrization_eq (Reach E) a b
30 
31 /-- A component has no incoming path from a different component. -/
32 def IsSource (E : V → V → Prop) (c : Component E) : Prop :=
33   ∀ a b, component E b = c → Reach E a b → component E a = c
34 
35 abbrev Source (E : V → V → Prop) := {c : Component E // IsSource E c}
36 
37 theorem source_iff (E : V → V → Prop) (v : V) :
38     IsSource E (component E v) ↔ ∀ a, Reach E a v → Reach E v a := by
39   constructor
40   · intro h a ha
41     exact ((component_eq_iff E a v).1 (h a v rfl ha)).2
42   · intro h a b hb hab
43     have hbv := ((component_eq_iff E b v).1 hb).1
44     have hav := hab.trans hbv
45     exact (component_eq_iff E a v).2 ⟨hav, h a hav⟩
46 
47 /-- The path-based source definition agrees with no incoming external edge. -/
48 theorem source_iff_no_external_edge (E : V → V → Prop) (c : Component E) :
49     IsSource E c ↔
50       ∀ a b, component E b = c → E a b → component E a = c := by
51   constructor
52   · intro h a b hb hab
53     exact h a b hb (.single hab)
54   · intro h a b hb hab
55     induction hab using Relation.ReflTransGen.head_induction_on with
56     | refl => exact hb
57     | @head a d had _ ih => exact h a d ih had
58 
59 /-- Every vertex in a finite graph lies downstream of an actual source component. -/
60 theorem source_reaches [Finite V] (E : V → V → Prop) (v : V) :
61     ∃ a, IsSource E (component E a) ∧ Reach E a v := by
62   let : Preorder V :=
63     { le := Reach E
64       le_refl := fun _ => .refl
65       le_trans := fun _ _ _ => Relation.ReflTransGen.trans }
66   obtain ⟨a, hav, ha⟩ := Finite.exists_le_minimal (p := fun _ : V => True) (a := v) trivial
67   exact ⟨a, (source_iff E a).2 (fun b hba => ha.2 trivial hba), hav⟩
68 
69 /-- All vertices, including seeds themselves by the empty path, are covered. -/
70 def Covers (E : V → V → Prop) (S : Finset V) : Prop :=
71   ∀ v, ∃ s ∈ S, Reach E s v
72 
73 def MeetsSources (E : V → V → Prop) (S : Finset V) : Prop :=
74   ∀ c : Source E, ∃ s ∈ S, component E s = c.val
75 
76 noncomputable def representative (E : V → V → Prop) (c : Component E) : V :=
77   ofAntisymmetrization (Reach E) c
78 
79 theorem component_representative (E : V → V → Prop) (c : Component E) :
80     component E (representative E c) = c :=
81   toAntisymmetrization_ofAntisymmetrization (Reach E) c
82 
83 theorem covers_meets_sources (E : V → V → Prop) (S : Finset V)
84     (hS : Covers E S) : MeetsSources E S := by
85   intro c
86   obtain ⟨s, hs, hpath⟩ := hS (representative E c.val)
87   exact ⟨s, hs, c.property s _ (component_representative E c.val) hpath⟩
88 
89 /-- Covering is exactly meeting all source components, for finite graphs. -/
90 theorem covers_iff_meets_sources [Finite V] (E : V → V → Prop) (S : Finset V) :
91     Covers E S ↔ MeetsSources E S := by
92   refine ⟨covers_meets_sources E S, ?_⟩
93   intro h v
94   obtain ⟨a, ha, hav⟩ := source_reaches E v
95   obtain ⟨s, hs, heq⟩ := h ⟨component E a, ha⟩
96   exact ⟨s, hs, (((component_eq_iff E s a).1 heq).1).trans hav⟩
97 
98 /-- Finiteness is inherited by the actual quotient and its source subtype. -/
99 instance componentFinite [Finite V] (E : V → V → Prop) : Finite (Component E) :=
100   inferInstanceAs (Finite (Quotient (AntisymmRel.setoid V (Reach E))))
101 
102 noncomputable instance sourceFintype [Finite V] (E : V → V → Prop) : Fintype (Source E) :=
103   Fintype.ofFinite _
104 
105 noncomputable def sourceRepresentative (E : V → V → Prop) (c : Source E) : V :=
106   representative E c.val
107 
108 theorem sourceRepresentative_injective (E : V → V → Prop) :
109     Function.Injective (sourceRepresentative E) := by
110   intro a b h
111   apply Subtype.ext
112   simpa only [sourceRepresentative, component_representative] using congrArg (component E) h
113 
114 noncomputable def canonicalSeeds [Finite V] (E : V → V → Prop) : Finset V := by
115   classical
116   exact Finset.univ.image (sourceRepresentative E)
117 
118 theorem canonicalSeeds_cover [Finite V] (E : V → V → Prop) :
119     Covers E (canonicalSeeds E) := by
120   classical
121   apply (covers_iff_meets_sources E _).2
122   intro c
123   exact ⟨sourceRepresentative E c, Finset.mem_image.mpr ⟨c, Finset.mem_univ c, rfl⟩,
124     component_representative E c.val⟩
125 
126 theorem canonicalSeeds_card [Finite V] (E : V → V → Prop) :
127     (canonicalSeeds E).card = Nat.card (Source E) := by
128   classical
129   simp only [canonicalSeeds, Finset.card_image_of_injective _ (sourceRepresentative_injective E),
130     Finset.card_univ, Nat.card_eq_fintype_card]
131 
132 /-- Every covering seed set has at least one distinct member per source component. -/
133 theorem source_count_le [Finite V] (E : V → V → Prop) (S : Finset V)
134     (hS : Covers E S) : Nat.card (Source E) ≤ S.card := by
135   classical
136   have h := covers_meets_sources E S hS
137   choose s hs hc using h
138   let f : Source E → {v // v ∈ S} := fun c => ⟨s c, hs c⟩
139   have hf : Function.Injective f := by
140     intro a b heq
141     apply Subtype.ext
142     have hs' : s a = s b := congrArg Subtype.val heq
143     exact (hc a).symm.trans ((congrArg (component E) hs').trans (hc b))
144   simpa only [Nat.card_eq_fintype_card, Fintype.card_coe] using Fintype.card_le_of_injective f hf
145 
146 /-- Existence of an optimal seed set, with the lower bound proved separately. -/
147 theorem minimum_seed_set [Finite V] (E : V → V → Prop) :
148     ∃ S : Finset V, Covers E S ∧ S.card = Nat.card (Source E) ∧
149       ∀ T : Finset V, Covers E T → S.card ≤ T.card := by
150   refine ⟨canonicalSeeds E, canonicalSeeds_cover E, canonicalSeeds_card E, ?_⟩
151   intro T hT
152   rw [canonicalSeeds_card]
153   exact source_count_le E T hT
154 
155 theorem exists_cover_card [Finite V] (E : V → V → Prop) :
156     ∃ n : ℕ, ∃ S : Finset V, Covers E S ∧ S.card = n :=
157   ⟨_, canonicalSeeds E, canonicalSeeds_cover E, rfl⟩
158 
159 /-- Rank is the least cardinality of a genuinely covering finite seed set. -/
160 noncomputable def seedRank [Finite V] (E : V → V → Prop) : ℕ :=
161   by
162   classical
163   exact Nat.find (exists_cover_card E)
164 
165 theorem seedRank_realized [Finite V] (E : V → V → Prop) :
166     ∃ S : Finset V, Covers E S ∧ S.card = seedRank E :=
167   by
168   classical
169   exact Nat.find_spec (exists_cover_card E)
170 
171 theorem seedRank_le [Finite V] (E : V → V → Prop) (S : Finset V)
172     (hS : Covers E S) : seedRank E ≤ S.card :=
173   by
174   classical
175   exact Nat.find_min' (exists_cover_card E) ⟨S, hS, rfl⟩
176 
177 /-- Paper X 7.3, with the minimization and component count independently defined. -/
178 theorem directed_minimum_seed [Finite V] (E : V → V → Prop) :
179     seedRank E = Nat.card (Source E) := by
180   apply Nat.le_antisymm
181   · simpa only [canonicalSeeds_card] using seedRank_le E _ (canonicalSeeds_cover E)
182   · obtain ⟨S, hS, hcard⟩ := seedRank_realized E
183     rw [← hcard]
184     exact source_count_le E S hS
185 
186 end PaperX.DirectedSeeds

Back to source controls