Lax Lean Archive

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

Preemptive shop scheduling

Lax434175.PreemptiveShops · concepts/Lax434175/PreemptiveShops.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

    The instances are those of shop scheduling. A preemptive schedule is a finite list of pieces. A piece processes one operation on a nonempty set of machines during an interval given by a start time and a length, both nonnegative rational numbers.

    A schedule is feasible for the kernel if two different pieces that belong to the same job or share a machine are disjoint in time, and every operation is completed: the lengths of its pieces sum to its processing time, or its processing time is 00 and it has a piece. As on parallel machines, an operation of length 00 thus still has a piece, which gives it a completion time. An operation starts when its first piece starts and completes when its last piece ends, and likewise a job.

    The shop-type field, the machine field and the processing-time field are those of non-preemptive shops: the operations of a flow shop or job shop must be processed in their given order, each completing before the next starts, and every piece of an operation occupies an admissible set of machines.

    Theorem. The shop-type, machine and processing-time fields of preemptive shops are sound.

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

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

    1 machineSets_sound proven

    2 processingTimes_sound proven

    3 shopType_sound proven

    Lean source view on GitHub

    1import Mathlib.Algebra.Order.Field.Rat
    2import Mathlib.Algebra.Order.Ring.Rat
    3import Lax434175.Shops
    4
    5/-!
    6---
    7title: Preemptive shop scheduling
    8type: theorem
    9---
    10The instances are those of shop scheduling. A preemptive schedule is a
    11finite list of pieces. A piece processes one operation on a nonempty set of
    12machines during an interval given by a start time and a length, both
    13nonnegative rational numbers.
    14
    15A schedule is feasible for the kernel if two different pieces that belong to
    16the same job or share a machine are disjoint in time, and every operation is
    17completed: the lengths of its pieces sum to its processing time, or its
    18processing time is 00 and it has a piece. As on parallel machines, an
    19operation of length 00 thus still has a piece, which gives it a completion
    20time. An operation starts
    21when its first piece starts and completes when its last piece ends, and
    22likewise a job.
    23
    24The shop-type field, the machine field and the processing-time field are
    25those of non-preemptive shops: the operations of a flow shop or job shop
    26must be processed in their given order, each completing before the next
    27starts, and every piece of an operation occupies an admissible set of
    28machines.
    29
    30**Theorem.** The shop-type, machine and processing-time fields of
    31preemptive shops are sound.
    32-/
    33
    34namespace Lax434175.PreemptiveShops
    35open Lax434175.Kernels Lax434175.Modules Lax434175.Shops
    36
    37/-- An operation is processed on a set of machines from `start` for `length`
    38time units. -/
    39structure Piece (x : Inst) where
    40 op : Op x
    41 machines : Finset (Fin x.machines)
    42 start : NNRat
    43 length : NNRat
    44
    45/-- The time at which a piece ends. -/
    46def Piece.finish {x : Inst} (q : Piece x) : NNRat := q.start + q.length
    47
    48structure Sched (x : Inst) where
    49 pieces : List (Piece x)
    50
    51/-- The pieces of an operation. -/
    52def piecesOf {x : Inst} (σ : Sched x) (o : Op x) : List (Piece x) :=
    53 σ.pieces.filter (fun q => decide (q.op = o))
    54
    55/-- The pieces of a job. -/
    56def piecesOfJob {x : Inst} (σ : Sched x) (j : Fin x.jobs) : List (Piece x) :=
    57 σ.pieces.filter (fun q => decide (q.op.1 = j))
    58
    59/-- Two pieces do not overlap in time. -/
    60def Apart {x : Inst} (a b : Piece x) : Prop :=
    61 a.finish ≤ b.start ∨ b.finish ≤ a.start
    62
    63def feasible (x : Inst) (σ : Sched x) : Prop :=
    64 (∀ q ∈ σ.pieces, q.machines.Nonempty) ∧
    65 σ.pieces.Pairwise
    66 (fun a b => (a.op.1 = b.op.1 ∨ ¬ Disjoint a.machines b.machines) → Apart a b) ∧
    67 ∀ o : Op x, ((piecesOf σ o).map fun q => q.length / (x.p o.1 o.2 : NNRat)).sum = 1 ∨
    68 ∃ q ∈ piecesOf σ o, x.p o.1 o.2 = 0
    69
    70/-- The start of the first piece of an operation. -/
    71def opStart {x : Inst} (σ : Sched x) (o : Op x) : NNRat :=
    72 (((piecesOf σ o).map Piece.start).min?).getD 0
    73
    74/-- The end of the last piece of an operation. -/
    75def opFinish {x : Inst} (σ : Sched x) (o : Op x) : NNRat :=
    76 (((piecesOf σ o).map Piece.finish).max?).getD 0
    77
    78/-- The kernel of preemptive shop scheduling. -/
    79def kernel : Kernel where
    80 Inst := Inst
    81 jobs := Inst.jobs
    82 release := Inst.r
    83 Sched := Sched
    84 feasible := feasible
    85 start _ σ j := (((piecesOfJob σ j).map Piece.start).min?).getD 0
    86 completion _ σ j := (((piecesOfJob σ j).map Piece.finish).max?).getD 0
    87
    88/-- The number of machines, a parameter of the kernel. -/
    89def machines : kernel.Inst → ℕ := Inst.machines
    90
    91/-- The operations of every job are processed in their given order. -/
    92def InOrder (x : Inst) (σ : Sched x) : Prop :=
    93 ∀ j (k k' : Fin (x.ops j)), k < k' → opFinish σ ⟨j, k⟩ ≤ opStart σ ⟨j, k'⟩
    94
    95/-- The order a shop type imposes on the operations of a job. -/
    96def ordered : ShopType → (x : Inst) → Sched x → Prop
    97 | .open, _, _ => True
    98 | .flow, x, σ => InOrder x σ
    99 | .job, x, σ => InOrder x σ
    100 | .flexibleFlow, x, σ => InOrder x σ
    101
    102/-- The shop-type field. -/
    103def shopType : Module kernel where
    104 Value := ShopType
    105 Data _ _ := Unit
    106 admits v x _ := v.holds x
    107 constraint v x _ σ := ordered v x σ
    108 le := ShopType.le
    109 embed _ _ _ := ()
    110
    111/-- The machine field. -/
    112def machineSets : Module kernel where
    113 Value := Machines
    114 Data := Machines.Data
    115 admits v _ d := v.admits d
    116 constraint v _ d σ := ∀ q ∈ Sched.pieces σ, v.view d q.op.1 q.op.2 q.machines
    117 le := Machines.le
    118 embed := Machines.embed
    119
    120/-- The processing-time field. -/
    121def processingTimes : Module kernel :=
    122 Module.ofRestriction ProcessingTimes ProcessingTimes.holds
    123 (fun v w => decide (v.rank ≤ w.rank))
    124
    125axiom shopType_sound : shopType.Sound
    126
    127axiom machineSets_sound : machineSets.Sound
    128
    129axiom processingTimes_sound : processingTimes.Sound
    130
    131end Lax434175.PreemptiveShops
    132
    Show ProofShow 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…