Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

A single server with setup times

Lax434175.Servers · concepts/Lax434175/Servers.lean · lax-434175

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    With a single server, every job on parallel machines, and every operation in a shop, needs a setup immediately before it is processed. The setup of job jj takes sjs_j time units, during which it occupies both the machines of the job and the server. Hence

    • the setup of a job starts no earlier than its release date rjr_j, so the job starts no earlier than rj+sjr_j + s_j; in a shop this holds for the first operation of the job, the one that starts when the job starts;
    • the setups of two different jobs do not overlap, since there is one server;
    • of two jobs that share a machine, the later one starts no earlier than the completion of the earlier one plus its own setup time.

    In a shop the setup of a later operation of a job may overlap the job's previous operation on another machine: setups are separable, and only the setup of the first operation waits for the release date. This is the model of Brucker, Knust and Wang (2005) and of the papers of the same group on a single server.

    The field has the value "none", without server and setups, and three values with a server: unit setup times, equal setup times, and arbitrary setup times. Unit is a special case of equal and equal of arbitrary; the value none is incomparable with the others.

    Theorem. The server field is sound over every machine model on parallel machines and for shops.

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 parallel_sound proven

    2 shop_sound proven

    Lean source view on GitHub

    1import Mathlib.Algebra.Order.Field.Rat
    2import Lax434175.ParallelMachines
    3import Lax434175.Shops
    4
    5/-!
    6---
    7title: A single server with setup times
    8type: theorem
    9---
    10With a single server, every job on parallel machines, and every operation in
    11a shop, needs a setup immediately before it is processed. The setup of job
    12jj takes sjs_j time units, during which it occupies both the machines of
    13the job and the server. Hence
    14
    15- the setup of a job starts no earlier than its release date rjr_j, so the
    16 job starts no earlier than rj+sjr_j + s_j; in a shop this holds for the first
    17 operation of the job, the one that starts when the job starts;
    18- the setups of two different jobs do not overlap, since there is one
    19 server;
    20- of two jobs that share a machine, the later one starts no earlier than the
    21 completion of the earlier one plus its own setup time.
    22
    23In a shop the setup of a later operation of a job may overlap the job's
    24previous operation on another machine: setups are separable, and only the
    25setup of the first operation waits for the release date. This is the model of
    26Brucker, Knust and Wang (2005) and of the papers of the same group on a single
    27server.
    28
    29The field has the value "none", without server and setups, and three values
    30with a server: unit setup times, equal setup times, and arbitrary setup
    31times. Unit is a special case of equal and equal of arbitrary; the value
    32none is incomparable with the others.
    33
    34**Theorem.** The server field is sound over every machine model on parallel
    35machines and for shops.
    36-/
    37
    38namespace Lax434175.Servers
    39open Lax434175.Kernels Lax434175.Modules
    40
    41inductive Value
    42 | none
    43 | unit
    44 | equal
    45 | arbitrary
    46 deriving DecidableEq
    47
    48/-- Setup times of `n` items; no data without a server. -/
    49def Data (Item : Type) : Value → Type
    50 | .none => Unit
    51 | .unit | .equal | .arbitrary => Item → ℕ
    52
    53/-- The setup times, where there is a server. -/
    54def view {Item : Type} : (v : Value) → Data Item v → Option (Item → ℕ)
    55 | .none, _ => Option.none
    56 | .unit, s | .equal, s | .arbitrary, s => some s
    57
    58/-- The condition on the setup times. -/
    59def Admits {Item : Type} : (v : Value) → Data Item v → Prop
    60 | .unit, s => ∀ a, s a = 1
    61 | .equal, s => ∃ c, ∀ a, s a = c
    62 | _, _ => True
    63
    64def le : Value → Value → Bool
    65 | .unit, .unit | .unit, .equal | .unit, .arbitrary => true
    66 | .equal, .equal | .equal, .arbitrary => true
    67 | .arbitrary, .arbitrary => true
    68 | .none, .none => true
    69 | _, _ => false
    70
    71def embed {Item : Type} : {v w : Value} → le v w = true → Data Item v → Data Item w
    72 | .none, .none, _, _ => ()
    73 | .unit, .unit, _, s | .unit, .equal, _, s | .unit, .arbitrary, _, s
    74 | .equal, .equal, _, s | .equal, .arbitrary, _, s | .arbitrary, .arbitrary, _, s => s
    75 | .none, .unit, h, _ | .none, .equal, h, _ | .none, .arbitrary, h, _
    76 | .unit, .none, h, _ | .equal, .none, h, _ | .equal, .unit, h, _
    77 | .arbitrary, .none, h, _ | .arbitrary, .unit, h, _ | .arbitrary, .equal, h, _ =>
    78 absurd h Bool.false_ne_true
    79
    80/-- The server constraints for items with given start and completion times,
    81release dates of their setups, setup times, and a relation "share a
    82machine". -/
    83def Served {Item : Type} (start completion release : Item → ℚ)
    84 (shares : Item → Item → Prop) (s : Item → ℕ) : Prop :=
    85 (∀ a, release a + s a ≤ start a) ∧
    86 (∀ a b, a ≠ b → start a + s b ≤ start b ∨ start b + s a ≤ start a) ∧
    87 ∀ a b, a ≠ b → shares a b → completion a + s b ≤ start b ∨ completion b + s a ≤ start a
    88
    89/-- The release date of the setup of an item: the release date of its job if
    90the item starts when its job starts (the first operation of the job), and `0`
    91otherwise. -/
    92def setupRelease {Item : Type} (start jobStart release : Item → ℚ) (a : Item) : ℚ :=
    93 if start a = jobStart a then release a else 0
    94
    95/-- The server field of a machine model on parallel machines. -/
    96def parallel (M : ParallelMachines.Model) : Module M.kernel where
    97 Value := Value
    98 Data v x := Data (Fin (M.kernel.jobs x)) v
    99 admits v _ d := Admits v d
    100 constraint v x d σ := ∀ s, view v d = some s →
    101 Served (fun j => (M.kernel.start x σ j : ℚ)) (fun j => (M.kernel.completion x σ j : ℚ))
    102 (fun j => (M.kernel.release x j : ℚ)) (fun i j => ∃ S S', M.uses x σ (Fin.cast (M.jobs_eq x) i) S ∧
    103 M.uses x σ (Fin.cast (M.jobs_eq x) j) S' ∧ ¬ Disjoint S S') s
    104 le := le
    105 embed h _ d := embed h d
    106
    107/-- The server field of shops: every operation needs a setup. -/
    108def shop : Module Shops.kernel where
    109 Value := Value
    110 Data v x := Data (Shops.Op x) v
    111 admits v _ d := Admits v d
    112 constraint v x d σ := ∀ s, view v d = some s →
    113 Served (fun o : Shops.Op x => (Shops.Sched.start σ o.1 o.2 : ℚ))
    114 (fun o => (Shops.finish x σ o : ℚ))
    115 (setupRelease (fun o : Shops.Op x => (Shops.Sched.start σ o.1 o.2 : ℚ))
    116 (fun o => (Shops.jobStart x σ o.1 : ℚ)) (fun o => (x.r o.1 : ℚ)))
    117 (fun a b => ¬ Disjoint (Shops.Sched.machines σ a.1 a.2) (Shops.Sched.machines σ b.1 b.2)) s
    118 le := le
    119 embed h _ d := embed h d
    120
    121axiom parallel_sound (M : ParallelMachines.Model) : (parallel M).Sound
    122
    123axiom shop_sound : shop.Sound
    124
    125end Lax434175.Servers
    126
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…