One family for shops with and without preemption
Lax434175.ShopFamily · concepts/Lax434175/ShopFamily.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Non-preemptive and preemptive shops share one machine model, in which a schedule is a finite list of pieces of operations as in preemptive shops. A schedule is feasible for this model if every piece occupies some machine and two different pieces that belong to the same job or share a machine are disjoint in time. An operation starts when its first piece starts and completes when its last piece ends; a job starts when its first piece starts and completes when its last piece ends.
The interruption field has the values of parallel machines, read per operation:
- none: every operation has exactly one piece, it starts at an integral time, and its length is the processing time of the operation;
- restarts: some piece of the operation has the full processing time as its length, no piece of the operation ends later, and every such piece ends at the same time;
- preemption: the lengths of the pieces of every operation sum to its processing time, or the processing time is and the operation has a piece;
- preemption without migration: preemption, and all pieces of every operation occupy the same set of machines.
The other fields are those of shops, read through the start and completion of operations: the shop type orders the operations of a job; the machine field restricts the machines of every piece; with no-wait a job completes at its start plus the sum of its processing times; of two operations of a job, the later one waits for the transportation delay, unless both delays between them are ; with a robot, one robot carries every job from an operation to the next and travels empty between the machines that the pieces of the operations occupy; the server, no-idle and batch-setup fields read "two operations share a machine" as "a piece of the one and a piece of the other share a machine". The remaining fields are the generic ones.
A problem of non-preemptive shops determines the problem of this family with the same values and no interruption, and a problem of preemptive shops the problem with the same values, preemption, and the value none in the fields that preemptive shops do not have.
Theorem. The two problems are special cases of each other. The fields of the family are sound, so that a specification that is field by field a special case of another describes a special case of the other's problem, and one that reduces to another describes a problem whose decision version reduces to that of the other.
Concept map
Evidence
This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.
1 family_sound proven
2 preemptiveShop_faithful proven
3 reducible_of_reduces proven
4 shop_faithful proven
5 specialCase_of_le proven
Lean source view on GitHub
| 1 | import Lax434175.ShopProblems |
| 2 | import Lax434175.PreemptiveShopProblems |
| 3 | import Lax434175.Interruption |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: One family for shops with and without preemption |
| 8 | type: theorem |
| 9 | --- |
| 10 | Non-preemptive and preemptive shops share one machine model, in which a |
| 11 | schedule is a finite list of pieces of operations as in preemptive shops. A |
| 12 | schedule is feasible for this model if every piece occupies some machine and |
| 13 | two different pieces that belong to the same job or share a machine are |
| 14 | disjoint in time. An operation starts when its first piece starts and |
| 15 | completes when its last piece ends; a job starts when its first piece starts |
| 16 | and completes when its last piece ends. |
| 17 | |
| 18 | The interruption field has the values of parallel machines, read per |
| 19 | operation: |
| 20 | |
| 21 | - none: every operation has exactly one piece, it starts at an integral time, |
| 22 | and its length is the processing time of the operation; |
| 23 | - restarts: some piece of the operation has the full processing time as its |
| 24 | length, no piece of the operation ends later, and every such piece ends at |
| 25 | the same time; |
| 26 | - preemption: the lengths of the pieces of every operation sum to its |
| 27 | processing time, or the processing time is and the operation has a |
| 28 | piece; |
| 29 | - preemption without migration: preemption, and all pieces of every |
| 30 | operation occupy the same set of machines. |
| 31 | |
| 32 | The other fields are those of shops, read through the start and completion |
| 33 | of operations: the shop type orders the operations of a job; the machine |
| 34 | field restricts the machines of every piece; with no-wait a job completes at |
| 35 | its start plus the sum of its processing times; of two operations of a job, |
| 36 | the later one waits for the transportation delay, unless both delays between |
| 37 | them are ; with a robot, one robot carries every job from an operation to |
| 38 | the next and travels empty between the machines that the pieces of the |
| 39 | operations occupy; the server, no-idle and batch-setup fields read "two |
| 40 | operations share a machine" as "a piece of the one and a piece of the other |
| 41 | share a machine". The remaining fields are the generic ones. |
| 42 | |
| 43 | A problem of non-preemptive shops determines the problem of this family with |
| 44 | the same values and no interruption, and a problem of preemptive shops the |
| 45 | problem with the same values, preemption, and the value none in the fields |
| 46 | that preemptive shops do not have. |
| 47 | |
| 48 | **Theorem.** The two problems are special cases of each other. The fields of |
| 49 | the family are sound, so that a specification that is field by field a |
| 50 | special case of another describes a special case of the other's problem, |
| 51 | and one that reduces to another describes a problem whose decision version |
| 52 | reduces to that of the other. |
| 53 | -/ |
| 54 | |
| 55 | namespace Lax434175.ShopFamily |
| 56 | open Lax434175.Problems Lax434175.Kernels Lax434175.Modules Lax434175.Assembly |
| 57 | open Lax434175 Lax434175.Shops |
| 58 | open Lax434175.PreemptiveShops (Piece piecesOf piecesOfJob Apart opStart opFinish) |
| 59 | |
| 60 | /-- Every piece occupies some machine, and two different pieces that belong to |
| 61 | the same job or share a machine do not overlap. -/ |
| 62 | def feasible {x : Inst} (σ : PreemptiveShops.Sched x) : Prop := |
| 63 | (∀ q ∈ σ.pieces, q.machines.Nonempty) ∧ |
| 64 | σ.pieces.Pairwise |
| 65 | (fun a b => (a.op.1 = b.op.1 ∨ ¬ Disjoint a.machines b.machines) → Apart a b) |
| 66 | |
| 67 | /-- The kernel of shops with pieces. -/ |
| 68 | def kernel : Kernel where |
| 69 | Inst := Inst |
| 70 | jobs := Inst.jobs |
| 71 | release := Inst.r |
| 72 | Sched := PreemptiveShops.Sched |
| 73 | feasible _ σ := feasible σ |
| 74 | start _ σ j := (((piecesOfJob σ j).map Piece.start).min?).getD 0 |
| 75 | completion _ σ j := (((piecesOfJob σ j).map Piece.finish).max?).getD 0 |
| 76 | |
| 77 | /-- The schedules that respect a way of interruption. -/ |
| 78 | def holds : Interruption.Mode → (x : Inst) → PreemptiveShops.Sched x → Prop |
| 79 | | .none, x, σ => ∀ o : Op x, ∃ q, piecesOf σ o = [q] ∧ |
| 80 | q.length = (x.p o.1 o.2 : NNRat) ∧ ∃ n : ℕ, q.start = (n : NNRat) |
| 81 | | .restarts, x, σ => ∀ o : Op x, ∃ q ∈ piecesOf σ o, q.length = (x.p o.1 o.2 : NNRat) ∧ |
| 82 | ∀ q' ∈ piecesOf σ o, q'.finish ≤ q.finish ∧ |
| 83 | (q'.length = (x.p o.1 o.2 : NNRat) → q'.finish = q.finish) |
| 84 | | .pmtn, x, σ => ∀ o : Op x, |
| 85 | ((piecesOf σ o).map fun q => q.length / (x.p o.1 o.2 : NNRat)).sum = 1 ∨ |
| 86 | ∃ q ∈ piecesOf σ o, x.p o.1 o.2 = 0 |
| 87 | | .pmtnNoMigration, x, σ => ∀ o : Op x, |
| 88 | (((piecesOf σ o).map fun q => q.length / (x.p o.1 o.2 : NNRat)).sum = 1 ∨ |
| 89 | ∃ q ∈ piecesOf σ o, x.p o.1 o.2 = 0) ∧ |
| 90 | ∀ q ∈ piecesOf σ o, ∀ q' ∈ piecesOf σ o, q.machines = q'.machines |
| 91 | |
| 92 | /-- The interruption field. -/ |
| 93 | def interruption : Module kernel where |
| 94 | Value := Interruption.Mode |
| 95 | Data _ _ := Unit |
| 96 | admits _ _ _ := True |
| 97 | constraint v x _ σ := holds v x σ |
| 98 | le v w := decide (v = w) |
| 99 | embed _ _ _ := () |
| 100 | |
| 101 | /-- The shop-type field. -/ |
| 102 | def shopType : Module kernel where |
| 103 | Value := ShopType |
| 104 | Data _ _ := Unit |
| 105 | admits v x _ := v.holds x |
| 106 | constraint v x _ σ := PreemptiveShops.ordered v x σ |
| 107 | le := ShopType.le |
| 108 | embed _ _ _ := () |
| 109 | |
| 110 | /-- The machine field. -/ |
| 111 | def machineSets : Module kernel where |
| 112 | Value := Machines |
| 113 | Data := Machines.Data |
| 114 | admits v _ d := v.admits d |
| 115 | constraint v _ d σ := ∀ q ∈ σ.pieces, v.view d q.op.1 q.op.2 q.machines |
| 116 | le := Machines.le |
| 117 | embed := Machines.embed |
| 118 | |
| 119 | /-- The processing-time field. -/ |
| 120 | def processingTimes : Module kernel := |
| 121 | Module.ofRestriction ProcessingTimes ProcessingTimes.holds |
| 122 | (fun v w => decide (v.rank ≤ w.rank)) |
| 123 | |
| 124 | /-- The no-wait field. -/ |
| 125 | def noWait : Module kernel where |
| 126 | Value := NoWait |
| 127 | Data _ _ := Unit |
| 128 | admits _ _ _ := True |
| 129 | constraint v x _ σ := v = .noWait → |
| 130 | ∀ j, kernel.completion x σ j = kernel.start x σ j + ∑ k, (x.p j k : NNRat) |
| 131 | le v w := decide (v = w) |
| 132 | embed _ _ _ := () |
| 133 | |
| 134 | /-- Of two operations of a job, the later one waits for the delay, unless both |
| 135 | delays between them are `0`. -/ |
| 136 | def Delayed (x : Inst) (t : Transportation.Delays x) (σ : PreemptiveShops.Sched x) : Prop := |
| 137 | ∀ j (k l : Fin (x.ops j)), k ≠ l → (t j k l = 0 ∧ t j l k = 0) ∨ |
| 138 | opFinish σ ⟨j, k⟩ + (t j k l : NNRat) ≤ opStart σ ⟨j, l⟩ ∨ |
| 139 | opFinish σ ⟨j, l⟩ + (t j l k : NNRat) ≤ opStart σ ⟨j, k⟩ |
| 140 | |
| 141 | /-- The machines that the pieces of an operation occupy. -/ |
| 142 | def opMachines {x : Inst} (σ : PreemptiveShops.Sched x) (o : Op x) : Finset (Fin x.machines) := |
| 143 | ((piecesOf σ o).map Piece.machines).foldr (· ∪ ·) ∅ |
| 144 | |
| 145 | /-- A single robot carries every job from each operation to the next, and |
| 146 | between two transports it travels empty from the machines where it delivers |
| 147 | the one to the machines where it picks up the other. -/ |
| 148 | def Carried (x : Inst) (t : Transportation.Delays x) (e : Transportation.EmptyMoves x) |
| 149 | (σ : PreemptiveShops.Sched x) : Prop := |
| 150 | ∃ depart : (j : Fin x.jobs) → Fin (x.ops j) → ℕ, |
| 151 | (∀ j (k l : Fin (x.ops j)), l.val = k.val + 1 → |
| 152 | opFinish σ ⟨j, k⟩ ≤ (depart j k : NNRat) ∧ |
| 153 | ((depart j k + t j k l : ℕ) : NNRat) ≤ opStart σ ⟨j, l⟩) ∧ |
| 154 | ∀ j (k l : Fin (x.ops j)) j' (k' l' : Fin (x.ops j')), l.val = k.val + 1 → |
| 155 | l'.val = k'.val + 1 → (⟨j, k⟩ : Op x) ≠ ⟨j', k'⟩ → |
| 156 | depart j k + t j k l + |
| 157 | Transportation.emptyTime e (opMachines σ ⟨j, l⟩) (opMachines σ ⟨j', k'⟩) ≤ |
| 158 | depart j' k' ∨ |
| 159 | depart j' k' + t j' k' l' + |
| 160 | Transportation.emptyTime e (opMachines σ ⟨j', l'⟩) (opMachines σ ⟨j, k⟩) ≤ |
| 161 | depart j k |
| 162 | |
| 163 | /-- The field of transportation delays. -/ |
| 164 | def transportation : Module kernel where |
| 165 | Value := Transportation.Value |
| 166 | Data _ x := Transportation.Data x |
| 167 | admits v _ d := v.admits d |
| 168 | constraint v x d σ := Delayed x d.1 σ ∧ (v.robot = true → Carried x d.1 d.2 σ) |
| 169 | le := Transportation.Value.le |
| 170 | embed _ _ d := d |
| 171 | |
| 172 | /-- A piece of one operation and a piece of another share a machine. -/ |
| 173 | def Shares {x : Inst} (σ : PreemptiveShops.Sched x) (a b : Op x) : Prop := |
| 174 | ∃ qa ∈ piecesOf σ a, ∃ qb ∈ piecesOf σ b, ¬ Disjoint qa.machines qb.machines |
| 175 | |
| 176 | /-- The server field: every operation needs a setup. -/ |
| 177 | def server : Module kernel where |
| 178 | Value := Servers.Value |
| 179 | Data v x := Servers.Data (Op x) v |
| 180 | admits v _ d := Servers.Admits v d |
| 181 | constraint v x d σ := ∀ s, Servers.view v d = some s → |
| 182 | Servers.Served (fun o : Op x => (opStart σ o : ℚ)) (fun o => (opFinish σ o : ℚ)) |
| 183 | (Servers.setupRelease (fun o : Op x => (opStart σ o : ℚ)) |
| 184 | (fun o => (kernel.start x σ o.1 : ℚ)) (fun o => (x.r o.1 : ℚ))) |
| 185 | (Shares σ) s |
| 186 | le := Servers.le |
| 187 | embed h _ d := Servers.embed h d |
| 188 | |
| 189 | /-- A piece of an operation occupies a machine. -/ |
| 190 | def Occupies {x : Inst} (σ : PreemptiveShops.Sched x) (o : Op x) (i : Fin x.machines) : Prop := |
| 191 | ∃ q ∈ piecesOf σ o, i ∈ q.machines |
| 192 | |
| 193 | /-- Every operation on a machine is immediately followed by another one on |
| 194 | that machine, unless none completes later. -/ |
| 195 | def Contiguous (x : Inst) (σ : PreemptiveShops.Sched x) : Prop := |
| 196 | ∀ i (a : Op x), Occupies σ a i → |
| 197 | (∃ b : Op x, b ≠ a ∧ Occupies σ b i ∧ opStart σ b = opFinish σ a) ∨ |
| 198 | ∀ b : Op x, Occupies σ b i → opFinish σ b ≤ opFinish σ a |
| 199 | |
| 200 | /-- The no-idle field. -/ |
| 201 | def noIdle : Module kernel where |
| 202 | Value := ShopExtras.NoIdle |
| 203 | Data _ _ := Unit |
| 204 | admits _ _ _ := True |
| 205 | constraint v x _ σ := v = .noIdle → Contiguous x σ |
| 206 | le v w := decide (v = w) |
| 207 | embed _ _ _ := () |
| 208 | |
| 209 | /-- On some machine, operation `b` follows operation `a`: `b` starts after `a` |
| 210 | completes, and no other operation on that machine lies in between. -/ |
| 211 | def Follows {x : Inst} (σ : PreemptiveShops.Sched x) (a b : Op x) : Prop := |
| 212 | opFinish σ a ≤ opStart σ b ∧ ∃ i, Occupies σ a i ∧ Occupies σ b i ∧ |
| 213 | ∀ c : Op x, c ≠ a → c ≠ b → Occupies σ c i → |
| 214 | ¬ (opFinish σ a ≤ opStart σ c ∧ opFinish σ c ≤ opStart σ b) |
| 215 | |
| 216 | /-- The batch-setup field. -/ |
| 217 | def batchSetups : Module kernel where |
| 218 | Value := ShopExtras.BatchSetups |
| 219 | Data := ShopExtras.BatchSetups.Data |
| 220 | admits _ _ _ := True |
| 221 | constraint v x d σ := ∀ a b : Op x, v.batch d a.1 ≠ v.batch d b.1 → |
| 222 | (Shares σ a b → opFinish σ a ≤ opStart σ b ∨ opFinish σ b ≤ opStart σ a) ∧ |
| 223 | (Follows σ a b → |
| 224 | opFinish σ a + (v.setup d (v.batch d a.1) (v.batch d b.1) : NNRat) ≤ opStart σ b) |
| 225 | le := ShopExtras.BatchSetups.le |
| 226 | embed := ShopExtras.BatchSetups.embed |
| 227 | |
| 228 | /-- The number of machines, a parameter of the kernel. -/ |
| 229 | def machines : kernel.Inst → ℕ := Inst.machines |
| 230 | |
| 231 | /-- The fields of the family: interruption and the fields of shops. -/ |
| 232 | inductive FieldName |
| 233 | | interruption |
| 234 | | field (i : ShopProblems.FieldName) |
| 235 | deriving DecidableEq |
| 236 | |
| 237 | instance : Fintype FieldName where |
| 238 | elems := {.interruption, .field .shopType, .field .machineSets, .field .machineCount, |
| 239 | .field .jobCount, .field .processingTimes, .field .noWait, .field .transportation, |
| 240 | .field .server, .field .noIdle, .field .batchSetups, .field .releaseDates, |
| 241 | .field .deadlines, .field .precedence} |
| 242 | complete x := by |
| 243 | cases x with |
| 244 | | interruption => decide |
| 245 | | field i => cases i <;> decide |
| 246 | |
| 247 | /-- The shop problems. -/ |
| 248 | abbrev family : Family kernel := |
| 249 | Thresholds.family FieldName fun |
| 250 | | .interruption => interruption |
| 251 | | .field .shopType => shopType |
| 252 | | .field .machineSets => machineSets |
| 253 | | .field .machineCount => Counts.module _ machines 1 |
| 254 | | .field .jobCount => Counts.module _ kernel.jobs |
| 255 | | .field .processingTimes => processingTimes |
| 256 | | .field .noWait => noWait |
| 257 | | .field .transportation => transportation |
| 258 | | .field .server => server |
| 259 | | .field .noIdle => noIdle |
| 260 | | .field .batchSetups => batchSetups |
| 261 | | .field .releaseDates => ReleaseDates.module _ |
| 262 | | .field .deadlines => Deadlines.module _ |
| 263 | | .field .precedence => Precedence.module _ machines |
| 264 | |
| 265 | instance : Fintype family.ModuleName := |
| 266 | inferInstanceAs (Fintype FieldName) |
| 267 | |
| 268 | /-- The specification `α | β | γ` of a shop problem. -/ |
| 269 | def spec (interruption : Interruption.Mode := .none) |
| 270 | (shopType : ShopType) |
| 271 | (machineSets : Machines) |
| 272 | (machineCount : Counts.Bound := .any) |
| 273 | (jobCount : Counts.Bound := .any) |
| 274 | (processingTimes : ProcessingTimes := .arbitrary) |
| 275 | (waiting : NoWait := .none) |
| 276 | (transportation : Transportation.Value := .none) |
| 277 | (server : Servers.Value := .none) |
| 278 | (idling : ShopExtras.NoIdle := .none) |
| 279 | (setups : ShopExtras.BatchSetups := .none) |
| 280 | (release : ReleaseDates.Value := .none) |
| 281 | (deadline : Deadlines.Value := .none) |
| 282 | (precedence : Precedence.Value := .none) |
| 283 | (objective : Objectives.Value) : Spec family where |
| 284 | module |
| 285 | | .interruption => interruption |
| 286 | | .field .shopType => shopType |
| 287 | | .field .machineSets => machineSets |
| 288 | | .field .machineCount => machineCount |
| 289 | | .field .jobCount => jobCount |
| 290 | | .field .processingTimes => processingTimes |
| 291 | | .field .noWait => waiting |
| 292 | | .field .transportation => transportation |
| 293 | | .field .server => server |
| 294 | | .field .noIdle => idling |
| 295 | | .field .batchSetups => setups |
| 296 | | .field .releaseDates => release |
| 297 | | .field .deadlines => deadline |
| 298 | | .field .precedence => precedence |
| 299 | objective := objective |
| 300 | |
| 301 | /-- The specification of the family with the values of a non-preemptive shop |
| 302 | problem. -/ |
| 303 | def ofShop (s : Spec ShopProblems.family) : Spec family where |
| 304 | module |
| 305 | | .interruption => Interruption.Mode.none |
| 306 | | .field .shopType => s.module .shopType |
| 307 | | .field .machineSets => s.module .machineSets |
| 308 | | .field .machineCount => s.module .machineCount |
| 309 | | .field .jobCount => s.module .jobCount |
| 310 | | .field .processingTimes => s.module .processingTimes |
| 311 | | .field .noWait => s.module .noWait |
| 312 | | .field .transportation => s.module .transportation |
| 313 | | .field .server => s.module .server |
| 314 | | .field .noIdle => s.module .noIdle |
| 315 | | .field .batchSetups => s.module .batchSetups |
| 316 | | .field .releaseDates => s.module .releaseDates |
| 317 | | .field .deadlines => s.module .deadlines |
| 318 | | .field .precedence => s.module .precedence |
| 319 | objective := s.objective |
| 320 | |
| 321 | /-- The specification of the family with the values of a preemptive shop |
| 322 | problem. -/ |
| 323 | def ofPreemptiveShop (s : Spec PreemptiveShopProblems.family) : Spec family where |
| 324 | module |
| 325 | | .interruption => Interruption.Mode.pmtn |
| 326 | | .field .shopType => s.module .shopType |
| 327 | | .field .machineSets => s.module .machineSets |
| 328 | | .field .machineCount => s.module .machineCount |
| 329 | | .field .jobCount => s.module .jobCount |
| 330 | | .field .processingTimes => s.module .processingTimes |
| 331 | | .field .noWait => NoWait.none |
| 332 | | .field .transportation => Transportation.Value.none |
| 333 | | .field .server => Servers.Value.none |
| 334 | | .field .noIdle => ShopExtras.NoIdle.none |
| 335 | | .field .batchSetups => ShopExtras.BatchSetups.none |
| 336 | | .field .releaseDates => s.module .releaseDates |
| 337 | | .field .deadlines => s.module .deadlines |
| 338 | | .field .precedence => s.module .precedence |
| 339 | objective := s.objective |
| 340 | |
| 341 | axiom shop_faithful (s : Spec ShopProblems.family) : |
| 342 | SpecialCase (problem _ s) (problem family (ofShop s)) ∧ |
| 343 | SpecialCase (problem family (ofShop s)) (problem _ s) |
| 344 | |
| 345 | axiom preemptiveShop_faithful (s : Spec PreemptiveShopProblems.family) : |
| 346 | SpecialCase (problem _ s) (problem family (ofPreemptiveShop s)) ∧ |
| 347 | SpecialCase (problem family (ofPreemptiveShop s)) (problem _ s) |
| 348 | |
| 349 | axiom family_sound : family.Sound |
| 350 | |
| 351 | axiom specialCase_of_le {s t : Spec family} : |
| 352 | s.le t → SpecialCase (problem family s) (problem family t) |
| 353 | |
| 354 | axiom reducible_of_reduces {s t : Spec family} : |
| 355 | Thresholds.Reduces s t → Reducible (problem family s) (problem family t) |
| 356 | |
| 357 | end Lax434175.ShopFamily |
| 358 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments