GraphSchedules.lean

1 module
2 public import Mathlib.Data.Finset.Lattice.Fold
3 public import Mathlib.Data.Finset.Card
4 public import Mathlib.Logic.Relation
5 public import Mathlib.Tactic
6 
7 /-!
8 Author: Komorebi P.
9 Paper VIII 6.6 and 10.3. Acyclicity means no nonempty directed cycle.
10 The level function is constructed from this hypothesis, not supplied as a
11 certificate. Tasks have unit duration and unrestricted parallelism. The empty
12 graph has depth zero, and zero-edge paths are included.
13 -/
14 public section
15 set_option autoImplicit false
16 namespace KomorebiPaperVIII
17 namespace DAG
18 open scoped BigOperators Classical
19 variable {V : Type*} [Fintype V]
20 
21 structure Graph (V : Type*) where
22   edge : V → V → Prop
23   acyclic : ∀ v, ¬ Relation.TransGen edge v v
24 
25 namespace Graph
26 variable (G : Graph V)
27 
28 noncomputable def ancestors (v : V) : Finset V := by
29   classical
30   exact Finset.univ.filter (fun u => Relation.TransGen G.edge u v)
31 
32 theorem mem_ancestors (u v : V) :
33     u ∈ G.ancestors v ↔ Relation.TransGen G.edge u v := by
34   classical
35   simp [ancestors]
36 
37 theorem ancestors_strict {u v : V} (h : G.edge u v) :
38     G.ancestors u ⊂ G.ancestors v := by
39   classical
40   apply Finset.ssubset_iff_subset_ne.mpr
41   constructor
42   · intro a ha
43     exact (G.mem_ancestors a v).2
44       (((G.mem_ancestors a u).1 ha).trans (Relation.TransGen.single h))
45   · intro he
46     have hm : u ∈ G.ancestors u := by
47       rw [he]
48       exact (G.mem_ancestors u v).2 (Relation.TransGen.single h)
49     exact G.acyclic u ((G.mem_ancestors u u).1 hm)
50 
51 theorem ancestors_card_lt {u v : V} (h : G.edge u v) :
52     (G.ancestors u).card < (G.ancestors v).card :=
53   Finset.card_lt_card (G.ancestors_strict h)
54 
55 theorem wellFounded : WellFounded G.edge :=
56   Subrelation.wf (fun h => G.ancestors_card_lt h)
57     (measure (fun v => (G.ancestors v).card)).wf
58 
59 noncomputable def level : V → ℕ := by
60   classical
61   exact G.wellFounded.fix (fun v f =>
62     1 + Finset.univ.sup (fun u : {u // G.edge u v} => f u.val u.property))
63 
64 theorem level_eq (v : V) :
65     G.level v = 1 + Finset.univ.sup (fun u : {u // G.edge u v} => G.level u.val) := by
66   classical
67   exact WellFounded.fix_eq G.wellFounded _ v
68 
69 theorem level_positive (v : V) : 0 < G.level v := by
70   classical
71   rw [G.level_eq]
72   omega
73 
74 theorem edge_level {u v : V} (h : G.edge u v) : G.level u < G.level v := by
75   classical
76   have hm := Finset.le_sup (f := fun w : {u // G.edge u v} => G.level w.val)
77     (Finset.mem_univ (⟨u,h⟩ : {u // G.edge u v}))
78   change G.level u ≤ _ at hm
79   rw [G.level_eq v]
80   omega
81 
82 /-- Paths are oriented source a to target b and record their edge count. -/
83 def Path : ℕ → V → V → Prop
84   | 0, b, a => b = a
85   | n+1, b, a => ∃ c, G.edge c b ∧ Path n c a
86 
87 theorem path_level_bound (n : ℕ) (b a : V) (h : G.Path n b a) :
88     G.level a + n ≤ G.level b := by
89   induction n generalizing b a with
90   | zero =>
91     have hab : b = a := h
92     subst b
93     omega
94   | succ n ih =>
95     obtain ⟨c,hc,hp⟩ := h
96     have h1 := ih c a hp
97     have h2 := G.edge_level hc
98     omega
99 
100 /-- Every level is witnessed by an actual directed path, not only an upper bound. -/
101 theorem level_attained (v : V) :
102     ∃ n a, G.Path n v a ∧ G.level v = n+1 := by
103   classical
104   induction v using G.wellFounded.induction with
105   | h v ih =>
106     by_cases hp : ∃ u, G.edge u v
107     · let : Nonempty {u // G.edge u v} := by
108         obtain ⟨u,hu⟩ := hp
109         exact ⟨⟨u,hu⟩⟩
110       obtain ⟨u,_,hu⟩ := Finset.exists_mem_eq_sup
111         (Finset.univ : Finset {u // G.edge u v}) Finset.univ_nonempty
112         (fun u => G.level u.val)
113       obtain ⟨n,a,hpath,hn⟩ := ih u.val u.property
114       refine ⟨n+1,a,⟨u.val,u.property,hpath⟩,?_⟩
115       rw [G.level_eq,hu,hn]
116       omega
117     · have : IsEmpty {u // G.edge u v} := ⟨fun u => hp ⟨u.val,u.property⟩⟩
118       refine ⟨0,v,rfl,?_⟩
119       rw [G.level_eq v]
120       simp
121 
122 /-- Stages are positive integers; zero denotes that no task has run yet. -/
123 def ValidSchedule (s : V → ℕ) : Prop :=
124   (∀ v, 0 < s v) ∧ ∀ u v, G.edge u v → s u < s v
125 
126 theorem level_valid : G.ValidSchedule G.level :=
127   ⟨G.level_positive,fun _ _ h => G.edge_level h⟩
128 
129 theorem level_minimal (s : V → ℕ) (hs : G.ValidSchedule s) (v : V) :
130     G.level v ≤ s v := by
131   classical
132   induction v using G.wellFounded.induction with
133   | h v ih =>
134     rw [G.level_eq]
135     have hm : Finset.univ.sup (fun u : {u // G.edge u v} => G.level u.val) ≤ s v - 1 := by
136       apply Finset.sup_le
137       intro u _
138       have h1 := ih u.val u.property
139       have h2 := hs.2 u.val v u.property
140       omega
141     have hpos := hs.1 v
142     omega
143 
144 noncomputable def depth : ℕ := Finset.univ.sup G.level
145 
146 theorem level_le_depth (v : V) : G.level v ≤ G.depth :=
147   Finset.le_sup (Finset.mem_univ v)
148 
149 /-- Item 10.3: a constructed schedule achieves the least possible stage count. -/
150 theorem optimal_depth (s : V → ℕ) (hs : G.ValidSchedule s) :
151     G.depth ≤ Finset.univ.sup s := by
152   classical
153   exact Finset.sup_le (fun v _ => (G.level_minimal s hs v).trans
154     (Finset.le_sup (Finset.mem_univ v)))
155 
156 theorem path_length_le_depth (n : ℕ) (b a : V) (h : G.Path n b a) :
157     n+1 ≤ G.depth := by
158   have h1 := G.path_level_bound n b a h
159   have h2 := G.level_positive a
160   have h3 := G.level_le_depth b
161   omega
162 
163 /-- Item 6.6: for nonempty graphs, depth is one plus the longest edge-path length. -/
164 theorem depth_attained [Nonempty V] :
165     ∃ n b a, G.Path n b a ∧ G.depth = n+1 ∧
166       ∀ m c d, G.Path m c d → m ≤ n := by
167   classical
168   obtain ⟨b,_,hb⟩ := Finset.exists_mem_eq_sup (Finset.univ : Finset V)
169     Finset.univ_nonempty G.level
170   obtain ⟨n,a,hp,hn⟩ := G.level_attained b
171   refine ⟨n,b,a,hp,hb.trans hn,?_⟩
172   intro m c d hm
173   have hbound := G.path_length_le_depth m c d hm
174   change G.depth = G.level b at hb
175   omega
176 
177 theorem empty_depth [IsEmpty V] : G.depth = 0 := by
178   classical
179   simp [depth]
180 
181 theorem same_level_independent {u v : V} (h : G.level u = G.level v) :
182     ¬ G.edge u v ∧ ¬ G.edge v u := by
183   constructor <;> intro he
184   · have := G.edge_level he; omega
185   · have := G.edge_level he; omega
186 
187 end Graph
188 end DAG
189 end KomorebiPaperVIII
190 
191 -- FIFTH BLOCK AXIOM AUDIT
192 #print axioms KomorebiPaperVIII.DAG.Graph.mem_ancestors
193 #print axioms KomorebiPaperVIII.DAG.Graph.ancestors_strict
194 #print axioms KomorebiPaperVIII.DAG.Graph.ancestors_card_lt
195 #print axioms KomorebiPaperVIII.DAG.Graph.wellFounded
196 #print axioms KomorebiPaperVIII.DAG.Graph.level_eq
197 #print axioms KomorebiPaperVIII.DAG.Graph.level_positive
198 #print axioms KomorebiPaperVIII.DAG.Graph.edge_level
199 #print axioms KomorebiPaperVIII.DAG.Graph.path_level_bound
200 #print axioms KomorebiPaperVIII.DAG.Graph.level_attained
201 #print axioms KomorebiPaperVIII.DAG.Graph.level_valid
202 #print axioms KomorebiPaperVIII.DAG.Graph.level_minimal
203 #print axioms KomorebiPaperVIII.DAG.Graph.level_le_depth
204 #print axioms KomorebiPaperVIII.DAG.Graph.optimal_depth
205 #print axioms KomorebiPaperVIII.DAG.Graph.path_length_le_depth
206 #print axioms KomorebiPaperVIII.DAG.Graph.depth_attained
207 #print axioms KomorebiPaperVIII.DAG.Graph.empty_depth
208 #print axioms KomorebiPaperVIII.DAG.Graph.same_level_independent
209 #print axioms KomorebiPaperVIII.DAG.Graph.level
210 #print axioms KomorebiPaperVIII.DAG.Graph.depth

Back to source controls