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

Completion-time objectives

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

proven

Loading review…

Sign in with ORCID

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

    Let CjC_j denote the completion time of job jj. The objective field has the values

    • makespan, Cmax⁡=max⁡jCjC_{\max} = \max_j C_j,
    • maximum lateness, Lmax⁡=max⁡j(Cj−dj)L_{\max} = \max_j (C_j - d_j),
    • total completion time, ∑jCj\sum_j C_j,
    • total weighted completion time, ∑jwjCj\sum_j w_j C_j,
    • total tardiness, ∑jTj\sum_j T_j with Tj=max⁡(0,Cj−dj)T_j = \max(0, C_j - d_j),
    • total weighted tardiness, ∑jwjTj\sum_j w_j T_j,
    • number of late jobs, ∑jUj\sum_j U_j with Uj=1U_j = 1 if Cj>djC_j > d_j and Uj=0U_j = 0 otherwise,
    • weighted number of late jobs, ∑jwjUj\sum_j w_j U_j,
    • number of jobs that are not just in time, ∑j(1−Zj)\sum_j (1 - Z_j) with Zj=1Z_j = 1 if Cj=djC_j = d_j and Zj=0Z_j = 0 otherwise, and its weighted version ∑jwj(1−Zj)\sum_j w_j (1 - Z_j),
    • total flow time, ∑jFj\sum_j F_j with Fj=Cj−rjF_j = C_j - r_j for the release date rjr_j, and its weighted version ∑jwjFj\sum_j w_j F_j,
    • maximum flow time, Fmax⁡=max⁡jFjF_{\max} = \max_j F_j, and its weighted version max⁡jwjFj\max_j w_j F_j.

    Maximizing the number of jobs that are on time, or just in time, is minimizing the number of jobs that are not.

    Two values restrict the due dates: total weighted tardiness with a common due date, dj=dd_j = d, and the weighted number of late jobs with due dates at most kk after the release dates, dj≤rj+kd_j \le r_j + k. Each is a special case of the unrestricted value, and a smaller kk of a larger one.

    A value carries weights wjw_j exactly if it is weighted and due dates djd_j exactly if it measures lateness, tardiness or being just in time. The makespan is the maximum lateness with dj=0d_j = 0; the maximum over an empty set of jobs is taken to be 00. The four values measuring completion time or tardiness are the single expression ∑jwjmax⁡(0,Cj−dj)\sum_j w_j \max(0, C_j - d_j), with wj=1w_j = 1 where weights are absent and dj=0d_j = 0 where due dates are absent; the two values counting late jobs are ∑jwjUj\sum_j w_j U_j with the same convention for the weights.

    A value is a special case of another value of the same kind that carries at least the same data.

    Theorem. Over every kernel, the objective field is sound.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.Algebra.BigOperators.Group.Finset.Basic
    2import Mathlib.Data.Fintype.BigOperators
    3import Mathlib.Data.Finset.Lattice.Fold
    4import Mathlib.Data.NNRat.BigOperators
    5import Mathlib.Algebra.Order.Field.Rat
    6import Lax434175.Modules
    7
    8/-!
    9---
    10title: Completion-time objectives
    11type: theorem
    12---
    13Let CjC_j denote the completion time of job jj. The objective field has the
    14values
    15
    16- makespan, Cmax⁡=max⁡jCjC_{\max} = \max_j C_j,
    17- maximum lateness, Lmax⁡=max⁡j(Cj−dj)L_{\max} = \max_j (C_j - d_j),
    18- total completion time, ∑jCj\sum_j C_j,
    19- total weighted completion time, ∑jwjCj\sum_j w_j C_j,
    20- total tardiness, ∑jTj\sum_j T_j with Tj=max⁡(0,Cj−dj)T_j = \max(0, C_j - d_j),
    21- total weighted tardiness, ∑jwjTj\sum_j w_j T_j,
    22- number of late jobs, ∑jUj\sum_j U_j with Uj=1U_j = 1 if Cj>djC_j > d_j and
    23 Uj=0U_j = 0 otherwise,
    24- weighted number of late jobs, ∑jwjUj\sum_j w_j U_j,
    25- number of jobs that are not just in time, ∑j(1−Zj)\sum_j (1 - Z_j) with
    26 Zj=1Z_j = 1 if Cj=djC_j = d_j and Zj=0Z_j = 0 otherwise, and its weighted version
    27 ∑jwj(1−Zj)\sum_j w_j (1 - Z_j),
    28- total flow time, ∑jFj\sum_j F_j with Fj=Cj−rjF_j = C_j - r_j for the release date
    29 rjr_j, and its weighted version ∑jwjFj\sum_j w_j F_j,
    30- maximum flow time, Fmax⁡=max⁡jFjF_{\max} = \max_j F_j, and its weighted version
    31 max⁡jwjFj\max_j w_j F_j.
    32
    33Maximizing the number of jobs that are on time, or just in time, is
    34minimizing the number of jobs that are not.
    35
    36Two values restrict the due dates: total weighted tardiness with a common
    37due date, dj=dd_j = d, and the weighted number of late jobs with due dates at
    38most kk after the release dates, dj≤rj+kd_j \le r_j + k. Each is a special case
    39of the unrestricted value, and a smaller kk of a larger one.
    40
    41A value carries weights wjw_j exactly if it is weighted and due dates djd_j
    42exactly if it measures lateness, tardiness or being just in time. The makespan is the maximum
    43lateness with dj=0d_j = 0; the maximum over an empty set of jobs is taken to
    44be 00. The four values measuring
    45completion time or tardiness are the single expression
    46∑jwjmax⁡(0,Cj−dj)\sum_j w_j \max(0, C_j - d_j), with wj=1w_j = 1 where weights are absent and
    47dj=0d_j = 0 where due dates are absent; the two values counting late jobs are
    48∑jwjUj\sum_j w_j U_j with the same convention for the weights.
    49
    50A value is a special case of another value of the same kind that carries at
    51least the same data.
    52
    53**Theorem.** Over every kernel, the objective field is sound.
    54-/
    55
    56namespace Lax434175.Objectives
    57open Lax434175.Kernels Lax434175.Modules
    58
    59inductive Value
    60 | makespan
    61 | lmax
    62 | sumC
    63 | sumWC
    64 | sumT
    65 | sumWT
    66 | sumU
    67 | sumWU
    68 | sumZ
    69 | sumWZ
    70 | sumF
    71 | sumWF
    72 | fmax
    73 | maxWF
    74 | sumWTCommon
    75 | sumWUWindow (k : ℕ)
    76 deriving DecidableEq
    77
    78/-- How the cost is formed from the completion times. -/
    79inductive Kind
    80 | maximum
    81 | tardiness
    82 | late
    83 | notJustInTime
    84 | flow
    85 | maximumFlow
    86 deriving DecidableEq
    87
    88def kind : Value → Kind
    89 | .makespan | .lmax => .maximum
    90 | .sumC | .sumWC | .sumT | .sumWT | .sumWTCommon => .tardiness
    91 | .sumU | .sumWU | .sumWUWindow _ => .late
    92 | .sumZ | .sumWZ => .notJustInTime
    93 | .sumF | .sumWF => .flow
    94 | .fmax | .maxWF => .maximumFlow
    95
    96/-- Whether the value carries weights. -/
    97def weighted : Value → Bool
    98 | .sumWC | .sumWT | .sumWU | .sumWZ | .sumWF | .maxWF | .sumWTCommon | .sumWUWindow _ => true
    99 | _ => false
    100
    101/-- Whether the value carries due dates. -/
    102def hasDueDates : Value → Bool
    103 | .lmax | .sumT | .sumWT | .sumU | .sumWU | .sumZ | .sumWZ | .sumWTCommon | .sumWUWindow _ => true
    104 | _ => false
    105
    106/-- Weights where the value is weighted, due dates where it has them. -/
    107def Data (K : Kernel) : Value → K.Inst → Type
    108 | .makespan, _ | .sumC, _ | .sumF, _ | .fmax, _ => Unit
    109 | .lmax, x | .sumWC, x | .sumT, x | .sumU, x | .sumZ, x | .sumWF, x | .maxWF, x =>
    110 Fin (K.jobs x) → ℕ
    111 | .sumWT, x | .sumWU, x | .sumWZ, x | .sumWTCommon, x | .sumWUWindow _, x =>
    112 (Fin (K.jobs x) → ℕ) × (Fin (K.jobs x) → ℕ)
    113
    114/-- The weight of a job; `1` when the value is unweighted. -/
    115def weight {K : Kernel} {x : K.Inst} : (v : Value) → Data K v x → Fin (K.jobs x) → ℕ
    116 | .sumWC, w | .sumWF, w | .maxWF, w => w
    117 | .sumWT, d | .sumWU, d | .sumWZ, d | .sumWTCommon, d | .sumWUWindow _, d => d.1
    118 | .makespan, _ | .lmax, _ | .sumC, _ | .sumT, _ | .sumU, _ | .sumZ, _ | .sumF, _
    119 | .fmax, _ => fun _ => 1
    120
    121/-- The due date of a job; `0` when the value has no due dates. -/
    122def dueDate {K : Kernel} {x : K.Inst} : (v : Value) → Data K v x → Fin (K.jobs x) → ℕ
    123 | .lmax, d | .sumT, d | .sumU, d | .sumZ, d => d
    124 | .sumWT, d | .sumWU, d | .sumWZ, d | .sumWTCommon, d | .sumWUWindow _, d => d.2
    125 | .makespan, _ | .sumC, _ | .sumWC, _ | .sumF, _ | .sumWF, _ | .fmax, _ | .maxWF, _ =>
    126 fun _ => 0
    127
    128/-- The cost of a schedule. Subtraction of nonnegative rationals is
    129truncated, so `C - d` is the tardiness `max(0, C - d)`. -/
    130def cost {K : Kernel} (v : Value) (x : K.Inst) (d : Data K v x) (σ : K.Sched x) : ℚ :=
    131 match kind v with
    132 | .maximum =>
    133 if h : 0 < K.jobs x then
    134 Finset.univ.sup' ⟨⟨0, h⟩, Finset.mem_univ _⟩
    135 (fun j => (K.completion x σ j : ℚ) - (dueDate v d j : ℚ))
    136 else 0
    137 | .tardiness =>
    138 ((∑ j, (weight v d j : NNRat) * (K.completion x σ j - (dueDate v d j : NNRat)) : NNRat) : ℚ)
    139 | .late =>
    140 ((∑ j, (weight v d j : NNRat) *
    141 (if (dueDate v d j : NNRat) < K.completion x σ j then 1 else 0) : NNRat) : ℚ)
    142 | .notJustInTime =>
    143 ((∑ j, (weight v d j : NNRat) *
    144 (if K.completion x σ j = (dueDate v d j : NNRat) then 0 else 1) : NNRat) : ℚ)
    145 | .flow =>
    146 ((∑ j, (weight v d j : NNRat) * (K.completion x σ j - (K.release x j : NNRat)) : NNRat) : ℚ)
    147 | .maximumFlow =>
    148 ((Finset.univ.sup fun j =>
    149 (weight v d j : NNRat) * (K.completion x σ j - (K.release x j : NNRat)) : NNRat) : ℚ)
    150
    151/-- The condition on the due dates of the two restricted values. -/
    152def admits {K : Kernel} : (v : Value) → (x : K.Inst) → Data K v x → Prop
    153 | .sumWTCommon, _, d => ∃ c, ∀ j, d.2 j = c
    154 | .sumWUWindow k, x, d => ∀ j, d.2 j ≤ K.release x j + k
    155 | _, _, _ => True
    156
    157/-- Comparison of the restrictions on the due dates. -/
    158def restrictionLe : Value → Value → Bool
    159 | .sumWTCommon, .sumWTCommon => true
    160 | .sumWUWindow k, .sumWUWindow l => decide (k ≤ l)
    161 | _, .sumWTCommon => false
    162 | _, .sumWUWindow _ => false
    163 | _, _ => true
    164
    165def le (v w : Value) : Bool :=
    166 decide (kind v = kind w) && (!weighted v || weighted w) && (!hasDueDates v || hasDueDates w) &&
    167 restrictionLe v w
    168
    169def embed {K : Kernel} : {v w : Value} → le v w = true → (x : K.Inst) → Data K v x → Data K w x
    170 | _, .makespan, _, _, _ | _, .sumC, _, _, _ | _, .sumF, _, _, _ | _, .fmax, _, _, _ => ()
    171 | v, .sumWC, _, _, d | v, .sumWF, _, _, d | v, .maxWF, _, _, d => weight v d
    172 | v, .lmax, _, _, d | v, .sumT, _, _, d | v, .sumU, _, _, d | v, .sumZ, _, _, d => dueDate v d
    173 | v, .sumWT, _, _, d | v, .sumWU, _, _, d | v, .sumWZ, _, _, d | v, .sumWTCommon, _, _, d
    174 | v, .sumWUWindow _, _, _, d => (weight v d, dueDate v d)
    175
    176/-- The objective field over a kernel. -/
    177def objective (K : Kernel) : Objective K where
    178 Value := Value
    179 Data := Data K
    180 admits := admits
    181 cost := cost
    182 le := le
    183 embed := embed
    184
    185axiom sound (K : Kernel) : (objective K).Sound
    186
    187end Lax434175.Objectives
    188
    Show Proof

    Discussion

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

    Loading discussion…